Re: type level functions (type of decreasing list)
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))
Stefan Holdermans
What about the following (tested with GHC 6.6)?
and oleg@pobox.com wrote:
One way is to use existentials:
<snip>
Perhaps a better -- and a more general alternative -- is to use type-level programming to its fullest.
Thanks everyone, those are interesting solutions! Thanks, Greg Buchholz
oleg@pobox.com wrote: ] ] One way is to use existentials: ]
data Seq1 a = forall b. (Pre a b, Show b) => Cons1 a (Seq1 b) | Nil1
] ] which perhaps not entirely satisfactory because we have to specify all ] the needed classes in the definition of Seq1. Yes, that seems pretty burdensome, since we can't now create even a simple function like "tail", right? Or at least I think existentials are the problem with this...
tail1 :: (Pre a b, Show b) => Seq1 a -> Seq1 b -- tail1 (Cons1 x xs) = xs tail1 Nil1 = error "empty Seq"
...ghci reports... Couldn't match expected type `b' (a rigid variable) against inferred type `b1' (a rigid variable) `b' is bound by the type signature for `tail_' at dec2.lhs:30:17 `b1' is bound by the pattern for `Cons1' at dec2.lhs:31:8-17 Expected type: Seq1 b Inferred type: Seq1 b1 In the expression: xs In the definition of `tail1': tail1 (Cons1 x xs) = xs ...and hugs... ERROR "dec2.lhs":31 - Existentially quantified variable in inferred type *** Variable : _3 *** From pattern : Cons1 x xs *** Result type : Seq1 _0 -> Seq1 _3 ] ] 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. <snip> ] > data Cons a b = Cons a b ] > data Nil = Nil ...if we build our lists with tuple-like Conses, our types end up being as long as our lists, right? So an infinite list has an infinite type, which seems like it could be problematic to type check. For example, here's an arbitrarly long increasing list...
data Seq' a = Cons' a (Seq' (Succ a)) | Nil' deriving Show
from :: a -> Seq' a from x = Cons' x (from (S x))
inf = from Z
...with some of the usual functions...
tail_ :: Seq' a -> Seq' (Succ a) tail_ (Cons' x xs) = xs
class Take a where take_ :: a -> (Seq' b) -> (Seq' b)
instance Take Zero where take_ Z _ = Nil'
instance Take a => Take (Succ a) where take_ (S n) (Cons' x xs) = Cons' x (take_ n xs) take_ _ Nil' = error "can't take_ that many"
class Drop a b c | a b -> c where drop_ :: a -> Seq' b -> Seq' c
instance Drop Zero b b where drop_ Z xs = xs
instance Drop a (Succ b) c => Drop (Succ a) b c where drop_ (S n) (Cons' x xs) = drop_ n xs drop_ _ Nil' = error "can't drop_ that many"
...Anyway, for fun, here's a list that alternates between two types in a linearly increasing manner. So you can start out with one Int and then two Strings, then three Ints, four Strings, etc. I don't know if it is going to yeild to a type classless GADT solution yet, but I'll keep thinking about it.
data Fancy a b left next = forall c d left' next' lz decleft . (Show c, Show d, Zerop left lz, If lz (Succ next) next next', Pre left decleft, If lz next decleft left', If lz b a c, If lz a b d ) => Cons a (Fancy c d left' next') | Nil
fancy :: Fancy Integer String Zero (Succ Zero) fancy = (Cons 1 (Cons "a" (Cons "b" (Cons 2 (Cons 3 (Cons 4 (Cons "c" (Cons "d" (Cons "e" (Cons "f" (Cons 5 (Cons 6 (Cons 7 (Cons 8 (Cons 9 Nil)))))))))))))))
instance (Show a, Show b) => Show (Fancy a b c d) where show (Cons x xs) = "(Cons " ++ (show x) ++ " " ++ (show xs) ++ ")" show Nil = "Nil"
data Succ a = S a deriving Show data Zero = Z deriving Show
data TTrue data TFalse
class Pre a b | a -> b instance Pre (Succ a) a instance Pre Zero Zero
class If p t e result | p t e -> result instance If TTrue a b a instance If TFalse a b b
class Zerop a b | a -> b instance Zerop Zero TTrue instance Zerop (Succ a) TFalse
participants (2)
-
Greg Buchholz -
oleg＠pobox.com