1 files changed, 62 insertions, 0 deletions
diff --git a/testsuite/tests/programs/thurston-modular-arith/Main.hs b/testsuite/tests/programs/thurston-modular-arith/Main.hs
new file mode 100644
index 0000000000..608025b1e1
--- /dev/null
+++ b/testsuite/tests/programs/thurston-modular-arith/Main.hs
@@ -0,0 +1,62 @@
+{-# LANGUAGE UndecidableInstances, ExistentialQuantification,
+              ScopedTypeVariables, Rank2Types #-}
+
+--	Modular arithmetic, due to Dale Thurston
+
+-- Here's a way to mimic dependent types using existential types,
+-- illustrated by an implementation of modular arithmetic.  To try it
+-- out, load modulus.hs and try something like
+--	inModulus (mkModulus (1234567890123::Integer)) (^ 98765432198765) 2
+-- to compute 2 to the 98765432198765'th power modulo 1234567890123.
+
+-- The key is the definitions at the top of TypeVal.hs:
+-- 
+--   class TypeVal a t | t -> a where
+--       -- typeToVal should ignore its argument.
+--       typeToVal :: t -> a
+--   
+--   data Wrapper a = forall t . (TypeVal a t) => Wrapper t
+--   
+--   class ValToType a where
+--      valToType :: a -> Wrapper a
+-- 
+-- `valToType' takes a value `x' and returns a (wrapped version of a)
+-- fake value in a new type; from the new type, `x' can be recovered by
+-- applying typeToVal.
+--
+-- This code works under ghc.  It uses existentially quantified data
+-- constructors, scoped type variables, and explicit universal
+-- quantification.
+
+
+module Main where
+
+import TypeVal
+
+default (Integer)
+
+main = print (map (inModulus (mkModulus (1234567890123::Integer)) (^98765432198765)) [2..1000])
+
+
+
+data Mod s a = Mod {value::a} deriving (Eq, Show)
+
+data Modulus a = forall s. TypeVal a s => Modulus (a -> Mod s a) (Mod s a -> a)
+
+mkModulus :: (ValToType a, Integral a) => a -> Modulus a
+mkModulus x = case valToType x of {Wrapper (y :: t) ->
+	      Modulus normalize (value :: Mod t a -> a)}
+
+normalize :: forall a s. (TypeVal a s, Integral a) => a -> Mod s a
+normalize x = (Mod (x `mod` typeToVal (undefined::s)))
+
+inModulus :: Modulus a -> (forall s . TypeVal a s =>  Mod s a -> Mod s a)
+	        -> a -> a
+inModulus (Modulus in_ out) f x = out (f (in_ x))
+
+instance (TypeVal a s, Integral a) => Num (Mod s a) where
+    Mod x + Mod y = normalize (x + y)
+    Mod x - Mod y = normalize (x - y)
+    negate (Mod x) = normalize (negate x)
+    Mod x * Mod y = normalize (x * y)
+    fromInteger a = normalize (fromInteger a)