apfelmus at quantentunnel.de apfelmus at quantentunnel.de
Wed Jan 31 10:28:26 EST 2007

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

> [...]

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

Isn't the problem simply that in the former 'thicken', the compiler can
not guarantee that the case

thicken (Fs i)  Fz      = Just Fz

does never show up when we have 'thicken :: Fin (S Z) -> ...'? I mean
the subtle point about Fin is that 'Fz' is the "only" inhabitant of 'Fin
(S Z)'. At least, this is what Epigram can deduce. But due to _|_, every
constructor that is declared may appear in the form of

Fs _|_

That's why only the latter 'thicken' can be correct.

Regards,
apfelmus

```