VictorTaelin

I: 1 5 9 3 0 0 A 8 1 E D F 6 5 4 8
O: 1 1 0 6 9 D A 4 5 E 0 5 3 F 8 8

I: 3 0 E C 6 1 F B 3 B 4 F 7 3 E 1
O: 3 3 6 7 E 4 F E 0 B 1 3 C F B 1

I: 8 4 7 C 1 8 7 1 F 0 1 B 9 8 7 6
O: 8 F 1 9 7 1 7 7 4 0 8 8 C B 1 6

I: 3 2 9 D A 2 C 2 D 3 F D 7 F B 6

VictorTaelin

THE PROBLEM

🌲 Invert a binary tree! 🌲

Except with 3 catches:

1. It must invert the keys ("bit-reversal permutation")
2. It must be a dependency-free, pure recursive function
3. It must have type Bit -> Tree -> Tree (i.e., a direct recursion with max 1 bit state)

VictorTaelin

Let an AB symbol be one of 4 possible variants:

  data AB : Set where
    A# : AB
    #A : AB
    B# : AB
    #B : AB

Let an AB Term be a list of AB symbols:

VictorTaelin

// Computes modular exponentiation by repeated ENUM rotation.
// 
// To compute `a ^ b % M`, we:
// - 1. Create a generic ENUM with M variants: enum T { v0, v1, v2, ... vM }
// - 2. Create a generic ENUM rotator: v0 -> v1, v1 -> v2, ... v1 -> v0
// - 3. Apply that rotator a^b times to v0; the result will be `a ^ b % M`!
// 
// To test this, we compute `(123 ^ 10) % 257`.
// This should require at least 792594609605189126649 function calls.
// A Macbook M3 would take about 25,000 years to *count* to that number.

VictorTaelin

<0>(HVM_MAIN_CALL)
----------------
<0>(HVM_MAIN_CALL)
----------------
<0>(Main)
----------------
<0>(Main)
----------------
<0>(Quote (APP (C2a) (C2b)) 0)
----------------

VictorTaelin

(Switch 0 z s) = z
(Switch n z s) = (s (- n 1))

//  (λx(bod) arg)
//  ------------- APP-LAM
//  x <- arg
//  bod
(APP (Lam bod) arg) =
  (bod arg)

VictorTaelin

Optimal Evaluation in 1 Minute (or 10 Minutes) (or 10 Years)

Short Version (1 minute)

A prerequisite to intelligence is the ability to find a program that explains a pattern. Programs are functions. To test a candidate program, we need to implement a "function evaluator". The problem is: all modern programming languages are sub-optimal "function evaluators", which, in the context of search, leads to massive slowdowns. To implement an optimal interpreter, we need to: 1. postpone the execution of expressions, to avoid wasted work, 2. cache the result of postponed expressions, to avoid duplicated work, 3. incrementally copy cached structures, to ensure 1 and 2 don't interfere. Haskell almost achieves this, but falls short on 3, because it is unable to incrementally copy lambdas. To solve this, we introduce the concept of a "superposition", which allows multiple versions of a term to exist simultaneously. This ensures that no work is ever wasted or duplicated, allowing us to optimally interpret (or com

VictorTaelin

Refactoring Kind's switch with ChatSH

(This is a readable version of my ChatSH session. For the full log, click here.)

Taelin: Hello. We're going to refactor an aspect of the implementation of the Kind language. Are you ready? Start by doing 'ls', then 'cat kind-lang.cabal' to get familiar with the repo.

ChatSH: Certainly! I'm ready to help you refactor an aspect of the Kind language implementation. Let's start by examining the repository structure and the contents of the Cabal file.

ls && echo "---" && cat kind-lang.cabal

VictorTaelin

SYSTEM:
You're a code completion assistant.

PROMPT:
-- Files for context:

-- Kind-Lang parser in Rust:

-- 
use crate::{*};

VictorTaelin

// tt.hs:

import Control.Monad (forM_)
import Data.Char (chr, ord)
import Debug.Trace
import Prelude hiding (LT, GT, EQ)
import System.Environment (getArgs)
import System.Exit (exitFailure)
import Text.Parsec ((<|>))
import qualified Data.Map.Strict as M