VictorTaelin

data Uni : Set where
  U : Uni

data ℕ : Set where
  Z : ℕ
  S : ℕ → ℕ

data Vec (A : Set) : ℕ → Set where
  []   : ∀{n} → Vec A n
  _::_ : ∀{n} → A → Vec A n → Vec A (S n)

VictorTaelin

-- Let's serialize lists of uints as follows:
-- 
-- <Uint> ::= 0 | 1 <Uint>
-- <List> ::= 0 | 1 <Uint> <List>
-- 
-- For example, [1,2,3] serializes to '1 10 1 110 1 1110 0'.
-- 
-- Let f be a function that, given a number N, and a list of
-- numbers XS, sets the Nth number on XS to 0. For example:
-- - f(2, [0,1,2,3,4]) = [0,1,0,3,4]

VictorTaelin

import Prelude.hvml

// Types
// -----

// Type ::= ⊥ | [Type]
// - ⊥         = ⊥   = the Empty type
// - [⊥]       = ⊤   = the Unit type
// - [[⊥]]     = ℕ   = the Nat type
// - [[[⊥]]]   = ℕ*  = the List type

VictorTaelin

Suppose you wanted to represent an 1D space in a pure functional language, i.e., with trees. Suppose that you also needed to shift the whole space left and right. An efficient way to do it would be to use a perfect binary tree to store locations, and bit-strings to represent paths. For example:

(((0 1) (2 3)) ((4 5) (6 7)))

The tree above would represent a space with 8 locations. Then, the path:

[1,0,0]

VictorTaelin

import Control.Monad (when)
import Data.Char (chr, ord)
import Data.IORef
import Data.Word
import Debug.Trace
import System.IO.Unsafe (unsafePerformIO)
import Text.Parsec hiding (State)
import qualified Data.IntMap.Strict as IntMap
import qualified Data.Map as Map
import qualified Text.Parsec as Parsec

VictorTaelin

╭────────────────────────────────────────────╮
│ ✻ Welcome to Claude Code research preview! │
│                                            │
│   /help for help                           │
│                                            │
│   cwd: /Users/v/vic/dev/IC                 │
╰────────────────────────────────────────────╯

! cat InteractionCalculus.md

VictorTaelin

HOC - Thesis and Future Direction

At HOC, we believe Interaction Nets technology can lead to valuable market products. Two years ago, we raised $4 million to explore and validate this idea. During this period, we developed HVM and Bend—tools that significantly speed up functional and symbolic programs.

As we wrap up this research phase, we've identified the Symbolic AI market as our best opportunity. This market is rapidly growing, highly values computational efficiency, and aligns perfectly with HVM's strengths in

VictorTaelin

This is a debugging challenge.
Read the document below, and identify the bug.

---

# 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.

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

# The Interaction Calculus

The Interaction Calculus (IC) is term rewritting 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: