1 {-# LANGUAGE ConstraintKinds #-}
2 {-# LANGUAGE EmptyCase #-}
3 {-# LANGUAGE InstanceSigs #-}
4 {-# LANGUAGE QuantifiedConstraints #-}
5 {-# LANGUAGE RankNTypes #-}
6 {-# LANGUAGE UndecidableInstances #-}
7 {-# OPTIONS_GHC -Wno-partial-fields #-}
9 module Symantic.Compiler.Term where
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)
21 import Symantic.Typer.Type (Ty)
23 type Semantic = Type -> Type
24 type Syntax = Semantic -> Constraint
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
31 instance Show (PerSyntax '[] a) where
32 showsPrec _p = \case {}
35 , Show (PerSyntax syns a)
37 Show (PerSyntax (syn ': syns) a)
40 PerSyntaxZ a -> showsPrec p a
41 PerSyntaxS s -> showsPrec p s
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
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)
56 -- * Type 'ForallSemantic'
57 data ForallSemantic (syns :: [Syntax]) (a :: Type)
58 = ForallSemantic (forall sem. Syntaxes syns sem => sem a)
60 -- * Class 'Abstractable'
61 class Abstractable meta sem where
62 -- type AbstractableLam sem (a::Type) :: Constraint
63 -- type AbstractableLam sem a = (()::Constraint)
65 -- | Lambda term abstraction, in HOAS (Higher-Order Abstract Syntax) style.
66 lam :: Ty meta '[] a -> (sem a -> sem b) -> sem (a -> b)
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)
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
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...
89 Abstractable meta (ForallSemantic syns)
91 lam aTy f = ForallSemantic (lam aTy (\a -> let ForallSemantic b = f (forallSem a) in b))
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)
97 (forall sem. Syntaxes syns sem => Unabstractable sem) =>
98 Unabstractable (ForallSemantic syns)
100 ForallSemantic a2b .@ ForallSemantic a = ForallSemantic (a2b .@ a)
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
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
118 ( forall sem. Syntaxes syns sem => Abstractable meta sem
119 , Syntaxes syns (ForallSemantic syns)
121 Abstractable meta (OpenTerm syns '[])
123 lam aTy f = E (lam aTy (runOpenTerm . f . E))
125 ( forall sem. Syntaxes syns sem => Constable sem
126 , Syntaxes syns (ForallSemantic syns)
128 Constable (OpenTerm syns vs)
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
142 instance Constable R where
149 runOpenTerm :: OpenTerm syns '[] a -> ForallSemantic syns a
150 runOpenTerm t = case t of E t' -> t'
152 eval :: Syntaxes syns R => OpenTerm syns '[] a -> a
154 | ForallSemantic sem <- runOpenTerm t =
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))
163 Unabstractable (OpenTerm syns vs)
169 ( forall sem. Syntaxes syns sem => Constable sem
170 , forall sem. Syntaxes syns sem => Unabstractable sem
171 , Syntaxes syns (ForallSemantic syns)
173 OpenTerm syns as (a -> b) ->
174 OpenTerm syns as a ->
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)
193 ( forall sem. Syntaxes syns sem => Functor sem
195 Functor (ForallSemantic syns)
197 fmap f (ForallSemantic sem) = ForallSemantic (fmap f sem)
198 a <$ (ForallSemantic sem) = ForallSemantic (a <$ sem)
200 ( forall sem. Syntaxes syns sem => Applicative sem
201 , Functor (ForallSemantic syns)
203 Applicative (ForallSemantic syns)
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)
211 ( forall sem. Syntaxes syns sem => Monad sem
212 , Applicative (ForallSemantic syns)
214 Monad (ForallSemantic syns)
216 (>>=) (ForallSemantic sa) f = ForallSemantic (sa >>= \a -> case f a of ForallSemantic sb -> sb)