Hi Bruno This looks like the stuff!
Lets also have naturals reflected at the value level:
data Nat :: * -> * where Zero :: Nat Z Succ :: Nat n -> Nat (S n)
Good plan. Of course, if you combine this method with Pablo's suggestion, you can make the class RepNat n whose method is repNat :: Nat n and then wrap your explicit versions in implicit versions. Implicit information inferred from type information but passed at run time: it's something we need to get used to. I'm glad we only need three definitions of the natural numbers, none of which is data Nat = Zero | Succ Nat
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.
That's a relief. Of course, in Epigram, you get that n is a successor for free, the moment you look at an element of Fin n.
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.
I thought that might work. Your solution is quite close to the Epigram version of the program, but you haven't covered the Zero (Fs i) (Fs j) case, which is impossible anyway. I suggest the following minor modification, whose significance is purely documentary.
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) j = undefined {- i stinks -} thicken (Succ _) (Fs i) Fz = Just Fz thicken (Succ n) (Fs i) (Fs j) = fmap Fs (thicken n i j)
The Epigram version explicitly refutes i in the case where it inhabits Fin Z. I thought of this example because of the other thread about empty cases.
Let me know if that helps.
It certainly delivers the necessary explanation. What has happened here? Somehow, we discovered that we had to shift some data from the static language to the dynamic language so that we could give the compiler enough information to see what was ok about the program we started with. There's something subtle here. If the compiler just magically swallowed my earlier program, I think we'd lose type safety, because it allows us to manufacture a non-_|_ inhabitant of (Fin Z) fromJust (thicken (Fs undefined) Fz) = Fz :: Maybe (Fin Z) So you really need a safety check there. Another way to do it, crudely but avoiding the run time numbers, is this
thicken :: Fin (S n) -> Fin (S n) -> Maybe (Fin n) thicken Fz Fz = Nothing thicken Fz (Fs j) = Just j thicken (Fs Fz) Fz = Just Fz thicken (Fs Fz) (Fs j) = fmap Fs (thicken Fz j) thicken (Fs (Fs i)) Fz = Just Fz thicken (Fs (Fs i)) (Fs j) = fmap Fs (thicken (Fs i) j)
That's just another way to get the strictness you need. Although it's ugly. Perhaps it's possible to pack up the explanation "every element of a finite set is an element of a nonempty finite set" as some sort of view, although not the sort of view currently being proposed, I guess. Exactly what information is needed in which phase and how totality or its absence affects what's possible are interesting and subtle questions. We live in interesting times. All the best Conor