hallettj

// Run with: deno run lazy-promise.js

// See https://github.com/sindresorhus/p-lazy
import PLazy from "https://cdn.skypack.dev/p-lazy"

const a = new PLazy(resolve => {
  console.log("this code does not execute")
  resolve()
})

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

/** 
 * From the W3C working draft
 * http://www.w3.org/TR/IndexedDB
 */

// synchronously set properties on a database and retrieve a record

var db = indexedDB.open('books', 'Book store', false);
if (db.version !== '1.0') {
  var olddb = indexedDB.open('books', 'Book store');

hallettj

import styles from "part:@sanity/base/theme/forms/text-input-style"
import FormField from "part:@sanity/components/formfields/default"
import { withDocument } from "part:@sanity/form-builder"
import PatchEvent, { set, unset } from "part:@sanity/form-builder/patch-event"

import * as React from "react"
import Datetime from "react-datetime"

class DatetimeInputRaw extends React.Component {
  render() {

hallettj

/*
 * Concept for emulating higher-kinded types using Flow. Instead of passing
 * a type that has not been applied to parameters, this pattern passes
 * a type-level function that will map a parameter type to the desired
 * higher-kinded type applied to the given parameter.
 *
 * @flow
 */

// a higher-kinded type is represented indirectly via a type-level function from

hallettj

; A monad comprehension is a syntactic construct that translates
; synchronous-looking code into a callback-based implementation.  Monads
; are a very general abstraction - which means that monad comprehensions
; have more expressive power than other sync-to-async code
; transformations.

; Here is an example that uses jQuery's $.get method to fetch resources:

(def post-with-author (id)
  (for

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)
}

hallettj

!
! Invert number row
!
! This changes the behavior of keys in the number row, but does not
! affect the number pad.
!
keycode  10 = exclam 1 1 exclam
keycode  11 = at 2 2 at
keycode  12 = numbersign 3 3 numbersign
keycode  13 = dollar 4 4 dollar

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

# 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),