[Haskell-cafe] How do I simulate dependent types using phantom
types?
DavidA
polyomino at f2s.com
Sat Aug 18 15:26:08 EDT 2007
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
More information about the Haskell-Cafe
mailing list