src/Symantic/Compiler/Term.hs

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