src/Symantic/Compiler/Term.hs

   1 {-# LANGUAGE ConstraintKinds #-}
   2 {-# LANGUAGE EmptyCase #-}
   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 Control.Monad (Monad (..))
  13 import Data.Function ((.))
  14 import Data.Function qualified as Fun
  15 import Data.Functor (Functor (..))
  16 import GHC.Types (Constraint, Type)
  17 import Symantic.Syntaxes.Classes (Unabstractable (..))
  18 import Text.Show (Show (..))
  19 import Unsafe.Coerce (unsafeCoerce)
  20
  21 import Symantic.Typer.Type (Ty)
  22
  23 type Semantic = Type -> Type
  24 type Syntax = Semantic -> Constraint
  25
  26 -- * Type 'PerSyntax'
  27 data PerSyntax :: [Syntax] -> (Syntax -> Type) -> Type where
  28   PerSyntaxZ :: a syn -> PerSyntax (syn ': syns) a
  29   PerSyntaxS :: PerSyntax syns a -> PerSyntax (not_s ': syns) a
  30
  31 instance Show (PerSyntax '[] a) where
  32   showsPrec _p = \case {}
  33 instance
  34   ( Show (a syn)
  35   , Show (PerSyntax syns a)
  36   ) =>
  37   Show (PerSyntax (syn ': syns) a)
  38   where
  39   showsPrec p = \case
  40     PerSyntaxZ a -> showsPrec p a
  41     PerSyntaxS s -> showsPrec p s
  42
  43 -- ** Class 'PerSyntaxable'
  44 class PerSyntaxable (syns :: [Syntax]) (syn :: Syntax) where
  45   perSyntax :: a syn -> PerSyntax syns a
  46 instance {-# OVERLAPS #-} PerSyntaxable (syn ': syns) syn where
  47   perSyntax = PerSyntaxZ
  48 instance PerSyntaxable syns syn => PerSyntaxable (not_syn ': syns) syn where
  49   perSyntax = PerSyntaxS . perSyntax
  50
  51 -- | Merge syntax 'Constraint's into a single 'Constraint'.
  52 type family Syntaxes (syns :: [(Type -> Type) -> Constraint]) (sem :: Type -> Type) :: Constraint where
  53   Syntaxes '[] sem = (() :: Constraint)
  54   Syntaxes (syn ': syns) sem = ((syn sem, Syntaxes syns sem) :: Constraint)
  55
  56 -- * Type 'ForallSemantic'
  57 data ForallSemantic (syns :: [Syntax]) (a :: Type)
  58   = ForallSemantic (forall sem. Syntaxes syns sem => sem a)
  59
  60 -- * Class 'Abstractable'
  61 class Abstractable meta sem where
  62   -- type AbstractableLam sem (a::Type) :: Constraint
  63   -- type AbstractableLam sem a = (()::Constraint)
  64
  65   -- | Lambda term abstraction, in HOAS (Higher-Order Abstract Syntax) style.
  66   lam :: Ty meta '[] a -> (sem a -> sem b) -> sem (a -> b)
  67
  68 -- * Class 'Constable'
  69 class Constable sem where
  70   constI :: sem (a -> a)
  71   constK :: sem (a -> b -> a)
  72   constS :: sem ((a -> b -> c) -> (a -> b) -> a -> c)
  73   constB :: sem ((b -> c) -> (a -> b) -> a -> c)
  74   constC :: sem ((a -> b -> c) -> b -> a -> c)
  75
  76 instance (forall sem. Syntaxes syns sem => Constable sem) => Constable (ForallSemantic syns) where
  77   constI = ForallSemantic constI
  78   constK = ForallSemantic constK
  79   constS = ForallSemantic constS
  80   constB = ForallSemantic constB
  81   constC = ForallSemantic constC
  82 instance
  83   ( forall sem. Syntaxes syns sem => Abstractable meta sem
  84   -- , forall sem a. syn sem => AbstractableLam sem a
  85   -- , forall sem. syn sem => AbstractableLam sem a
  86   -- , forall sem. syn sem => Typeable sem -- user instance not accepted
  87   -- , forall s1 s2. (syn s1, syn s2) => s1 ~ s2 -- crazy...
  88   ) =>
  89   Abstractable meta (ForallSemantic syns)
  90   where
  91   lam aTy f = ForallSemantic (lam aTy (\a -> let ForallSemantic b = f (forallSem a) in b))
  92     where
  93       -- Safe here because (a :: sem a) and (b :: sem b) share the same 'sem'.
  94       forallSem :: sem a -> ForallSemantic syns a
  95       forallSem a = ForallSemantic (unsafeCoerce a)
  96 instance
  97   (forall sem. Syntaxes syns sem => Unabstractable sem) =>
  98   Unabstractable (ForallSemantic syns)
  99   where
 100   ForallSemantic a2b .@ ForallSemantic a = ForallSemantic (a2b .@ a)
 101
 102 -- * Type 'OpenTerm'
 103 data OpenTerm (syns :: [Syntax]) (vs :: [Type]) (a :: Type) where
 104   -- E contains embedded closed (i.e. already abstracted) terms.
 105   E :: ForallSemantic syns a -> OpenTerm syns vs a
 106   -- V represents a reference to the innermost/top environment
 107   -- variable, i.e. Z
 108   V :: OpenTerm syns (a ': vs) a
 109   -- N represents internalizing the innermost bound variable as a
 110   -- function argument. In other words, we can represent an open
 111   -- term referring to a certain variable as a function which
 112   -- takes that variable as an argument.
 113   N :: OpenTerm syns vs (a -> b) -> OpenTerm syns (a ': vs) b
 114   -- For efficiency, there is also a special variant of N for the
 115   -- case where the term does not refer to the topmost variable at all.
 116   W :: OpenTerm syns vs b -> OpenTerm syns (a ': vs) b
 117 instance
 118   ( forall sem. Syntaxes syns sem => Abstractable meta sem
 119   , Syntaxes syns (ForallSemantic syns)
 120   ) =>
 121   Abstractable meta (OpenTerm syns '[])
 122   where
 123   lam aTy f = E (lam aTy (runOpenTerm . f . E))
 124 instance
 125   ( forall sem. Syntaxes syns sem => Constable sem
 126   , Syntaxes syns (ForallSemantic syns)
 127   ) =>
 128   Constable (OpenTerm syns vs)
 129   where
 130   constI = E constI
 131   constK = E constK
 132   constS = E constS
 133   constB = E constB
 134   constC = E constC
 135
 136 -- * Type 'R'
 137 newtype R a = R {unR :: a}
 138 instance Abstractable meta R where
 139   lam _aTy f = R (unR . f . R)
 140 instance Unabstractable R where
 141   R f .@ R x = R (f x)
 142 instance Constable R where
 143   constI = R Fun.id
 144   constK = R Fun.const
 145   constS = R (<*>)
 146   constB = R (.)
 147   constC = R Fun.flip
 148
 149 runOpenTerm :: OpenTerm syns '[] a -> ForallSemantic syns a
 150 runOpenTerm t = case t of E t' -> t'
 151
 152 eval :: Syntaxes syns R => OpenTerm syns '[] a -> a
 153 eval t
 154   | ForallSemantic sem <- runOpenTerm t =
 155       unR sem
 156
 157 instance
 158   ( forall sem. Syntaxes syns sem => Constable sem
 159   , forall sem. Syntaxes syns sem => Unabstractable sem
 160   , Syntaxes syns (ForallSemantic syns)
 161   -- , forall a as. syns (OpenTerm syns (as)) => syns (OpenTerm syns (a ': as))
 162   ) =>
 163   Unabstractable (OpenTerm syns vs)
 164   where
 165   (.@) = appOpenTerm
 166
 167 appOpenTerm ::
 168   forall syns as a b.
 169   ( forall sem. Syntaxes syns sem => Constable sem
 170   , forall sem. Syntaxes syns sem => Unabstractable sem
 171   , Syntaxes syns (ForallSemantic syns)
 172   ) =>
 173   OpenTerm syns as (a -> b) ->
 174   OpenTerm syns as a ->
 175   OpenTerm syns as b
 176 W e1 `appOpenTerm` W e2 = W (e1 `appOpenTerm` e2)
 177 W e `appOpenTerm` E d = W (e `appOpenTerm` E d)
 178 E d `appOpenTerm` W e = W (E d `appOpenTerm` e)
 179 W e `appOpenTerm` V = N e
 180 V `appOpenTerm` W e = N (E (constC .@ constI) `appOpenTerm` e)
 181 W e1 `appOpenTerm` N e2 = N (E constB `appOpenTerm` e1 `appOpenTerm` e2)
 182 N e1 `appOpenTerm` W e2 = N (E constC `appOpenTerm` e1 `appOpenTerm` e2)
 183 N e1 `appOpenTerm` N e2 = N (E constS `appOpenTerm` e1 `appOpenTerm` e2)
 184 N e `appOpenTerm` V = N (E constS `appOpenTerm` e `appOpenTerm` E constI)
 185 V `appOpenTerm` N e = N (E (constS .@ constI) `appOpenTerm` e)
 186 E d `appOpenTerm` N e = N (E (constB .@ d) `appOpenTerm` e)
 187 E d `appOpenTerm` V = N (E d)
 188 V `appOpenTerm` E d = N (E (constC .@ constI .@ d))
 189 N e `appOpenTerm` E d = N (E (constC .@ constC .@ d) `appOpenTerm` e)
 190 E d1 `appOpenTerm` E d2 = E (d1 .@ d2)
 191
 192 instance
 193   ( forall sem. Syntaxes syns sem => Functor sem
 194   ) =>
 195   Functor (ForallSemantic syns)
 196   where
 197   fmap f (ForallSemantic sem) = ForallSemantic (fmap f sem)
 198   a <$ (ForallSemantic sem) = ForallSemantic (a <$ sem)
 199 instance
 200   ( forall sem. Syntaxes syns sem => Applicative sem
 201   , Functor (ForallSemantic syns)
 202   ) =>
 203   Applicative (ForallSemantic syns)
 204   where
 205   pure a = ForallSemantic (pure a)
 206   liftA2 f (ForallSemantic a) (ForallSemantic b) = ForallSemantic (liftA2 f a b)
 207   (<*>) (ForallSemantic f) (ForallSemantic a) = ForallSemantic ((<*>) f a)
 208   (<*) (ForallSemantic f) (ForallSemantic a) = ForallSemantic ((<*) f a)
 209   (*>) (ForallSemantic f) (ForallSemantic a) = ForallSemantic ((*>) f a)
 210 instance
 211   ( forall sem. Syntaxes syns sem => Monad sem
 212   , Applicative (ForallSemantic syns)
 213   ) =>
 214   Monad (ForallSemantic syns)
 215   where
 216   (>>=) (ForallSemantic sa) f = ForallSemantic (sa >>= \a -> case f a of ForallSemantic sb -> sb)
 217   return = pure
 218   (>>) = (*>)