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
@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

signature EQ =
sig
type t
val eq : t * t -> bool
end
signature SHOW =
sig
type t
val toString : t -> string
@henrytill
henrytill / exists.ml
Created March 26, 2017 16:23 — forked from jonsterling/exists.ml
existential quantifier in OCaml
(* an abstract signature for instantiations of the existential quantifier *)
module type EXISTS =
sig
(* the predicate *)
type 'a phi
(* the existential type *)
type t
(* the introduction rule *)
@henrytill
henrytill / recur.ml
Created March 25, 2017 19:47 — forked from tel/recur.ml
Not as bad as I feared
module type Functor = sig
type 'a t
val map : ('a -> 'b) -> ('a t -> 'b t)
end
module Mu (F : Functor) : sig
type t = { mu : t F.t }
val cata : ('a F.t -> 'a) -> (t -> 'a)
end = struct
@henrytill
henrytill / FAlg.ml
Created March 25, 2017 19:47 — forked from tel/FAlg.ml
More F-algebra things in OCaml
module type Functor = sig
type 'a t
val map : ('a -> 'b) -> ('a t -> 'b t)
end
module Iso = struct
type ('a, 'b) t = { fwd : 'a -> 'b; bck : 'b -> 'a }
let fwd i = i.fwd
let bck i = i.bck