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 (skipSyn ': 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 'AnySemantic'
  57 data AnySemantic (syns :: [Syntax]) (a :: Type)
  58   = AnySemantic (forall sem. Syntaxes syns sem => sem a)
  59
  60 instance
  61   ( forall sem. Syntaxes syns sem => Functor sem
  62   ) =>
  63   Functor (AnySemantic syns)
  64   where
  65   fmap f (AnySemantic sem) = AnySemantic (fmap f sem)
  66   a <$ (AnySemantic sem) = AnySemantic (a <$ sem)
  67 instance
  68   ( forall sem. Syntaxes syns sem => Applicative sem
  69   , Functor (AnySemantic syns)
  70   ) =>
  71   Applicative (AnySemantic syns)
  72   where
  73   pure a = AnySemantic (pure a)
  74   liftA2 f (AnySemantic a) (AnySemantic b) = AnySemantic (liftA2 f a b)
  75   (<*>) (AnySemantic f) (AnySemantic a) = AnySemantic ((<*>) f a)
  76   (<*) (AnySemantic f) (AnySemantic a) = AnySemantic ((<*) f a)
  77   (*>) (AnySemantic f) (AnySemantic a) = AnySemantic ((*>) f a)
  78 instance
  79   ( forall sem. Syntaxes syns sem => Monad sem
  80   , Applicative (AnySemantic syns)
  81   ) =>
  82   Monad (AnySemantic syns)
  83   where
  84   (>>=) (AnySemantic sa) f = AnySemantic (sa >>= \a -> case f a of AnySemantic sb -> sb)
  85   return = pure
  86   (>>) = (*>)
  87 instance
  88   (forall sem. Syntaxes syns sem => Unabstractable sem) =>
  89   Unabstractable (AnySemantic syns)
  90   where
  91   AnySemantic a2b .@ AnySemantic a = AnySemantic (a2b .@ a)
  92
  93 -- * Class 'Abstractable'
  94 class Abstractable meta sem where
  95   -- type AbstractableLam sem (a::Type) :: Constraint
  96   -- type AbstractableLam sem a = (()::Constraint)
  97
  98   -- | Lambda term abstraction, in HOAS (Higher-Order Abstract Syntax) style.
  99   lam :: Ty meta '[] a -> (sem a -> sem b) -> sem (a -> b)
 100
 101 -- * Class 'Constable'
 102 class Constable sem where
 103   constI :: sem (a -> a)
 104   constK :: sem (a -> b -> a)
 105   constS :: sem ((a -> b -> c) -> (a -> b) -> a -> c)
 106   constB :: sem ((b -> c) -> (a -> b) -> a -> c)
 107   constC :: sem ((a -> b -> c) -> b -> a -> c)
 108
 109 instance (forall sem. Syntaxes syns sem => Constable sem) => Constable (AnySemantic syns) where
 110   constI = AnySemantic constI
 111   constK = AnySemantic constK
 112   constS = AnySemantic constS
 113   constB = AnySemantic constB
 114   constC = AnySemantic constC
 115 instance
 116   ( forall sem. Syntaxes syns sem => Abstractable meta sem
 117   -- , forall sem a. syn sem => AbstractableLam sem a
 118   -- , forall sem. syn sem => AbstractableLam sem a
 119   -- , forall sem. syn sem => Typeable sem -- user instance not accepted
 120   -- , forall s1 s2. (syn s1, syn s2) => s1 ~ s2 -- crazy...
 121   ) =>
 122   Abstractable meta (AnySemantic syns)
 123   where
 124   lam aTy f = AnySemantic (lam aTy (\a -> let AnySemantic b = f (forallSem a) in b))
 125     where
 126       -- Safe here because (a :: sem a) and (b :: sem b) share the same 'sem'.
 127       forallSem :: sem a -> AnySemantic syns a
 128       forallSem a = AnySemantic (unsafeCoerce a)
 129
 130 -- * Type 'OpenTerm'
 131 data OpenTerm (syns :: [Syntax]) (vs :: [Type]) (a :: Type) where
 132   -- E contains embedded closed (i.e. already abstracted) terms.
 133   E :: AnySemantic syns a -> OpenTerm syns vs a
 134   -- V represents a reference to the innermost/top environment
 135   -- variable, i.e. Z
 136   V :: OpenTerm syns (a ': vs) a
 137   -- N represents internalizing the innermost bound variable as a
 138   -- function argument. In other words, we can represent an open
 139   -- term referring to a certain variable as a function which
 140   -- takes that variable as an argument.
 141   N :: OpenTerm syns vs (a -> b) -> OpenTerm syns (a ': vs) b
 142   -- For efficiency, there is also a special variant of N for the
 143   -- case where the term does not refer to the topmost variable at all.
 144   W :: OpenTerm syns vs b -> OpenTerm syns (a ': vs) b
 145 instance
 146   ( forall sem. Syntaxes syns sem => Abstractable meta sem
 147   , Syntaxes syns (AnySemantic syns)
 148   ) =>
 149   Abstractable meta (OpenTerm syns '[])
 150   where
 151   lam aTy f = E (lam aTy (runOpenTerm . f . E))
 152 instance
 153   ( forall sem. Syntaxes syns sem => Constable sem
 154   , Syntaxes syns (AnySemantic syns)
 155   ) =>
 156   Constable (OpenTerm syns vs)
 157   where
 158   constI = E constI
 159   constK = E constK
 160   constS = E constS
 161   constB = E constB
 162   constC = E constC
 163
 164 -- * Type 'R'
 165 newtype R a = R {unR :: a}
 166 instance Abstractable meta R where
 167   lam _aTy f = R (unR . f . R)
 168 instance Unabstractable R where
 169   R f .@ R x = R (f x)
 170 instance Constable R where
 171   constI = R Fun.id
 172   constK = R Fun.const
 173   constS = R (<*>)
 174   constB = R (.)
 175   constC = R Fun.flip
 176
 177 runOpenTerm :: OpenTerm syns '[] a -> AnySemantic syns a
 178 runOpenTerm t = case t of E t' -> t'
 179
 180 eval :: Syntaxes syns R => OpenTerm syns '[] a -> a
 181 eval t
 182   | AnySemantic sem <- runOpenTerm t =
 183       unR sem
 184
 185 instance
 186   ( forall sem. Syntaxes syns sem => Constable sem
 187   , forall sem. Syntaxes syns sem => Unabstractable sem
 188   , Syntaxes syns (AnySemantic syns)
 189   -- , forall a as. syns (OpenTerm syns (as)) => syns (OpenTerm syns (a ': as))
 190   ) =>
 191   Unabstractable (OpenTerm syns vs)
 192   where
 193   (.@) = appOpenTerm
 194
 195 appOpenTerm ::
 196   forall syns as a b.
 197   ( forall sem. Syntaxes syns sem => Constable sem
 198   , forall sem. Syntaxes syns sem => Unabstractable sem
 199   , Syntaxes syns (AnySemantic syns)
 200   ) =>
 201   OpenTerm syns as (a -> b) ->
 202   OpenTerm syns as a ->
 203   OpenTerm syns as b
 204 W e1 `appOpenTerm` W e2 = W (e1 `appOpenTerm` e2)
 205 W e `appOpenTerm` E d = W (e `appOpenTerm` E d)
 206 E d `appOpenTerm` W e = W (E d `appOpenTerm` e)
 207 W e `appOpenTerm` V = N e
 208 V `appOpenTerm` W e = N (E (constC .@ constI) `appOpenTerm` e)
 209 W e1 `appOpenTerm` N e2 = N (E constB `appOpenTerm` e1 `appOpenTerm` e2)
 210 N e1 `appOpenTerm` W e2 = N (E constC `appOpenTerm` e1 `appOpenTerm` e2)
 211 N e1 `appOpenTerm` N e2 = N (E constS `appOpenTerm` e1 `appOpenTerm` e2)
 212 N e `appOpenTerm` V = N (E constS `appOpenTerm` e `appOpenTerm` E constI)
 213 V `appOpenTerm` N e = N (E (constS .@ constI) `appOpenTerm` e)
 214 E d `appOpenTerm` N e = N (E (constB .@ d) `appOpenTerm` e)
 215 E d `appOpenTerm` V = N (E d)
 216 V `appOpenTerm` E d = N (E (constC .@ constI .@ d))
 217 N e `appOpenTerm` E d = N (E (constC .@ constC .@ d) `appOpenTerm` e)
 218 E d1 `appOpenTerm` E d2 = E (d1 .@ d2)