Skip to content

Instantly share code, notes, and snippets.

@henrytill
henrytill / tuple.agda
Created December 19, 2024 21:18 — forked from bobatkey/tuple.agda
"A Quick Introduction to Denotational Semantics using Agda" notes for talk given at TUPLE 2024 (https://typesig.comp-soc.com/tuple/)
{-# OPTIONS --postfix-projections #-}
module tuple where
------------------------------------------------------------------------------
--
@henrytill
henrytill / effects.py
Created December 15, 2024 08:22 — forked from ezyang/effects.py
from dataclasses import dataclass
from typing import Generator, TypeVar, Any, Callable, Optional, cast, NamedTuple, Dict, Type, Tuple, Generic
R = TypeVar("R")
Eff = Generator[Tuple[Any, ...], Any, R]
def handle_op(
g: Eff[R],
op: Tuple[Any, ...],
@henrytill
henrytill / code.ml
Created November 26, 2024 05:16 — forked from Drup/code.ml
GATDs gone mild
(** Supporting code for the "GADTs gone mild" talk *)
(** Compact Arrays
https://blogs.janestreet.com/why-gadts-matter-for-performance/
*)
module CompactArray = struct
type 'a t =
| Array of 'a array
| String of string
@henrytill
henrytill / runner.py
Created November 14, 2024 08:26 — forked from dpiponi/runner.py
Are these runners?
# Python 3
import collections
Write = collections.namedtuple("Write", ["written"])
def hello_world():
yield Write("Hello, world!")
yield Write("Hello, world!")
return 1
def identity(gen):
{-# LANGUAGE DeriveDataTypeable, GeneralizedNewtypeDeriving, TemplateHaskell, FlexibleInstances #-}
{-# OPTIONS_GHC -Wall -fno-warn-missing-signatures #-}
module QQAST where
import Control.Applicative
import Control.Exception
import Control.Monad.State
import Data.Data (Data)
import Data.Generics (extQ)
import Data.IORef
AccessModifierOffset: -8
AlignAfterOpenBracket: DontAlign
AlignConsecutiveMacros: true
AlignOperands: DontAlign
AlignTrailingComments: true
AllowAllArgumentsOnNextLine: true
AllowAllParametersOfDeclarationOnNextLine: false
AllowShortBlocksOnASingleLine: Empty
AllowShortCaseLabelsOnASingleLine: true
AllowShortEnumsOnASingleLine: true
@henrytill
henrytill / latency.markdown
Created May 23, 2017 21:07 — forked from hellerbarde/latency.markdown
Latency numbers every programmer should know

Latency numbers every programmer should know

L1 cache reference ......................... 0.5 ns
Branch mispredict ............................ 5 ns
L2 cache reference ........................... 7 ns
Mutex lock/unlock ........................... 25 ns
Main memory reference ...................... 100 ns             
Compress 1K bytes with Zippy ............. 3,000 ns  =   3 µs
Send 2K bytes over 1 Gbps network ....... 20,000 ns  =  20 µs
SSD random read ........................ 150,000 ns  = 150 µs

Read 1 MB sequentially from memory ..... 250,000 ns = 250 µs

@henrytill
henrytill / landins_knot.ml
Created March 28, 2017 20:53
Landin's Knot
(** "Landin's Knot" - implements recursion by backpatching *)
let landins_knot f =
let r = ref (fun x -> assert false) in
let fixedpoint = f (fun x -> !r x) in
r := fixedpoint;
fixedpoint
let factorial =
let g f x =
if x = 0 then
signature EQ =
sig
type t
val eq : t * t -> bool
end
signature SHOW =
sig
type t
val toString : t -> string