Hi Ki
Yung,
It depends a bit on what you want to use these lists for, but the
following encoding works for your examples and doesn't need the type
class.
data E
data O
type Even = (E,O)
type Odd = (O,E)
data List p a where
Nil :: List a Even
Cons :: a -> List a (p1,p2) -> List a (p2,p1)
head (Cons x _) = x
tail (Cons _ xs) = xs
test1 = Nil :: forall a. List a Even
test2 = Cons True Nil :: List Bool Odd
test3 = Cons False (Cons True Nil) :: List Bool Even
test4 = tail test3 :: List Bool Odd
Cheers,
Martijn
Ahn, Ki Yung wrote:
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
[email protected]
http://www.haskell.org/mailman/listinfo/haskell
|
_______________________________________________
Haskell mailing list
[email protected]
http://www.haskell.org/mailman/listinfo/haskell
