Stream: t-compiler/const-eval

Topic: const types


RalfJ (Jan 22 2019 at 16:21, on Zulip):

@varkor Just catching up on the const-generics RFC. One thing I am really confused about is your notion of "const types". You seem to take that for granted. I never considered it, and I think it is not necessary. Could you briefly explain what you mean by that? what distinguishes "const" from "non-const" types? (See https://www.ralfj.de/blog/2018/07/19/const.html for my previous thoughts on const-ness.)

varkor (Jan 22 2019 at 16:25, on Zulip):

I don't think const types are necessary either

RalfJ (Jan 22 2019 at 16:25, on Zulip):

specifically, I see no good reason to make const X: bool = true; and let x = true; have a different type. that's just the same type used in two different contexts.

varkor (Jan 22 2019 at 16:25, on Zulip):

at one point, I was considering them, but later I removed them from my model

RalfJ (Jan 22 2019 at 16:26, on Zulip):

so the appendix of https://varkor.github.io/blog/2019/01/11/const-types-traits-and-implementations-in-Rust.html about the two versions of each type is outdated in that respect?

varkor (Jan 22 2019 at 16:26, on Zulip):

wait, I misinterpreted, sorry

varkor (Jan 22 2019 at 16:27, on Zulip):

hmm

oli (Jan 22 2019 at 16:27, on Zulip):

I think we reached the point of "the set of const types is equal to the set of types" in https://github.com/rust-rfcs/const-eval/pull/8#issuecomment-452713799

varkor (Jan 22 2019 at 16:28, on Zulip):

I think my last view was that there's no need to talk about "const types" in the language itself

varkor (Jan 22 2019 at 16:29, on Zulip):

but it makes sense to consider them from the perspective of a type theoretic model

RalfJ (Jan 22 2019 at 16:29, on Zulip):

I disagree, but it may not be necessary for us to agree on the model as long as we agree on the lang design ;)

varkor (Jan 22 2019 at 16:29, on Zulip):

but I'm not claiming my model is canonical — I'm sure there are other models that don't view types in that way

varkor (Jan 22 2019 at 16:30, on Zulip):

I'm happy as long as there is some model :P

varkor (Jan 22 2019 at 16:31, on Zulip):

that said, I would be interested in discussing inaccuracies/simplifications of my model, but if we agree on the design, then it's an unrelated issue, yeah

varkor (Jan 22 2019 at 16:34, on Zulip):

