Skip to content

Instantly share code, notes, and snippets.

@Zafnok
Last active August 21, 2024 06:50
Show Gist options
  • Save Zafnok/31f490e4b6abcfa10623c0cc70ba065a to your computer and use it in GitHub Desktop.
Save Zafnok/31f490e4b6abcfa10623c0cc70ba065a to your computer and use it in GitHub Desktop.
Understanding how HVM works

Understanding how HVM works

Introduction

HVM takes the ideas of Interaction Combinators and combines it with the ideas of Type Systems, Functional Programming, and Compilers, to create an implementation of Yves Lafont's ideas into a highly parallelized runtime.

Resources

Start with the HVM whitepaper and HOW page of the repo, and if that makes sense to you, great! You're probably too smart for everything after. Otherwise, read into the next sections to develop the knowledge you're missing.

Intro to Lambda Calculus

Much of the Interaction Combinator papers are written with an audience presumed to be familiar with lambda calculus, so it is good to have some knowledge here before jumping into the Interaction Combinators section.

  • Programming Languages interactive book (good for lambda calculus, functional programming, and type systems!)

Afterwards, to bridge the gap between this and Interaction Combinators, it's recommended to read (at least) the first 3 chapters of The optimal implementation of functional programming languages.

Interaction Combinators

Start Here

HVM is highly based on Yves Lafont's ideas of Interaction Nets and Interaction Combinators.

Additional Resources

Easy to understand introduction to how interaction combinators can work to facilitate a compiler's inner workings: https://www.youtube.com/watch?v=GawiQQCn3bk

Advanced resources building upon the above concepts:

Type Systems

Functional Programming

Start Here

Additional Resources

Graph Reduction

Compilers

Uncategorized

@NoamDev
Copy link

NoamDev commented May 22, 2024

Haha, the optimal implementation of functional programming is mostly useful to understand how to translate a lambda calculus term into a sharing graph, which is basically an interaction net.

So I'd say it's the bridge between lambda calculus and interaction combinators.

Note 1: You only need the first three chapters at the most to understand sharing graphs.
Note 2: HVM actually implements a simplified version of that.

@QuentinWach
Copy link

This is quite nice. Thank you!

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment