Re: [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

 dataZero = 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
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

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

[DavidA]

Twan van Laarhoven twanvl at gmail.com writes:

 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))

Thanks to all respondents for this suggestion. That works great.

 
 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)

Well actually, your first attempt *did* work for me (using GHC 6.6.1). Is this 
not behaviour that I can rely on?

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