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 / 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.