[Haskell] How to define tail function for Even/Odd GADT lists?
Simon PeytonJones
simonpj at microsoft.com
Thu Apr 24 03:52:26 EDT 2008
[Redirecting to ghcusers]
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 reexpressing 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: haskellbounces at haskell.org [mailto:haskellbounces 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 fglasgowexts 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
More information about the Glasgowhaskellusers
mailing list