This is still a work in progress.

No really, what's this type system?

Eventually? I want

• Linear
• call-by-push-value with
• arbitrary rank type and kind polymorphism and
• graded (co)effects.

We can take this one at a time.

Linear

Linear logic, seemingly like everything else in academia, is at once a dense subject of study with profound implications, and also a very simple idea.

As it applies to programming the basic idea is to think of types as defining resources, and the values of those types as matter which can't simply be duplicated or discarded (ignored) at will! The arrogance! So if you bind a value to a name in some scope you must use it exactly once within that scope.

Here is what pure linear file I/O would look like in pseudo-code:

file_handle := open_file ("foo.txt");
(file_handle, line_1) := read_line (file_handle);
(file_handle, line_2) := read_line (file_handle);
close (file_handle);

Notice that file_handle must be re-bound after each use, because each binding must be used exactly once. There are many systems for relaxing and extending this system to other uses, but that is the basic premise.

The appeal of linear logic in programming circles, it seems, stemmed from the promise of being able to prevent memory leaks statically at compile-time -- if you can't use a pointer twice without explicitly duplicating it, it's hard to use it a million times on accident in a loop!

On the other hand, not being able to write let square x = x * x without resorting to a helper utility is a pretty draconian restriction. One of psilo's goals is to deliver on the promises of linear logic in an intuitive way such that linearity aids development.

Call-By-Push-Value

Most languages are "strict", or call-by-value: all procedure arguments must be fully evaluated before they may be passed along. There are usually ways to explicitly circumvent this for when a computation needs to be delayed.

Some, like Haskell, are "lazy", or call-by-name/need: a term passed to a function is not evaluated fully until absolutely necessary.

It's why in Haskell, this interactive session terminates:

> fix f = let x = f x in x
> bottom = fix id
> 1 + (const 2 bottom)
3

bottom is not actually evaluated by const and so the fact that it does not terminate is no matter.

Psilo is both and neither!

Call-by-push-value subsumes both of these and instead encodes evaluation order in the type system.

A positive type is "data": it is defined by the shape of its values. You could conceivably come up with a way to print it out on paper. It's static, at rest.

A negative type is a "computation": it a process executing, a function during application, dynamic, "in motion."

Crucially, the system provides ways to convert a term between these two polarities: for instance, a function might be "suspended" to be "resumed" later, and the resulting thunk could be passed as an argument. Likewise, a static piece of data may be promoted into a do-nothing function that simply returns that value.

And it so happens it combines well with linearity.

All together, say it with me: Linear Call-By-Push-Value!

It turns out that linear types and CBPV very naturally and elegantly pair with one another: positive terms are precisely those which may be duplicated or ignored without a second-thought; negative terms are those which must be treated linearly.

Example: a function λ x. f x is negative, while its argument x is positive and the function term f is also negative, as is the entire expression f x.

Coeffects!

It so-happens that you can regard the linear logic I described above as a specialization of a more general idea called coeffects. I call them coeffects because

1. Believe it or not that's the term in the literature, and
2. The only other appropriate name I can honestly think of is "context" which is the most overloaded term in programming.

You can think of the linear logic described above as a coeffect where each bound term has a number attached to it defining how many times it may be used in a scope.

A more exotic example might be defining an enum of security roles that attach to every term the moment they are created, and rules for then performing security auditing statically at compile time.

A coeffect system is a set of rules for defining contextual data like that, along with the rules for the compiler to then enforce certain constraints.

Part of my current work is figuring out how this integrates with linear CBPV and thus how it should be represented syntactically.

Arbitrary-rank type and kind polymorphism.

I'm out of time for today!

• kinds: the "types of types". Basic types have kind *, and a function from type A : * to B : * is itself a third function type, A -> B : * -> * -> *.
• arbitrary rank types: I can write types like, eg ∀A B. (∀R. (A -> R) -> R) -> B. Future drafts will spell this out more.
• "kind polymorphism?" Yeah what, did you think * is the only kind?

That sounds like a tall order.

At the moment, besides the rules for shift and reset, this module competently implements a basic version of System F with let-polymorphism. Once the delimited control operators are settled, the next step will probably be adding surface syntax for the type language and implementing arbitrary-rank polymorphism, because in general my inference algorithm will need to be assisted just a little by the programmer sometimes with type annotations, and I don't have a type annotation syntax yet.

After that, finally, I'll likely be ready to tackle (co)effects.

Papers and posts I am cribbing from:

• https://www.microsoft.com/en-us/research/wp-content/uploads/2016/02/putting.pdf
• https://github.com/sdiehl/write-you-a-haskell/blob/master/chapter7/poly_constraints/src/Infer.hs
• https://cs-people.bu.edu/gaboardi/publication/GaboardiEtAlIicfp16.pdf
• others, stay tuned.