Arie Peterson
Right. So, let's try to fit GHC's singleton types to the reflection library.
I'm not sure if you're supposed to use the reflection library that way. The idea is simply this: reify :: a -> (forall s. Reifies s a => Proxy s -> r) -> r You pass in a value, any value you like actually ('reify' is fully polymorphic in 'a'), and the continuation receives a proxy that contains a type that represents that value. You can then use the 'Reifies' class to recover the original value from the type 's'. This goes with almost no runtime cost. In particular you should not write Reifies instances yourself. Let's say you want to write a data type for modular arithmetic that encodes the modulus in its type: {-# LANGUAGE ScopedTypeVariables #-} import Data.Proxy import Data.Reflection import Text.Printf data Mod n a = Mod !a !a instance (Integral a) => Eq (Mod n a) where Mod n x == Mod _ y = mod (x - y) n == 0 instance (Integral a, Show a) => Show (Mod n a) where show (Mod n x) = printf "(%s mod %s)" (show (mod x n)) (show n) instance (Integral a, Reifies n a) => Num (Mod n a) where Mod n x + Mod _ y = Mod n (mod (x + y) n) Mod n x - Mod _ y = Mod n (mod (x - y) n) Mod n x * Mod _ y = Mod n (mod (x * y) n) negate (Mod n x) = Mod n (n - x) abs = id signum x@(Mod _ 0) = x signum (Mod n _) = Mod n 1 fromInteger x = Mod n (mod (fromInteger x) n) where n = reflect (Proxy :: Proxy n) Notice that for speed I'm also saving the modulus as a value in the data constructor 'Mod'. Reflection is only used in the 'fromInteger' function, where the Mod value is first constructed. Then you can use reification to lift a modulus into its corresponding type. This is a very flexible interface that can carry type-level moduli even through a large monadic action: withModulus :: forall a b. (Integral a) => a -> (forall n. (Reifies n a) => (a -> Mod n a) -> (Mod n a -> a) -> b) -> b withModulus n k = reify n $ \(_ :: Proxy n) -> k (\x -> Mod n (mod x n) :: Mod n a) (\(Mod _ x) -> x) Usage: withModulus 101 $ \to from -> from $ (to 3 + 4)^17 The following is a highly simplified interface if you don't need a monad or anything, but just want to perform modular arithmetic: withModulus' :: forall a. a -> (forall n. (Reifies n a) => Mod n a) -> a withModulus' n mx = reify n $ \(_ :: Proxy n) -> case mx :: Mod n a of Mod _ x -> x Usage: withModulus' 101 ((3 + 4)^17) Greets, Ertugrul -- Not to be or to be and (not to be or to be and (not to be or to be and (not to be or to be and ... that is the list monad.