Mantis Bug Tracker

View Issue Details Jump to Notes ] Issue History ] Print ]
IDProjectCategoryView StatusDate SubmittedLast Update
0006014OCamlOCaml typingpublic2013-05-13 14:492013-06-28 12:54
Reporteryallop 
Assigned Togarrigue 
PrioritynormalSeveritytweakReproducibilityalways
StatusconfirmedResolutionopen 
PlatformOSOS Version
Product Version 
Target VersionlaterFixed in Version 
Summary0006014: Existentials not allowed with 'let and'
DescriptionGiven

   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
TagsNo tags attached.
Attached Files

- Relationships
related to 0006057resolvedgarrigue « match e with p -> » does not generalize « e » 

-  Notes
(0009279)
garrigue (manager)
2013-05-14 01:46

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.
(0009280)
frisch (developer)
2013-05-14 11:28

Is there any hope to have "built-in" support for opening GADTs while type-checking let bindings?
(0009281)
garrigue (manager)
2013-05-14 12:33

> 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?
(0009282)
gasche (developer)
2013-05-14 15:00

> 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.
(0009283)
frisch (developer)
2013-05-14 15:20

> 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).
(0009633)
garrigue (manager)
2013-06-28 12:54

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.

- Issue History
Date Modified Username Field Change
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


Copyright © 2000 - 2011 MantisBT Group
Powered by Mantis Bugtracker