CodaFi

/// 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 proof

I hereby claim:

• I am codafi on github.
• I am codafi (https://keybase.io/codafi) on keybase.
• I have a public key ASDZRsz1ccwqgRCrEtq-yb_P-6dJRTzOEDdtGS69ZbYfsAo

To claim this, I am signing this object:

CodaFi

/// 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

module Basics where

open import Agda.Primitive using (Level)

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

data Zero : Set where

CodaFi

// 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

//: 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 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

#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

/// 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

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 {