[Haskell-cafe] Smart Constructor Puzzle

[Stefan O'Rear]

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
>
> 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.  Some Haskeller, notably Alex Jacobson, prefer to
   use a 'proxy' type to make this value irrelevance explicit:

data Proxy s  -- for H98, data Proxy s = Proxy_ !(Proxy s)

2. The reason this doesn't work is that the scope of s in the type
   signature is the type signature, and the scope of s in the other type
   signature is the other type signature.  They are very different type
   variables, and you cannot assign the type forall s. s to pGetValue -
   it has class constraints.  The effect you are trying to achieve
   cannot be directly achieved in H98 (this is considered one of H98's
   few major flaws)...

   2a: Use GHC extentions (ScopedTypeVariables).  This extends the scope
       of type variables to include the definition.  For backwards
       compatibility, it only applies to new-style explicit
       quantification:

       vecLength :: forall s. Peano s => Vec s t -> Int

   2b: Use functions with type constraints to force relations between
       types:

       vecLength v = pToInt (vToPeano v) where
           vToPeano = undefined :: Vec s t -> s

       Figuring out why this works should be enlightening, and it seems
       hard to explain, so I'm leaving it as an excersize. :)

Stefan
-------------- next part --------------
A non-text attachment was scrubbed...
Name: not available
Type: application/pgp-signature
Size: 189 bytes
Desc: Digital signature
Url : http://www.haskell.org/pipermail/haskell-cafe/attachments/20071220/5d9eed0f/attachment.bin