I'm playing around with smart constructors, and I have encountered a weird puzzle.
My goal is to do vector arithmetic. I'm using smart constructors so that I can store a vector as a list and use the type system to staticly enforce the length of a vector. So my first step is to define Peano numbers at the type level. > data PZero = PZero deriving (Show) > data PSucc a = PSucc a deriving (Show) > > type P1 = PSucc PZero > type P2 = PSucc P1 > type P3 = PSucc P2 > -- etc Next, I define a vector type and tag it with a Peano number. > data Vec s t = Vec [t] deriving (Eq, Ord, Show, Read) Now I can define a few smart constructors. > vec0 :: Vec PZero t > vec0 = Vec [] > > vec1 :: t -> Vec P1 t > vec1 x = Vec [x] > > vec2 :: t -> t -> Vec P2 t > vec2 x y = Vec [x, y] > > vec3 :: t -> t -> t -> Vec P3 t > vec3 x y z = Vec [x, y, z] Now here's the puzzle. I want to create a function "vecLength" that accepts a vector and returns its length. The catch is that I want to calculate the length based on the /type/ of the vector, without looking at the number of elements in the list. So I started by defining a class that allows me to convert a Peano number to an integer. I couldn't figure out how to define a function that converts the type directly to an integer, so I am using a two-step process. Given a Peano type /t/, I would use the expression "pToInt (pGetValue :: t)". > class Peano t where > pGetValue :: t > pToInt :: t -> Int > > instance Peano PZero where > pGetValue = PZero > pToInt _ = 0 > > instance (Peano t) => Peano (PSucc t) where > pGetValue = PSucc pGetValue > pToInt (PSucc a) = 1 + pToInt a Finally, I tried to define vecLength, but I am getting an error. > vecLength :: (Peano s) => Vec s t -> Int > vecLength _ = pToInt (pGetValue :: s) < Could not deduce (Peano s1) from the context () < arising from a use of `pGetValue' < Possible fix: < add (Peano s1) to the context of the polymorphic type `forall s. s' < In the first argument of `pToInt', namely `(pGetValue :: s)' < In the expression: pToInt (pGetValue :: s) < In the definition of `vecLength': < vecLength _ = pToInt (pGetValue :: s) Any suggestions? -- Ron _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
