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

18 Oct 2006

      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

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

Stefan Holdermans