[Haskell-cafe] GADTs: the plot thickens?
Conor McBride
ctm at cs.nott.ac.uk
Wed Jan 31 06:46:40 EST 2007
Hi folks
A puzzle for you (and for me too). I just tried to translate an old
Epigram favourite (which predates Epigram by some time) into GADT-speak.
It went wrong. I had a feeling it might. I wonder how to fix it: I
imagine it's possible to fix it, but that some cunning may be necessary.
Here it is:
Type-level Nat
> data Z = Z
> data S x = S x
Finite sets: Fin Z is empty, Fin (S n) has one more element than Fin n
> data Fin :: * -> * where
> Fz :: Fin (S n)
> Fs :: Fin n -> Fin (S n)
The "thinning" function: thin i is the order-preserving embedding from
Fin n to Fin (S n) which never returns i.
> thin :: Fin (S n) -> Fin n -> Fin (S n)
> thin Fz i = Fs i
> thin (Fs i) Fz = Fz
> thin (Fs i) (Fs j) = Fs (thin i j)
Its partial inverse, "thickening" has the spec
thicken i i = Nothing
thicken i (thin i j) = Just j
> thicken :: Fin (S n) -> Fin (S n) -> Maybe (Fin n)
> thicken Fz Fz = Nothing
> thicken Fz (Fs j) = Just j
> thicken (Fs i) Fz = Just Fz
> thicken (Fs i) (Fs j) = fmap Fs (thicken i j)
The trouble is that whilst thin compiles, thicken does not. GHC rightly
complains
Thicken.lhs:18:32:
Couldn't match expected type `n' (a rigid variable)
against inferred type `S n1'
`n' is bound by the type signature for `thicken'
at Thicken.lhs:15:19
Expected type: Fin n
Inferred type: Fin (S n1)
In the first argument of `Just', namely `Fz'
In the expression: Just Fz
The trouble is that (Fs i) is only known to be of some type Fin (S n),
so we need to return the Fz :: Fin n, and there ain't no such beast.
The question is how to explain that this program actually does make some
sense.
One to ponder.
Cheers
Conor
More information about the Haskell-Cafe
mailing list