log-e-sappho/README.md

# 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, δ


// using cyclic proof strategy, rule for dealing with aliases/type operators
// becomes really simple. However, this requires well-formedness rules on types
// to exclude typedefs like
// type A = A
// Or that our cycle detection excludes paths between "identical" states.
γ ⊢ expand(a[t..]), δ
----
γ ⊢ a[t..], δ

expand(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]
ρ; γ ⊢ δ


ρ; t[n/x], s[n/y] ⊢ u[n/z]
----
ρ; forall x. t, forall y. s ⊢ forall z. u
```


### 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
                  t, (γ >> m)       if t == box 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
                 t, (γ [n])         if t == box s, for some s
                 γ [n]              otherwise
```

### Recursive subtyping

Type aliases creates the possibility of recursive types, and thus we need to
handle recursive subtyping

Handling subtyping co-inductively would enable us to handle the relation
```
type A = { x : { y : A } }
type B = { y : { x : B } }

A <: { x : B }
{ x : B } <: A
```


We have made progress if we "switch context"

If we make progress and end up at the same sequent, co-induction gives us the
conclusion.

Some actions/rules lead to equivalent contexts, i.e. does not switch
context/make progress.

### Other

True ~ { x : True } on the left
False ~ { x : False } on the right

or rather

True ~ { x : True } in positive position
False ~ { x : False } in negative position





### implication
```

γ ⊢ s => t, u => s, δ

if s, then u => s holds
if ¬s, then s => t holds

```


altho
```
γ ⊢ s => t, s, δ
```

Given the msph program
```
nominal n

type Woops[e] = {
	member f : (e <: false => n) | (e <: false)
}

type Noooes = {
	member f : true
}
```
we can prove that, for any type `t`
```
Noooes <: Woops[t]
```

The derivation looks like this:
```
---- [identity]
true, t <: false ⊢ n, (t <: false)
---- [impl-right]
true ⊢ (t <: false => n), (t <: false)
---- [disj-right]
true ⊢ (t <: false => n) | (t <: false)
---- [member]
{ f : true } ⊢ { f : (t <: false => n) | (t <: false) }
---- [expand-right]
{ f : true } ⊢ Woops[t]
---- [expand-left]
Nooes ⊢ Woops[t]
---- [impl-right]
⊢ Nooes => Woops[t]
---- [box-right]
⊢ Nooes <: Woops[t]
```

This looks a bit dangerous at first. However, if we translate the implication to
using disjunction and negation, we get
```
(t <: false => N) | (t <: false) == (¬(t <: false) | n) | (t <: false)
```

Considering the two cases
```
(1) t == false
(2) t != false
```
we see that in (1)
```
(¬(t <: false) | n) | (t <: false) ==
(¬(true) | n) | (true) ==
true
```
and in (2)
```
(¬(t <: false) | n) | (t <: false) ==
(¬(false) | n) | false ==
(true | n) | false ==
true
```

## What is true?

Our "set interpretation" of types says `true` represents the full universe of
"things".

What are these things?

For all intents and purposes, a programmer can look at them as the values of
our language.

What does this mean in practical terms?

Well, it means something of type `true` is "a value".

What is "a value" then?

That's a good question. It can be anything really.

An integer?

Yep!

A function?

Yes, m'am!

A solution to the halting problem?

Well, yeah! But good luck constructing that.

A...

I think you get my point. A value can be anything from a simple integer to
nuclear apocalypse. The thing is, from the point of view of our program, it
means "we cannot really say anything here".

But couldn't that be dangerous?

Depends on what you mean by dangerous.

I mean, to be able to give everything a type?

Well, let me ask you this: do you like rat poison?

What? To eat?

Yeah!

Nooo, that'd be dangerous!

Yeah, exactly my point.

What?

You know what rat poison is obviously, despite it being dangerous?

Well, yeah...

Maybe you got it already, but my point is: rat poison is dangerous, but you
still know about it, and its existance. So, something being dangerous does not
mean you have this blank spot of knowledge that you just keep ignoring because
of this perceived danger.





### interpretation of ⊢
what is the interpretation of

γ ⊢ δ?


given a concrete type k

conjunction of γ hold for k

then 

disjunction of δ hold for k