Unify GADT syntax

[jordwalke]

See the discussion here: #491 (comment)

We can make GADTs less scary, by making them a natural syntactic extension of regular variant declarations.

One proposal is as follows, but is more verbose, so if you have better ideas, please discuss here:

If regular variant definitions were as follows:

type something = 
  | Constructor (int, int) : something
  | Another (list int) : something;

Then creating a GADT is not such a huge step, and the syntax helps to explain what GADTs are in the first place.

type something 'a = 
  | Constructor (int, int) : something int
  | Another (list int) : something unit;

The only problem is that (as the first example shows), in the case of regular variant definitions, there is a lot of redundancy. I'm hoping someone has a good proposed solution for this.

[ghost]

One possibility, borrowing from flow would be to use a special declaration local type, e.g., this.

With -> (favoring curried constructors):

type something = 
  | Constructor: (int, int) => this
  | Another: (list int) => this;

Closer to the current style:

type something = 
  | Constructor (int, int): this
  | Another (list int): this;

and

type something 'a = 
  | Constructor (int, int): this int
  | Another (list int): this unit;

Potential advantages are that this syntax might be intuitive to someone who has already used flow and is familiar with the idea of constructor functions there. On the other hand, it might be a little bit confusing if the user thought this had something to do with declaring a class.

[jordwalke]

I like that idea. It needn't be something restricted merely to GADT syntax unification, you could probably also use it in recursive type declarations, couldn't you?

type list 'a =
   | []
   | Const 'a (this 'a);

I just realized that the one major downside to unifying GADT syntax is that things get really verbose when you have many type parameters and aren't making use of GADTs.

type myType 'a 'b 'c =
   | C1 : this 'a 'b 'c
   | C2 : this 'a 'b 'c;

Maybe you could then, instead have this be sugar for myType 'a 'b 'c.

[jordwalke]

In OCaml, there's a way to alias shortcuts in type definitions using as, and another way using constraint. Normally, constraints would work for creating aliases to types, but the constraints apply to the entire type definition so I believe they're meaningless for ADT/GADTs.

type myType 'a 'b = | C ('a, 'b) : 'this
     constraint 'this = myType 'a 'b;

Error: Constraints are not satisfied in this type.
       Type 'this should be an instance of ('a, 'b) myType

However, having a this keyword which is an alias to theCurrentType 'x 'y ...'z would be very handy, but we'd likely have to accomplish via some other way besides constraints.

[ghost]

I like that idea. It needn't be something restricted merely to GADT syntax unification, you could probably also use it in recursive type declarations, couldn't you?

Sure, I don't see why not.

I just realized that the one major downside to unifying GADT syntax is that things get really verbose when you have many type parameters and aren't making use of GADTs.

Good point.

Maybe you could then, instead have this be sugar for myType 'a 'b 'c.

That seems like a pretty good choice to me. Another option could be to use ellipses if there's some other reason that just plain this doesn't work.

type myType 'a 'b 'c =
   | C1 : this …
   | C2 : this …;

or without this:

type myType 'a 'b 'c =
   | C1 : myType …
   | C2 : myType …;

[artemkin]

Personally, I don't like the idea of making ADT syntax more verbose just to make it more consistent with GADTs. IMHO, conciseness is a major OCaml feature. But yes, I totally agree about GADTs syntax. It is hardly consistent with other parts.

I would just consider a concrete example:

ADT

type expr =
  | SDefaultInt
  | SDefaultBool
  | SDefaultString
  | SInt of int
  | SBool of bool
  | SString of string

let str = function
  | SDefaultInt -> "42"
  | SDefaultBool -> "true"
  | SDefaultString -> "foo"
  | SInt n -> string_of_int n
  | SBool b -> string_of_bool b
  | SString s -> s

A sum type constructor may have zero or more type parameters specified immediately after of keyword. Return type is the same for all constructors, so it is implicit and never specified.

GADT

type _ expr =
  | DefaultInt : int expr
  | DefaultBool : bool expr
  | DefaultString : string expr
  | Int : int -> int expr
  | Bool : bool -> bool expr
  | String : string -> string expr

