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