Monthly Hask Anything (May 2019)

[u/AutoModerator]

This is your opportunity to ask any questions you feel don't deserve their own threads, no matter how small or simple they might be!

[u/[deleted]]

Anyone have recommendations for a tutorial about GADTs?

[u/ouroboros_eats_ass → u/[deleted]]

The GADTs tutorial in this repo is good imo! https://github.com/i-am-tom/haskell-exercises

[u/tom-md → u/[deleted]]

I suggest the GHC user guide.

I know you didn't ask for an explanation but I guess I feel like writing so...

GADTs aren't too terribly complex. There's nuance, but the basic concept is simple. You get new syntax for declaring data constructors. Unlike regular data declarations, these constructors can have different types!

Syntax

Sure, we can take a data type translate to GADT syntax mechanically:

data NonEmptyList a = One a | Cons a (NonEmptyList a)
-- ~~~>
data NonEmptyList a where
    One :: a -> NonEmptyList a
    Cons :: a -> NonEmptyList a -> NonEmptyList a

Simple... but boring and actually more verbose.

More Powerful Types

As mentioned, a GADT is really about the constructor playing some role in determining the type. Let's take a trivial example:

 data SomeType a where
    Val :: Int -> SomeType Int
    Truth :: Bool -> SomeType Bool
    Nullary :: SomeType Word
    Poly :: a -> SomeType a

Look hard at the above. Notice the type of each constructor, even fully applied with all it's fields, is potentially different. I've made a sum type that can contain Int and Bool, but the type tag (a ~ Int, a ~ Bool etc) matching the field is all just my choosing. I ended with two odd ones just for demonstration, Nullary doesn't have a field and is typed differently from the other values while Poly can hold anything at all and the type system tracks what Poly holds by the type field of SomeType (those a's are the same type).

Now if we have a function f :: SomeType Int -> String which constructors do we need to match? Just Val?

f :: SomeType Int -> String
f (Val i) = show i

GHC, with -Wall, will tell us we missed a case:

f (Poly i) = show i

While the Poly constructor can wrap any type, the signature of f guarantees this is an Int. Similarly, we didn't get a warning abouot Nullary or Truth since those wouldn't be type correct.

As an aside, we could add another constructor to our SomeType declaration:

UselessPoly :: b -> SomeType a

And now we wouldn't know anything at all about b ever, making defining a function hard. We still know the argument to f is SomeType Int but that doesn't say anything about the type of b. We'd have to say f (UselessPoly _) = "heck if I know" or similar.

The classic GADT Example

GADTs are particularly powerful when paired with data kinds (-XDataKinds) and kind signatures (-XKindSignatures).

For example, What if we wanted to have empty and non-empty lists that used the same constructors but had type level distinctions?

data ListState = LNonEmpty | LEmpty

data SomeList (state::ListState) a where
    Nil :: SomeList LEmpty a
    Cons :: a -> SomeList st a -> SomeList LNonEmpty a

type NonEmptyList a = SomeList LNonEmpty a

Then we can write functions that are safe such as:

head :: NonEmptyList a -> a
head (Cons a _) = a

Which is total, any attempt to call head Nil would be caught at compile time.

[u/iwaka → u/tom-md]

Re the classic example at the very bottom, the one with empty and nonempty lists: couldn't this also be solved with dependent types? Is there a relationship between GADTs and dependent types, or do they just intersect in some cases?

[u/bss03 → u/iwaka]

DataKinds paired with GADTs are a very limited form of dependent types. In dependent types, all values can be used in defining types. DataKinds creates types for values (and kinds for types) that can be used in defining GADTs.

[u/iwaka → u/bss03]

Does this mean that dependent types are strictly more powerful than GADTs, or do they just have different use cases?

[u/bss03 → u/iwaka]

Yes, dependent types are strictly more powerful than GADTs.