sappho short

- sappho types intro
- a quick look at msph and spho

The types

We take a look at the grammar for sappho types

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. modal 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)
       | ( t )


x ∈ var
n ∈ nominal
a ∈ opname

The type t <: s would be syntactic sugar for box (t => s)

msph and spho

msph is a minimal language for describing types in sappho and a partial implementation (as of 2025-06-25). The goal being to have a prototype for deciding subtyping by the end of the summer. Right now it includes

parser (prefix notation &, |, =>, ->)
iterative decorators adding scope, type, and binding data.
interface with these decorations is implemented as a separate library, spho.

spho is the WIP type system implementation, as of now having bindings to

handle type representation data structures
handle scoping of names and bindings
initial progress on subtyping implementation

Left to do to get a prototype subtype checker working:

handling of subtyping sequent judgement rules
search heuristic for basic proof search
cyclic proof search

Thoughts

maybe eventually add a basic term language and interpreter
can we use external software/libraries for proof search?

interpretation of types

- example programs in `msph`
	- unified syntax for types and bounded polymorphism
	- example: self typing
	- example: conditional method existence
	- example: capabilities?
- the meaning of `true` and existence of methods.
	- undefined behaviour and `true`?
- how does this relate to the denotation stuff from before?

formal rules and the sequent calculus

Check formalities.md. - simple rules - type constructor rules - recursion and cyclic proofs

next steps?

- formals:
	- formulate theorems
		- if we use semantic subtyping, isn't it enough to
		  prove subtyping sound with regards to set denotation?
	- specify term language?
- implementation: sequent calculus based subtyping decider
	- simple rules, should be fairly simple
	- type constructors, straightforward hopefully
	- recursion and cyclic proofs... `¯\_(ツ)_/¯`
- describe use of language with type system (interpretation of types)

2.7 KiB Raw Blame History