Greg,
What about the following (tested with GHC 6.6)?
{-# OPTIONS -fglasgow-exts #-}
data Zero = Zero
data Succ n = Succ n
zero = Zero
one = Succ zero
two = Succ one
three = Succ two
-- etc
data Seq :: * - * where
Nil :: Seq Zero
Cons :: Succ n - Seq n - Seq
I'm wondering about creating a data structure that has the type of
decreasing numbers. If I want an increasing list, it is easy...
{-# OPTIONS -fglasgow-exts #-}
data Succ a = S a deriving Show
data Zero = Z deriving Show
data Seq' a = Cons' a (Seq' (Succ a)) | Nil' deriving
Here's an attempt with GADTs:
\begin{code}
{-# OPTIONS_GHC -fglasgow-exts #-}
data Succ a
data Zero
data Seq a b where
Cons :: a - Seq a b - Seq a (Succ b)
Nil :: Seq a Zero
\end{code}
Seems to work for me.
Spencer Janssen
On Oct 17, 2006, at 6:37 PM, Greg Buchholz wrote:
I'm
Spencer Janssen wrote:
] Here's an attempt with GADTs:
]
] \begin{code}
] {-# OPTIONS_GHC -fglasgow-exts #-}
] data Succ a
] data Zero
] data Seq a b where
] Cons :: a - Seq a b - Seq a (Succ b)
] Nil :: Seq a Zero
] \end{code}
]
] Seems to work for me.
Hmm. Maybe I'm missing
