hallettj

/*
 * The implementation
 */

function du(comprehension) {
    return function(/* args */) {
        var gen = comprehension.apply(null, arguments)
        return next();

        function next(v) {

hallettj

Keybase proof

I hereby claim:

• I am hallettj on github.
• I am hallettj (https://keybase.io/hallettj) on keybase.
• I have a public key whose fingerprint is A378 B079 9F05 93C0 B499 DD02 8FB4 E35F E86B 913B

To claim this, I am signing this object:

hallettj

module Logic

infixr 1 ==>

(==>) : Bool -> Bool -> Bool
False ==> _ = True
True  ==> x = x

data Exists : (A : Type) -> (P : A -> Bool) -> Type where
  exists : {A : Type} -> {P : A -> Bool} -> (a : A) -> so (P a) -> Exists A P

hallettj

# Category Theory proofs in Idris

Idris is a language with dependent types, and is similar to Agda.
What distinguishes Idris is that it is intended to be a general-purpose language first,
and a theorem prover second.
To that end it supports optional totality checking
and features to support writing DSLs:
type classes,
do notation,
monad comprehensions (i.e., a more general form of list comprehension),

hallettj

/* @flow */

type Tree<T> =
  | { type: "Node", value: T, left: Tree<T>, right: Tree<T> }
  | { type: "EmptyTree" }

function find<T>(p: (v: T) => boolean, t: Tree<T>): T | void {
  var l, v

  if (t.type === "Node") {

hallettj

Quickstart

Get a development environment and project scaffold set up in a jiffy.

Development environment

First install node and npm. There are instructions here:

hallettj

var execFile    = require('child_process').execFile;
var flow        = require('flow-bin');
var gulp        = require('gulp');
var path        = require('path')
var util        = require('gulp-util');
var webpack     = require('webpack');
var gulpWebpack = require('gulp-webpack');
var _           = require('lodash');

gulp.task('build', ['flow:check'], function() {

hallettj

This is a patch that adds Electron support to the Redux TodoMVC example app.

The original app is found at: https://github.com/rackt/redux/tree/master/examples/todomvc

After changes are applied, the app can be run in Electron with the commands:

npm install && node_modules/.bin/webpack && npm run electron

hallettj

import Data.List (groupBy, sort, sortOn, transpose)

type Vector = [Double]
type Matrix = [Vector]  -- two-dimensional matrix


{- Distance functions -}

-- type for a distance function
type Distance = Vector -> Vector -> Double

hallettj

/*
 * `match` is a helper function for writing pattern matches on types that are
 * implemented using Scott encoding.
 *
 * @flow
 */

export function match<A,B>(matcher: A): (match: (matcher: A) => B) => B {
  return match => match(matcher)
}