[Haskell-cafe] How do I simulate dependent types using phantom types?

2007-08-18 Thread DavidA 
Hi,

I am trying to implement quadratic fields Q(sqrt d). These are numbers of the 
form a + b sqrt d, where a and b are rationals, and d is an integer.

In an earlier attempt, I tried
data QF = QF Integer Rational Rational
(see http://www.polyomino.f2s.com/david/haskell/hs/QuadraticField.hs.txt)
The problem with this approach is that it's not really type-safe:
I can attempt to add a + b sqrt 2 to c + d sqrt 3, whereas this should be a 
type error because 2 /= 3.

So I thought I'd have a go at doing it with phantom types. In effect I'd be 
using phantom types to simulate dependent types. Here's the code:

{-# OPTIONS_GHC -fglasgow-exts #-}

import Data.Ratio

class IntegerType a where
value :: Integer

data Two
instance IntegerType Two where value = 2

data Three
instance IntegerType Three where value = 3

data QF d = QF Rational Rational deriving (Eq)

instance IntegerType d = Show (QF d) where
show (QF a b) = show a ++  +  ++ show b ++  sqrt  ++ show value

instance IntegerType d = Num (QF d) where
QF a b + QF a' b' = QF (a+a') (b+b')
negate (QF a b) = QF (-a) (-b)
QF a b * QF c d = QF (a*c + b*d*value) (a*d + b*c)
fromInteger n = QF (fromInteger n) 0

The problem is, this doesn't work. GHC complains:
The class method `value'
mentions none of the type variables of the class IntegerType a
When checking the class method: value :: Integer
In the class declaration for `IntegerType'

Is what I'm trying to do reasonable? If no, what should I be doing instead? If 
yes, why doesn't GHC like it?

Thanks, David

___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] How do I simulate dependent types using phantom types?

2007-08-18 Thread Lennart Augustsson 
Use
  value :: a - Integer


On 8/18/07, DavidA [EMAIL PROTECTED] wrote:

 Hi,

 I am trying to implement quadratic fields Q(sqrt d). These are numbers of
 the
 form a + b sqrt d, where a and b are rationals, and d is an integer.

 In an earlier attempt, I tried
 data QF = QF Integer Rational Rational
 (see http://www.polyomino.f2s.com/david/haskell/hs/QuadraticField.hs.txt)
 The problem with this approach is that it's not really type-safe:
 I can attempt to add a + b sqrt 2 to c + d sqrt 3, whereas this should be
 a
 type error because 2 /= 3.

 So I thought I'd have a go at doing it with phantom types. In effect I'd
 be
 using phantom types to simulate dependent types. Here's the code:

 {-# OPTIONS_GHC -fglasgow-exts #-}

 import Data.Ratio

 class IntegerType a where
 value :: Integer

 data Two
 instance IntegerType Two where value = 2

 data Three
 instance IntegerType Three where value = 3

 data QF d = QF Rational Rational deriving (Eq)

 instance IntegerType d = Show (QF d) where
 show (QF a b) = show a ++  +  ++ show b ++  sqrt  ++ show value

 instance IntegerType d = Num (QF d) where
 QF a b + QF a' b' = QF (a+a') (b+b')
 negate (QF a b) = QF (-a) (-b)
 QF a b * QF c d = QF (a*c + b*d*value) (a*d + b*c)
 fromInteger n = QF (fromInteger n) 0

 The problem is, this doesn't work. GHC complains:
 The class method `value'
 mentions none of the type variables of the class IntegerType a
 When checking the class method: value :: Integer
 In the class declaration for `IntegerType'

 Is what I'm trying to do reasonable? If no, what should I be doing
 instead? If
 yes, why doesn't GHC like it?

 Thanks, David

 ___
 Haskell-Cafe mailing list
 Haskell-Cafe@haskell.org
 http://www.haskell.org/mailman/listinfo/haskell-cafe

___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] How do I simulate dependent types using phantom types?

2007-08-18 Thread Twan van Laarhoven 

DavidA wrote:


Hi,

I am trying to implement quadratic fields Q(sqrt d). These are numbers of the 
form a + b sqrt d, where a and b are rationals, and d is an integer.


...

class IntegerType a where
value :: Integer

The problem is, this doesn't work. GHC complains:
The class method `value'
mentions none of the type variables of the class IntegerType a
When checking the class method: value :: Integer
In the class declaration for `IntegerType'

Is what I'm trying to do reasonable? If no, what should I be doing instead? If 
yes, why doesn't GHC like it?


You are on the right track. The problem with the class method is that it 
doesn't use type 'a' anywhere, consider

 f :: Integer
 f = value
What class instance should be used here?

The solution is to use a dummy parameter:
 class IntegerType a where
 value :: a - Integer
And call it like:
 f = value (undefined :: Two)

So for instance:
 instance IntegerType d = Show (QF d) where
 show (QF a b) = show a ++  +  ++ show b ++  sqrt 
   ++ show (value (undefined::d))

The problem is that this doesn't work, because d is not in scope, you 
need the scoped type variables extension:


 valueOfQF :: forall a. IntegerType a = QF a - Integer
 valueOfQF qf = value (undefined :: a)

or maybe better, change the class:

 class IntegerType a where
 value :: QF a - Integer

Now you can simply use

 instance IntegerType d = Show (QF d) where
 show qf@(QF a b) = show a ++  +  ++ show b ++  sqrt 
 ++ show (value qf)

Twan
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe