119 lines
2.1 KiB
Markdown
119 lines
2.1 KiB
Markdown
# log-e-sappho
|
||
|
||
experimental type system implementation
|
||
|
||
## sappho grammar
|
||
|
||
```
|
||
s, t ::= s | t (disjunction, a.k.a. union)
|
||
| s & t (conjunction, a.k.a. intersection)
|
||
| s => t (implication)
|
||
| s -> t (arrow, a.k.a. function)
|
||
| forall x . t (forall, polymorphic)
|
||
| box t (box, modular logic)
|
||
| a [t..] (type operator application)
|
||
| x (variable)
|
||
| n (nominal)
|
||
| true (true, a.k.a. top)
|
||
| false (false, a.k.a. bottom)
|
||
| { m : t } (member, a.k.a. atomic record)
|
||
|
||
|
||
x ∈ var
|
||
n ∈ nominal
|
||
a ∈ opname
|
||
```
|
||
|
||
## sappho subtyping rules
|
||
|
||
```
|
||
s, t, γ ⊢ δ
|
||
---- [conj-left]
|
||
s & t, γ ⊢ δ
|
||
|
||
γ ⊢ s, t, δ
|
||
---- [disj-right]
|
||
γ ⊢ s | t, δ
|
||
|
||
s, γ ⊢ δ
|
||
t, γ ⊢ δ
|
||
---- [disj-left]
|
||
s | t, γ ⊢ δ
|
||
|
||
γ ⊢ s, δ
|
||
γ ⊢ t, δ
|
||
---- [conj-right]
|
||
γ ⊢ s & t, δ
|
||
|
||
// XXX
|
||
s => t, s, t, γ ⊢ δ
|
||
---- [impl-left]
|
||
s => t, s, γ ⊢ δ
|
||
|
||
// discussion about implication below
|
||
s, γ ⊢ t, δ
|
||
---- [impl-right]
|
||
γ ⊢ s => t, δ
|
||
|
||
|
||
// box works as a kind of "forall" for concrete types
|
||
box t, t, γ ⊢ δ
|
||
---- [box-left]
|
||
box t, γ ⊢ δ
|
||
|
||
// (.)-- filters the contexts.
|
||
γ-- ⊢ t, δ--
|
||
---- [box-right]
|
||
γ ⊢ box t, δ
|
||
|
||
|
||
|
||
```
|
||
|
||
|
||
### context operators
|
||
|
||
```
|
||
(t, γ)-- =def= t, γ-- if t == box s
|
||
γ-- otherwise
|
||
```
|
||
|
||
What happens when box is buried under type operators, like box s & box t? It
|
||
could be that the above definition filters out too much of the contexts.
|
||
|
||
My gut feeling™ makes me think it is just a matter of reordering sequent rules
|
||
to get keep the things wanted in context, which for an algorithm sucks, but from
|
||
a declarative standpoint would be okay. This needs some further validation, and
|
||
of course a reformulation for the actual algorithm.
|
||
|
||
|
||
|
||
|
||
### implication
|
||
```
|
||
|
||
γ ⊢ s => t, u => s, δ
|
||
|
||
if s, then u => s holds
|
||
if ¬s, then s => t holds
|
||
|
||
```
|
||
|
||
|
||
|
||
### interpretation of ⊢
|
||
what is the interpretation of
|
||
|
||
γ ⊢ δ?
|
||
|
||
|
||
given a concrete type k
|
||
|
||
conjunction of γ hold for k
|
||
|
||
then
|
||
|
||
disjunction of δ hold for k
|
||
|
||
|
||
|