[Haskell] How to define tail function for Even/Odd GADT lists?
simonpj at microsoft.com
Thu Apr 24 03:52:26 EDT 2008
[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.
| -----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 )
| 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.
| 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
More information about the Glasgow-haskell-users