Skip to content

Instantly share code, notes, and snippets.

@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))))]
View Zub.agda
record Preorder (A : Set) : Set1 where
field rel : (x y : A) Set
field ident : {x} rel x x
field compo : {x y z} rel x y rel y z rel x z
open Preorder public
-- "indiscrete if P has a least element, discrete otherwise"
data Zub {A} (P : Preorder A) : A → A → Set where
refl : {x} Zub P x x
@rntz
rntz / fringe.rkt
Last active Sep 12, 2018
That "fringe" function, reimplemented in Racket
View fringe.rkt
#lang racket
;; The fringe of a tree is all the things in it that aren't conses - including
;; '(). For example, the fringe of '((1 . 2) ((3)) 4) is '(1 2 3 () () 4 ()).
(define example '((1 . 2) ((3)) 4))
(define example-fringe '(1 2 3 () () 4 ()))
;; (fringe tree) computes a "stream" of the fringe of a tree. In this case, a
;; "stream" is a function that takes a function getter and calls (getter elem
;; rest), where elem is the next element in the stream and rest is a stream of
@rntz
rntz / TerminationFail.agda
Created Sep 6, 2018
some agda that obviously terminates, but not to agda
View TerminationFail.agda
postulate
A : Set
_≤_ : A A Set
: A
_∨_ : A A A
id : {a} a ≤ a
_•_ : {a b c} a ≤ b b ≤ c a ≤ c
data Tree : Set where
empty : Tree
You can’t perform that action at this time.