Reify.hs

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