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

[Derek Elkins]

On Sat, 2007-08-18 at 19:26 +0000, 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.
> 
> 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?

When you write 'value' how is GHC supposed to know what instance you
want?  The typical trick is to add what could be called a phantom
argument to propagate the type.  I.e.
class IntegerType a where value :: a -> Integer
instance IntegerType Two where value _ = 2
value (undefined :: Two) == 2