puffnfresh

This is my short-ish tutorial on how to implement closures in
a simple functional language: Foo.

First, some boilerplate.

> {-# LANGUAGE DeriveFunctor, TypeFamilies #-}
> import Control.Applicative
> import Control.Monad.Gen
> import Control.Monad.Writer
> import Data.Functor.Foldable

puffnfresh

with import <nixpkgs> { };

let
  img = "bzImage";
  hyperkitCommand = ''
    ${hyperkit}/bin/hyperkit \
      -A \
      -m 512M \
      -s 0,hostbridge \
      -s 1,lpc \

puffnfresh

open import Data.Container using (Container; Shape; Position)
open import Data.Container.Combinator using (id)
open import Data.Container.FreeMonad using (_⋆C_)
open import Data.Sum using (inj₂)
open import Data.Unit.Base using (tt)
open import Level using (lift; _⊔_)

record M {a b} (A : Set a) (B : A → Set b) : Set (a ⊔ b) where
  coinductive
  field

puffnfresh

open import Coinduction using (♯_)
open import Data.Container using (ν)
open import Data.Container.Combinator using (id)
open import Data.Container.FreeMonad using (_⋆C_)
open import Data.M using (inf)
open import Data.Sum using (inj₂)
open import Data.Unit.Base using (tt)
open import Level using (lift)

Partiality : ∀ {α} → Set α → Set α

puffnfresh

open import Coinduction using (∞; ♯_)
open import Data.Product using (_×_)
open import Data.Sum using (_⊎_; inj₁)
open import Data.Unit.Base using (⊤; tt)
open import Data.Empty using (⊥)
open import Level using (suc; _⊔_; zero)

data F {α} : Set (suc α) where
  K   : Set α → F
  _+_ : F {α} → F {α} → F

puffnfresh

Here's a list of recent papers and articles which made a big impact to how I program:

• Notions of Computation as Monoids demonstrates Arrows are exactly Strong profunctors with a Category
• Stackless Scala With Free Monads how to trampoline by encoding a free monad under strict evaluation
• Stack Safety for Free gives generic recursive monadic code while using constant stack size under strict evaluation

puffnfresh

open import Data.Bool
open import Data.Fin
open import Data.Integer hiding (suc)
open import Data.List
open import Data.Nat
open import Data.Nat.DivMod
open import Data.Unit
open import Relation.Nullary

isZero : ℕ -> Bool

puffnfresh

Keybase proof

I hereby claim:

• I am puffnfresh on github.
• I am puffnfresh (https://keybase.io/puffnfresh) on keybase.
• I have a public key ASBZdZZFWx_a_z-Koc1OeP__z_GZxSHsKA-Rmf1f99ABsgo

To claim this, I am signing this object:

puffnfresh

declare namespace F {
    class Either<A, B> {
        private constructor();

        // Hack to make A and B covariant.
        private a: A;
        private b: B;

        static Left<A, B>(a: A): Either<A, B>;
        static Right<A, B>(b: B): Either<A, B>;

puffnfresh

class Wat<A> {
    constructor(a: A) {}
}

var z: Wat<number> = new Wat<string>("Hello");

// The above compiles. Wat.