Thybault Soulthym

How to install

Install something that supports UserCSS, e.g. Stylus.
Click the "Raw" button next to xchan.user.css below.
Click "Install style" (or whatever it's called in your extension).

It will auto-update if I change the style here.

Report bugs as comments.

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.

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

The Interaction Calculus

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

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

An IC term is defined by the following grammar:

Truly Optimal Evaluation with Unordered Superpositions

In this post, I'll address two subjects:

How to solve HVM's quadratic slowdown compared to GHC in some cases
Why that is relevant to logic programming, unification, and program search

Optimal Evaluators aren't Optimal

HVM3's Optimal Atomic Linker (with Polarization)

Atomic linking is at the heart of HVM's implementation: it is what allows threads to collaborate towards massive parallelism. All major HVM versions started with a better atomic linker. From slow, buggy locks (HVM1), to AtomicCAS (HVM1.5), to AtomicSwap (HVM2), the algorithm became simpler and faster over the years.

On the initial HVM3 implementation, I noticed that one of the cases on the atomic linker never happened. After some reasoning, I now understand why, and

Fast Discrete Program Search 2

I am investigating how to use Bend (a parallel language) to accelerate Symbolic AI; in special, Discrete Program Search. Basically, think of it as an alternative to LLMs, GPTs, NNs, that is also capable of generating code, but by entirely different means. This kind of approach was never scaled with mass compute before - it wasn't possible! - but Bend changes this. So, my idea was to do it, and see where it goes.

Now, while I was implementing some candidate algorithms on Bend, I realized that, rather than mass parallelism, I could use an entirely different mechanism to speed things up: SUP Nodes. Basically, it is a feature that Bend inherited from its underlying model ("Interaction Combinators") that, in simple terms, allows us to combine multiple functions into a single superposed one, and apply them all to an argument "at the same time". In short, it allows us to call N functions at a fraction of the expected cost. Or, in simple terms: why parallelize when we can share?

A

	import itertools

	from dataclasses import dataclass


	type Name = int

	name = itertools.count()

	import itertools

	from dataclasses import dataclass


	type Name = int

	name = itertools.count()

	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.