What is a GADT?

GADTs can be seen as a restricted form of dependent types, where the stage-distinction between terms and types is not lost. They allow data constructors to bear extra type annotations that can describe the shape, size, content, or other properties of the data. These annotations can be used to express key invariants of the data structures, and thus rule out invalid uses of the data. – ref

GADT version of Monad

Remember my previous comment about Monad implemented using GADT?

All GADT does there is about registering.

Now I make a slight correction: In fact, all GADT does there is about promise. The type signature D a does not exactly mean that there is an element of type a wrapped in D, instead, it means that something will happen in the computation of D a and will certainly return you an element of type a upon request. This kind of construction defines information/existence in a most abstract way, that is great!

We should use GADT there, instead of normal ADT, because the concept we are trying to define there is not normal Monad, instead, it is a Monad that wrapped in a single type. That is, Return and Bind is used to build AST declared by a single type. And the AST definition, not like those in ADT, can wrap computational effect inside.

We know there could be something silently happened along the computational chain of a Monad. Unlike a normal ADT Monad, the GADT Monad defined here allows arbitrary side effects to be defined later and uses some trigger function to trigger the computation chain, a very clever implementation of lazy evaluation.(laziness not provided by haskell, but provided by GADT definition itself)

GADT as singleton type

The GADT concept can go farther. That is, it not only works as indexed type, where a type parameter reflects a property of the value contents. But also a singleton type, where a GADT value represents exactly one type. The value of this singleton type can then serve to trigger the polytypic behavior of a function.

Let's learn this through an example in haskell:

For more details(the original ocaml version of demonstration), one can follow this tutorial

{-# LANGUAGE GADTs #-}

data Typ a where
    TInt    :: Typ Int
    TString :: Typ String
    TPair   :: (Typ a, Typ b) -> Typ (a, b)

The Typ type defined above is a haskell GADT, where the type constructor could return different forms of Typ a, including Type Int, Type String and Typ (a, b). This allows a more fine-grained control of a type polymorphisms. (remind that normal ADT is defined in the way M a => D a where a belongs to the typeclass M, this kind of control is obviously looser than what we see here in GADT). Also note that the TInt and TString constructors do not take any arguments and are therefore singleton types. However, their type signatures are Typ Int and Typ String, which suggests that they are related to Int and String types. This is similar to the promise idea we have seen before.

Then, let us define a pretty print function for this GADT type:

to_string :: Typ a -> a -> String 
to_string TInt    x = show x 
to_string TString x = "s:" ++ x 
to_string (TPair (tx, ty)) (x, y) = "(" 
            ++ (to_string tx x) 
            ++ "," 
            ++ (to_string ty y) 
            ++ ")"

This function takes one argument, tx :: Typ a, and another, x :: a, and returns the nicely formatted string representation of x. Note that we can see from this that tx :: Typ a only acts as a trigger for the polytypic behavior of the function to_string, i.e., if Type a is a Typ Int, the function will use show for x or, if it is a Typ String, it will use \x -> "s:" ++ x instead.

Finally, let's run this in a demo:

main :: IO ()
main = do 
    let s = TPair (TInt, TString)
        t = (1, "a")
    print $ to_string s t

It will nicely print "(1,s:a)" in terminal.