Skip to content

Instantly share code, notes, and snippets.

from talon import Context, Module, actions, speech_system
from talon import speech_system
from talon.lib import flac
from talon_init import TALON_HOME
import os
import struct
import wave
from datetime import datetime
rntz /
Last active Jun 17, 2020
Uniform handling of delimiters in talon
from talon import Module, Context, actions
delimiters = {x[0]: x[1] for x in "() [] {} <> “”".split()}
mod = Module()
class Actions:
def delimiter_close(delimiter: str) -> str:
"""Turns a delimiter into its corresponding closing delimiter."""
return delimiters.get(delimiter, delimiter)
# this will work with python 3, but probably not python 2
from functools import reduce
class BoolSemi:
zero = False
one = True
def plus(x, y):
return x or y
def times(x, y):
return x and y
rntz /
Last active Sep 9, 2019
A simple inlining pass in tagless-final style.
(* Inlining for the λ-calculus, implemented in tagless final style. This seems
* like it _must_ be related to Normalization By Evaluation (see eg [1,2]),
* since they both amount to β-reduction (plus η-expansion in extensional NBE),
* and the techniques have a similar "flavor", but I don't immediately see a
* formal connection.
* [1]
* [2]
rntz / hang.tex
Created Jul 2, 2019
a file that hangs pdflatex
View hang.tex
rntz / mystery.hs
Last active Jul 1, 2019
it is a mystery
View mystery.hs
-- I'm honestly slightly perturbed that this works.
-- Adapted from code in the `timeit` package.
-- Returns the time in seconds it took to evaluate the argument.
-- Of course, if the argument thunk was already forced, this will be small.
foo :: a -> IO Double
foo x = do
t1 <- getCPUTime
t2 <- seq x getCPUTime
return (fromIntegral (t2-t1) * 1e-12)
rntz / knuth-metafont-sample.tex
Created Mar 6, 2019
A sample from "The Concept of a Metafont", for font rendering comparison purposes
View knuth-metafont-sample.tex
%% This recreates the abstract from "The Concept of a Meta-Font" by Don Knuth,
%% Observe that "modern" Computer Modern as rendered in a PDF viewer(*) is much
%% lighter in weight (has much thinner strokes) than Computer Modern as printed
%% in 1982.
%% (*) In my case, evince 3.30.1 on Ubuntu Linux 18.10 on a 4K screen in 2019.
%% Different PDF viewers on different operating systems and different screens
%% may have different font rendering behavior - in particular, I have heard that
rntz / wut.c
Created Mar 1, 2019
floating point wat
View wut.c
#include <stdio.h>
#define MAGIC 99586915107664152904966939075856564224.0
int main() {
float x = MAGIC;
if (x == 1.0/(1.0/x)) printf("float division involutive.\n");
if (x != 1/(1/x)) printf("... but not with 1/(1/x).\n");
double y = MAGIC;
if (y == 1/(1/y)) printf("... but it is with doubles.\n");
return 0;
rntz / Runtime.hs
Created Feb 14, 2019
A seminaïve, mildly optimizing compiler from modal Datafun to Haskell, in OCaml.
View Runtime.hs
-- The Datafun runtime.
module Runtime where
import qualified Data.Set as Set
import Data.Set (Set)
class Eq a => Preord a where
(<:) :: a -> a -> Bool
class Preord a => Semilat a where
rntz / AxiomOfChoice.agda
Created Nov 5, 2018
The axiom of choice, interpreted with constructive & classical existentials.
View AxiomOfChoice.agda
-- The axiom of choice is equivalent to the following schema:
-- (∀(a ∈ A) ∃(b ∈ B) P(a,b))
-- implies
-- ∃(f ∈ A → B) ∀(a ∈ A) P(a, f(a))
-- Here I give two interpretations of this statement into Agda's constructive
-- type theory:
-- 1. Interpreting ∃ "constructively" as Σ. Values of Σ come with a witness
You can’t perform that action at this time.