GADT constructor syntax
[
Home
]
[ Index:
by date

by threads
]
[ Message by date: previous  next ] [ Message in thread: previous  next ] [ Thread: previous  next ]
[ Message by date: previous  next ] [ Message in thread: previous  next ] [ Thread: previous  next ]
Date:   (:) 
From:  Jacques Le Normand <rathereasy@g...> 
Subject:  GADT constructor syntax 
Dear camllist, I would like to start a constructive discussion on the syntax of GADT constructors of the ocaml gadt branch, which can be found at: https://sites.google.com/site/ocamlgadt/ There are two separate issues: 1) general constructor form option a) type _ t = TrueLit : bool t  IntLit of int : int lit option b) type _ t = TrueLit : bool t  IntLit : int > int lit I'm open to other options. The branch has used option b) from the start, but I've just switched to option a) to see what it's like Personal opinion: I slightly prefer option b), because it makes it clear that it's a gadt constructor right from the start. This is useful because the type variables in gadt constructors are independent of the type parameters of the type, consider: type 'a t = Foo of 'a : 'b t this, counter intuitively, creates a constructor Foo of type forall 'd 'e. 'd t > 'e t. 2) explicit quantification of existential variables option a) leave existential variables implicitly quantified. For example: type _ u = Bar of 'a t : u or type _ u = Bar : 'a t > u option b) specifically quantify existential variables. For example: type _ u = Bar of 'a. 'a t : u or type _ u = Bar : 'a. 'a t > u Currently, the branch uses option a). Personal opinion: I prefer option b). This is for four reasons: I) the scope of the explicitly quantified variable is not clear. For example, how do you interpret: type _ u = Bar of 'a. 'a : 'a t or type _ u = Bar : 'a. 'a > 'a t In one interpretation bar has type forall 'a 'b. 'a > 'b t and in another interpretation it has type forall 'a. 'a > 'a t. My inclination would be to flag it as an error. II) In the example of option b), the 'a variable is quantified as a universal variable but, in patterns, it is used as an existential variable. This is something I found very confusing in Haskell where they actually use the 'forall' keyword. III) option a) is the current Haskell GADT syntax and I've never heard anyone complain about it IIII) I don't see how option b) improves either readability or bug prevention I look forward to hearing your opinions. Jacques Le Normand