[Haskell] How to define tail function for Even/Odd GADT lists?

[Simon Peyton-Jones]

[Redirecting to ghc-users]

You're right that tailList "ought" to work.  There are at least two reasons that it doesn't.

First, GHC does not have a robust implementation of GADTs + functional dependencies. The interaction is very tricky.

So I tried re-expressing it using type families, thus:

    data Even; data Odd

    type family Flip a :: *
    type instance Flip Even = Odd
    type instance Flip Odd = Even

    data List a b where
       Nil  :: List a Even
       Cons :: a -> List a b -> List a (Flip b)

    tailList :: List a b -> List a (Flip b)
    tailList (Cons _ xs) = xs

(I find the program quite a bit easier to read in this form.)

Now I get the error (from the HEAD)

    Occurs check: cannot construct the infinite type: b = Flip (Flip b)
    In the pattern: Cons _ xs
    In the definition of `tailList': tailList (Cons _ xs) = xs

There's a bug here -- reporting an occurs check is premature.  But there is also a real problem: if you look at the type constraints arising from tailList you'll see that you get
        c ~ Flip b
        b ~ Flip c
where c is the existential you get from the GADT match. Now, *we* know that b = Flip (Flip b) is always tru, but GHC doesn't. After all, you could add new type instances

        type instance Flip Int = Bool
        type instance Flip Bool = Char

and then the equation wouldn't hold. The best we can hope for is to get

        tailList :: (b ~ Flip (Flip b)) => List a b -> List a (Flip b)

although this too is rejected at the moment because of the above bug.

What we really want is a *closed* type family, like this

        type family Flip a where
                Flip Even = Odd
                Flip Odd = Even

(preferably supported by kinds) and even *then* it's not clear whether it's reasonable to expect the compiler to solve the above problem by trying all possibilities.  This relates to http://hackage.haskell.org/trac/ghc/ticket/2101

That is probably more than you wanted to know.  Since there's a bug here, I'll make a ticket.

Simon

| -----Original Message-----
| From: haskell-bounces at haskell.org [mailto:haskell-bounces at haskell.org] On Behalf Of Ahn, Ki Yung
| Sent: 23 April 2008 21:33
| To: Haskell at haskell.org
| Subject: [Haskell] How to define tail function for Even/Odd GADT lists?
|
| Using GADTs and functional dependencies, we can define GADT lists
| that statically distinguishes even length lists from odd length lists.
|
| > data Even
| > data Odd
| >
| > class Flip b c | b -> c, c -> b where
| >
| > instance Flip Even Odd where
| > instance Flip Odd Even where
| >
| > data List a b where
| >   Nil  :: List a Even
| >   Cons :: Flip b c => a -> List a b -> List a c
|
| For example,
|
| Nil :: forall a. List a Even
| Cons True Nil :: List Bool Odd
| Cons False (Cons True Nil) :: List Bool Even
|
|
| We were able to define the function that returns the head.
|
| > headList :: List a b -> a
| > headList (Cons x _) = x
|
| However, we were not able to write a function that returns the tail.
|
| > tailList :: Flip b c => List a b -> List a c
| > tailList (Cons _ xs) = xs
|
| Is there a way to define the tailList function within the current
| GHC type system implementation (maybe using some other language
| extensions), or do we need to improve the type system regarding
| GADTs and functional dependencies?
|
| $ ghci -fglasgow-exts EOlist.hs
| GHCi, version 6.8.2: http://www.haskell.org/ghc/  :? for help
| Loading package base ... linking ... done.
| [1 of 1] Compiling Main             ( EOlist.lhs, interpreted )
|
| EOlist.lhs:30:25:
|     Couldn't match expected type `c' against inferred type `b1'
|       `c' is a rigid type variable bound by
|           the type signature for `tailList' at EOlist.lhs:29:21
|       `b1' is a rigid type variable bound by
|            the constructor `Cons' at EOlist.lhs:30:12
|       Expected type: List a c
|       Inferred type: List a b1
|     In the expression: xs
|     In the definition of `tailList': tailList (Cons _ xs) = xs
| Failed, modules loaded: none.
| Prelude>
|
| Note: You can save this message content as EOList.lhs and load the
| script with ghci to observe the type error message above.
| _______________________________________________
| Haskell mailing list
| Haskell at haskell.org
| http://www.haskell.org/mailman/listinfo/haskell