[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@haskell.org [mailto:haskell-bounces@haskell.org] On Behalf Of Ahn, Ki Yung | Sent: 23 April 2008 21:33 | To: Haskell@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@haskell.org | http://www.haskell.org/mailman/listinfo/haskell