Skip to content

Instantly share code, notes, and snippets.

View VictorTaelin's full-sized avatar

Victor Taelin VictorTaelin

View GitHub Profile
@VictorTaelin
VictorTaelin / gist:632067b6849c619ef0408347150a3a5e
Created August 6, 2025 00:37
parse loop debugging prompt: gpt-oss vs kimi k2 vs qwen3 coder vs Qwen3 235B A22B Thinking 2507
-- TASK: create a Parser for Kind7.
-- - don't be inventive, just use a simple approach that is guaranteed to work
-- - keep it simple and idiomatic
-- - include nice error messages
-- On the 'parseApp parser:
-- - support (f x y z) as an alias to (((f x) y) z)
-- - do so by parsing '(', then terms until you hit a ')', then foldl to build the App
-- Note on operators:
# Bend prelude
# ------------
type Maybe<A: Set>:
case @None:
case @Some:
value: A
type Result<F: Set, D: Set>:
case @Done:

I'm thinking on how to add funext to a Type Theory in the spirit of that answer

my understanding is that OTT, as presented, introduces computation rules for a built-in identity / propositional equality type. for example, in OTT, we'd have something like:

Eq (A,B) (a0,b0) (a1,b1)

reduce to

(Eq A a0 a1 , Eq B b0 b1)

@VictorTaelin
VictorTaelin / wow.txt
Created June 19, 2025 04:16
OpenAI Codex / o3 implemented the datatype syntax sugar on Bend2
╭──────────────────────────────────────────────────────────────╮
│ ● OpenAI Codex (research preview) v0.1.2505172129 │
╰──────────────────────────────────────────────────────────────╯
╭──────────────────────────────────────────────────────────────╮
│ localhost session: b966636e1ecf42a59c8fef1192074e17 │
│ ↳ workdir: ~/vic/dev/bend │
│ ↳ model: o3 │
│ ↳ provider: openai │
│ ↳ approval: suggest │
╰──────────────────────────────────────────────────────────────╯
@VictorTaelin
VictorTaelin / flattener.hs
Last active June 15, 2025 23:17
flattener
module Main where
import Data.List (nub)
-- Pattern Matching Flattener Algorithm
-- ====================================
--
-- This algorithm converts pattern matching expressions with multiple
-- scrutinees into nested case trees with single scrutinees.
--
@VictorTaelin
VictorTaelin / question.txt
Created May 6, 2025 21:55
Insanely hard prompt - question and answer
-- OldCheck:
-- (omitted)
# The Interaction Calculus
The [Interaction Calculus](https://github.com/VictorTaelin/Interaction-Calculus)
is a minimal term rewriting system inspired by the Lambda Calculus (λC), but
with some key differences:
1. Vars are affine: they can only occur up to one time.
2. Vars are global: they can occur anywhere in the program.
-- OldCheck:
-- (omitted)
# The Interaction Calculus
The [Interaction Calculus](https://github.com/VictorTaelin/Interaction-Calculus)
is a minimal term rewriting system inspired by the Lambda Calculus (λC), but
with some key differences:
1. Vars are affine: they can only occur up to one time.
2. Vars are global: they can occur anywhere in the program.
@VictorTaelin
VictorTaelin / sort.agda
Created March 30, 2025 19:07
terminating sort in agda
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
VictorTaelin / vibe_test_prompt.hs
Created March 27, 2025 03:01
Vibe Test Prompt
-- 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
VictorTaelin / kolmolang.hvml
Last active March 24, 2025 11:29
Kolmogorov Complexity minimizing language
import Prelude.hvml
// Types
// -----
// Type ::= ⊥ | [Type]
// - ⊥ = ⊥ = the Empty type
// - [⊥] = ⊤ = the Unit type
// - [[⊥]] = ℕ = the Nat type
// - [[[⊥]]] = ℕ* = the List type