src/Symantic/Compiler/Term.hs

   1 {-# LANGUAGE ConstraintKinds #-}
   2 {-# LANGUAGE InstanceSigs #-}
   3 {-# LANGUAGE QuantifiedConstraints #-}
   4 {-# LANGUAGE RankNTypes #-}
   5 {-# LANGUAGE UndecidableInstances #-}
   6
   7 module Symantic.Compiler.Term where
   8
   9 import Control.Applicative (Applicative (..))
  10 import Control.Monad (Monad (..))
  11 import Data.Function ((.))
  12 import Data.Function qualified as Fun
  13 import Data.Functor (Functor (..))
  14 import Data.Int (Int)
  15 import GHC.Types (Constraint, Type)
  16 import Symantic.Syntaxes.Classes (Unabstractable (..))
  17 import Unsafe.Coerce (unsafeCoerce)
  18
  19 import Symantic.Typer.Type (Ty)
  20
  21 type Semantic = Type -> Type
  22 type Syntax = Semantic -> Constraint
  23
  24 -- | Merge syntax 'Constraint's into a single 'Constraint'.
  25 type family Syntaxes (syns :: [(Type -> Type) -> Constraint]) (sem :: Type -> Type) :: Constraint where
  26   Syntaxes '[] sem = (() :: Constraint)
  27   Syntaxes (syn ': syns) sem = ((syn sem, Syntaxes syns sem) :: Constraint)
  28
  29 -- * Type 'ForallSemantic'
  30 data ForallSemantic (syns :: [Syntax]) (a :: Type)
  31   = ForallSemantic (forall sem. Syntaxes syns sem => sem a)
  32
  33 -- * Class 'Abstractable'
  34 class Abstractable meta sem where
  35   -- type AbstractableLam sem (a::Type) :: Constraint
  36   -- type AbstractableLam sem a = (()::Constraint)
  37
  38   -- | Lambda term abstraction, in HOAS (Higher-Order Abstract Syntax) style.
  39   lam :: Ty meta '[] a -> (sem a -> sem b) -> sem (a -> b)
  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 (ForallSemantic syns) where
  50   constI = ForallSemantic constI
  51   constK = ForallSemantic constK
  52   constS = ForallSemantic constS
  53   constB = ForallSemantic constB
  54   constC = ForallSemantic constC
  55 instance
  56   ( forall sem. Syntaxes syns sem => Abstractable meta 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   Abstractable meta (ForallSemantic syns)
  63   where
  64   lam aTy f = ForallSemantic (lam aTy (\a -> let ForallSemantic 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 -> ForallSemantic syns a
  68       forallSem a = ForallSemantic (unsafeCoerce a)
  69 instance
  70   (forall sem. Syntaxes syns sem => Unabstractable sem) =>
  71   Unabstractable (ForallSemantic syns)
  72   where
  73   ForallSemantic a2b .@ ForallSemantic a = ForallSemantic (a2b .@ a)
  74
  75 -- * Type 'OpenTerm'
  76 data OpenTerm (syns :: [Syntax]) (vs :: [Type]) (a :: Type) where
  77   -- E contains embedded closed (i.e. already abstracted) terms.
  78   E :: ForallSemantic syns a -> OpenTerm syns vs a
  79   -- V represents a reference to the innermost/top environment
  80   -- variable, i.e. Z
  81   V :: OpenTerm syns (a ': vs) a
  82   -- N represents internalizing the innermost bound variable as a
  83   -- function argument. In other words, we can represent an open
  84   -- term referring to a certain variable as a function which
  85   -- takes that variable as an argument.
  86   N :: OpenTerm syns vs (a -> b) -> OpenTerm syns (a ': vs) b
  87   -- For efficiency, there is also a special variant of N for the
  88   -- case where the term does not refer to the topmost variable at all.
  89   W :: OpenTerm syns vs b -> OpenTerm syns (a ': vs) b
  90 instance
  91   ( forall sem. Syntaxes syns sem => Abstractable meta sem
  92   , Syntaxes syns (ForallSemantic syns)
  93   ) =>
  94   Abstractable meta (OpenTerm syns '[])
  95   where
  96   lam aTy f = E (lam aTy (runOpenTerm . f . E))
  97 instance
  98   ( forall sem. Syntaxes syns sem => Constable sem
  99   , Syntaxes syns (ForallSemantic syns)
 100   ) =>
 101   Constable (OpenTerm syns vs)
 102   where
 103   constI = E constI
 104   constK = E constK
 105   constS = E constS
 106   constB = E constB
 107   constC = E constC
 108
 109 -- * Type 'R'
 110 newtype R a = R {unR :: a}
 111 instance Abstractable meta R where
 112   lam _aTy f = R (unR . f . R)
 113 instance Unabstractable R where
 114   R f .@ R x = R (f x)
 115 instance Constable R where
 116   constI = R Fun.id
 117   constK = R Fun.const
 118   constS = R (<*>)
 119   constB = R (.)
 120   constC = R Fun.flip
 121
 122 runOpenTerm :: OpenTerm syns '[] a -> ForallSemantic syns a
 123 runOpenTerm t = case t of E t' -> t'
 124
 125 eval :: Syntaxes syns R => OpenTerm syns '[] a -> a
 126 eval t
 127   | ForallSemantic sem <- runOpenTerm t =
 128       unR sem
 129
 130 instance
 131   ( forall sem. Syntaxes syns sem => Constable sem
 132   , forall sem. Syntaxes syns sem => Unabstractable sem
 133   , Syntaxes syns (ForallSemantic syns)
 134   -- , forall a as. syns (OpenTerm syns (as)) => syns (OpenTerm syns (a ': as))
 135   ) =>
 136   Unabstractable (OpenTerm syns vs)
 137   where
 138   (.@) = appOpenTerm
 139
 140 appOpenTerm ::
 141   forall syns as a b.
 142   ( forall sem. Syntaxes syns sem => Constable sem
 143   , forall sem. Syntaxes syns sem => Unabstractable sem
 144   , Syntaxes syns (ForallSemantic syns)
 145   ) =>
 146   OpenTerm syns as (a -> b) ->
 147   OpenTerm syns as a ->
 148   OpenTerm syns as b
 149 W e1 `appOpenTerm` W e2 = W (e1 `appOpenTerm` e2)
 150 W e `appOpenTerm` E d = W (e `appOpenTerm` E d)
 151 E d `appOpenTerm` W e = W (E d `appOpenTerm` e)
 152 W e `appOpenTerm` V = N e
 153 V `appOpenTerm` W e = N (E (constC .@ constI) `appOpenTerm` e)
 154 W e1 `appOpenTerm` N e2 = N (E constB `appOpenTerm` e1 `appOpenTerm` e2)
 155 N e1 `appOpenTerm` W e2 = N (E constC `appOpenTerm` e1 `appOpenTerm` e2)
 156 N e1 `appOpenTerm` N e2 = N (E constS `appOpenTerm` e1 `appOpenTerm` e2)
 157 N e `appOpenTerm` V = N (E constS `appOpenTerm` e `appOpenTerm` E constI)
 158 V `appOpenTerm` N e = N (E (constS .@ constI) `appOpenTerm` e)
 159 E d `appOpenTerm` N e = N (E (constB .@ d) `appOpenTerm` e)
 160 E d `appOpenTerm` V = N (E d)
 161 V `appOpenTerm` E d = N (E (constC .@ constI .@ d))
 162 N e `appOpenTerm` E d = N (E (constC .@ constC .@ d) `appOpenTerm` e)
 163 E d1 `appOpenTerm` E d2 = E (d1 .@ d2)
 164
 165 instance
 166   ( forall sem. Syntaxes syns sem => Functor sem
 167   ) =>
 168   Functor (ForallSemantic syns)
 169   where
 170   fmap f (ForallSemantic sem) = ForallSemantic (fmap f sem)
 171   a <$ (ForallSemantic sem) = ForallSemantic (a <$ sem)
 172 instance
 173   ( forall sem. Syntaxes syns sem => Applicative sem
 174   , Functor (ForallSemantic syns)
 175   ) =>
 176   Applicative (ForallSemantic syns)
 177   where
 178   pure a = ForallSemantic (pure a)
 179   liftA2 f (ForallSemantic a) (ForallSemantic b) = ForallSemantic (liftA2 f a b)
 180   (<*>) (ForallSemantic f) (ForallSemantic a) = ForallSemantic ((<*>) f a)
 181   (<*) (ForallSemantic f) (ForallSemantic a) = ForallSemantic ((<*) f a)
 182   (*>) (ForallSemantic f) (ForallSemantic a) = ForallSemantic ((*>) f a)
 183 instance
 184   ( forall sem. Syntaxes syns sem => Monad sem
 185   , Applicative (ForallSemantic syns)
 186   ) =>
 187   Monad (ForallSemantic syns)
 188   where
 189   (>>=) (ForallSemantic sa) f = ForallSemantic (sa >>= \a -> case f a of ForallSemantic sb -> sb)
 190   return = pure
 191   (>>) = (*>)