Instantly share code, notes, and snippets.

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]
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
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
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
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
View Reverse2.agda
{-# OPTIONS --postfix-projections #-}
open import Data.List using (List; []; _∷_; _++_)
open import Function using (flip)
open import Level
open import Relation.Binary using (Rel; _=[_]⇒_)
open import Relation.Binary.PropositionalEquality
module Reverse2 where
-- Some general abstract nonsense.
View Reverse.agda
open import Level renaming (zero to lzero; suc to lsuc)
open import Relation.Binary
open import Data.List
open import Data.List.Properties
open import Data.Unit hiding (_≤_)
open import Data.Product
open import Relation.Binary.PropositionalEquality
open import Data.Fin
open import Data.Nat ashiding (_≤_)
View makeAgdaDepGraph.sh
#!/bin/bash
set -e
echo "digraph {"
# Generate the node names.
find . -iname '*.agda' '!' -name '.*' |
sed -Ee 's,^\./,,;s,.agda$,,;s,/,.,g;s/.*/"&" [label="&"];/'
# Generate edges.
find . -iname '*.agda' '!' -name '.*' |
View bidirectional-structural.ml
(* A bidirectionally-typed λ-calculus looks like:
types A,B ∷= base | A → B
terms M ∷= E | λx.M
exprs E ∷= x | E M | (M : A)
This is an exploration of how to encode this in OCaml using _structural_
typing (polymorphic variants & equirecursive types), rather than _nominal_
typing. *)