[Haskell-cafe] GADTs: the plot thickens?
ctm at cs.nott.ac.uk
Wed Jan 31 06:46:40 EST 2007
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:
> 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
Couldn't match expected type `n' (a rigid variable)
against inferred type `S n1'
`n' is bound by the type signature for `thicken'
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
One to ponder.
More information about the Haskell-Cafe