Skip to content

Instantly share code, notes, and snippets.

View record.py
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
ALWAYS_RECORD = True
@rntz
rntz / delimiters.py
Last active Jun 17, 2020
Uniform handling of delimiters in talon
View delimiters.py
from talon import Module, Context, actions
delimiters = {x[0]: x[1] for x in "() [] {} <> “”".split()}
mod = Module()
@mod.action_class
class Actions:
def delimiter_close(delimiter: str) -> str:
"""Turns a delimiter into its corresponding closing delimiter."""
return delimiters.get(delimiter, delimiter)
View fun-with-semirings.py
# 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
rntz / inlining-tagless-final.ml
Last active Sep 9, 2019
A simple inlining pass in tagless-final style.
View inlining-tagless-final.ml
(* 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] https://gist.github.com/rntz/f2f15f6cb4b8690c3599119225a57d33
* [2] http://homepages.inf.ed.ac.uk/slindley/nbe/nbe-cambridge2016.pdf
*)
@rntz
rntz / hang.tex
Created Jul 2, 2019
a file that hangs pdflatex
View hang.tex
\documentclass{article}
\RequirePackage{hyperref}
\RequirePackage{silence}
\begin{document}
\section{\ensuremath{\mathbf{foo}}}
\end{document}
@rntz
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
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,
%% https://s3-us-west-2.amazonaws.com/visiblelanguage/pdf/16.1/the-concept-of-a-meta-font.pdf
%%
%% 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
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
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
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.