Skip to content

Instantly share code, notes, and snippets.

Robert Widmann CodaFi

Block or report user

Report or block CodaFi

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
CodaFi / MBE.swift
Created Jul 8, 2018
Macro-by-Example: Deriving Syntactic Transformations from their Specifications, Re-Typeset
View MBE.swift
//: Foreword
//: This playground is the culmination of a week of digging around
//: for the oldest papers I could find about (Lisp) macros and their evolution.
//: I found this paper particularly enlightening as it is the place where Scheme
//: and Rust-style "Macro-by-Example" macros first came into their own. In
//: addition, this paper discusses the implementation challenges faced by
//: previous macro systems and Kohlbecker's first go at MBEs.
//: I have re-typeset this paper because [the one hosted by IU](
View SevenInOne.swift
//: Playground - noun: a place where people can play
//: Roots of Unity Often Lie
indirect enum BTree {
case empty
case branch(BTree, BTree)
func encode(_ t: (BTree, BTree, BTree, BTree, BTree, BTree, BTree)) -> BTree {
switch t {
CodaFi / Nub.agda
Created Apr 20, 2018
Agda wrote nub for me (with some prodding)
View Nub.agda
module Untitled where
open import Data.Nat
open import Data.Nat.Properties
open import Data.Char hiding (_≟_)
open import Data.Bool hiding (_≟_)
open import Data.List
open import Data.Unit hiding (_≟_)
open import Data.Empty
open import Relation.Nullary
View turing-fake.swift
struct State0 {}; struct State1 {}; struct FinalState {} /*States*/
struct Symbol {}; struct Blank {} /*Symbols*/
struct Left {}; struct Right {} /*Directions*/
struct EndOfTape {} /*End of Tape*/
struct Transition<StartState, StartHead, EndState, EndHead, Direction> {
static func transitionOne() -> Transition<State0, Blank, State1, Symbol, Left> { fatalError() }
static func transitionTwo() -> Transition<State1, Blank, State0, Symbol, Right> { fatalError() }
static func transitionThree<State>() -> Transition<State, Symbol, FinalState, Symbol, Left> { fatalError() }
View AlgaSketch.swift
struct G<A> {
let vertices : [A]
let edges: [(A, A)]
let gex = G(vertices: [1, 2, 3], edges: [(1, 2), (2, 3)])
let gbad = G(vertices: [1], edges: [(1, 2)])
View MonadsAsModules.agda
module MonadsAsModules where
import Agda.Primitive using (Level)
id : {k}{X : Set k} X X
id x = x
const : {a b} {A : Set a} {B : Set b} A B A
const x _ = x
CodaFi / update-swift-dev
Last active Feb 13, 2018 — forked from ddunbar/update-swift-dev
This is the script I currently use on OS X to get a working "swift-dev.xctoolchain" out of a built Swift. It isn't designed to work for anyone but me, but it should be easy to adapt. I always run this after every build, and then use `TOOLCHAINS=swift-dev swift build` (etc) to use the development compiler.
View update-swift-dev
set -e
if [ -z "${SWIFTPM_CONFIGURATION}" ]; then
if [ -z "${CONFIGURATION}" ]; then
View 3SAT.swift
// swift -Xfrontend -debug-constraints
infix operator ^&&^ : LogicalConjunctionPrecedence
infix operator ^||^ : LogicalConjunctionPrecedence
struct T{}
struct F{}
func λ(_ f : (T) -> ()) {
CodaFi / Subtyping.swift
Created Mar 31, 2017
"Efficient Subtyping" (if you ignore all the inefficiencies).
View Subtyping.swift
indirect enum Type : CustomStringConvertible {
case TyVar(String)
case Top
case Bottom
case Arrow(Type, Type)
case Pair(Type, Type)
case Rec(String, Type)
func subst(_ s : String, _ t : Type) -> Type {
switch self {

Explicit Toll-Free Conversions


To continue removing further implicit conversions from the language, implicit toll-free bridging should be deprecated in Swift 3 and removed in Swift 4.0.

You can’t perform that action at this time.