# draft of presentation

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


### The types

We take a look at the grammar for sappho types

```cmath
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)
       | ( t )


x ∈ var
n ∈ nominal
a ∈ opname
```

The type `t <: s` would be expressive 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
	- simple rules
	- type constructor rules
	- recursion and cyclic proofs
* next steps?
	- implementation: sequent calculus based subtyping decider
		- simple rules, should be fairly simple
		- type constructors, straightforward hopefully
		- recursion and cyclic proofs... `¯\_(ツ)_/¯`
	- formals:
		- formulate theorems
			- if we use semantic subtyping, isn't it enough to
			  prove subtyping sound with regards to set denotation?
		- specify term language?