Skip to content

Instantly share code, notes, and snippets.

View emekoi's full-sized avatar
📚

Emeka Nkurumeh emekoi

📚
View GitHub Profile
#!/usr/bin/sh
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
VictorTaelin / implementing_fft.md
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
Hirrolot / a-preface.md
Last active January 15, 2024 15:28
Higher-order polymorphic lambda calculus (Fω)
@Hirrolot
Hirrolot / cps-eval.ml
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
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 https://gist.github.com/Hirrolot/27e6b02a051df333811a23b97c375196
@Hirrolot
Hirrolot / CoC.ml
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
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
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"
https://dl.acm.org/doi/10.1145/3549822
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
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
mb64 / hm_with_kinds.ml
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