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