(you're right in that I'm writing as if it's "taken for granted" in that post — that was more to attempt to not make the writing more confusing with lots of conditional phrasing, more than an assertion that I think this is the definitive model 😁)

RalfJ (Jan 22 2019 at 17:53, on Zulip):

so basically with the latest RFC and the ?const in it, we got 3 levels for generic arguments:

unfortunately this is not in sync with const fn vs fn, the latter is really ?const fn... :/

what about trait objects? which kinds of bounds can occur there? is there dyn ?const Trait?

RalfJ (Jan 22 2019 at 17:53, on Zulip):

I'd assume it's like fn ptrs, but then dyn Trait and Trait are very different in const context

RalfJ (Jan 22 2019 at 17:54, on Zulip):

(with the methods of the former not callable)

RalfJ (Jan 22 2019 at 18:20, on Zulip):

that said, I would be interested in discussing inaccuracies/simplifications of my model, but if we agree on the design, then it's an unrelated issue, yeah

Here's my biggest issue: the embedding of the const universe in the run-time universe is actually not universal. to use terminology from my blog post, a function being const-safe does not imply it being run-time-safe, because the quantification over the const-invariant of the type occurs both in positive and negative position. So this functor U you describe, I don't think it exists for the function type.

Now I cannot even say if that's an inaccuracy, because your theory is all definitions and no (claimed) theorems -- so, I am not sure what to learn from it TBH. How does it relate to the notion I call "const-safety", which I think is the most important in this entire type system design endavor: Making sure that during const evalaution we don't run code that is unfit for const evaluation.

RalfJ (Jan 22 2019 at 18:23, on Zulip):

To give an example for my claim:

const fn const_safe_but_not_safe(x: &i32, y: usize) { unsafe {
  if x as *const i32 == y as *const i32 {
    // This is unreachable in const context, because `usize` must never be a pointer. Hence we can do whatever we want.
    *(0usize as *mut u8) = 0;
  }
}

This function, when called from a safe const context, can never cause an error. From a safe run-time context it can easily cause UB. And yet you claim every const fn can be mapped to a fn.

varkor (Jan 22 2019 at 20:25, on Zulip):

is this function callable at run-time though?

varkor (Jan 22 2019 at 20:26, on Zulip):

if you can call it, even if it's not safe, then I'm considering it a valid function

varkor (Jan 22 2019 at 20:26, on Zulip):

if there are some functions that may only be called at compile-time, then I agree that my model is inaccurate

varkor (Jan 22 2019 at 20:27, on Zulip):

if not, though, I'm more concerned about the type system than actual safety

varkor (Jan 22 2019 at 20:27, on Zulip):

(which is less important in practice, but still a valuable aspect to consider)

varkor (Jan 22 2019 at 20:28, on Zulip):

because your theory is all definitions and no (claimed) theorems

mhm, unfortunately I have less time to spend playing around with this than I would like

RalfJ (Jan 22 2019 at 20:57, on Zulip):

if you can call it, even if it's not safe, then I'm considering it a valid function

in that case your model does not properly reflect whether functions are safe to call, which is the prime purpose of a type system -- and it is a type (and effect) system we are designing here.

RalfJ (Jan 22 2019 at 20:57, on Zulip):

if not, though, I'm more concerned about the type system than actual safety

I agree modelling a type system is valuable, but usually that comes with a claim of type safety. I am not asking for a proof of it, but in your definitions I do not see what the claim would even look like.

varkor (Jan 22 2019 at 21:55, on Zulip):

(deleted)

varkor (Jan 22 2019 at 21:58, on Zulip):

regardless, how are you proposing the const_safe_but_not_safe function be uncallable at run-time?

varkor (Jan 22 2019 at 21:58, on Zulip):

at the moment, it's not represented in the type at all (without some ad hoc rule about usize, etc.)

varkor (Jan 22 2019 at 21:58, on Zulip):

so surely the current type system is failing in that regard

varkor (Jan 22 2019 at 22:00, on Zulip):

I agree modelling a type system is valuable, but usually that comes with a claim of type safety.

Rust's type system is unsound as it stands, so I don't see that a reasonable claim at type safety can be made

varkor (Jan 22 2019 at 22:00, on Zulip):

proposing variations on the type system is a different matter

varkor (Jan 22 2019 at 22:01, on Zulip):

I wasn't intending to come up with a model suitable for formal verification, etc.

varkor (Jan 22 2019 at 22:01, on Zulip):

it's more idealised

varkor (Jan 22 2019 at 22:02, on Zulip):

maybe it's true that it's a valid model without unsafe?

centril (Jan 22 2019 at 22:05, on Zulip):

Rust's type system is unsound as it stands, so I don't see that a reasonable claim at type safety can be made

@varkor uhm... elaborate?

varkor (Jan 22 2019 at 22:08, on Zulip):

you can trivially cause UB

varkor (Jan 22 2019 at 22:08, on Zulip):

if you set out to do it

varkor (Jan 22 2019 at 22:08, on Zulip):

if you want to prove soundness, it has to be for a subset of the language

rkruppe (Jan 22 2019 at 22:12, on Zulip):

While it's technically correct that Rust's type system does not ensure the type safety of programs involving unsafe, it is also pretty clear that everyone here is deeply aware of it, so I don't see a reason to point it out like that.

varkor (Jan 22 2019 at 22:19, on Zulip):

my point is that you can only get so far modelling type safety in the presence of unsafe, so it's not entirely unreasonable to have a model of the type system that ignores it

varkor (Jan 22 2019 at 22:19, on Zulip):

more accurate models are more useful, but less accurate ones aren't necessarily not useful

rkruppe (Jan 22 2019 at 22:23, on Zulip):

What you can do with type safety, and with CTFE as well, is to lay out a complete but not-statically-checkable definition of what the desired safety property is (no runtime UB / no code that CTFE can't handle) and then see how well proposed static analyses approximate that end goal, and in particular whether they are sound.

varkor (Jan 22 2019 at 22:27, on Zulip):

sure, I don't dispute that

varkor (Jan 22 2019 at 22:28, on Zulip):

models that demonstrate soundness for subsets of the language can be useful too, though

varkor (Jan 22 2019 at 22:30, on Zulip):

so while a complete model would detail exactly when any behaviour is safe/unsafe/etc., that doesn't obviate other models

rkruppe (Jan 22 2019 at 22:31, on Zulip):

A model for a subset of the language should, however, come with a way to tell when that model applies.

varkor (Jan 22 2019 at 22:31, on Zulip):

agreed

varkor (Jan 22 2019 at 22:31, on Zulip):

in the model in question, my conjecture is that it could apply for a subset of the language where unsafe doesn't exist

varkor (Jan 22 2019 at 22:33, on Zulip):

(which is the context in which Ralf pointed out my draft model was oversimplified)

rkruppe (Jan 22 2019 at 22:33, on Zulip):

I know basically nothing about your model but in general I have a lot of reservation about models that completely ignore unsafe, because unsafe can add new capabilities to safe interfaces, so compositional reasoning is ham-strung

varkor (Jan 22 2019 at 22:34, on Zulip):

it's more like a first-pass litmus test

varkor (Jan 22 2019 at 22:34, on Zulip):

if a feature doesn't even fit into a model without unsafe, there's no way it's feasible with unsafe as well

varkor (Jan 22 2019 at 22:34, on Zulip):

but a feature should definitely be considered in light of unsafe if it seems all right without it

rkruppe (Jan 22 2019 at 22:35, on Zulip):

for a very particular interpretation of "doesn't fit without unsafe"

varkor (Jan 22 2019 at 22:35, on Zulip):

well, in any such model

varkor (Jan 22 2019 at 22:35, on Zulip):

as long as there exists some (reasonable) model, then it's fine

rkruppe (Jan 22 2019 at 22:35, on Zulip):

for example, a bunch of std APIs seem overly complicated or unnecessary or vacuous if one ignores unsafe

varkor (Jan 22 2019 at 22:36, on Zulip):

in any simplification of the language, some features/functions are going to seem unnecessary

varkor (Jan 22 2019 at 22:36, on Zulip):

I do think you want as precise a model as possible

varkor (Jan 22 2019 at 22:37, on Zulip):

which goes hand-in-hand with the sort of formal verification Ralf, etc. are doing

varkor (Jan 22 2019 at 22:37, on Zulip):

I'm really just having fun by trying to define a simplified model from a more type theoretic perspective

rkruppe (Jan 22 2019 at 22:37, on Zulip):

I don't really want anything specific in this discussion, I'm way too behind on all the const trait bounds discussion.

rkruppe (Jan 22 2019 at 22:38, on Zulip):

But ultimately I am curious whether this "const types" idea is giving any useful intuition for the real problem of handling the whole language, and the discussion so far doesn't give that impression

varkor (Jan 22 2019 at 22:38, on Zulip):

I think the essence of the discussion at this point is that, though we may have come to it by different reasoning, most people seem reasonably happy with the design of the const trait bounds RFC at the moment

varkor (Jan 22 2019 at 22:38, on Zulip):

hmm

rkruppe (Jan 22 2019 at 22:39, on Zulip):

Partly because it doesn't seem there is a precise connection to the more detailed/complete approaches like CTFE safety

rkruppe (Jan 22 2019 at 22:39, on Zulip):

or at least it's not clear to me (nor to Ralf IIUC) what it is

varkor (Jan 22 2019 at 22:39, on Zulip):

I kind of expect them to coïncide if it was pushed

varkor (Jan 22 2019 at 22:40, on Zulip):

but part of the problem is that it's not well-defined

varkor (Jan 22 2019 at 22:40, on Zulip):

(that is, my formulation)

varkor (Jan 22 2019 at 22:40, on Zulip):

so it's not easy to make concrete statements about

varkor (Jan 22 2019 at 22:40, on Zulip):

it was something to lend myself intuition, and I thought some people might find it more helpful

varkor (Jan 22 2019 at 22:40, on Zulip):

I think it very much depends on how you're thinking about it

varkor (Jan 22 2019 at 22:41, on Zulip):

if you're concerned with the precise details around CTFE and unsafe, etc., then you want a very accurate model, and having something vaguer and more loosely connected isn't helpful at all

varkor (Jan 22 2019 at 22:42, on Zulip):

but if you want to know what "const" means in terms of a programming language in general, I find it helpful to take a wider perspective, and brush over the details

varkor (Jan 22 2019 at 22:43, on Zulip):

I think you can get some way just by pretending a language is more "nicely behaved" (for some such definition) than it really is, to get an overall intuition

rkruppe (Jan 22 2019 at 22:44, on Zulip):

I agree that it's about how you're thinking about it, but not like that. The reason I have difficulties with what you're describing (in this channel) is that type systems mostly are an unfortunate approximation, an incomplete proof calculus, for what I actually care about (how programs behave when run) -- at least when talking about languages like Rust, where Curry-Howard is no good. One can then fruitfully restrict attention to subsets of programs or aspects of behavior (e.g., disregard divergence), but it's still very "bottom up".

varkor (Jan 22 2019 at 23:06, on Zulip):

yeah, I find the actual run-time behaviour less interesting than the type system in and of itself

varkor (Jan 22 2019 at 23:07, on Zulip):

which I completely accept is less useful

varkor (Jan 22 2019 at 23:07, on Zulip):

but explains why I'm tending to think about it very differently

varkor (Jan 22 2019 at 23:07, on Zulip):

I suppose I'm interested in where the two intersect

varkor (Jan 22 2019 at 23:09, on Zulip):

but I can content myself with pretending it's closer to the pure mathematical perspective than it actually is in reality

centril (Jan 22 2019 at 23:15, on Zulip):

@varkor I thought it was generally accepted that unsafe { .. } is a "believe me" construct that you use to do manual "proofs" of type safety and that it is the users responsibility to restore type system invariants, progress & preservation at the boundaries...

Agda and Coq have "believe me" constructs as well; but usually this does not lead anyone to state that Agda is unsound...

varkor (Jan 22 2019 at 23:16, on Zulip):

in that case, the fact that the CT model fails for Ralf's example is not important, no?

centril (Jan 22 2019 at 23:16, on Zulip):

I didn't read all of the backlog so idk

centril (Jan 22 2019 at 23:17, on Zulip):

I know of few programming languages that don't have "believe me" constructs of some form

centril (Jan 22 2019 at 23:19, on Zulip):

@varkor if we develop a denotational semantics of Rust, what would be the category? For Haskell this is a complete partial order iirc

varkor (Jan 22 2019 at 23:20, on Zulip):

some sort of category of partial maps, I'm sure

varkor (Jan 22 2019 at 23:20, on Zulip):

though honestly, my interests are far more focused on the type system than the run-time behaviour

centril (Jan 22 2019 at 23:22, on Zulip):

@varkor that seems like a very proof irrelevant perspective =P

varkor (Jan 22 2019 at 23:24, on Zulip):

it's distinguishing the type system from the programming language

varkor (Jan 22 2019 at 23:24, on Zulip):

you can have a type theory without a run-time semantics (operational or denotational)

centril (Jan 22 2019 at 23:31, on Zulip):

@varkor sure; but if your type theory is not in sync with the dynamic semantics, bad things happen...

Moreover, in a less boring type system (e.g. dependently typed) dynamic semantics become part of the types (well... not really, but at that point you might as well use the normalization rules as the runtime semantics anyways

varkor (Jan 22 2019 at 23:32, on Zulip):

LMK if you want to collaborate on a denotational semantics ;)

centril (Jan 23 2019 at 00:03, on Zulip):

ehehe :P some day, some day ;)

RalfJ (Jan 23 2019 at 10:11, on Zulip):

@varkor if we develop a denotational semantics of Rust, what would be the category? For Haskell this is a complete partial order iirc

AFAIK nobody has demonstrated categorical semantics for higher-order imperative (let alone concurrent) languages. one of many reasons why I have big reservations about categorical semantics.

RalfJ (Jan 23 2019 at 10:13, on Zulip):

also in terms of type systems, AFAIK a categorical treatment of dependent types is a mess at best. I like category theory for some things but I feel that in some PL circles it is awfully overrated.
Anyway, I'll stop ranting now^^

Last update: Nov 15 2019 at 20:25UTC