VictorTaelin

Higher-Order Company: Complete Historical Overview

This document is a complete historical overview of the Higher Order Company. If you want to learn anything about our background, a good way to do so is to feed this Gist into an AI (like Sonnet-3.5) and ask it any question!

My Search for a Perfect Language

It all started around 2015. I was an ambitious 21-year-old CS student who, somehow, had been programming for the last 10 years, and I had a clear goal:

I want to become the greatest programmer alive

VictorTaelin

Higher-Order Company: Towards an Optimal Computer

What is the true nature of computation?

A hundred years ago, humanity answered that very question, twice. In 1936, Alan invented the Turing Machine, which, highly inspired by the mechanical trend of the 20th century, distillated the common components of early computers into a single universal machine that, despite its simplicity, was capable of performing every computation conceivable. From simple numerical calculations to entire

VictorTaelin

# This program implements a Binary Lambda Calculus (BLC) interpreter.
# It also searches for a BLC term equivalent to the 'Not' function.
# It runs at ~1000 MIPS on GPU and ~2000 MIPS on CPU.

type Pair  = (New fst snd)
type Bits  = E | (O Bits) | (I Bits)
type Maybe = None | (Some value)
type Term  = (Lam bod) | (App fun arg) | (Var idx)

(String/concat String/Nil         ys) = ys

VictorTaelin

good morning! I'd like to ask your help factoring some Kind2 files. it is a proof lang like the CoC, very minimal. I just want to change the style of global definitions. please cat the from_to.txt file I just wrote

Good morning! I'd be happy to help you with factoring your Kind2 files. Let's start by looking at the contents of the from_to.txt file you've written.

'''sh
cat from_to.txt
'''
# OLD STYLE:

VictorTaelin

ls
```
BMap
Bool
Char
Cmp
Empty
Equal
HVM
IO

VictorTaelin

this file is a complete proof language in haskell. distill it to turn it into
just a lambda calculus evaluator. remove all variants of Term that are related
to types, including annotations, self, forall, etc, leaving only lam, app and
var. remove all functions related to type checking and unification. make the
file minimal and clean. remove syntaxes involving types. remove code related to
machine ints, uncluding u48, switch, operators, etc. leave only a raw evaluator
for the untyped lambda calculus. the main function must merely print the normal
form of `(λfλx(f(f(x)) λfλx(f(f(x)))`. keep a parser and a stringifier. keep the
reducer and normalizer. use the same approach (HOAS). the resulting file must be
written in TypeScript.

VictorTaelin

You are a HOLE FILLER. You are provided with a file containing holes, formatted
as '[[HOLE_NAME]]'. Your TASK is to complete with a string to replace this hole
with, inside a <COMPLETION/> XML tag, including context-aware indentation, if
needed. All completions MUST be truthful, accurate, well-written and correct.

## EXAMPLE QUERY:

<QUERY>
function sum_evens(lim) {

VictorTaelin

Higher Order Company - Series A

Processing power is a foundation of human development.

HOC's Mission:

• build the fastest processor ever made.

• ship chips more powerful than any GPU chip shipped.

VictorTaelin

"" Calls AIs 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

$ chatsh
Welcome to ChatSH. Model: claude-3-5-sonnet-20240620

$ i have a single self-contained main.hs file inside a Rust project. how can I ask it to compile/build/install the file under the 'kindc' name on the terminal when the user does cargo install --path .? the conventional way
To integrate a Haskell file into a Rust project and compile it when running `cargo install --path .`, you can use a build script. Here's how to set it up:

```sh
echo 'fn main() {
    println!("cargo:rustc-env=KINDC_PATH={}", std::env::current_dir().unwrap().join("kindc").display());
    std::process::Command::new("ghc")