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

[Bertram Felgenhauer]

DavidA wrote:
> Twan van Laarhoven <twanvl <at> gmail.com> writes:
> > The solution is to use a dummy parameter:
> >  > class IntegerType a where
> >  >     value :: a -> Integer
> 
> Thanks to all respondents for this suggestion. That works great.

I prefer a slightly elaborate way,

> newtype Mark n t = Mark t

> -- provide conversion from and to dummy functions because they are
> -- much more convenient to use.
> toDummy :: Mark n t -> n -> t
> toDummy (Mark x) _ = x

> fromDummy :: (n -> t) -> Mark n t
> fromDummy f = Mark (f undefined)

> class Natural a where
>    value' :: Mark a Integer

> value :: Natural a => a -> Integer
> value = toDummy value'

The advantage of this approach is that the 'Natural' class dictionary
contains a constant Integer value, not some function that the compiler
doesn't know anything about. This makes no difference for simple uses,
but once you define type level natural numbers, like

> data    Zero = Zero
> newtype D0 a = D0 a
> newtype D1 a = D1 a

with instances,

> instance Natural Zero where
>     value' = Mark 0

> instance Natural a => Natural (D0 a) where
>     value' = fromDummy (\(D0 d) -> value d * 2)

> instance Natural a => Natural (D1 a) where
>     value' = fromDummy (\(D1 d) -> value d * 2 + 1)

you get an actual speedup at runtime, because the value represented by
the type is passed directly in the class dictionary and doesn't have to
be recomputed each time "value" is called. (Note: it *is* possible to
share intermediate results even with dummy functions, but I got a
significant speed boost in my modular arithmetic code with this
trick anyway.)

This also opens up a *naughty* way to construct such phantom types in
GHC. When I say "naughty" I mean it - use this code at your own risk.

> -- Or is this reify? I'm confused about the convention here.
> reflect :: Integer -> (forall n . Nat n => Mark n a) -> a
> reflect = flip unsafeCoerce

which can be used like this:

*Test> reflect 42 value'
42
*Test> reflect 7 (fromDummy (\d -> value d * 6))
42

It is an interesting exercise to implement

  reflect :: Integer -> (forall n . Nat n => Mark n a) -> a

using Zero, D0 and D1 :)

Bertram