GADTs.

gadt.hs

{-# LANGUAGE GADTs #-}
{-# LANGUAGE Rank2Types #-}

{-
  Lets start ^^ by enabling some language extensions. GADTs to encode our data types and
  Rank2Types for the existental we will need to hide our types when we don't care about
  the invariant.
 -}


{-
  Lets start with our key data type, we want to be able to represent
  keys that point to a String, an Int or a Bool.
 -}
data Key a
  {- TODO -}


{-
  Lets than create an "entry in a bag" that holds any well typed
  key-value pair. Note well that we explicitly want to hide the
  invariants that our keys maintain at this point.
 -}
data Entry
  {- TODO -}

{-
  A simple representation of a Bag as a list of entries.
 -}
type Bag =
  [Entry]

flag :: Key Bool
flag = error "todo: flag"

counter :: Key Int
counter = error "todo: counter"

name :: Key String
name = error "todo: name"

stuff :: Bag
stuff =
  error "todo: an example bag of stuff using our flag, counter and name keys"

get :: Key a -> Bag -> Maybe a
get =
  error "todo: a generic get operation with a much better api and fewer possible errors."

gadt.md

A Basic GADT Challenge

• I have a bag of stuff.
• My bag is awesome it can hold different types of things allocated by a name.
• My bag is kind of ok, in that it can only hold certain types of things. Specifically it can hold Int's, String's and Bool's. But this also makes it convenient to access those things.
• Conveniently the key tells me what type to expect.

In my haskell2010 world, I implement this as a simple data type:

data Key = Key String
data Value = I Int | S String | B Bool
data Bag = Bag [(Key, Value)]

And I can implement things like:

data Result a =
    NotFound
  | InvalidType String
  | Value a

getBool :: Bag -> Key -> a Bool

But this is obviously less than desirable, I have two errors to handle:

1. Whether the value exists or not
2. Whether the value was a bool

I also didn't use the info, that I know the type based on my key.

Lets build better a Key data type such that it encodes the type of the value, and then change value, such that it can only be indexed by an appropriately typed key.

The point of this exercise is to:

• Learn how to encode an invariant using GADTs and phantom types.

• Hide that invariant using existential types.

• Use pattern matching to "re-learn" about your extra invariant in your implementation such that we can build a better API (for example an API where we can't get store the wrong type data against a key.

• Experiment with why you would use GADTs over more traditional data types.

• Discuss the balance of trading off forcing error handling as "proof" carying code vs returning error conditions.