[Haskell-cafe] Type level functions (type of decreasing list)

[Stefan Holdermans]

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 (Succ n)

   mySeq = Cons three (Cons two (Cons one Nil))

HTH,

   Stefan