Henning Thielemann lemming at henning-thielemann.de
Fri Dec 21 06:14:34 EST 2007

```On Thu, 20 Dec 2007, Stefan O'Rear wrote:

> On Thu, Dec 20, 2007 at 11:39:42PM -0500, Ronald Guida wrote:
> > > 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
>
> ...
>
> > 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

Why the two methods pGetValue and pToInt? I thought that pGetValue should
have signature pGetValue :: t -> Peano and that pToInt can convert the
result from pGetValue to Int.

> > Finally, I tried to define vecLength, but I am getting an error.
> >
> > > vecLength :: (Peano s) => Vec s t -> Int
> > > vecLength _ = pToInt (pGetValue :: s)
>
> 1. pGetValue is unneccessary, undefined :: s will work just as well.
>    This is a fairly standard approach; the precision values in Floating,
>    bitSize :: Bits a => a -> Int, and sizeOf :: Storable a => a -> Int
>    all work this way.