Conor McBride ctm at cs.nott.ac.uk
Wed Jan 31 09:01:23 EST 2007

```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

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
> 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

```