Instantly share code, notes, and snippets.

• Sort options
Last active Mar 29, 2018
Derivation of Law of the Excluded Middle from call/cc
View LEM.idr
 %default total postulate callCC : ((a -> Void) -> a) -> a peirce : ((a -> b) -> a) -> a peirce f = callCC (f . (void .)) notExcludedMiddleImpliesExcludedMiddle : Not (Dec p) -> Dec p notExcludedMiddleImpliesExcludedMiddle notExcludedMiddle = No (notExcludedMiddle . Yes)
Last active Nov 28, 2017
Dependent sums subsume algebraic data types in presence of enums
View NatSum.idr
 %hide Nat %hide Nat.S %hide Nat.Z function : List Type -> Type -> Type function [] b = b function (a :: as) b = a -> function as b infixr 10 *->
Last active Nov 7, 2017
Optional Default Raw
View Default.swift
 extension Optional { subscript (default value: Wrapped) -> Wrapped { get { return self ?? value } set { self = newValue } } }
Created Oct 19, 2017
DynamicDict
View DynamicDict.py
 #!/usr/bin/python import string class DynamicDict: def __init__(self, function): self._function = function def __getitem__(self, key): return self._function(key)
Last active Oct 7, 2017
Idris Spiral
View Spiral.idr
 import Data.Vect Matrix : Nat -> Nat -> Type -> Type Matrix r c a = Vect r (Vect c a) unrotate : Matrix r c a -> Matrix c r a unrotate = reverse . transpose spiral : Matrix r c a -> Vect (r * c) a spiral {r=Z} [] = []
Last active Jul 18, 2017
Mean Monoid
View Mean.swift
 infix operator ☹: AdditionPrecedence struct Mean: ExpressibleByFloatLiteral, ExpressibleByIntegerLiteral { private let total: Float private let count: Int private init(total: Float, count: Int) { self.total = total self.count = count }
Last active May 7, 2017
Lambda Calculus w/o Parenthesis
View OpenClose.js
 //// Implementation OPEN = Symbol("open") CLOSE = Symbol("close") function run(program) { function applyUntilClose(continuation = x => x) { function iter(f) { if (f === OPEN) { return applyUntilClose(r => iter(r)) } else if (f == CLOSE) { throw new Error("Unexpected empty grouping")
Last active May 6, 2017