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