<!DOCTYPE html PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN">
<html>
<head>
  <meta content="text/html;charset=EUC-KR" http-equiv="Content-Type">
</head>
<body bgcolor="#ffffff" text="#000000">
<font face="Helvetica, Arial, sans-serif"><font face="Verdana">Hi Ki
Yung,<br>
<br>
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.</font><font face="Courier New, Courier, monospace"> <br>
<blockquote type="cite">data E<br>
data O<br>
  <br>
type Even = (E,O)<br>
type Odd&nbsp; = (O,E)<br>
  <br>
data List p a where<br>
&nbsp; Nil&nbsp; :: List a Even<br>
&nbsp; Cons :: a -&gt; List a (p1,p2) -&gt; List a (p2,p1)<br>
  <br>
head (Cons x _)&nbsp; = x<br>
tail (Cons _ xs) = xs<br>
  <br>
test1 = Nil :: forall a. List a Even<br>
test2 = Cons True Nil :: List Bool Odd<br>
test3 = Cons False (Cons True Nil) :: List Bool Even<br>
test4 = tail test3 :: List Bool Odd<br>
</blockquote>
<font face="Verdana">Cheers,<br>
Martijn<br>
</font></font><br>
</font>Ahn, Ki Yung wrote:
<blockquote cite="mid:480F9D02.3090406@gmail.com" type="cite">
  <pre wrap="">Using GADTs and functional dependencies, we can define GADT lists
that statically distinguishes even length lists from odd length lists.

  </pre>
  <blockquote type="cite">
    <pre wrap="">data Even
data Odd

class Flip b c | b -&gt; c, c -&gt; 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 =&gt; a -&gt; List a b -&gt; List a c
    </pre>
  </blockquote>
  <pre wrap=""><!---->
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.

  </pre>
  <blockquote type="cite">
    <pre wrap="">headList :: List a b -&gt; a
headList (Cons x _) = x
    </pre>
  </blockquote>
  <pre wrap=""><!---->
However, we were not able to write a function that returns the tail.

  </pre>
  <blockquote type="cite">
    <pre wrap="">tailList :: Flip b c =&gt; List a b -&gt; List a c
tailList (Cons _ xs) = xs
    </pre>
  </blockquote>
  <pre wrap=""><!---->
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: <a class="moz-txt-link-freetext" href="http://www.haskell.org/ghc/">http://www.haskell.org/ghc/</a>  :? 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&gt;

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
<a class="moz-txt-link-abbreviated" href="mailto:Haskell@haskell.org">Haskell@haskell.org</a>
<a class="moz-txt-link-freetext" href="http://www.haskell.org/mailman/listinfo/haskell">http://www.haskell.org/mailman/listinfo/haskell</a>
  </pre>
</blockquote>
<br>
</body>
</html>