[Haskell-cafe] Smart Constructor Puzzle

[Twan van Laarhoven]

Ronald Guida wrote:

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

The type 's' is not available outside the type signature. There is an 
extension, ScopedTypeVariables that does just this, allowing you to write:

    {-# LANGUAGE ScopedTypeVariables #-}

    vecLength :: forall s. (Peano s) => Vec s t -> Int
    vecLength _ = pToInt (pGetValue :: s)

An alternative is to use a 'fake' function to force a value to be of type s

    vecLength :: (Peano s) => Vec s t -> Int
    vecLength v = pToInt (phantomType v)

    phantomType :: Vec s t -> s
    phantomType = undefined

Also, undefined and type signatures are the key to writing short classes in 
these situations:

   class ToInt a where
         toInt :: a -> Int
   instance ToInt PZero where
         toInt _ = 0
   instance ToInt a => ToInt (PSucc a) where
         toInt _ = toInt (undefined :: a) + 1

Twan