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 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
On Dec 21, 2007 4:39 AM, Ronald Guida
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 Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
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
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
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.
What about functions of type bitSize :: Bits a => (a, Int) This would also make explicit, that you don't have to provide a value of type 'a'. 'sizeOf' might still return different size depending on the value, right? E.g. when converting a sum data type to a (C++) object.
participants (5)
-
Henning Thielemann -
Luke Palmer -
Ronald Guida -
Stefan O'Rear -
Twan van Laarhoven