src/Symantic/Syntaxes/Reify.hs

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