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

jduey

Intro

I want a good FP language that runs on an HVM. So I'm taking the HVM3 implementation and modifying to have the features I want. Check out the HVM3 Repo for the details of how it works first.

Terms

Terms are always 64-bits wide with a Tag in the lower 4 bits, giving 16 different possible tags.

Numbers

There are two tags for number terms, I60 and F60 for 60-bit integer and floats.

EduardoRFS

Inductive t_eq {A} (x : A) : A -> Type :=
  | t_refl : t_eq x x.
Definition coe {A} {x y : A} (C : A -> Type) (p : t_eq x y) (H : C x) : C y :=
  match p in (t_eq _ z) return C z with | t_refl _ => H end.
Definition sym {A} {x y : A} (p : t_eq x y) : t_eq y x :=
  coe (fun z => t_eq z x) p (t_refl x).
Definition ap {A B x y} (f : A -> B) (H : t_eq x y) : t_eq (f x) (f y) :=
  coe (fun z => t_eq (f x) (f z)) H (t_refl (f x)).
Definition coe_inj {A} {x y : A} (C : A -> Type)
  (p : t_eq x y) {H1 H2} (H : t_eq (coe C p H1) (coe C p H2)) : t_eq H1 H2.

LeeeeT

import itertools

from dataclasses import dataclass


type Name = int

name = itertools.count()

LeeeeT

import itertools

from dataclasses import dataclass


type Name = int

name = itertools.count()