|Anonymous | Login | Signup for a new account||2017-09-24 08:37 CEST|
|Main | My View | View Issues | Change Log | Roadmap|
|View Issue Details|
|ID||Project||Category||View Status||Date Submitted||Last Update|
|0006014||OCaml||typing||public||2013-05-13 14:49||2017-03-07 14:20|
|Target Version||later||Fixed in Version|
|Summary||0006014: Existentials not allowed with 'let and'|
type t = T : 'a -> t
the following is accepted:
let T x = T 3 in ()
but a slight variant using 'let and' (or 'let rec and') is rejected:
let T x = T 3 and () = () in ()
with the message:
Error: Unexpected existential
|Tags||No tags attached.|
Indeed, "let T x = T 3 in expr" is handled as syntactic sugar for "match T 3 with T x -> expr".
This is not the case for the two other constructs.
This should probably be documented.
|Is there any hope to have "built-in" support for opening GADTs while type-checking let bindings?|
> Is there any hope to have "built-in" support for opening GADTs while type-checking let bindings?
There are several cases:
* simple let bindings (not rec, no and) are already supported.
* multiple non-recursive let-bindings could probably be supported with some effort.
Part of the problem is the semantics: if we use the classical approach of converting to a big tuple, we have the side-effect that equations are propagated from the left to the right. Do we really want that? Is there any other approach.
* recursive let bindings: honestly I don't know what it would mean for an existential type variable to be accessed in the body of its own definition...
So don't hold your breath.
Do you have any practical example where this would be handy?
> Part of the problem is the semantics: if we use the classical approach of converting to a big tuple, we have the side-effect that equations are propagated from the left to the right. Do we really want that? Is there any other approach.
How can the propagation be a problem? Can we run into, say, ambiguity errors that wouldn't have existed in absence of propagation? I think people would expect (let p1 = e1 and p2 = e2 in e3) and (match e1,e2 with p1,p2 -> e3) to have the same behavior. They also expect nonrec-"and"-bindings to be independent and reorderable, but they can probably live with the idea that opening GADTs breaks this property. This will in any case be much less surprising than single-let succeeding and let-and failing to type-check.
> * recursive let bindings: honestly I don't know what it would mean for an existential type variable to be accessed in the body of its own definition...
Pattern-matching is not allowed as the defined-part of a let rec (only in function arguments), so I don't see how GADTs can be opened in that case.
> Part of the problem is the semantics: if we use the classical approach of converting to a big tuple
My question was rather: can we support directly, at reasonable cost, the opening of GADTs existentials in the normal type-checking of let bindings, without going to an encoding into a "match".
Non-recursive "let and" bindings are not very different from a sequence of single let bindings, except for scope management, but this does not seem very deep (we could just type-check each let-binding in the same initial environment, no?). So supporting them again by a translation to match cases should be doable (but it might not justify the effort, I agree).
I don't think it would be a good idea to duplicate the code in type_let, as this just increases the chances for bugs.
If we agree that the semantics should be that of a big a tuple, it shall probably be fine.
I don't think there is any overhead involved, at least for native code.
|2013-05-13 14:49||yallop||New Issue|
|2013-05-14 01:46||garrigue||Note Added: 0009279|
|2013-05-14 11:28||frisch||Note Added: 0009280|
|2013-05-14 12:33||garrigue||Note Added: 0009281|
|2013-05-14 12:33||garrigue||Assigned To||=> garrigue|
|2013-05-14 12:33||garrigue||Status||new => confirmed|
|2013-05-14 15:00||gasche||Note Added: 0009282|
|2013-05-14 15:20||frisch||Note Added: 0009283|
|2013-06-18 10:32||frisch||Severity||minor => tweak|
|2013-06-18 10:32||frisch||Target Version||=> later|
|2013-06-28 11:18||frisch||Relationship added||related to 0006057|
|2013-06-28 12:54||garrigue||Note Added: 0009633|
|2017-02-23 16:45||doligez||Category||OCaml typing => typing|
|2017-03-07 14:20||shinwell||Severity||tweak => feature|
|Copyright © 2000 - 2011 MantisBT Group|