Ronald Guida ronguida at mindspring.com
Thu Dec 20 23:39:42 EST 2007

```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

```