Ben Lippmeier
University of New South Wales

Capabilities, Coeffects and Lax Truth
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~

The Disciple Core intermediate language is a version of System-F with region
and effect typing, used in the DDC research compiler. Disciple Core has had a
few long standing limitations, the foremost of which involves the mutability
annotations attached to data types. Values such as arrays can be mutable or
immutable, and the choice is tracked as a constraint at the type level. For
example, we write (Mutable r => Array r Int) for the type of a mutable array
of integers and (Const r => Array r Int) for the type of a constant
(immutable) array of integers. The 'r' is a region variable, and (Mutable r =>
...) and (Const r => ...) are type class constraints on that region variable.
Now, although the use of type class constraints allows us to write code that
is polymorphic over mutability, there is no safe way to destructively
initialize a mutable array and then treat it as immutable from then on. With
array programs implemented in Disciple (as well as in Haskell), this
programming pattern is ubiquitous, and typically implemented with a dodgy
coercion function like 'unsafeFreezeArray'.

In Disciple Core, although the use of mutability constraints like (Mutable r
=> ...) and (Const r => ...) makes it easy to abstract over the mutability of
some data type, the evidence-based encoding of type class constraints makes
them impossible to revoke. In the operational semantics, to satisfy a
constraint like (Mutable r => ...) we pass a "proof witness" of type (Mutable
r). However, a "proof witness" is typically understood to be to true forever
-- not just true while we initialize our array, then false afterwards. Without
some notion of linearity, once we've passed a proof witness to a function, we
can't be sure to get it back.

It turns out this problem can be solved by representing mutability as a
"capability" or "coeffect" instead of a "constraint". Happily, we can also
combine traditional effect information (Read, Write and Alloc), as well as
information about the distinctness (non-aliasing) of regions into the same
system. Whereas an "effect" describes an /action/ performed on the context of
evaluation, a "coeffect" describes a restriction on the /form/ of that
context. The new system is informed by Pfenning's work on computational logic
and lax truth, and embeds Filinski's monadic reification and reflection
operators, which I will also introduce.