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