Subject: Re: type level functions (type of decreasing list) Newsgroups: gmane.comp.lang.haskell.cafe Date: Wednesday 18th October 2006 06:21:19 UTC (over 10 years ago) Greg Buchholz wrote: > I'm wondering about creating a data structure that has the type of > decreasing numbers. > I can try... > > class Pre a b | a -> b > instance Pre (Succ a) a > instance Pre Zero Zero > > data (Pre a b) => Seq a = Cons a (Seq b) | Nil > > decreasing = Cons three (Cons two (Cons one Nil)) > > ...but that complains about "Not in scope: type variable `b'" One way is to use existentials: > data Seq1 a = forall b. (Pre a b, Show b) => Cons1 a (Seq1 b) | Nil1 > > decreasing1 = Cons1 three (Cons1 two (Cons1 one Nil1)) which perhaps not entirely satisfactory because we have to specify all the needed classes in the definition of Seq1. Perhaps a better -- and a more general alternative -- is to use type-level programming to its fullest. The following defines a list whose elements are constrained to be in the decreasing, increasing, or any other (defined in the future) order. This example shows that Haskell truly has more kinds than it is commonly acknowledged. For more details on constrained lists (list of odd numerals, even numerals, etc), please see the following implementation of Tim Sheard's `Half' example http://pobox.com/~oleg/ftp/Haskell/Half.hs > data Succ a = S a > data Zero = Z > > zero = Z > one = S zero > two = S one > three = S two > > class KIND l a b > > data Cons a b = Cons a b > data Nil = Nil > > > data Increasing = Increasing > instance KIND Increasing a (Succ a) > data Decreasing = Decreasing > instance KIND Decreasing (Succ a) a > -- one can add non-increasing, non-decreasing, etc. > > class ConstrainedL c l > instance ConstrainedL c Nil > instance ConstrainedL c (Cons a Nil) > instance (KIND c a b, ConstrainedL c (Cons b l)) > => ConstrainedL c (Cons a (Cons b l)) > > -- smart constructors. > -- Alternatively, define > as_increasing :: ConstrainedL Increasing l => l -> l > consi :: ConstrainedL Increasing (Cons a l) => a -> l -> Cons a l > consi = Cons > consd :: ConstrainedL Decreasing (Cons a l) => a -> l -> Cons a l > consd = Cons > incr = consi one (consi two (consi three Nil)) > -- No instance for (KIND Increasing (Succ Zero) (Succ (Succ (Succ Zero)))) > -- incr1 = consi one (consi three Nil) > decr = consd three (consd two (consd one Nil)) -- No instance for (KIND Decreasing (Succ (Succ Zero)) (Succ (Succ (Succ Zero)) -- decr1 = consd three (consd two (consd three Nil)) |
|||