progress 2025-06-27

docs/about/progress.md

@@ -0,0 +1,87 @@
+# 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
+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... `¯\_(ツ)_/¯`