sin-ack

How to install

1. Install something that supports UserCSS, e.g. Stylus.
2. Click the "Raw" button next to xchan.user.css below.
3. 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.

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()

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.

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

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

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:

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

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

VictorTaelin

Higher-Order Company: Towards an Optimal Computer

What is the true nature of computation?

A hundred years ago, humanity answered that very question, twice. In 1936, Alan invented the Turing Machine, which, highly inspired by the mechanical trend of the 20th century, distillated the common components of early computers into a single universal machine that, despite its simplicity, was capable of performing every computation conceivable. From simple numerical calculations to entire