Skip to content

Instantly share code, notes, and snippets.

View VictorTaelin's full-sized avatar

Victor Taelin VictorTaelin

3.6k followers · 22 following
View GitHub Profile
@VictorTaelin
VictorTaelin / gist:7c7c8b4e8869de50e219f8821d5dc7bd
Created December 6, 2024 13:48
satoshi nakamoto é a cia, é literalmente a tradução em japonês. BTC foi criado pelo governo dos EUA pra pagar a dívida americana, e as moedas do satoshi vão formar a reserva americana em 20XX. a cada 4 anos eles dão pump pra convencer o mundo a entrar. é bem genial
@VictorTaelin
VictorTaelin / coc_superposer.hvml
Created November 30, 2024 17:38
HVM3 CoC Superposer / Enumerator - nice state
// Extending the CoC enumerator with more types (WIP)
data List {
#Nil
#Cons{head tail}
}
data Bits {
#O{pred}
#I{pred}
@VictorTaelin
VictorTaelin / algebra_tree.hvml
Created November 29, 2024 20:06
// Repeated Application
@rep(n f x) = ~ n !f !x {
0: x
p: !&0{f0 f1}=f (f0 @rep(p f1 x))
}
// Squared Application
@sqr(n f x) = ~ n !f !x {
0: x
p:!&0{p0 p1}=(+ p 1)
@VictorTaelin
VictorTaelin / superposed_lambda_calculus_evaluator.c
Last active November 29, 2024 15:51
A Superposed λ-Calculus Enumerator for Program Search
// This file is a mirror of:
// https://github.com/HigherOrderCO/HVM3/blob/main/book/lambda_enumerator_optimal.hvml
// An Optimal λ-Calculus Enumerator for Program Search
// ---------------------------------------------------
// This file shows a template on how to enumerate superposed terms in a
// higher-order language (here, the affine λ-Calculus) for proof search.
// Instead of generating the source syntax (like superposing all binary strings
// and parsing it as a binary λ-calculus), we create a superposition of all
// λ-terms *directly*, in a way that head constructors are emitted as soon as
@VictorTaelin
VictorTaelin / optimal_linear_context_passing.md
Last active December 1, 2024 22:32
Optimal Linear Context Passing

Optimal Linear Context Passing

In functional algorithms, it is common to pass a context down recursive calls. In Haskell-like languages, this is done like:

foo (App fun arg) ctx = App (foo fun ctx) (foo arg ctx)

This inoffensive-looking line can have harsh performance implications, specially

@VictorTaelin
VictorTaelin / itt_wip.hvml
Created November 26, 2024 01:39
ITT WIP
data List {
#Nil
#Cons{head tail}
}
data Pair {
#Pair{fst snd}
}
data Term {
@VictorTaelin
VictorTaelin / code.c
Created November 24, 2024 13:15
sharpobject's code
// Post: https://x.com/VictorTaelin/status/1854326873590792276
// Note: The atomics must be kept.
// Note: This will segfault on non-Apple devices due to upfront mallocs.
#include <stdint.h>
#include <stdatomic.h>
#include <stdlib.h>
#include <stdio.h>
#include <time.h>
#include <string.h>
@VictorTaelin
VictorTaelin / hvm_pitch_benchmarks.md
Last active November 28, 2024 14:56
HVM - Pitch Benchmarks

HVM3 - Pitch Benchmarks

Stress Test - HVM's Historic Progress

This is a stress test of the maximum possible throughput of the HVM. It is a very simple program that just loops in a "best case" scenario: i.e., maximum parallelism, and maximum compiled speed (since it compiles to a C loop). I like it because it highlights each major generational breakthrough:

@VictorTaelin
VictorTaelin / pseudo_metavar_factors.hvml
Created November 19, 2024 21:18
lambda encoded version
// Repeated Application
@rep(n f x) = ~ n {
0: x
p: !&0{f0 f1}=f (f0 @rep(p f1 x))
}
// Squared Application (with Bin)
@sqr(n f x) = ((n
λnp λf λx !&0{f0 f1}=f @sqr(np λk(f0 (f1 k)) x)
λnp λf λx !&0{fX f0}=f !&0{f1 f2}=fX @sqr(np λk(f0 (f1 k)) (f2 x))
@VictorTaelin
VictorTaelin / gist:38a273eef435f3c7e8862f27c55dc8fd
Created November 19, 2024 01:57
#1{#1{#1{#1{#1{#1{#1{#1{#1{#1{#1{#1{#1{#1{#1{#1{#1{#1{#1{#1{#1{#0{#0{#0{#0{#0{#0{#1{#0{#0{#2{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}) #1{#1{#0{#1{#1{#1{#1{#0{#0{#1{#0{#0{#1{#1{#1{#0{#1{#0{#1{#0{#1{#0{#1{#0{#1{#1{#1{#1{#1{#1{#0{#0{#0{#1{#0{#0{#0{#0{#0{#0{#0{#1{#0{#0{#0{#1{#1{#0{#0{#1{#0{#0{#1{#1{#0{#1{#1{#1{#0{#0{#1{#0{#0{#0{#2{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}})
λso ((so #1{#1{#1{#1{#1{#1{#1{#1{#1{#1{#1{#1{#1{#1{#1{#1{#1{#1{#1{#1{#1{#1{#1{#1{#1{#1{#1{#1{#1{#1{#1{#1{#1{#1{#1{#1{#1{#1{#1{#1{#1{#1{#1{#1{#1{#1{#1{#1{#1{#1{#1{#1{#1{#1{#1{#0{#0{#0{#0{#0{#0{#0{#1{#1{#2{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}) #1{#1{#0{#1{#1{#1{#1{#0{#0{#1{#0{#0{#1{#1{#1{#0{#1{#0{#1{#0{#1{#0{#1{#0{#1{#1{#1{#1{#1{#1{#0{#0{#0{#1{#0{#0{#0{#0{#0{#0{#0{#1{#0{#0{#0{#1{#1{#0{#0{#1{#0{#0{#1{#1{#0{#1{#1{#1{#0{#0{#1{#1{#1{#1{#2{}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}}})
λsp ((sp #1{#1{#1{#1{#1{#1{#1{#1{#1{#1{#1{#1{#1{#1{#1{#1{#1{#1{#1{#1{