let value : type a. a expr -> a = function
  | DefaultInt -> 42
  | DefaultBool -> true
  | DefaultString -> "foo"
  | Int n -> n
  | Bool b -> b
  | String s -> s

A GADT's constructor may have zero or more type parameters specified immediately after colon. Return type should be always specified after ->.

To make it more consistent, I would keep ADT syntax as is, but change GADT syntax to:

type _ expr =
  | DefaultInt => int expr
  | DefaultBool => bool expr
  | DefaultString => string expr
  | Int of int => int expr
  | Bool of bool => bool expr
  | String of string => string expr

It looks like a natural extension of regular sum type to me.

[jordwalke]

One thought about arrows before GADT types: Suppose we create an extension (ppx or compiler pull request) to implement type constructors as functions. I feel in that case, we would want the arrows to designate the return type, and yet they would already be used in cases where the constructors were not functions. It might be wise to reserve that arrow for the day when type constructors are functions.

[artemkin]

@jordwalke hmm... arrows already designate the return type of GADT constructor in proposed syntax. How can introducing first class constructor functions affect this?

I guess ppx_variants_conv would just generate something like:

let default_int : int expr
let default_bool : bool expr
let default_string : string expr
let int : int => int expr
let bool : bool => bool expr
let string : string => string expr

[jordwalke]

@jordwalke hmm... arrows already designate the return type of GADT constructor in proposed syntax.

You could argue that this is not true because arrows don't describe the "return type" of GADT constructors if they're not truly functions - they don't "return" anything. What if you wanted to distinguish between constructors that are functions (via some ppx extension etc) and ones that aren't? The ones that are indeed functions would have "return types" and I think arrows would be appropriate. When there also exists constructors which are not first class functions, you'd probably expect that there be no arrow to describe their type. At least those are my current thoughts on it.

[foretspaisibles]

I second @artemkin opinion that it is a bad thing to make the declaration of sum types more verbose to make GADT's look less odd.

I do not understand how this syntax improves the consistency:

type _ expr =
  | DefaultInt => int expr
  | DefaultBool => bool expr
  | DefaultString => string expr
  | Int of int => int expr
  | Bool of bool => bool expr
  | String of string => string expr

In upstream OCaml, the : is always used to introduce a type annotation (or in the broader sense, a module type), so that it seems a rather clumsy move to me to take something clean “I introduce a type annotation with colon” to something a bit strange like “sometimes I introduce type annotation with colon, sometimes with =>”

[artemkin]

@michipili I meant inconsistency of of in regular sum types, and : in GADTs. of is a kind of type annotation as well.

To convert ADT to GADT, you would need to replace String of string with String : string -> string expr. In proposed syntax, you would just add => string expr to explicitly specify return type.

@jordwalke

constructors if they're not truly functions - they don't "return" anything

It can be treated as a zero arity function, so it depends on the point of view)) Anyway, you can always use unary constructor with a parameter of unit type:

| SomeString of unit => string expr

[foretspaisibles]

@artemkin I see, thank you for the clarification! An inconvenient of the -> or => in the declaration is that it hints at functions, and type constructors are not functions. Maybe the : would be here of great use:

type _ expr =
  | DefaultInt : int expr
  | DefaultBool : bool expr
  | DefaultString : string expr
  | Int of int : int expr
  | Bool of bool : bool expr
  | String of string : string expr

This is consistent with usual type annotations introduced by :. While we are at it, I think the declaration of functions using GADTs in this form

let f: type a. a expr -> int = …

is a bit awkward, esp. since the concurrent way

let f (type a) (expr : a expr) : int =
  …

does not mention the ..

Does it seem doable (and desirable?) to change the former to let f: (type a) a expr -> int = … ? Or something totally different?

I do not want to let this thread drift too far away but it seems natural to discuss the syntax of functions using some types with the syntax of the definition of thee types.

[artemkin]

@michipili I like the idea of using :.