Skip to content

Instantly share code, notes, and snippets.

Michael Arntzenius rntz

Block or report user

Report or block rntz

Hide content and notifications from this user.

Learn more about blocking users

Contact Support about this user’s behavior.

Learn more about reporting abuse

Report abuse
View GitHub Profile
@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
@rntz
rntz / quasicontracts.rkt
Created Oct 14, 2018
Hijacking quasiquotation to construct contracts
View quasicontracts.rkt
#lang racket
(require syntax/parse/define)
;; Let's define a quasiquoter that generates contracts.
(define-for-syntax quasiquote-contract
(syntax-parser
#:literals (unquote unquote-splicing)
[(_ name:id) #''name]
[(_ ,x:expr) #'x]
@rntz
rntz / bidir-nbe.ml
Last active Oct 7, 2018
Bidirectional typechecking and normalisation by evaluation for a simply-typed lambda calculus, all in one
View bidir-nbe.ml
(* Based on http://homepages.inf.ed.ac.uk/slindley/nbe/nbe-cambridge2016.pdf *)
exception TypeError
type tp = Base | Fn of tp * tp
let subtype (x: tp) (y: tp): bool = x = y
type sym = {name: string; id: int}
let next_id = ref 0
let nextId() = let x = !next_id in next_id := x + 1; x
@rntz
rntz / bidir-nbe.rkt
Last active Oct 7, 2018
Bidirectional typechecking and normalisation by evaluation for a simply-typed lambda calculus, all in one
View bidir-nbe.rkt
;; Based on http://homepages.inf.ed.ac.uk/slindley/nbe/nbe-cambridge2016.pdf
#lang racket
;; Checks that a term has a type and returns its denotation.
(define (check cx tp-expect term)
(match term
[`(lambda (,x) ,body)
(match-define `(-> ,A ,B) tp-expect)
(define thunk (check (hash-set cx x A) B body))
(lambda (env) (lambda (v) (thunk (hash-set env x v))))]
You can’t perform that action at this time.