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, c.f. 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

---- [identity]
ρ; s, γ ⊢ s, δ

---- [true-right]
ρ; γ ⊢ true, δ

---- [false-left]
ρ; false, γ ⊢ δ

ρ; 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
// remove s => t? always make progress
ρ; s => t, s, t, γ ⊢ δ
---- [impl-left]
ρ; s => t, s, γ ⊢ δ

// discussion about implication below
// check how "normal sequent calculus handles this"
ρ; 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, δ


// recursion through operators are handled using the recursion context ρ
// XXX compare with iso-recursive subtyping (double expansion)
---- [op-discharge]
a [t..], ρ; γ ⊢ a [t..], δ

a [t..]*, ρ; γ ⊢ expand(a [t..]), δ
---- [op-expand1]
ρ; γ ⊢ a [t..], δ

a [t..], ρ; γ ⊢ expand(a [t..]), δ
---- [op-expand2]
a [t..]*, ρ; γ ⊢ a [t..], δ



// member types are filtered according to member name
ρ; γ >> m ⊢ δ >> m
---- [member]
ρ; γ ⊢ δ


// foralls are unwrapped and variable substituted with fresh name
// i.e. we treat the bound variable nominally
n fresh
ρ; γ [n] ⊢ δ [n]
---- [forall]
ρ; γ ⊢ δ

context operators

box filtering

(t, γ)-- =def= t, γ--       if t == box s, for some s
               γ--          otherwise

member unwrapping

(t, γ) >> m =def= s, (γ >> m)       if t == { m : s }, for some s
                  γ >> m            otherwise

forall-unwrapping and substitution

(t, γ) [n] =def= s [n/x], (γ [n])   if t == forall x . s, for some x, s
                 γ [n]              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

3.4 KiB Raw Blame History Unescape Escape