Skip to content

Instantly share code, notes, and snippets.

View emekoi's full-sized avatar

Emeka Nkurumeh emekoi

View GitHub Profile
set -e
files="$(fd -e .el .)"
sd -s '^\\\\\\\\begin{code}' '^[\t ]*\```\s*haskell.*?' $files
sd -s '\\\\begin{code}' '```\s*haskell.*?' $files
sd -s '\\begin{code}' '```\s*haskell.*?' $files
sd -s '^\\\\\\\\end{code}' '^[\t ]*\```' $files
VictorTaelin /
Last active May 24, 2024 23:39
Implementing complex numbers and FFT with just datatypes (no floats)

Implementing complex numbers and FFT with just datatypes (no floats)

In this article, I'll explain why implementing numbers with just algebraic datatypes is desirable. I'll then talk about common implementations of FFT (Fast Fourier Transform) and why they hide inherent inefficiencies. I'll then show how to implement integers and complex numbers with just algebraic datatypes, in a way that is extremely simple and elegant. I'll conclude by deriving a pure functional implementation of complex FFT with just datatypes, no floats.

Hirrolot /
Last active January 15, 2024 15:28
Higher-order polymorphic lambda calculus (Fω)
Hirrolot /
Created March 24, 2023 10:34
A simple CPS evaluation as in "Compiling with Continuations", Andrew W. Appel
type cps_var =
(* Taken from the lambda term during CPS conversion. *)
| CLamVar of string
(* Generated uniquely during CPS conversion. *)
| CGenVar of int
type cps_term =
| CFix of (cps_var * cps_var list * cps_term) list * cps_term
| CAppl of cps_var * cps_var list
| CRecord of cps_var list * binder
AndrasKovacs / HOASOnly.hs
Last active February 27, 2024 15:50
HOAS-only lambda calculus
{-# language BlockArguments, LambdaCase, Strict, UnicodeSyntax #-}
Minimal dependent lambda caluclus with:
- HOAS-only representation
- Lossless printing
- Bidirectional checking
- Efficient evaluation & conversion checking
Inspired by
Hirrolot /
Last active May 24, 2024 23:57
How to implement dependent types in 80 lines of code
type term =
| Lam of (term -> term)
| Pi of term * (term -> term)
| Appl of term * term
| Ann of term * term
| FreeVar of int
| Star
| Box
let unfurl lvl f = f (FreeVar lvl)
gelisam / MutuCheckInfer.hs
Last active November 4, 2023 03:44
A recursion scheme for mutually-recursive types
-- Defining a custom recursion scheme to manipulate two mutually-recursive
-- types, in the context of a toy bidirectional type checker.
{-# LANGUAGE DerivingStrategies, GeneralizedNewtypeDeriving, ScopedTypeVariables #-}
module Main where
import Test.DocTest
import Control.Monad (when)
import Data.Bifunctor (Bifunctor(bimap))
import Data.Bifoldable (Bifoldable(bifoldMap), bitraverse_)
AndrasKovacs / NbESharedQuote.hs
Last active May 10, 2024 07:34
NbE with implicit sharing in quotation
At ICFP 2022 I attended a talk given by Tomasz Drab, about this paper:
"A simple and efficient implementation of strong call by need by an abstract machine"
This is right up my alley since I've implemented strong call-by-need evaluation
quite a few times (without ever doing more formal analysis of it) and I'm also
interested in performance improvements. Such evaluation is required in
conversion checking in dependently typed languages.
karthick18 / vmsplice.c
Created April 13, 2022 19:09
Use splice with vmsplice to move user space buffers to output file
* An example using vmsplice to move user space buffers to pipe before using
* splice syscall which avoids copying to/from user space buffers to kernel space
* and uses the pipe buffers allocated in kernel space as an intermediate to directly xfer from one file to another
* gcc -o splice splice.c -g
#define _GNU_SOURCE
#include <stdio.h>
mb64 /
Created February 13, 2022 00:16
Hindley-Milner type checking with higher-kinded types, in OCaml
type name = string
module AST = struct
type ty =
| TFun of ty * ty
| TNamed of string
| TApp of ty * ty
type exp =
| Annot of exp * ty