Carlo Hamalainen


Fiddling with GADTs

2013-05-16

Check the depth of the structure:

*Main> depth T0
0
*Main> depth (Tm T0)
1
*Main> depth (Tm (Tm (Tm (Tm T0))))
4

The function twoOfSameDepth expects both parameters to be of the same depth. If not, you get a type error.

*Main> :t twoOfSameDepth T0 T0
twoOfSameDepth T0 T0 :: Int
*Main> :t twoOfSameDepth T0 (Tm T0)

<interactive>:1:20:
    Couldn't match expected type `'Z' with actual type `S n0'
    Expected type: T 'Z
      Actual type: T (S n0)
    In the return type of a call of `Tm'
    In the second argument of `twoOfSameDepth', namely `(Tm T0)'

The function secondIsPlusOne expects the second parameter to be of depth one more than the first parameter:

*Main> :t secondIsPlusOne T0 (Tm T0)
secondIsPlusOne T0 (Tm T0) :: Bool
*Main> :t secondIsPlusOne T0 (Tm (Tm T0))

<interactive>:1:25:
    Couldn't match expected type `'Z' with actual type `S n0'
    Expected type: T 'Z
      Actual type: T (S n0)
    In the return type of a call of `Tm'
    In the first argument of `Tm', namely `(Tm T0)'
*Main> 

In Matt's LambdaJam talk/jam you can see how this idea can be used to help with implementing a b-tree data structure.