Victor Taelin 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

Company:

HOC: Towards an Optimal Computer: why interaction paradigm can improve computers.
HOC: Can we build an optimal processor?: like above, but as a tweet.
HOC: Complete Historical Overview: the lore behind HOC's creation.

Theory:

Interaction Combinators - Y.Lafont 1997: a concurrent model of computation
Symmetric Interaction Combinators - Damiano Mazza 2009: a symmetric variant (used by HVM)
The Optimal Implementation of Functional Programming Languages - best book to learn
[BOHM](https://www.cambridge.org/core/services/aop-cambridge-core/content/

Note: This is an old post from back when I was trying to make sense of why inets are so fast for evaluating some λ-terms. It has some silly bits, I learned a lot since and could probably write a better article today, but I think this can still be insightful for these getting started, so I'll leave it here.

Yesterday, I reported the bizarre observation that certain functions can behave as if they had negative complexity. If you haven’t checked that article yet, it isn’t necessary, but you should, as it may blow your mind. In short, the λ-term f(bits) = copy(comp(inc,n,bits)), when given to optimal λ-calculus evaluator, is asymptotically faster than g(bits) = comp(inc,n,bits); i.e.,copy (a O(1) operation for a fixed size) behaves as if it had a O(1/n) complexity, causing the program to run faster by doing more things (!?).

That’s not the only bizarre complexity result I had when

Getters and Setters in Kind

The verbosity of nested fields

One of the most annoying aspects of pure functional programming is getting, setting and mutating deeply nested fields. In impure languages like JavaScript, this was never a problem. For example, consider the following object:

	// ./../HVM_old.kind//

	// NOTE: we're refactoring HVM to replace RTerm by a U64.
	// Your goal is to help us with this refactor.

	// Higher-order Virtual Machine
	// ============================

	// Core Types
	// ----------

	// Higher-order Virtual Machine
	// ============================

	// Core Types
	// ----------

	data HVM/Pol {
	#Pos
	#Neg
	}

	You're a code completion assistant.
	###
	-- Checker:
	--
	module Kind.Type where

	import qualified Data.IntMap.Strict as IM
	import qualified Data.Map.Strict as M

	import Debug.Trace

	You're a code completion assistant.

	###

	-- Type.hs:
	--
	module Kind.Type where

	import qualified Data.IntMap.Strict as IM
	import qualified Data.Map.Strict as M

	You're a code completion assistant.
	###
	--
	module Kind.Type where

	import qualified Data.IntMap.Strict as IM
	import qualified Data.Map.Strict as M

	import Debug.Trace
	import Data.Word (Word32)

	from: https://discord.com/channels/767397347218423858/767397347218423861/1296580936292499540


	Taelin — Today at 5:41 PM
	@AndrasKovacs i see you often treat lambda-case and case-of with different constructors. why? is there any obvious cons to just treating (λ{ ... } arg) as a case-of?
	Taelin — Today at 6:09 PM
	actually, also, consider this:

	Main
	: ∀(P: ∀(x: B/Bool) *) →