]> Git — Sourcephile - haskell/symantic-base.git/blob - src/Symantic/Reify.hs
copyright: fix REUSE
[haskell/symantic-base.git] / src / Symantic / Reify.hs
1 {-# LANGUAGE TemplateHaskell #-}
2 {-# OPTIONS_GHC -Wno-incomplete-patterns #-} -- For reifyTH
3 -- | Reify an Haskell value using type-directed normalisation-by-evaluation (NBE).
4 module Symantic.Reify where
5
6 import Control.Monad (Monad(..))
7 import qualified Data.Function as Fun
8 import qualified Language.Haskell.TH as TH
9
10 import Symantic.Lang (Abstractable(..))
11
12 -- | 'ReifyReflect' witnesses the duality between @meta@ and @(repr a)@.
13 -- It indicates which type variables in @a@ are not to be instantiated
14 -- with the arrow type, and instantiates them to @(repr _)@ in @meta@.
15 -- This is directly taken from: http://okmij.org/ftp/tagless-final/course/TDPE.hs
16 --
17 -- * @meta@ instantiates polymorphic types of the original Haskell expression
18 -- with @(repr _)@ types, according to how 'ReifyReflect' is constructed
19 -- using 'base' and @('-->')@. This is obviously not possible
20 -- if the orignal expression uses monomorphic types (like 'Int'),
21 -- but remains possible with constrained polymorphic types (like @(Num i => i)@),
22 -- because @(i)@ can still be inferred to @(repr _)@,
23 -- whereas the finally chosen @(repr)@
24 -- (eg. 'E', or 'Identity', or 'TH.CodeQ', or ...)
25 -- can have a 'Num' instance.
26 -- * @(repr a)@ is the symantic type as it would have been,
27 -- had the expression been written with explicit 'lam's
28 -- instead of bare haskell functions.
29 -- DOC: http://okmij.org/ftp/tagless-final/cookbook.html#TDPE
30 -- DOC: http://okmij.org/ftp/tagless-final/NBE.html
31 -- DOC: https://www.dicosmo.org/Articles/2004-BalatDiCosmoFiore-Popl.pdf
32 data ReifyReflect repr meta a = ReifyReflect
33 { -- | 'reflect' converts from a *represented* Haskell term of type @a@
34 -- to an object *representing* that value of type @a@.
35 reify :: meta -> repr a
36 -- | 'reflect' converts back an object *representing* a value of type @a@,
37 -- to the *represented* Haskell term of type @a@.
38 , reflect :: repr a -> meta
39 }
40
41 -- | The base of induction : placeholder for a type which is not the arrow type.
42 base :: ReifyReflect repr (repr a) a
43 base = ReifyReflect{reify = Fun.id, reflect = Fun.id}
44
45 -- | The inductive case : the arrow type.
46 -- 'reify' and 'reflect' are built together inductively.
47 infixr 8 -->
48 (-->) :: Abstractable repr =>
49 ReifyReflect repr m1 o1 -> ReifyReflect repr m2 o2 ->
50 ReifyReflect repr (m1 -> m2) (o1 -> o2)
51 r1 --> r2 = ReifyReflect
52 { reify = \meta -> lam (reify r2 Fun.. meta Fun.. reflect r1)
53 , reflect = \repr -> reflect r2 Fun.. (.@) repr Fun.. reify r1
54 }
55
56 -- * Using TemplateHaskell to fully auto-generate 'ReifyReflect'
57
58 -- | @$(reifyTH 'Foo.bar)@ calls 'reify' on 'Foo.bar'
59 -- with an 'ReifyReflect' generated from the infered type of 'Foo.bar'.
60 reifyTH :: TH.Name -> TH.Q TH.Exp
61 reifyTH name = do
62 info <- TH.reify name
63 case info of
64 TH.VarI n (TH.ForallT _vs _ctx ty) _dec ->
65 [| reify $(genReifyReflect ty) $(return (TH.VarE n)) |]
66 where
67 genReifyReflect (TH.AppT (TH.AppT TH.ArrowT a) b) = [| $(genReifyReflect a) --> $(genReifyReflect b) |]
68 genReifyReflect TH.VarT{} = [| base |]