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 |
This is a guide to Vim Script development for Python developers. Sample code for the various expressions, statements, functions and programming constructs is shown in both Python and Vim Script. This is not intended to be a tutorial for developing Vim scripts. It is assumed that the reader is familiar with Python programming.
For an introduction to Vim Script development, refer to usr_41.txt, eval.txt and Learn Vimscript the Hard Way
For a guide similar to this one for JavaScript developers, refer to Vim Script for the JavaScripter
This guide only describes the programming constructs that are present in both Python and Vim. The constructs that are unique to Vim (e.g. autocommands, [key-mapping](https://vimhelp.org/map.txt.html#key-m
