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 are always 64-bits wide with a Tag in the lower 4 bits, giving 16 different possible tags.
There are two tags for number terms, I60 and F60 for 60-bit integer and floats.
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 ...
The Interaction Calculus (IC) is term rewriting system inspired by the Lambda Calculus (λC), but with some major differences:
An IC term is defined by the following grammar:
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
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
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
In this article, I'll explain why implementing numbers with just algebraic datatypes is desirable. I'll then talk about common implementations of FFT (Fast Fourier Transform) and why they hide inherent inefficiencies. I'll then show how to implement integers and complex numbers with just algebraic datatypes, in a way that is extremely simple and elegant. I'll conclude by deriving a pure functional implementation of complex FFT with just datatypes, no floats.
Since v8.1 (May 2018), Vim has shipped with a built-in terminal. See https://vimhelp.org/terminal.txt.html or type :help terminal for more info.
Why use this? Mainly because it saves you jumping to a separate terminal window. You can also use Vim commands to manipulate a shell session and easily transfer clipboard content between the terminal and files you're working on.
| " Vim syntax file | |
| " Language: Todo | |
| " Maintainer: Huy Tran | |
| " Latest Revision: 14 June 2020 | |
| if exists("b:current_syntax") | |
| finish | |
| endif | |
| " Custom conceal |
