# [Haskell-cafe] Computed promoted natural

Ertugrul Söylemez es at ertes.de
Fri Nov 9 17:53:54 CET 2012

Arie Peterson <ariep at xs4all.nl> wrote:

> 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

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.
-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 836 bytes
Desc: not available