[Haskell-cafe] Computed promoted natural

[Ertugrul Söylemez]

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
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.
-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 836 bytes
Desc: not available
URL: <http://www.haskell.org/pipermail/haskell-cafe/attachments/20121109/c544dbfb/attachment.pgp>