
DavidA wrote:
Twan van Laarhoven
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