paf31

const int SPEAKER1 = 13;
const int SPEAKER2 = 11;

const int PITCH[8] = { 727, 647, 611, 545, 485, 458, 408, 363 };

char PITCH1[61] = { 
   'E', 'E', 'F', 'G', 'G', 'F', 'E', 'D', 'C', 'C', 'D', 'E', 'E', 'D', 'D', 
   'E', 'E', 'F', 'G', 'G', 'F', 'E', 'D', 'C', 'C', 'D', 'E', 'D', 'C', 'C',
   'D', 'E', 'C', 'D', 'E', 'F', 'E', 'C', 'D', 'E', 'F', 'E', 'D', 'C', 'D', 'G',
   'E', 'E', 'F', 'G', 'G', 'F', 'E', 'D', 'C', 'C', 'D', 'E', 'D', 'C', 'C'

paf31

{-# LANGUAGE Rank2Types, DeriveFunctor #-}

newtype Rec f = In { out :: f (Rec f) }

fold :: (Functor f, Functor g) => (forall a b a' b'. (a -> b -> x) -> (a -> b' -> x) -> (a' -> b -> x) -> a' -> b' -> f a -> g b-> x) -> Rec f -> Rec g -> x
fold phi = let f = \x y -> (phi f f f) x y (out x) (out y) in f

data List a t = Nil | Cons a t deriving (Show, Functor)

nil = In Nil

paf31

{-# LANGUAGE Rank2Types #-}

import Control.Monad (join)

data Free f a = Return a | Bind (f (Free f a))

instance (Functor f) => Monad (Free f) where
  return = Return
  (Return x) >>= f = f x
  (Bind xs) >>= f = Bind $ fmap (>>= f) xs

paf31

> {-# LANGUAGE DataKinds, GADTs, TypeFamilies, TypeOperators #-}

> import Prelude hiding (Functor, succ)

> infixl 1 :+
> infixl 2 :.

> data Type = Unit | (:+) Type Type | (:.) Type Type | Rec Functor

> infixl 1 :++

paf31

I've recently been thinking about how to generialize an efficient version of the snoc operation on lists.

Specifically, one can represent lists by indentifying them with their fold functions:

> -- data List a = List { fold :: forall r. r -> (a -> r -> r) -> r }

This representation, as in the case of difference lists, admits efficient versions of the cons operation at both ends of the list:

> -- cons :: a -> List a -> List a
> -- cons a l = List (\r0 acc -> acc a $ fold l r0 acc)

paf31

module Main where

import Data.Maybe
import Control.Monad
import Control.Monad.Trans
import System.Time
import System.Directory
import Happstack.Server
import qualified Text.Blaze.Html4.Strict as H
import qualified Text.Blaze.Html4.Strict.Attributes as A

paf31

> {-# LANGUAGE RankNTypes, DataKinds, GADTs, TypeOperators, FlexibleInstances #-}

> module Elim where

Last time, I wrote a little bit about encoding linear lambda terms in Haskell using promoted datatypes to represent the set of variables 

appearing in a term. This time I'd like to look at an algorithm for abstraction elimination for linear lambda terms.

I covered abstraction elimination once before when I spoke about adding lambdas to the Purity compiler. Abstraction elimination is the 

paf31

> {-# LANGUAGE DataKinds, TypeOperators, GADTs #-}

> data Stack xs where
>   Empty :: Stack '[]
>   Push :: x -> Stack xs -> Stack (x ': xs)

> pop :: Stack (x ': xs) -> Stack xs
> pop (Push _ s) = s

> peek :: Stack (x ': xs) -> x

paf31

Consider the following recursive function definitions. What do they have in common?

> -- equals 0 0 = True
> -- equals 0 n = False
> -- equals n 0 = False
> -- equals n m = equals (n - 1) (n - 2)

> -- unify (Unknown n) (Unknown m) = [(n, m)]
> -- unify (Arrow x y) (Arrow w z) = (unify x w) ++ (unify y z)
> -- unify _ _ = error "Cannot unify"

paf31

In this post, I'd like to look at the problem of encoding linear lambda terms in Haskell. Specifically, I'd like to look at how to restrict the class of expressible lambda terms to only allow variables to be applied exactly once.

For example, the combinator K x y = x should be disallowed because the variable y is never used, and the combinator S x y z = x z (y z) should be disallowed because the variable z is used more than once.

The combinators S and K form a basis for the set of unrestricted lambda terms, so one should ask, is there anything interesting left after they are removed? Indeed, one can find a useful basis for the class of linear lambda terms, which we will express in Haskell below.

> {-# LANGUAGE RankNTypes, DataKinds, GADTs, TypeOperators #-}

> module Lin where