src/Symantic/Compiler/Term.hs

   1 {-# LANGUAGE AllowAmbiguousTypes #-}
   2 {-# LANGUAGE ConstraintKinds #-}
   3 {-# LANGUAGE InstanceSigs #-}
   4 {-# LANGUAGE QuantifiedConstraints #-}
   5 {-# LANGUAGE RankNTypes #-}
   6 {-# LANGUAGE UndecidableInstances #-}
   7 {-# OPTIONS_GHC -Wno-partial-fields #-}
   8
   9 module Symantic.Compiler.Term where
  10
  11 import Data.Function qualified as Fun
  12 import Data.Monoid (Monoid)
  13 import GHC.Types (Constraint, Type)
  14 import Symantic.Semantics.Eval (Eval (..))
  15 import Symantic.Semantics.Forall
  16 import Symantic.Syntaxes.Classes (Instantiable (..), Syntaxes, Unabstractable (..))
  17 import Symantic.Syntaxes.Classes qualified as Sym
  18 import Type.Reflection (Typeable)
  19 import Unsafe.Coerce (unsafeCoerce)
  20
  21 import Symantic.Typer.Type (Ty, monoTy)
  22
  23 type Semantic = Type -> Type
  24 type Syntax = Semantic -> Constraint
  25
  26 -- * Class 'AbstractableTy'
  27 class AbstractableTy ty sem where
  28   -- | Lambda term abstraction, in HOAS (Higher-Order Abstract Syntax) style.
  29   lamTy :: ty a -> (sem a -> sem b) -> sem (a -> b)
  30
  31 fun ::
  32   forall prov sem a b.
  33   Monoid prov =>
  34   AbstractableTy (Ty prov '[]) sem =>
  35   Typeable a =>
  36   (sem a -> sem b) ->
  37   sem (a -> b)
  38 fun = lamTy (monoTy @_ @prov)
  39
  40 instance
  41   ( forall sem. Syntaxes syns sem => AbstractableTy (Ty prov '[]) sem
  42   -- , forall sem a. syn sem => AbstractableLam sem a
  43   -- , forall sem. syn sem => AbstractableLam sem a
  44   -- , forall sem. syn sem => Typeable sem -- user instance not accepted
  45   -- , forall s1 s2. (syn s1, syn s2) => s1 ~ s2 -- crazy...
  46   ) =>
  47   AbstractableTy (Ty prov '[]) (Forall syns)
  48   where
  49   lamTy aTy f = Forall (lamTy aTy (\a -> let Forall b = f (forallSem a) in b))
  50     where
  51       -- Safe here because (a :: sem a) and (b :: sem b) share the same 'sem'.
  52       forallSem :: sem a -> Forall syns a
  53       forallSem a = Forall (unsafeCoerce a)
  54
  55 -- * Type 'OpenTerm'
  56 data OpenTerm (syns :: [Syntax]) (vs :: [Type]) (a :: Type) where
  57   -- | 'E' contains embedded closed (i.e. already abstracted) terms.
  58   E :: Forall syns a -> OpenTerm syns vs a
  59   -- | 'V' represents a reference to the innermost/top environment variable, i.e. Z
  60   V :: OpenTerm syns (a ': vs) a
  61   -- | 'N' represents internalizing the innermost bound variable as a
  62   -- function argument. In other words, we can represent an open
  63   -- term referring to a certain variable as a function which
  64   -- takes that variable as an argument.
  65   N :: OpenTerm syns vs (a -> b) -> OpenTerm syns (a ': vs) b
  66   -- | 'W' is a special variant of N for efficiency,
  67   -- in the case where the term does not refer
  68   -- to the topmost variable at all.
  69   W :: OpenTerm syns vs b -> OpenTerm syns (a ': vs) b
  70 instance
  71   ( forall sem. Syntaxes syns sem => AbstractableTy (Ty prov '[]) sem
  72   , Syntaxes syns (Forall syns)
  73   ) =>
  74   AbstractableTy (Ty prov '[]) (OpenTerm syns '[])
  75   where
  76   lamTy aTy f = E (lamTy aTy (unE Fun.. f Fun.. E))
  77 instance
  78   ( forall sem. Syntaxes syns sem => Unabstractable sem
  79   , Syntaxes syns (Forall syns)
  80   ) =>
  81   Unabstractable (OpenTerm syns vs)
  82   where
  83   ap = E Sym.ap
  84   const = E Sym.const
  85   id = E Sym.id
  86   (.) = E (Sym..)
  87   flip = E Sym.flip
  88   ($) = E (Sym.$)
  89
  90 instance AbstractableTy (Ty prov '[]) Eval where
  91   lamTy _aTy f = Eval (unEval Fun.. f Fun.. Eval)
  92
  93 runOpenTerm :: Syntaxes syns Eval => OpenTerm syns '[] a -> a
  94 runOpenTerm t | E (Forall sem) <- t = unEval sem
  95
  96 unE :: OpenTerm syns '[] a -> Forall syns a
  97 unE t = case t of E t' -> t'
  98
  99 instance
 100   ( forall sem. Syntaxes syns sem => Unabstractable sem
 101   , forall sem. Syntaxes syns sem => Instantiable sem
 102   , Syntaxes syns (Forall syns)
 103   ) =>
 104   Instantiable (OpenTerm syns vs)
 105   where
 106   (.@) = appOpenTerm
 107
 108 appOpenTerm ::
 109   forall syns as a b.
 110   ( forall sem. Syntaxes syns sem => Unabstractable sem
 111   , forall sem. Syntaxes syns sem => Instantiable sem
 112   , Syntaxes syns (Forall syns)
 113   ) =>
 114   OpenTerm syns as (a -> b) ->
 115   OpenTerm syns as a ->
 116   OpenTerm syns as b
 117 E d `appOpenTerm` N e = N (E ((Sym..) .@ d) `appOpenTerm` e)
 118 E d `appOpenTerm` V = N (E d)
 119 E d `appOpenTerm` W e = W (E d `appOpenTerm` e)
 120 E d1 `appOpenTerm` E d2 = E (d1 .@ d2)
 121 N e `appOpenTerm` E d = N (E (Sym.flip .@ Sym.flip .@ d) `appOpenTerm` e)
 122 N e `appOpenTerm` V = N (E Sym.ap `appOpenTerm` e `appOpenTerm` E Sym.id)
 123 N e1 `appOpenTerm` N e2 = N (E Sym.ap `appOpenTerm` e1 `appOpenTerm` e2)
 124 N e1 `appOpenTerm` W e2 = N (E Sym.flip `appOpenTerm` e1 `appOpenTerm` e2)
 125 V `appOpenTerm` E d = N (E (Sym.flip .@ Sym.id .@ d))
 126 V `appOpenTerm` N e = N (E (Sym.ap .@ Sym.id) `appOpenTerm` e)
 127 V `appOpenTerm` W e = N (E (Sym.flip .@ Sym.id) `appOpenTerm` e)
 128 W e `appOpenTerm` E d = W (e `appOpenTerm` E d)
 129 W e `appOpenTerm` V = N e
 130 W e1 `appOpenTerm` N e2 = N (E (Sym..) `appOpenTerm` e1 `appOpenTerm` e2)
 131 W e1 `appOpenTerm` W e2 = W (e1 `appOpenTerm` e2)