Safe Haskell | None |
---|---|

Language | Haskell2010 |

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

- Believe it or not that's the term in the literature, and
- 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:

## Synopsis

- type TypeVar = Int
- data Type
- type Sigma = Type
- type Rho = Type
- type Tau = Type
- ty_int :: Rho
- ty_float :: Rho
- ty_bool :: Rho
- ty_bottom :: Rho
- ty_fun_sig :: [Type] -> Type -> Type
- data Frame = Frame {}
- frame_empty :: Frame
- frame_extend :: Frame -> (Symbol, Type) -> Frame
- frame_remove :: Frame -> Symbol -> Frame
- frame_extends :: Frame -> [(Symbol, Type)] -> Frame
- frame_lookup :: Symbol -> Frame -> Maybe Type
- frame_merge :: Frame -> Frame -> Frame
- frames_merge :: [Frame] -> Frame
- frame_singleton :: Symbol -> Type -> Frame
- frame_keys :: Frame -> [Symbol]
- frames_fromList :: [(Symbol, Type)] -> Frame
- frames_toList :: Frame -> [(Symbol, Type)]
- type Infer = ReaderT Frame (StateT InferState (Except String))
- data InferState = InferState {}
- default_infer_state :: InferState
- newtype Subst = Subst (Map TypeVar Rho)
- type Constraint = (Type, Type)
- type Unifier = (Subst, [Constraint])
- type Solve a = ExceptT String Identity a
- class Substitutable a where
- substitute :: Subst -> a -> a
- ftv :: a -> Set TypeVar

- run_infer :: Frame -> Infer a -> Either String a
- typecheck :: Frame -> CbpvExp -> Either String Type
- close_over :: Type -> Sigma
- normalize :: Sigma -> Sigma
- in_frame :: (Symbol, Type) -> Infer a -> Infer a
- in_frames :: [(Symbol, Type)] -> Infer a -> Infer a
- lookup_in_frame :: Symbol -> Infer (Rho, [Constraint])
- fresh :: Infer Tau
- instantiate :: Sigma -> Infer Rho
- generalize :: Frame -> Rho -> Sigma
- skolemize :: Sigma -> Infer ([TypeVar], Rho)
- infer :: CbpvExp -> Infer (Rho, [Constraint])
- subst_empty :: Subst
- compose :: Subst -> Subst -> Subst
- run_solve :: [Constraint] -> Either String Subst
- unify_many :: [Type] -> [Type] -> Solve Subst
- unifies :: Type -> Type -> Solve Subst
- solver :: Unifier -> Solve Subst
- bind :: TypeVar -> Type -> Solve Subst
- occurs_check :: Substitutable a => TypeVar -> a -> Bool
- solve_inference :: [Constraint] -> (Subst -> Infer a) -> Infer a
- prim_type :: Symbol -> Maybe Sigma
- data Graph node key = Graph {}
- graph_fromList :: Ord key => [(node, key, [key])] -> Graph node key
- vertex_labels :: Functor f => Graph b t -> f Vertex -> f b
- vertex_label :: Graph b t -> Vertex -> b
- topo :: Graph node key -> [node]
- make_dep_graph :: Map Symbol CbpvExp -> Graph (Symbol, CbpvExp) Symbol

# (basic) Type language

#### Instances

Eq Type Source # | |

Ord Type Source # | |

Show Type Source # | |

Substitutable Constraint Source # | |

Defined in Types substitute :: Subst -> Constraint -> Constraint Source # | |

Substitutable Type Source # | |

# Typing environment ("frame")

frame_empty :: Frame Source #

frames_merge :: [Frame] -> Frame Source #

frame_keys :: Frame -> [Symbol] Source #

# Inference monad

data InferState Source #

# Constraint solving monad

type Constraint = (Type, Type) Source #

type Unifier = (Subst, [Constraint]) Source #

class Substitutable a where Source #

#### Instances

Substitutable Constraint Source # | |

Defined in Types substitute :: Subst -> Constraint -> Constraint Source # | |

Substitutable Frame Source # | |

Substitutable Type Source # | |

Substitutable a => Substitutable [a] Source # | |

# Inference

close_over :: Type -> Sigma Source #

lookup_in_frame :: Symbol -> Infer (Rho, [Constraint]) Source #

skolemize :: Sigma -> Infer ([TypeVar], Rho) Source #

Deep skolemization. Returns the skolem variables and the skolemized ρ-type.

infer :: CbpvExp -> Infer (Rho, [Constraint]) Source #

Type inference rules for `CbpvExp`

ressions.
All functions have at least one (terminal) argument of type ⊥.

# Constraint solver

subst_empty :: Subst Source #

# Compose substitutions

# Run the constraint solver

# Unification solver

occurs_check :: Substitutable a => TypeVar -> a -> Bool Source #

solve_inference :: [Constraint] -> (Subst -> Infer a) -> Infer a Source #

# Graph implementation

graph_fromList :: Ord key => [(node, key, [key])] -> Graph node key Source #

vertex_label :: Graph b t -> Vertex -> b Source #