Skip to content

Instantly share code, notes, and snippets.

@Goheeca
Last active Nov 30, 2021
Embed
What would you like to do?
reflection + template haskell issue
{-# LANGUAGE TemplateHaskell #-}
module Main where
import Reificator
main :: IO ()
main = pure $$(guardTH (operationTest 11 7 4) [|| () ||])
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
-- Doesn't build without this switch, uncomment for a successful build:
-- {-# 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 NumericPrelude.Numeric
import NumericPrelude.Base
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' :: 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' (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
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")
flags: {}
extra-package-dbs: []
packages:
- '.'
extra-deps: []
resolver: lts-18.5
# 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
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment