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