paf31

# empty and unit types

type (Void,,,) = lfix id
type (Unit,MakeUnit,) = Void -> Void
data Unique = MakeUnit id

# natural number type

type (Nat,MakeNat,UnmakeNat,FoldNat) = lfix const Unit + id

paf31

# Iterate a function n times
data Iterate = f => FoldNat <const id, g => $g . $f>

# Subtract a number by iterating the predecessor function
data Sub = Iterate Pred

# Test whether a natural number is zero or non-zero
data IsZero = <const True, const False> . UnNat

# Test whether or not two natural numbers are equal

paf31

> {-# LANGUAGE GADTs #-}
> {-# LANGUAGE PolyKinds #-}

> import Data.List

The following type definition will be lifted to the kind level, generating two constructors Z :: Nat and S :: Nat -> Nat

> data Nat = Z | S Nat

> _1 = S Z

paf31

In this post, I'd like to revisit Algorithm W, which I discussed when I wrote about Purity's typechecker.

Recalling the approach taken before, a term was typed by collecting constraints between unknown type variables by traversing the term in question, and then solving those constraints by substitution. This time I'd like to generalize the second part of the algorithm, to solve constraints over any term functor by substitution.

> {-# LANGUAGE EmptyDataDecls #-}
> {-# LANGUAGE RankNTypes #-}
> {-# LANGUAGE FlexibleInstances #-}

> module Solver where

paf31

In the following, I will write a polykinded version of the combinators fold and unfold, along with three examples: folds for regular datatypes 
(specialized to kind *), folds for nested datatypes (specialized to kind * -> *), and folds for mutually recursive data types (specialized to 
the product kind (*,*)). The approach should generalise easily enough to things such as types indexed by another kind (e.g. by specializing to 
kind Nat -> *, using the XDataKinds extension), or higher order nested datatypes (e.g. by specializing to kind (* -> *) -> (* -> *)).

The following will compile in the new GHC 7.4.1 release. We require the following GHC extensions:

> {-# LANGUAGE GADTs #-}
> {-# LANGUAGE PolyKinds #-}
> {-# LANGUAGE KindSignatures #-}

paf31

> {-# LANGUAGE MultiParamTypeClasses, FlexibleInstances #-}

> newtype MRec m f = MRec { runMRec :: m (f (MRec m f)) }

> mkMRec :: (Monad m) => f (MRec m f) -> MRec m f
> mkMRec = MRec . return

> class Distributive f g where
>   dist :: g (f a) -> f (g a)

paf31

As my first venture into the world of Haskell as a scripting language, I decided to write a small command line tool to automate the task of producing HTML suitable for Blogger posts from Literate Haskell files.

The tool can be invoked on the command line. It takes Literate Haskell on standard input, which it assumes is formatted correctly, and formats the code as HTML on standard output.

> module Main where

> import Data.List ( intercalate )

> isComment ('>':' ':_) = False
> isComment _ = True

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

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

> {-# 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