reify
で型に情報を閉じ込めて、reflect
で取り出すというもの。情報の持ち運びのために、最後にダミーの型を持つようなファントム型を定義する(ここではM
)。
% runghc
{-# LANGUAGE NoMonomorphismRestriction, ScopedTypeVariables #-}
module Main (main) where
import Data.Proxy
import Data.Reflection
main :: IO ()
main = do
print $ reify 7 (\(_ :: Proxy s) -> unM (culc :: (Integral a, Reifies s a) => M a s))
print $ reify 9 (\(_ :: Proxy s) -> unM (culc :: (Integral a, Reifies s a) => M a s))
return ()
newtype M a s = M { unM :: a } deriving (Eq, Show)
add, mul :: (Integral a, Reifies s a) => M a s -> M a s -> M a s
add a b = M $ (unM a + unM b) `mod` (reflect a)
mul a b = M $ (unM a * unM b) `mod` (reflect a)
culc :: (Integral a, Reifies s a) => M a s
culc = (M 3 `add` M 2) `mul` M 5
4
7
型のあわせ方は http://www.cs.rutgers.edu/~ccshan/prepose/prepose.pdf を参照した。