Hello Conor,
The following seems to work:
On 31 Jan 2007, at 11:46, Conor McBride wrote:
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
Lets also have naturals reflected at the value level:
> data Nat :: * -> * where
> Zero :: Nat Z
> Succ :: Nat n -> Nat (S n)
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.
Now we modify thin to take an extra Nat n (not needed, but just to
show the duality with thickening):
> thin :: Nat n -> Fin (S n) -> Fin n -> Fin (S n)
> thin n Fz i = Fs i
> thin (Succ n) (Fs i) (Fz) = Fz
> thin (Succ n) (Fs i) (Fs j) = Fs (thin n i j)
The thing to note here is that only:
> thin (Succ n) (Fs i) (Fz) = Fz
is well typed; if you had the case:
> thin Zero (Fs i) (Fz) = Fz
you get:
Conor.lhs:28:21:
Inaccessible case alternative: Can't match types `S n' and `Z'
In the pattern: Fz
In the definition of `thin': thin Zero (Fs i) (Fz) = Fz
Failed, modules loaded: none.
Its partial inverse, "thickening" has the spec
thicken i i = Nothing
thicken i (thin i j) = Just j
Now lets go for the thickening function:
> thicken :: Nat n -> Fin (S n) -> Fin (S n) -> Maybe (Fin n)
> thicken n Fz Fz = Nothing
> thicken n Fz (Fs j) = Just j
> thicken Zero (Fs i) Fz = Nothing
> thicken (Succ _) (Fs i) Fz = Just Fz
> thicken (Succ n) (Fs i) (Fs j) = fmap Fs (thicken n i j)
Note that this version of thicken is more precise than the version
you had -- your third case splits into two
different cases now. The problem is that when you had:
> thicken (Fs i) Fz = ...
you need to account for two possibilities: the first possibility is
(Fz :: Fin (S Zero)), to which you want to return Nothing
and (Fz :: Fin (S (S n))) for which you can safely return Just Fz.
Let me know if that helps.
Cheers,
Bruno
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
