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 Unsafe.Coerce (unsafeCoerce)
  17
  18 import Symantic.Typer.Type (Ty)
  19
  20 type Semantic = Type -> Type
  21 type Syntax = Semantic -> Constraint
  22
  23 -- | Like 'FinalSyntax' but partially applicable.
  24 --class FinalSyntax syns sem => ForallSyntaxes syns (sem::Type -> Type) where
  25 --instance ForallSyntaxes '[] sem
  26 --instance ((syn sem, ForallSyntaxes syns sem)::Constraint) => ForallSyntaxes (syn ': syns) sem
  27
  28 -- | Merge syntax 'Constraint's into a single 'Constraint'.
  29 type family FinalSyntax (syns :: [(Type -> Type) -> Constraint]) (sem :: Type -> Type) :: Constraint where
  30   FinalSyntax '[] sem = (() :: Constraint)
  31   FinalSyntax (syn ': syns) sem = ((syn sem, FinalSyntax syns sem) :: Constraint)
  32
  33 data Semantics (syns :: [Syntax]) (a :: Type) = Semantics {unForallSem :: forall sem. FinalSyntax syns sem => sem a}
  34
  35 -- * Type 'CtxTe'
  36
  37 -- | GADT for an /interpreting context/:
  38 -- accumulating at each /lambda abstraction/
  39 -- the term of the introduced variable.
  40 data CtxTe (sem :: Type -> Type) (as :: [Type]) where
  41   CtxTeZ :: CtxTe sem '[]
  42   CtxTeS :: sem a -> CtxTe sem as -> CtxTe sem (a ': as)
  43
  44 infixr 5 `CtxTeS`
  45
  46 class Addable sem where
  47   lit :: Int -> sem Int
  48   neg :: sem (Int -> Int)
  49   add :: sem (Int -> Int -> Int)
  50
  51 class Mulable sem where
  52   mul :: sem Int -> sem Int -> sem Int
  53
  54 class Abstractable meta sem where
  55   -- type AbstractableLam sem (a::Type) :: Constraint
  56   -- type AbstractableLam sem a = (()::Constraint)
  57
  58   -- | Lambda term abstraction, in HOAS (Higher-Order Abstract Syntax) style.
  59   lam :: Ty meta '[] a -> (sem a -> sem b) -> sem (a -> b)
  60
  61 class UnAbstractable sem where
  62   -- | Application, aka. unabstract.
  63   (.@) :: sem (a -> b) -> sem a -> sem b
  64
  65 instance (forall sem. FinalSyntax syn sem => Constable sem) => Constable (Semantics syn) where
  66   constI = Semantics constI
  67   constK = Semantics constK
  68   constS = Semantics constS
  69   constB = Semantics constB
  70   constC = Semantics constC
  71 instance (forall sem. FinalSyntax syn sem => Addable sem) => Addable (Semantics syn) where
  72   lit n = Semantics (lit n)
  73   neg = Semantics neg
  74   add = Semantics add
  75 instance (forall sem. FinalSyntax syn sem => Mulable sem) => Mulable (Semantics syn) where
  76   mul (Semantics a) (Semantics b) = Semantics (mul a b)
  77 instance
  78   ( forall sem. FinalSyntax syn sem => Abstractable meta sem
  79   -- , forall sem a. syn sem => AbstractableLam sem a
  80   -- , forall sem. syn sem => AbstractableLam sem a
  81   -- , forall sem. syn sem => Typeable sem -- user instance not accepted
  82   -- , forall s1 s2. (syn s1, syn s2) => s1 ~ s2 -- crazy...
  83   ) =>
  84   Abstractable meta (Semantics syn)
  85   where
  86   lam aTy f = Semantics (lam aTy (\a -> let Semantics b = f (forallSem a) in b))
  87     where
  88       -- Safe here because (a :: sem a) and (b :: sem b) share the same 'sem'.
  89       forallSem :: sem a -> Semantics syn a
  90       forallSem a = Semantics (unsafeCoerce a)
  91 instance
  92   (forall sem. FinalSyntax syn sem => UnAbstractable sem) =>
  93   UnAbstractable (Semantics syn)
  94   where
  95   Semantics a2b .@ Semantics a = Semantics (a2b .@ a)
  96
  97 data TTerm (syn :: [Syntax]) (vs :: [Type]) (a :: Type) where
  98   -- TVar :: Var vs a -> TTerm syn vs a
  99   TConst :: Semantics syn a -> TTerm syn vs a
 100   TLam :: TTerm syn (a ': vs) b -> TTerm syn vs (a -> b)
 101   TApp :: TTerm syn vs (a -> b) -> TTerm syn vs a -> TTerm syn vs b
 102
 103 data OTerm (syn :: [Syntax]) (vs :: [Type]) (a :: Type) where
 104   -- E contains embedded closed (i.e. already abstracted) terms.
 105   E :: Semantics syn a -> OTerm syn vs a
 106   -- V represents a reference to the innermost/top environment
 107   -- variable, i.e. Z
 108   V :: OTerm syn (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 :: OTerm syn vs (a -> b) -> OTerm syn (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 :: OTerm syn vs b -> OTerm syn (a ': vs) b
 117 instance
 118   ( forall sem. FinalSyntax syn sem => Abstractable meta sem
 119   , FinalSyntax syn (Semantics syn)
 120   ) =>
 121   Abstractable meta (OTerm syn '[])
 122   where
 123   lam aTy f = E (lam aTy (runOTerm . f . E))
 124 instance
 125   ( forall sem. FinalSyntax syn sem => Constable sem
 126   , FinalSyntax syn (Semantics syn)
 127   ) =>
 128   Constable (OTerm syn 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 newtype R a = R {unR :: a}
 137 instance Abstractable meta R where
 138   lam _aTy f = R (unR . f . R)
 139 instance UnAbstractable R where
 140   R f .@ R x = R (f x)
 141 instance Constable R where
 142   constI = R Fun.id
 143   constK = R Fun.const
 144   constS = R (<*>)
 145   constB = R (.)
 146   constC = R Fun.flip
 147
 148 runOTerm :: OTerm syn '[] a -> Semantics syn a
 149 runOTerm t = case t of E t' -> t'
 150
 151 eval :: FinalSyntax syn R => OTerm syn '[] a -> a
 152 eval t
 153   | Semantics sem <- runOTerm t =
 154       unR sem
 155
 156 class Constable sem where
 157   constI :: sem (a -> a)
 158   constK :: sem (a -> b -> a)
 159   constS :: sem ((a -> b -> c) -> (a -> b) -> a -> c)
 160   constB :: sem ((b -> c) -> (a -> b) -> a -> c)
 161   constC :: sem ((a -> b -> c) -> b -> a -> c)
 162
 163 instance
 164   ( forall sem. FinalSyntax syn sem => Constable sem
 165   , forall sem. FinalSyntax syn sem => UnAbstractable sem
 166   , FinalSyntax syn (Semantics syn)
 167   -- , forall a as. syn (OTerm syn (as)) => syn (OTerm syn (a ': as))
 168   ) =>
 169   UnAbstractable (OTerm syn vs)
 170   where
 171   (.@) = appOTerm
 172
 173 appOTerm ::
 174   forall syn as a b.
 175   ( forall sem. FinalSyntax syn sem => Constable sem
 176   , forall sem. FinalSyntax syn sem => UnAbstractable sem
 177   , FinalSyntax syn (Semantics syn)
 178   ) =>
 179   OTerm syn as (a -> b) ->
 180   OTerm syn as a ->
 181   OTerm syn as b
 182 W e1 `appOTerm` W e2 = W (e1 `appOTerm` e2)
 183 W e `appOTerm` E d = W (e `appOTerm` E d)
 184 E d `appOTerm` W e = W (E d `appOTerm` e)
 185 W e `appOTerm` V = N e
 186 V `appOTerm` W e = N (E (constC .@ constI) `appOTerm` e)
 187 W e1 `appOTerm` N e2 = N (E constB `appOTerm` e1 `appOTerm` e2)
 188 N e1 `appOTerm` W e2 = N (E constC `appOTerm` e1 `appOTerm` e2)
 189 N e1 `appOTerm` N e2 = N (E constS `appOTerm` e1 `appOTerm` e2)
 190 N e `appOTerm` V = N (E constS `appOTerm` e `appOTerm` E constI)
 191 V `appOTerm` N e = N (E (constS .@ constI) `appOTerm` e)
 192 E d `appOTerm` N e = N (E (constB .@ d) `appOTerm` e)
 193 E d `appOTerm` V = N (E d)
 194 V `appOTerm` E d = N (E (constC .@ constI .@ d))
 195 N e `appOTerm` E d = N (E (constC .@ constC .@ d) `appOTerm` e)
 196 E d1 `appOTerm` E d2 = E (d1 .@ d2)
 197
 198 data CONST syn a where
 199   -- CInt :: Int -> Const Int
 200   -- CIf :: Const (Bool -> a -> a -> a)
 201   -- CAdd :: Const (Int -> Int -> Int)
 202   -- CGt :: Ord a => Const (a -> a -> Bool)
 203   F :: Semantics syn a -> CONST syn a
 204   I :: CONST syn (a -> a)
 205   K :: CONST syn (a -> b -> a)
 206   S :: CONST syn ((a -> b -> c) -> (a -> b) -> a -> c)
 207   B :: CONST syn ((b -> c) -> (a -> b) -> a -> c)
 208   C :: CONST syn ((a -> b -> c) -> b -> a -> c)
 209
 210 -- conv :: Term vs α -> OTerm vs α
 211 -- conv = \case
 212 --  TVar VZ -> V
 213 --  TVar (VS x) -> W (conv (TVar x))
 214 --  TLam t -> case conv t of
 215 --    V -> E (embed I)
 216 --    E d -> E (K .$$ d)
 217 --    N e -> e
 218 --    W e -> K .$$ e
 219 --  TApp t1 t2 -> conv t1 $$ conv t2
 220 --  TConst c -> embed c
 221
 222 instance
 223   ( forall sem. FinalSyntax syn sem => Functor sem
 224   ) =>
 225   Functor (Semantics syn)
 226   where
 227   fmap f (Semantics sem) = Semantics (fmap f sem)
 228   a <$ (Semantics sem) = Semantics (a <$ sem)
 229 instance
 230   ( forall sem. FinalSyntax syn sem => Applicative sem
 231   , Functor (Semantics syn)
 232   ) =>
 233   Applicative (Semantics syn)
 234   where
 235   pure a = Semantics (pure a)
 236   liftA2 f (Semantics a) (Semantics b) = Semantics (liftA2 f a b)
 237   (<*>) (Semantics f) (Semantics a) = Semantics ((<*>) f a)
 238   (<*) (Semantics f) (Semantics a) = Semantics ((<*) f a)
 239   (*>) (Semantics f) (Semantics a) = Semantics ((*>) f a)
 240 instance
 241   ( forall sem. FinalSyntax syn sem => Monad sem
 242   , Applicative (Semantics syn)
 243   ) =>
 244   Monad (Semantics syn)
 245   where
 246   (>>=) (Semantics sa) f = Semantics (sa >>= \a -> case f a of Semantics sb -> sb)
 247   return = pure
 248   (>>) = (*>)