VictorTaelin

Truly Optimal Evaluation with Unordered Superpositions

In this post, I'll address two subjects:

1. How to solve HVM's quadratic slowdown compared to GHC in some cases

2. Why that is relevant to logic programming, unification, and program search

Optimal Evaluators aren't Optimal

VictorTaelin

The Interaction Calculus

The Interaction Calculus (IC) is term rewriting system inspired by the Lambda Calculus (λC), but with some major differences:

1. Vars are affine: they can only occur up to one time.
2. Vars are global: they can occur anywhere in the program.
3. There is a new core primitive: the superposition.

An IC term is defined by the following grammar:

EduardoRFS

Self Types + Sigma for Induction

This is a different technique that can be used for self types in more traditional MLTT settings, by doing induction through pairs instead of functions.

This idea was inspired by a comment from Ryan Brewer on the PLD Discord server. Paraphrasing it something, something inductive types positives so pairs.

edit: As pointed out by Ryan Brewer, I hallucinated half of the message ...

Self Typed Booleans