VictorTaelin

" Calls GPT-4 to fill holes in the current file,
" omitting collapsed folds to save prompt space

function! SaveVisibleLines(dest)
  let l:visibleLines = []
  let lnum = 1
  while lnum <= line('$')
    if foldclosed(lnum) == -1
      call add(l:visibleLines, getline(lnum))
      let lnum += 1

VictorTaelin

Can a simple functional sieve be fast? Optimizing Tromp's algorithm on HVM.

Today, John Tromp - creator of the Binary λ-Calculus, and one of the smartest functional wizards alive - ported his famous prime number generator (first published 12 years ago!) to HVM:

VictorTaelin

Y = λf (f (Y f))

(App n) = match n {
  0: λf λx x
  +: λf λx (App (/ n 2) λx(f (f x)) (match m = (% n 2) { 0: x; +: (f x) }))
}

B0 = λb0 λb1 b0
B1 = λb0 λb1 b1

VictorTaelin

Brief history of Type Theory - Human Timeline

All started around 1930, when mathematicians discovered the λ-calculus. It was Turing complete, so we wrote programs on it. Everything was great, until the first program crashed and the first paradox was found. The world was in flames, so humans looked for better.

Around 1940, the simple type was discovered. It solved everything: math was consistent again, programs stopped crashing. People were happy, until someone tried to make a linked list.

"Why do I need to duplicate my entire codebase?" - asked the angry developers.

At this point, half of humanity gave up on types. A duck religion was born. The other half looked for better.

VictorTaelin

// Interaction Calculus of Constructions
// =====================================

// Type
// ----

data Term
  = (Lam bod)
  | (App fun arg)
  | (Val bod)

VictorTaelin

// In this file, I explored the idea of computing the solution of:
// (3^x) % (2^s) == 1
// By using superpositions. The approach I used is to create an hand-optimized
// Mul3 function that seems to be efficient, and then creating a superposition
// of all Church Nats, as a perfect binary tree in the shape {{{0 1} {2 3}}...},
// and then applying that to `mul3` of `1`. As a result, we'll have a sup of all
// multiples of 3 (as binary strings). We can then call the function "Is1" on
// that sup. The result is a big superpositions of `0`, except for the places
// where we have a solution for the equation, which are `1`. This algorithm,
// despite all involved functions fusing, is exponential. After thinking about

VictorTaelin

// COMPUTATION RULES
// ===================================================
// APP | ((λx body) arg)
//  X  | ---------------------------------------------
// LAM | x ~ arg; body
// ===================================================
// APP | ({fst snd} arg)
//  X  | ---------------------------------------------
// SUP | dup #L{a,b} = arg; {(fst a) (snd b)}
// ===================================================

VictorTaelin

Solving SAT via interaction net superpositions

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

VictorTaelin

// THOUGHTS
//
// Consider FP: ∃f ∀a ∀b (f (mul a b) b) == b
//
// FP can be proven with a pair:
//
// - F: (a b: Nat) -> Nat
// - P: (a b: Nat) -> (F (mul a b) b) == b
//
// In the proof P, we pattern-match on 'a' and 'b'. Note that EVERY equality can

VictorTaelin

// A nano dependent type-checker featuring inductive types via self encodings.
// All computation rules are justified by interaction combinator semantics,
// resulting in major simplifications and improvements over old Kind-Core.
// Specifically, computable annotations (ANNs) and their counterpart (ANN
// binders) and a new self encoding based on equality (rather than dependent
// motives) greatly reduce code size. A more complete file, including
// superpositions (for optimal unification) is available on the
// Interaction-Type-Theory repository.
// Credits also to Franchu and T6 for insights.