CodaFi’s gists

CodaFi / AlgorithmW.swift

Last active July 14, 2025 16:31

A Swift Playground containing Martin Grabmüller's "Algorithm W Step-by-Step"

	/// Playground - noun: a place where people can play
	/// I am the very model of a modern Judgement General

	//: # Algorithm W

	//: In this playground we develop a complete implementation of the classic
	//: algorithm W for Hindley-Milner polymorphic type inference in Swift.

	//: ## Introduction

CodaFi / keybase.md

Created January 31, 2017 20:25

I hereby claim:

To claim this, I am signing this object:

CodaFi / FileCheck.swift

Last active February 3, 2018 23:09

A self-contained port of FileCheck to Swift

	/// Playground - noun: a place where people can play
	/// FileCheck yourself before you wreck yourself

	import Foundation
	#if os(Linux)
	import Glibc

	typealias NSRegularExpression = RegularExpression
	#else
	import Darwin

CodaFi / Basics.agda

Created October 30, 2016 05:50

	module Basics where

	open import Agda.Primitive using (Level)

	data ℕ : Set where
	zero : ℕ
	suc : ℕ → ℕ

	data Zero : Set where

CodaFi / Contents.swift

Created July 6, 2016 05:57

	// A translation http://kcsrk.info/ocaml/types/2016/06/30/behavioural-types/
	// of a translation https://hal.archives-ouvertes.fr/hal-01216310

	enum Violation : ErrorProtocol {
	case Linearity
	}

	/* sealed */
	protocol Operation { associatedtype T }
	//{

CodaFi / Kanren.swift

Created April 8, 2016 15:55

An implementation of μKanren in Swift (http://webyrd.net/scheme-2013/papers/HemannMuKanren2013.pdf)

	//: Playground - noun: a place where people can play
	//: http://webyrd.net/scheme-2013/papers/HemannMuKanren2013.pdf

	typealias Var = Int
	typealias Subst = [(Var, Term)]
	typealias State = (Subst, Int)
	typealias Goal = State -> Stream

	indirect enum Stream {
	case Nil, Cons(State, Stream), Lazy(() -> Stream)

CodaFi / Ornaments.agda

Created April 1, 2016 01:27

	-- Ornaments explore the transformation of "simple" datatypes by introducing
	-- an indexing structure that allows decorating the type with extra information.
	module Ornaments where

	open import Agda.Primitive

	record ⊤ : Set where
	constructor ⋆

	data _≡_ ..{ℓ} {A : Set ℓ} (x : A) : A → Set ℓ where

CodaFi / Object.h

Created January 19, 2016 04:54

The headers of the oldest version of the Objective-C runtime I could still find. Extracted from an old NeXT image.

	#ident "@(#) Object.h, Rev 2.10, 96/08/02"
	//
	// Copyright (c) 1995-1996, Sun Microsystems, Inc.
	// portions (c) Copyright 1988, 1989 NeXT, Inc.
	// All rights reserved.

	#ifndef _OBJC_OBJECT_H_
	#define _OBJC_OBJECT_H_

	#import <objc/objc.h>

CodaFi / ABT.swift

Last active February 3, 2018 22:57

Abstract Binding Trees ~(http://www.cs.cmu.edu/~rjsimmon/15312-s14/hws/hw1update2-handout.pdf) in Swift

	/// An operator is given by a list of arities, where each element indicates the number of
	/// variables bound by the operator at that position and the length of the list determines the
	/// number of variables the operator accepts. The full generalization of arity is called
	/// the operator's "valence".
	///
	/// For example, if I have a little calculator language with let-bindings, its operators
	/// would look like this:
	///
	///
	/// enum CalcOps : Operator {

CodaFi / Trees.swift

Last active June 3, 2019 03:47

A small propositional logic proof tree generator and prover.

	indirect enum Formula : CustomStringConvertible {
	case Var(String)
	case Or(Formula, Formula)
	case And(Formula, Formula)
	case Imply(Formula, Formula)
	case BiImply(Formula, Formula)
	case Negate(Formula)

	var description : String {
	switch self {

Robert Widmann CodaFi