Generalized algebraic data types

[brendanzab]

Would be lovely to have GADTs!

Eg.

type Expr : Type -> Type =
    | Bool  : Bool     -> Expr Bool
    | Int   : Int      -> Expr Int
    | Equal : Expr Int -> Expr Int  -> Expr Bool

type StateEff : Type -> Type -> Type =
    | Get : StateEff s s
    | Put : s -> StateEff s ()

• https://en.wikipedia.org/wiki/Generalized_algebraic_data_type
• https://wiki.haskell.org/Generalised_algebraic_datatype
• https://downloads.haskell.org/~ghc/7.0-latest/docs/html/users_guide/data-type-extensions.html#gadt
• http://research.microsoft.com/en-us/um/people/simonpj/papers/gadt/

[brendanzab]

Not sure how row polymorphism fits in with this though - I haven't really been able to find anything in the literature about it row polymorphic GADTs.

I am wondering if our unions should be closed by default, but that is a different discussion...

[Marwes]

Closed by default seems like what one wants most of the time. No idea how row polymorphism works with GADTs either. GADTs do make inference undecidable however so possibly row-polymorphism would make it even more undecidable (not that the current type system is decidable either, but there is a risk of introducing to much undecidable constructs).

[Nadrieril]

GADTs can have decidable inference with only a few annotations (see here for example), at least in system F. In Fω however, i.e. with arbitrary type lambdas, I'm not sure this would work as well...