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

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

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

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

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

# 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

# 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