Yazalde Filimone yazaldefilimone

Higher-Order Company: Complete Historical Overview

This document is a complete historical overview of the Higher Order Company. If you want to learn anything about our background, a good way to do so is to feed this Gist into an AI (like Sonnet-3.5) and ask it any question!

My Search for a Perfect Language

It all started around 2015. I was an ambitious 21-year-old CS student who, somehow, had been programming for the last 10 years, and I had a clear goal:

I want to become the greatest programmer alive

Can a simple functional sieve be fast? Optimizing Tromp's algorithm on HVM.

Today, John Tromp - creator of the Binary λ-Calculus, and one of the smartest functional wizards alive - ported his famous prime number generator (first published 12 years ago!) to HVM:

Solving SAT via interaction net superpositions

I've recently been amazed, if not mind-blown, by how a very simple, "one-line" SAT solver on Interaction Nets can outperform brute-force by orders of magnitude by exploiting "superposed booleans" and optimal evaluation of λ-expressions. In this brief note, I'll provide some background for you to understand how this works, and then I'll present a simple code you can run in your own computer to observe and replicate this effect. Note this is a new observation, so I know little about how this algorithm behaves asymptotically, but I find it quite

ported from https://hub.darcs.net/dolio/agda-share/browse/PHOASNorm.agda

JS

const Lam = bod => lam => app => vah => lam(bod);
const App = fun => arg => lam => app => vah => app(fun)(arg);
const Var = exp => lam => app => vah => vah(exp);

const nz = v => nz => ns => nz(v);

Compilers, programming languages and virtual machines

	{-# OPTIONS --copatterns #-}

	module UntypedLambda where

	open import Size
	open import Function

	mutual

	data Delay (A : Set) (i : Size) : Set where

	// Interaction Calculus of Constructions
	// =====================================

	// Type
	// ----

	data Term
	= (Lam bod)
	\| (App fun arg)
	\| (Val bod)

	import { useEffect, useState } from "react";

	const defaultEvents = [
	"mousemove",
	"mousedown",
	"touchstart",
	"keydown",
	"wheel",
	"resize",
	];

	// A nano dependent type-checker featuring inductive types via self encodings.
	// All computation rules are justified by interaction combinator semantics,
	// resulting in major simplifications and improvements over old Kind-Core.
	// Specifically, computable annotations (ANNs) and their counterpart (ANN
	// binders) and a new self encoding based on equality (rather than dependent
	// motives) greatly reduce code size. A more complete file, including
	// superpositions (for optimal unification) is available on the
	// Interaction-Type-Theory repository.
	// Credits also to Franchu and T6 for insights.

	import * as React from 'react';

	const useIsFirstRender = (): boolean => {
	const isFirst = React.useRef(true);

	if (isFirst.current) {
	isFirst.current = false;

	return true;
	} else {