Goheeca · November 30, 2021 22:19 · Nov 30, 2021 · Nov 30, 2021 · Nov 30, 2021 · Nov 30, 2021
diff --git a/Reificator.hs b/Reificator.hs
@@ -21,8 +21,6 @@ import qualified Algebra.Additive as AG
 
 import NumericPrelude.Numeric
 import NumericPrelude.Base
-import Math.NumberTheory.Moduli (invertSomeMod, modulo, getVal, SomeMod(..))
-import GHC.Natural (naturalFromInteger)
 
 import Debug.Trace (trace)
 

diff --git a/Reificator.hs b/Reificator.hs
@@ -46,15 +46,15 @@ using d m = reify d $ \(_ :: Proxy s) ->
 
 instance ReifiableConstraint AG.C where
   data Def AG.C a = ReifiedAdditive {
-    zero_f :: a,
-    plus_f :: a -> a -> a,
-    negate_f :: a -> a }
+    zero' :: a,
+    plus' :: a -> a -> a,
+    negate' :: a -> a }
   reifiedIns = Sub Dict
 
 instance Reifies s (Def AG.C a) => AG.C (Lift AG.C a s) where
-  zero = a where a = Lift $ zero_f (reflect a)
-  a + b = Lift $ plus_f (reflect a) (lower a) (lower b)
-  negate a = Lift $ negate_f (reflect a) (lower a)
+  zero = a where a = Lift $ zero' (reflect a)
+  a + b = Lift $ plus' (reflect a) (lower a) (lower b)
+  negate a = Lift $ negate' (reflect a) (lower a)
 
 
 reifiedAdditive :: Integer -> Def AG.C Integer

diff --git a/Reificator.hs b/Reificator.hs
@@ -18,8 +18,6 @@ import Data.Constraint.Unsafe
 import Data.Kind
 
 import qualified Algebra.Additive as AG
-import qualified Algebra.Ring as R
-import qualified Algebra.Field as F
 
 import NumericPrelude.Numeric
 import NumericPrelude.Base

diff --git a/Reificator.hs b/Reificator.hs
@@ -1,4 +1,4 @@
--- Doesn't build with this option:
+-- Doesn't build without this switch, uncomment for a successful build:
 -- {-# OPTIONS_GHC -fno-solve-constant-dicts #-}
 
 {-# LANGUAGE Rank2Types, FlexibleContexts, TypeFamilies #-}

diff --git a/Main.hs b/Main.hs
@@ -0,0 +1,7 @@
+{-# LANGUAGE TemplateHaskell #-}
+module Main where
+
+import Reificator
+
+main :: IO ()
+main = pure $$(guardTH (operationTest 11 7 4) [|| () ||])
diff --git a/Reflection-TH.cabal b/Reflection-TH.cabal
@@ -0,0 +1,11 @@
+name:                Reflection-TH
+version:             0.0.0
+build-type:          Simple
+cabal-version:       >=1.10
+
+executable Reflection-TH
+  main-is:             Main.hs
+  other-modules:       Reificator
+  other-extensions:    NoImplicitPrelude, Rank2Types, FlexibleContexts, UndecidableInstances, TypeFamilies, FlexibleInstances, ConstraintKinds, PolyKinds, TypeOperators, ScopedTypeVariables
+  build-depends:       base >=4.7, arithmoi >=0.4, numeric-prelude >=0.4, reflection >=2.1, constraints >=0.8, template-haskell >= 2.16.0.0
+  default-language:    Haskell2010
diff --git a/Reificator.hs b/Reificator.hs
@@ -0,0 +1,84 @@
+-- Doesn't build with this option:
+-- {-# OPTIONS_GHC -fno-solve-constant-dicts #-}
+
+{-# LANGUAGE Rank2Types, FlexibleContexts, TypeFamilies #-}
+{-# LANGUAGE ConstraintKinds, PolyKinds, TypeOperators #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+
+{-# LANGUAGE TypeFamilies, FlexibleInstances, UndecidableInstances #-}
+
+{-# LANGUAGE NoImplicitPrelude #-}
+
+module Reificator where
+
+import Data.Proxy
+import Data.Reflection
+import Data.Constraint
+import Data.Constraint.Unsafe
+import Data.Kind
+
+import qualified Algebra.Additive as AG
+import qualified Algebra.Ring as R
+import qualified Algebra.Field as F
+
+import NumericPrelude.Numeric
+import NumericPrelude.Base
+import Math.NumberTheory.Moduli (invertSomeMod, modulo, getVal, SomeMod(..))
+import GHC.Natural (naturalFromInteger)
+
+import Debug.Trace (trace)
+
+import Language.Haskell.TH.Syntax (TExp(..))
+import Control.Monad.Fail
+
+
+newtype Lift (p :: Type -> Constraint) (a :: Type) (s :: Type) = Lift { lower :: a }
+
+class ReifiableConstraint p where
+  data Def (p :: Type -> Constraint) (a :: Type) :: Type
+  reifiedIns :: Reifies s (Def p a) :- p (Lift p a s)
+
+using :: forall p a. ReifiableConstraint p => Def p a -> (p a => a) -> a
+using d m = reify d $ \(_ :: Proxy s) ->
+  let replaceProof :: Reifies s (Def p a) :- p a
+      replaceProof = trans proof reifiedIns
+        where proof = unsafeCoerceConstraint :: p (Lift p a s) :- p a
+  in m \\ replaceProof
+
+
+instance ReifiableConstraint AG.C where
+  data Def AG.C a = ReifiedAdditive {
+    zero_f :: a,
+    plus_f :: a -> a -> a,
+    negate_f :: a -> a }
+  reifiedIns = Sub Dict
+
+instance Reifies s (Def AG.C a) => AG.C (Lift AG.C a s) where
+  zero = a where a = Lift $ zero_f (reflect a)
+  a + b = Lift $ plus_f (reflect a) (lower a) (lower b)
+  negate a = Lift $ negate_f (reflect a) (lower a)
+
+
+reifiedAdditive :: Integer -> Def AG.C Integer
+reifiedAdditive prime =
+  ReifiedAdditive
+    0
+    (fmap (`mod` prime) . (+))
+    ((`mod` prime) . negate)
+
+
+debug = flip trace
+
+operationTest modulus x y = result `debug` (
+    "modulus: " ++ show modulus ++
+    "\nx: " ++ show x ++
+    "\ny: " ++ show y ++
+    "\nsum: " ++ show left ++
+    "\nresult: " ++ show result
+  )
+  where inField = using $ reifiedAdditive modulus
+        left = inField $ x + y
+        result = (left == inField zero)
+
+
+guardTH cond val = if cond then val else fmap TExp (fail "Nope")
diff --git a/stack.yaml b/stack.yaml
@@ -0,0 +1,6 @@
+flags: {}
+extra-package-dbs: []
+packages:
+- '.'
+extra-deps: []
+resolver: lts-18.5
diff --git a/stack.yaml.lock b/stack.yaml.lock
@@ -0,0 +1,12 @@
+# This file was autogenerated by Stack.
+# You should not edit this file by hand.
+# For more information, please see the documentation at:
+#   https://docs.haskellstack.org/en/stable/lock_files
+
+packages: []
+snapshots:
+- completed:
+    size: 585817
+    url: https://raw.githubusercontent.com/commercialhaskell/stackage-snapshots/master/lts/18/5.yaml
+    sha256: 22d24d0dacad9c1450b9a174c28d203f9bb482a2a8da9710a2f2a9f4afee2887
+  original: lts-18.5