{-# LANGUAGE TemplateHaskell #-}
{-# OPTIONS_GHC -Wno-incomplete-patterns #-} -- For reifyTH
-- | Reify an Haskell value using type-directed normalisation-by-evaluation (NBE).
module Symantic.Reify where

import Control.Monad (Monad(..))
import qualified Data.Function as Fun
import qualified Language.Haskell.TH as TH

import Symantic.Lang (Abstractable(..))

-- | 'ReifyReflect' witnesses the duality between @meta@ and @(repr a)@.
--  It indicates which type variables in @a@ are not to be instantiated
--  with the arrow type, and instantiates them to @(repr _)@ in @meta@.
--  This is directly taken from: http://okmij.org/ftp/tagless-final/course/TDPE.hs
--
-- * @meta@ instantiates polymorphic types of the original Haskell expression
--   with @(repr _)@ types, according to how 'ReifyReflect' is constructed
--   using 'base' and @('-->')@. This is obviously not possible
--   if the orignal expression uses monomorphic types (like 'Int'),
--   but remains possible with constrained polymorphic types (like @(Num i => i)@),
--   because @(i)@ can still be inferred to @(repr _)@,
--   whereas the finally chosen @(repr)@
--   (eg. 'E', or 'Identity', or 'TH.CodeQ', or ...)
--   can have a 'Num' instance.
-- * @(repr a)@ is the symantic type as it would have been,
--   had the expression been written with explicit 'lam's
--   instead of bare haskell functions.
-- DOC: http://okmij.org/ftp/tagless-final/cookbook.html#TDPE
-- DOC: http://okmij.org/ftp/tagless-final/NBE.html
-- DOC: https://www.dicosmo.org/Articles/2004-BalatDiCosmoFiore-Popl.pdf
data ReifyReflect repr meta a = ReifyReflect
  { -- | 'reflect' converts from a *represented* Haskell term of type @a@
    -- to an object *representing* that value of type @a@.
    ReifyReflect repr meta a -> meta -> repr a
reify   :: meta -> repr a
    -- | 'reflect' converts back an object *representing* a value of type @a@,
    -- to the *represented* Haskell term of type @a@.
  , ReifyReflect repr meta a -> repr a -> meta
reflect :: repr a -> meta
  }

-- | The base of induction : placeholder for a type which is not the arrow type.
base :: ReifyReflect repr (repr a) a
base :: ReifyReflect repr (repr a) a
base = ReifyReflect :: forall (repr :: * -> *) meta a.
(meta -> repr a) -> (repr a -> meta) -> ReifyReflect repr meta a
ReifyReflect{reify :: repr a -> repr a
reify = repr a -> repr a
forall a. a -> a
Fun.id, reflect :: repr a -> repr a
reflect = repr a -> repr a
forall a. a -> a
Fun.id}

-- | The inductive case : the arrow type.
-- 'reify' and 'reflect' are built together inductively.
infixr 8 -->
(-->) :: Abstractable repr =>
         ReifyReflect repr m1 o1 -> ReifyReflect repr m2 o2 ->
         ReifyReflect repr (m1 -> m2) (o1 -> o2)
ReifyReflect repr m1 o1
r1 --> :: ReifyReflect repr m1 o1
-> ReifyReflect repr m2 o2
-> ReifyReflect repr (m1 -> m2) (o1 -> o2)
--> ReifyReflect repr m2 o2
r2 = ReifyReflect :: forall (repr :: * -> *) meta a.
(meta -> repr a) -> (repr a -> meta) -> ReifyReflect repr meta a
ReifyReflect
  { reify :: (m1 -> m2) -> repr (o1 -> o2)
reify   = \m1 -> m2
meta -> (repr o1 -> repr o2) -> repr (o1 -> o2)
forall (repr :: * -> *) a b.
Abstractable repr =>
(repr a -> repr b) -> repr (a -> b)
lam (ReifyReflect repr m2 o2 -> m2 -> repr o2
forall (repr :: * -> *) meta a.
ReifyReflect repr meta a -> meta -> repr a
reify ReifyReflect repr m2 o2
r2 (m2 -> repr o2) -> (repr o1 -> m2) -> repr o1 -> repr o2
forall b c a. (b -> c) -> (a -> b) -> a -> c
Fun.. m1 -> m2
meta (m1 -> m2) -> (repr o1 -> m1) -> repr o1 -> m2
forall b c a. (b -> c) -> (a -> b) -> a -> c
Fun.. ReifyReflect repr m1 o1 -> repr o1 -> m1
forall (repr :: * -> *) meta a.
ReifyReflect repr meta a -> repr a -> meta
reflect ReifyReflect repr m1 o1
r1)
  , reflect :: repr (o1 -> o2) -> m1 -> m2
reflect = \repr (o1 -> o2)
repr -> ReifyReflect repr m2 o2 -> repr o2 -> m2
forall (repr :: * -> *) meta a.
ReifyReflect repr meta a -> repr a -> meta
reflect ReifyReflect repr m2 o2
r2 (repr o2 -> m2) -> (m1 -> repr o2) -> m1 -> m2
forall b c a. (b -> c) -> (a -> b) -> a -> c
Fun.. repr (o1 -> o2) -> repr o1 -> repr o2
forall (repr :: * -> *) a b.
Abstractable repr =>
repr (a -> b) -> repr a -> repr b
(.@) repr (o1 -> o2)
repr (repr o1 -> repr o2) -> (m1 -> repr o1) -> m1 -> repr o2
forall b c a. (b -> c) -> (a -> b) -> a -> c
Fun.. ReifyReflect repr m1 o1 -> m1 -> repr o1
forall (repr :: * -> *) meta a.
ReifyReflect repr meta a -> meta -> repr a
reify ReifyReflect repr m1 o1
r1
  }

-- * Using TemplateHaskell to fully auto-generate 'ReifyReflect'

-- | @$(reifyTH 'Foo.bar)@ calls 'reify' on 'Foo.bar'
-- with an 'ReifyReflect' generated from the infered type of 'Foo.bar'.
reifyTH :: TH.Name -> TH.Q TH.Exp
reifyTH :: Name -> Q Exp
reifyTH Name
name = do
  Info
info <- Name -> Q Info
TH.reify Name
name
  case Info
info of
    TH.VarI Name
n (TH.ForallT [TyVarBndr]
_vs Cxt
_ctx Type
ty) Maybe Dec
_dec ->
      [| reify $(genReifyReflect ty) $(return (TH.VarE n)) |]
    where
    genReifyReflect :: Type -> Q Exp
genReifyReflect (TH.AppT (TH.AppT Type
TH.ArrowT Type
a) Type
b) = [| $(genReifyReflect a) --> $(genReifyReflect b) |]
    genReifyReflect TH.VarT{} = [| base |]