GADTs: the plot thickens?

Previous Topic Next Topic
 
classic Classic list List threaded Threaded
9 messages Options
Reply | Threaded
Open this post in threaded view
|

GADTs: the plot thickens?

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

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Fwd: GADTs: the plot thickens?

Pablo Nogueira-2
---------- Forwarded message ----------
From: Pablo Nogueira <[hidden email]>
Date: 31-Jan-2007 12:04
Subject: Re: [Haskell-cafe] GADTs: the plot thickens?
To: Conor McBride <[hidden email]>


I haven't tried this yet, but would declaring the class Nat be a starting point?

class Nat n
instance Nat Z
instance Nat n => Nat (S n)

data Fin :: * -> * where
   Fz :: Nat n => Fin (S n)
   Fs :: Nat n => Fin n -> Fin (S n)

thin :: Nat n => Fin (S n) -> Fin n -> Fin (S n)
thicken :: Fin (S n) -> Fin (S n) -> Maybe (Fin n)

Btw, apparently we have to use GHC HEAD if we want GADTs to compile properly.

The error seems very similar to the one you get when trying to write
(++) for dependent lists with length encoded as GADTs. To make sure I
understand,  you are asking if there is a hack that will enable us to
tell the Haskell type checker that  n = (S n1), right?

Regards,
P.
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: GADTs: the plot thickens?

Bruno Oliveira-5
In reply to this post by Conor McBride
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
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: GADTs: the plot thickens?

Pablo Nogueira-2
Bruno,

> Now we modify thin to take an extra Nat n (not needed, but just to
> show the duality with thickening):

I'm puzzled by the "not needed" bit. Isn't the introduction of  Fin's
indices reflected as values in  the GADT , and the fact that the GADT
makes that reflection, what makes it work?

P.
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: GADTs: the plot thickens?

Bruno Oliveira-5
Hello Pablo,

What I meant was simply that the function thin does not need the  
extra Nat n argument to compile;
Conor's original version was already compiling:

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

The reason why I modified thin was to show the similarity with  
thicken (since thicken is the partial inverse
of thin). When you have the new version of thin:

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

it becomes easier to see how to define the inverse, for example we  
can see that there is not a case for:

 > thin Zero  (Fs i)  (Fz)    = Fz    -- type-error

which hints for the following case in thicken:

 > thicken Zero             (Fs i)  Fz      = Nothing

So, although having the new version of thin helps you with the  
definition of thicken, we do not need it to have
a working thin function. That's all I meant.

Cheers,

Bruno

On 31 Jan 2007, at 12:57, Pablo Nogueira wrote:

> Bruno,
>
>> Now we modify thin to take an extra Nat n (not needed, but just to
>> show the duality with thickening):
>
> I'm puzzled by the "not needed" bit. Isn't the introduction of  Fin's
> indices reflected as values in  the GADT , and the fact that the GADT
> makes that reflection, what makes it work?
>
> P.
> _______________________________________________
> Haskell-Cafe mailing list
> [hidden email]
> http://www.haskell.org/mailman/listinfo/haskell-cafe

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: GADTs: the plot thickens?

Pablo Nogueira-2
Aha, of course, Sorry, I misunderstood you.
P.
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: GADTs: the plot thickens?

Conor McBride
In reply to this post by Conor McBride
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

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: GADTs: the plot thickens?

Wolfram Kahl
In reply to this post by Conor McBride
Hi Connor,

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


To me, this looks more like ordinal numbers than like general finite sets:
For each type-level natural number n, the set  Fin n  contains
all object-level natural numbers k < n,
where  k = Fs^k Fz .

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


So ``thin Fz i''  is defined for  i = undefined :: Fin Z.

If you don't want this kind of effect, you might consider to keep the empty
type away from your calculations:

> {-# OPTIONS -fglasgow-exts #-}
> data Z = Z
> data S x = S x

> data Fin :: * -> * where
>   Fz :: Fin (S n)
>   Fs :: Fin (S n) -> Fin (S (S n))

> thin :: Fin (S (S n)) -> Fin (S n) -> Fin (S (S n))
> thin Fz      i       = Fs i
> thin (Fs i)  Fz      = Fz
> thin (Fs i)  (Fs j)  = Fs (thin i j)

This gets me one line farther into thicken.
But what is possible now:

Add a lifting (or embedding) function:

> lift :: forall n . Fin n -> Fin (S n)
> lift Fz = Fz
> lift (Fs i) = Fs (lift i)

> thicken0 :: forall n . Fin n -> Fin n -> Maybe (Fin n)
> thicken0 Fz      Fz      = Nothing
> thicken0 Fz      (Fs j)  = Just (lift j)
> thicken0 (Fs i)  Fz      = Just Fz
> thicken0 (Fs i)  (Fs j)  = case (thicken0 i j) of
>      Nothing -> Nothing
>      Just k -> Just (Fs k)


I think that one ley to your trouble is the fact that there is,
as far as I can see, no direct way to define
a predicate determining whether an Fin (S n) element
is the largest of its type:

> isMax :: forall n . Fin (S n) -> Bool
> isMax = undefined

This would need a type case on  Fz :: Fin (S Z)  ---
I'd dig through Oleg's posts about type equality checking.

If you can make this possible, cou can also define

> unlift :: forall n . Fin (S n) -> Maybe (Fin n)
> unlift = undefined

and get your original thicken from that.


Wolfram
_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: GADTs: the plot thickens?

Heinrich Apfelmus
In reply to this post by Conor McBride
> 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

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe