gmane.comp.lang.haskell.cafe

Ronald Guida | 21 Dec 05:37

Smart Constructor Puzzle

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

(Continue reading)

headers

Luke Palmer | 21 Dec 05:56

Re: Smart Constructor Puzzle

On Dec 21, 2007 4:39 AM, Ronald Guida <ronguida <at> mindspring.com> wrote:
> Finally, I tried to define vecLength, but I am getting an error.
>
>  > vecLength :: (Peano s) => Vec s t -> Int
>  > vecLength _ = pToInt (pGetValue :: s)

The s in (pGetValue :: s) is different from the s in (Peano s).  Use
the "scoped type variables" extension:

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

The forall introduces a scope for s, which type signatures usually do not.

Luke

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

(Continue reading)

headers

Twan van Laarhoven | 21 Dec 06:01

Re: Smart Constructor Puzzle

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]

(Continue reading)

headers

Stefan O'Rear | 21 Dec 06:03

Re: Smart Constructor Puzzle

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

(Continue reading)

headers

Henning Thielemann | 21 Dec 12:14

Re: Smart Constructor Puzzle


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

(Continue reading)