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|]