blog.poucet.org Rotating Header Image

Haskell

Levenshtein Distance in Haskell

Seeing how lately the levenschtein distance is so popular, I thought I’d add a haskell version to the mix.

The code below is pretty self-explanatory, using the typical memoization pattern. I do wonder, however, what would happen if somehow GHC supported lazily-resizable arrays. Perhaps then you could do this on infinite lists and only ask the levenschtein distance up to a certain index.

module Lev whereimport Data.Array

levenshtein :: (Eq a) => [a] -> [a] -> Integer
levenshtein xs ys = arr ! (lenx, leny)
  where arr :: (Array (Int, Int) Integer)
        arr                   = array ((0,0), (lenx, leny))  [((ix, iy), worker ix iy) |
                                                              ix <- [0..lenx], iy <- [0..leny] ]
        lenx                  = length xs
        leny                  = length ys
        arrx                  = listArray (1, lenx) xs
        arry                  = listArray (1, leny) ys
        worker 0      iy      = fromIntegral iy
        worker ix     0       = fromIntegral ix
        worker ix     iy      = minimum [1 + arr ! (ix-1, iy), 1 + arr ! (ix, iy-1),
                                         cost ix iy + arr ! (ix-1, iy-1)]
        cost ix iy            = if (arrx ! ix) == (arry ! iy) then 0 else 1

Continued Fractions in Haskell

Using the Fractional Type that we introduced in a previous blogpost, we build a module for continued fractions in Haskell in this entry. As usual, the code is licensed BSD and is authored by myself. Nonetheless, I would like to thank Cale Gibbard for his invaluable input for the debugging of certain parts of it. Since this is quite a big blog post, I’ve decided to post it already partially finished, as I have a short attention span but wanted to get the code out there. So be warned that this is WIP, and is not finished yet. I will remove this notice when it is.

Originally, I read about continued fractions on “Arithmetic with Continued Fractions” by Dominus. Intrigued by them, I digged a bit further, but sadly was unable to find much more than the original paper translated in plain html with rather old and hard to read notation. What intrigued me about this notation is that one could get real numbers to an unlimited precision in a lazy language like Haskell. After all, using laziness, we only compute what we really need. So once we have some continued fraction, it is easy to imagine only getting N parts of it to get a value within some eps of the final value. This is where this module originally originated. Another interesting aspect of continued fractions is that they can be used to represent both rational and irrational numbers to any precision. Additionally, a nice feature of them is that all rational numbers have a finite representation with them.

After having completely implemented the continued fractions, I noticed that it was actually really hard to deal with irrational numbers. The current implementation of continued fractions simply does not support them. That being said, I think it is a simple extension of this implementation that can support them rather well. I will focus on this and try to write it down here after detailing the implementation as it is.

Continued Fraction Representations

There are various representations for continued fractions, as can be seen in the list below. All of them allow for representing any number, however some of them are more convenient than others.

  • a0 + ‎b0‎a1 + ‎b1‎a2 + ‎b2
  • a0 + 1‎a1 + 1‎a2 + 1

The second representation is often named regular continued fractions. The advantage of the prior representation is that it’s easier to represent certain irrational numbers such as pi:

  • π4 = ‎1‏‎1+‎1‏‎3+‎4‏‎5+‎9‏‎7+‎16‏/…
  • pi4 : a0 = 0, b0 = 1, ∀ i > 0.(ai, bi) = (2·i−1,i2)

That being said, the advantage of the latter representation is that all numbers are uniquely representable (well not quite exactly, but we’ll look at that later).

Continued Fractions Arithmetic

TODO

Continued Fractions Implementation

Using the custom definition of Fraction from one of my previous blogposts we can now go ahead and define the actual code for continued fractions. First we start with the header of the file, with the license, some specific GHC flags and some imports:

> {-# LANGUAGE BangPatterns #-}
> ------------------------------------------------------------------------------
> -- CF.hs - Continued Fractions
> --
> -- Authors: Christophe Poucet -
> -- License: BSD
> -- Created: 01/22/2008 06:59:59 AM CET, last modified 01/25/2008
> --
> -- Copyright 2008 © Christophe Poucet. All Rights Reserved.
> -- Thanks to Cale Gibbard for his invaluable input
> ------------------------------------------------------------------------------
> module CF where -- (CF, approximate, approximations) where
> import Fraction
> import Data.List
> import Data.Ratio

The first important data type, obviously, is the continued fraction, which is a list of digits. Additionally, we want two structures to store the transformation ‘matrices’ for the arithmetic of one or two continued fractions. These are T4 and T8 respectively.

> --
> -- * Data definitions
> --
> newtype CF a = CF [a]
> deriving (Eq, Show)
>
> data T4 a = T4 !a !a !a !a
> deriving (Eq)
>
> data T8 a = T8 !a !a !a !a !a !a !a !a
> deriving (Eq)

Simple function to turn a continued fraction into an exact value. The code from this comes from “Functional Pearl – Enumerating Rationals” by Jeremy Gibbons et al. It is much more efficient than the original solution I had.

> -- 
> -- | exact : Calculates the exact value of a continued fraction
> --
> exact :: (Integral a, Fractional b) => CF a -> b
> exact (CF ps) = a/b
> where (a, b) = foldr op (1,0) . map fromIntegral $ ps
> op m (n,d) = (m*n+d, n)

Checks whether a continued fraction is infinity. Notice that the for the case that any digits are negative, the logic is cruder. Then again, we do not allow negative digits, and this is simply a remnant from some deep debugging.

> --
> -- | isInfinity : Checks whether a CF is infinity
> --
> isInfinity (CF xs) = check xs || (any (<0) $ drop 1 xs)
> where check [] = True
> check (_:0:xs) = check xs
> check _ = False

TODO

> ------------------------------------------------------------------------------
> -- * Core Functions
> ------------------------------------------------------------------------------
> ------------------------------------------------------------------------------
> --
> -- | morph : allows for scaling and addition of normal numbers to a CF
> --
> -- a + bx
> -- (T4 a b c d) : z = --------
> -- c + dx
> --
> ------------------------------------------------------------------------------
> morph :: (Integral a) => T4 a -> CF a -> CF a
> morph (T4 a b c d) (CF xs) = CF $ worker a b c d xs
> where worker !a !b !c !d xs =
> --------------------------------------------------------------------
> case () of
> _ | infinity -> []
> ------------------------------------------------------------------
> _ | fixed -> z:worker a' b' c' d' xs
> where a' = c
> b' = d
> c' = (a-c*z)
> d' = (b-d*z)
> ------------------------------------------------------------------
> _ | not ended -> worker a' b' c' d' (tail xs)
> where a' = b
> b' = (a+b*x)
> c' = d
> d' = (c+d*x)
> ------------------------------------------------------------------
> _ | otherwise -> worker a' b' c' d' xs
> where a' = b
> b' = b
> c' = d
> d' = d
> --------------------------------------------------------------------
> where qs@[q1, q2] = case () of
> _ | ended -> [a :~: c, b :~: d]
> _ | otherwise -> [(a + b*x ) :~: (c + d*x) ,
> (a + b*(x+1)) :~: (c + d*(x+1)) ]
> infinity = c == 0 && d == 0
> ended = null xs
> all_equal = equal . filter (not . isNan) $ qs
> -- Note, lossy-fraction's equality is -NOT- transitive
> fixed = not infinity && not vanishing && all_equal
> -- Vanishing: We do not cross 0 in our quadrant, subject to 'equal qs'
> vanishing = not ended && signum c /= (signum d * signum x)
> x = head xs
> z = toIntegral . head . filter (not . isNan) $ qs

TODO

> ------------------------------------------------------------------------------
> --
> -- | arithmetic : allows for arithmetic operators between two CFs'
> --
> -- a + bx + cy + dxy
> -- (T8 a b c d e f g h) : z = -------------------
> -- e + fx + gy + hxy
> --
> ------------------------------------------------------------------------------
> arithmetic :: (Integral a) => T8 a -> CF a -> CF a -> CF a
> arithmetic (T8 a b c d e f g h) (CF xs) (CF ys) = CF $ worker a b c d e f g h xs ys
> where worker :: (Integral a) =>
> a -> a -> a -> a ->
> a -> a -> a -> a ->
> [a] -> [a] -> [a]
> worker !a !b !c !d !e !f !g !h xs ys =
> --------------------------------------------------------------------
> case () of
> _ | infinity -> []
> ------------------------------------------------------------------
> -- We have an integer value that is the same for the entire quadrant
> _ | fixed -> z:worker a' b' c' d' e' f' g' h' xs ys
> where {
> a' = e ; b' = f ; c' = g ; d' = h;
> e' = (a-e*z); f' = (b-f*z); g' = (c-g*z); h' = (d-h*z)
> }
> ------------------------------------------------------------------
> -- x /= inf || y /= inf
> _ | not ended ->
> --------------------------------------------------------------
> case () of
> ------------------------------------------------------------
> -- X shows largest variance
> _ | choose_x ->
> case () of
> ------------------------------------------------------
> -- x == inf, change variance along x to 0
> _ | ended_x -> worker a' b' c' d' e' f' g' h' xs ys
> where {
> a' = 0 ; b' = b ; c' = 0 ; d' = d;
> e' = 0 ; f' = f ; g' = 0 ; h' = h
> }
> ------------------------------------------------------
> -- x /= inf
> _ | otherwise -> worker a' b' c' d' e' f' g' h' (tail xs) ys
> where {
> a' = b ; b' = (a+b*x); c' = d ; d' = (c+d*x);
> e' = f ; f' = (e+f*x); g' = h ; h' = (g+h*x)
> }
> ------------------------------------------------------------
> -- Y shows largest variance
> _ | otherwise ->
> case () of
> ------------------------------------------------------
> -- y == inf, change variance along y to 0
> _ | ended_y -> worker a' b' c' d' e' f' g' h' xs ys
> where {
> a' = 0 ; b' = 0 ; c' = c ; d' = d;
> e' = 0 ; f' = 0 ; g' = g ; h' = h
> }
> ------------------------------------------------------
> -- y /= inf
> _ | otherwise -> worker a' b' c' d' e' f' g' h' xs (tail ys)
> where {
> a' = c ; b' = d ; c' = (a+c*y); d' = (b+d*y);
> e' = g ; f' = h ; g' = (e+g*y); h' = (f+h*y)
> }
> --------------------------------------------------------------
> where choose_x | numNans >= 3 = not ended_x
> | isNan d_x && isNan d_y = d_xy_x > d_xy_y
> | isNan d_x && isNan d_xy_y = d_xy_x > d_y
> | isNan d_xy_x && isNan d_y = d_x > d_xy_y
> | isNan d_xy_x && isNan d_xy_y = d_x > d_y
> | numNans >= 2 = not ended_x
> | isNan d_x = d_xy_x > max d_y d_xy_y
> | isNan d_xy_x = d_x > max d_y d_xy_y
> | isNan d_y = max d_x d_xy_x > d_xy_y
> | isNan d_xy_y = max d_x d_xy_x > d_y
> | otherwise = max d_x d_xy_x > max d_y d_xy_y
> ds = [d_x, d_y, d_xy_x, d_xy_y]
> numNans = length . filter isNan $ ds
> d_x = abs $ q2 - q1
> d_y = abs $ q3 - q1
> d_xy_x = abs $ q4 - q3
> d_xy_y = abs $ q4 - q2
> ------------------------------------------------------------------
> -- x == inf && y == inf
> _ | otherwise -> worker a' b' c' d' e' f' g' h' xs ys
> where {
> a' = d ; b' = d ; c' = d ; d' = d;
> e' = h ; f' = h ; g' = h ; h' = h
> }
> --------------------------------------------------------------------
> where qs@[q1, q2, q3, q4] = case () of
> _ | ended -> [a :~: e, b :~: f, c :~: g, d :~: h]
> _ | ended_x -> [(a + c*y ) :~: (e + g*y ) ,
> (b + d*y ) :~: (f + h*y ) ,
> (a + c*(y+1)) :~: (e + g*(y+1)) ,
> (b + d*(y+1)) :~: (f + h*(y+1)) ]
> _ | ended_y -> [(a + b*x ) :~: (e + f*x ) ,
> (a + b*(x+1)) :~: (e + f*(x+1)) ,
> (c + d*x ) :~: (g + h*x ) ,
> (c + d*(x+1)) :~: (g + h*(x+1)) ]
> _ | otherwise -> [(a + b*x + c*y + d*x*y ) :~: (e + f*x + g*y + h*x*y ) ,
> (a + b*(x+1) + c*y + d*(x+1)*y ) :~: (e + f*(x+1) + g*y + h*(x+1)*y ) ,
> (a + b*x + c*(y+1) + d*x*(y+1) ) :~: (e + f*x + g*(y+1) + h*x*(y+1) ) ,
> (a + b*(x+1) + c*(y+1) + d*(x+1)*(y+1)) :~: (e + f*(x+1) + g*(y+1) + h*(x+1)*(y+1)) ]
>
> infinity = e == 0 && f == 0 && g == 0 && h == 0
> all_equal = equal . filter (not . isNan) $ qs
> -- Note, lossy-fraction's equality is -NOT- transitive
> ended_x = null xs
> ended_y = null ys
> ended = ended_x && ended_y
> -- Note, lossy-fraction's equality is -NOT- transitive
> fixed = not infinity && not vanishing && all_equal
> -- Vanishing: We do not cross 0 in our quadrant, subject to 'equal qs'
> vanishing = case () of
> --------------------------------------------------------------
> _ | not ended_x && not ended_y ->
> -- -e - f*x
> -- y(x) = ----------
> -- g + h*x
> --
> within y (-e - f*x) (g + h*x) ||
> withinS y (-e - f*(x+1)) (g + h*(x+1)) ||
> -- -e - g*y
> -- x(y) = ----------
> -- f + h*y
> --
> within x (-e - g*y) (f + h*y) ||
> withinS x (-e - g*(y+1)) (f + h*(y+1))
> --------------------------------------------------------------
> _ | not ended_x ->
> signum g /= (signum h * signum x)
> --------------------------------------------------------------
> _ | not ended_y ->
> signum f /= (signum h * signum y)
> --------------------------------------------------------------
> _ | otherwise ->
> False
> x = head xs
> y = head ys
> z = toIntegral . head . filter (not . isNan) $ qs
> --
> -- ** Comparison
> --
> instance (Ord a) => Ord (CF a) where
> compare (CF ps) (CF qs) = comp ps qs
> where comp [] [] = EQ
> comp (x:xs) [] = LT
> comp [] (y:ys) = GT
> comp (x:xs) (y:ys) = if c == EQ then comp ys xs else c
> where c = compare x y

> --
> -- ** Standard Arithmetic operators
> --
> instance (Integral a) => Num (CF a) where
> x + y = arithmetic (T8 0 1 1 0 1 0 0 0) x y
> x * y = arithmetic (T8 0 0 0 1 1 0 0 0) x y
> x - y = arithmetic (T8 0 1 (-1) 0 1 0 0 0) x y
> negate (CF ps) = CF $ worker ps
> where worker [] = []
> worker [a] = [-a]
> worker [a,2] = [-a-1,2]
> worker (a:1:b:r) = (-a-1):(b+1):r
> worker (a:b:r) = (-a-1):1:(b-1):r
> abs (CF []) = CF []
> abs cx@(CF (x:xs)) | x < 0 = negate cx
> | otherwise = cx
> signum (CF []) = fromInteger 1
> signum (CF (x:xs)) | x < 0 = fromInteger (-1)
> | x == 0 &&
> null xs = fromInteger 0
> | otherwise = fromInteger 1
> fromInteger x = CF [fromInteger x]
> --
> -- ** Enumeration
> --
> instance (Integral a) => Enum (CF a) where
> succ x = morph (T4 1 1 1 0) x
> pred x = morph (T4 (-1) 1 1 0) x
> toEnum x = fromInteger . toInteger $ x
> fromEnum (CF []) = error "fromEnum: The CF is infinity"
> fromEnum (CF (x:xs)) = fromIntegral x
> enumFrom x = iterate succ x
> enumFromThen x y = iterate ((y-x)+) x
> enumFromTo x y = takeWhile (<= y) $ enumFrom x
> enumFromThenTo x y z = takeWhile p (enumFromThen x y)
> where p | y >= x = (<= z)
> | otherwise = (>= z)
> --
> -- ** Fractional
> --
> instance (Integral a) => Fractional (CF a) where
> x / y = arithmetic (T8 0 1 0 0 0 0 1 0) x y
> recip x = morph (T4 1 0 0 1) x
> fromRational x = CF $ loop (numerator x) (denominator x)
> where loop n b | b == 0 = []
> | otherwise = let (d,m) = n `divMod` b in fromIntegral d:loop b m
> instance (Integral a) => Real (CF a) where
> toRational cf = exact cf

> ------------------------------------------------------------------------------
> -- * Helper functions
> ------------------------------------------------------------------------------
> none :: (a -> Bool) -> [a] -> Bool
> none f l = not . any f $ l
> {-# INLINE none #-}
>
> equal :: (Eq a) => [a] -> Bool
> equal (x:xs) = all (x ==) xs
> equal _ = True
> {-# INLINE equal #-}
>
> -- within z a b == z <= a/b < z+1
> -- Could be rephrased as a CF function: a :~: b == z :~: 1
> within z a b | b == 0 = a == 0
> | b > 0 = b*z <= a && a < b*(z+1)
> | otherwise = b*z >= a && a > b*(z+1)
> {-# INLINE within #-}
>
> -- withinS z a b == z < a/b < z+1
> -- Could be rephrased as a CF function: a :~: b == z :~: 1 && a /= z*b
> withinS z a b | b == 0 = a == 0
> | b > 0 = b*z < a && a < b*(z+1)
> | otherwise = b*z > a && a > b*(z+1)
> {-# INLINE withinS #-}

A simple test to see whether a continued fraction is normalized (something very crucial during the debugging of two CF arithmetic) is simply to check what happens when you multiply it by 1.

> --
> -- | isNormalized : Whether a CF is in the proper normal form
> --
> isNormalized cf@(CF xs) = xs == ys
> where (CF ys) = morph (T4 0 1 1 0) cf

Finally, we simply define some show instances for the T4 and T8 data structure, to ease algorithmic debugging (which was a great must during the development of this library).

> instance Show a => Show (T4 a) where
> show (T4 a b c d) = unlines [unwords ["|/", as, bs, "\\"],
> unwords ["|\\", cs, ds, "/"]]
> where s = map show [a,b,c,d]
> len = maximum . map length $ s
> [as,bs,cs,ds] = map (\x -> take (len - length x) spaces ++ x) s
> spaces = cycle " "
>
> instance Show a => Show (T8 a) where
> show (T8 a b c d e f g h) = unlines [unwords ["|/", as, bs, cs, ds, "\\"],
> unwords ["|\\", es, fs, gs, hs, "/"]]
> where s = map show [a,b,c,d,e,f,g,h]
> len = maximum . map length $ s
> [as,bs,cs,ds,es,fs,gs,hs] = map (\x -> take (len - length x) spaces ++ x) s
> spaces = cycle " "

Some final thoughts

Now as mentioned, I’d explain some issues regarding the use of this for irrationals and a possible solution. After implementing this system, I was obviously curious to try this out on an irrational. So I tried multiplying the CF for √2 with itself. And after seeing it not converge at all, I kept wondering why. Now I know, and it also shows a way to fix it so that it will work. Due to the representation I use for continued fractions, I am guaranteed that the integer part will always be stable. The problem is that I can not have negative additions, only positive ones. This means that if I were able to get the stable part ’2′ early, then the remaining infinite digits of the CF for √2 would have to add up to 0. One possibility for ‘fixing’ this is by changing the measure of stability. If we allow negative digits, we could choose to stabilize a digit as long as the different quotients are all within some ε from a given integer, and not require them all to be falling on the same side. This would, of course, mean, that it is possible to have negative digits further in the stream. Whether we want this or not is a big question, since they open up a whole other can of worms regarding stability of the number and such, perhaps a more mathematically-inclined person could build further upon this idea.

TypeChecking Lambda Calculus using TyperMonad (courtesy of Saizan)

While I had planned to show how to use the typechecker monad presented in in an earlier blog post by showing how to typecheck MiniML, I was positively surprised to find out that people had actually started using due to it’s simplicity. More specifically, Saizan in the #haskell channel on Freenode had written a type-checker for a simple typed lambda-calculus. With his permission, I have presented it here along with some modifications. His original code was a bit shorter, which goes to show how easy the monad is, but I’ve introduced a few helper functions that I should’ve introduced in the original blog post but didn’t because at the time I felt like they would confuse the issue too much. As such, the contents of the actual typechecking is almost the same, except for a few details which I shall mention in the body of this blogpost.


I’m just going to walk straight through the code as it’s rather straightforward.

> module STLC where
> import TypeChecker
> import qualified Data.Map as M
> import Control.Monad
> import MonadScope
> import MonadEnv
> import MonadSupply

First we introduce a function that replaces type variables with other type variables in types, this is rather straight forward. Given an environment, replace variables when you find them.

> ------------------------------------------------------------------------------
> -- substVar : Replaces variables with other variables within a type
> ------------------------------------------------------------------------------
> substVar :: [(Var, Var)] -> MonoType -> MonoType
> substVar subst tx@(TyVar x) =
> case x `lookup` subst of
> Nothing -> tx
> Just y -> TyVar y
> substVar subst (TyConst n ts) =
> TyConst n . map (substVar subst) $ ts
> substVar subst (TyFun ta tb) =
> TyFun (substVar subst ta) (substVar subst tb)

Next is an important function, and something that Saizan missed in his original post. This is actually part of my TypeChecker.hs file which I trimmed down for the previous blogpost. When you have a polytype (some type that says \forall variables. type) and you want to actually use it, you have to make a monotype out of it. Now, a polytype contains a monotype, but it can not simply be used as is. This is something that was missing in the original code, though in the case of this specific code, it would not have made a difference so it. It is important to instantiate a polytype’s free-variables with fresh type-variables, or you can end up over-specifying a type. More specifically, I think this is what makes or breaks the Monomorphism Restriction, though if I’m wrong, feel free to point that out. Just to give you an idea, assume the following code (in -some- functional language)


let id x = x in
(id 'b', id 1)

What will happen, when typechecking this code is that in the scope of the body of that let-clause, the identifier ‘id’ will refer to a polytype (Namely: forall a. a -> a). Now, if this polytype’s forall bit is simply dropped and the mono-type is used, we’ll end up with the ‘a’ being unified both with Char and Integer. Hence, it is important to instantiate each use of ‘id’ to make sure that fresh variables are used instead of ‘a’. The following function does that, using the functionality of substVar.

> ------------------------------------------------------------------------------
> -- instantiate : Instantiates a polytype, making sure all free type-variables
> -- are fresh
> ------------------------------------------------------------------------------
> instantiate :: (TyperMonad m) => PolyType -> m MonoType
> instantiate (TyPoly is t) = do
> is' <- mapM (\x -> supply) is
> return $ substVar (zip is is') t

Because we have scoping, we want to find the type of a variable. The following code finds the poly-type of a let-bound (or lambda-bound) variable in the scope, and then makes sure to instantiate it properly so that we do not get the monomorphism restriction.

> ------------------------------------------------------------------------------
> -- findType : Finds the type of a variable within the current scope
> ------------------------------------------------------------------------------
> findType :: (TyperMonad m) => String -> m MonoType
> findType x = find x >>= (maybe (error $ "Variable not in scope: " ++ x) instantiate) >>= normalize

Obviously, since we’re dealing with scopes, we also have to create new scopes.
The following function comes directly from Saizan’s code, except that I’ve taken out the dual of instantiate, namely generalize. Additionally, sometimes it’s useful to get a poly-type without generalizing any of the free-variables in the monotype (for instance patterns, though at the moment I can’t recall why). Actually, Saizan corrected me after this post went public, lambda-bound variables should be non-generalized (which looking back at my old-code makes sense, since they’re also patterns).

> ------------------------------------------------------------------------------
> -- generalize : Generalizes a monotype to a polytype by generalizing over all
> -- of its free variables
> ------------------------------------------------------------------------------
> generalize :: (TyperMonad m) => MonoType -> m PolyType
> generalize = liftM toPoly . normalize

> ------------------------------------------------------------------------------
> -- nogeneralize : Turns a type into a polytype without generalizing any of
> -- it's free variables (and thus when instantiated, this can lead to the
> -- monomorphism restriction)
> ------------------------------------------------------------------------------
> nogeneralize :: (TyperMonad m) => MonoType -> m PolyType
> nogeneralize = liftM (TyPoly []) . normalize

> ------------------------------------------------------------------------------
> -- withinScope : Applies a TyperMonad action within a nested scope with a new
> -- variable with a given type
> ------------------------------------------------------------------------------
> withinScope :: (TyperMonad m) => String -> MonoType -> m a -> m a
> withinScope x t ma = do
> pt <- nogeneralize t
> scope (M.insert x pt) ma

A last little helper function to generate unique typevariables…

> supplyVar :: TyperMonad m => m MonoType
> supplyVar = liftM TyVar supply

… and we get to the actual lambdacalculus. It’s a very simple calculus, with only three forms: identifiers (variables), lambda abstractions and function application.

> ------------------------------------------------------------------------------
> -- Simple Typed Lambda Calculus
> ------------------------------------------------------------------------------
> type Id = String
> data Expr = Var Id
> | Lambda Id Expr
> | App Expr Expr

Here the code differs just -slightly- with Saizan’s original code. Instead of normalizing after checking each sub-expression, it is perfectly fine to normalize at the end. Even if you were decorating the expression-tree, you’d still have to wait until the end, because only then could all types be normalized. So there’s no point, really, in normalizing before typechecking (and thus unification) is finished.

> typeCheck :: (TyperMonad m) => Expr -> m MonoType
> typeCheck e = check e >>= normalize
> where check (Var x) = findType x
> check (Lambda x b) = do
> tx <- supplyVar
> tb <- withinScope x tx $ check b
> return $ TyFun tx tb
> check (App a b) = do
> ta <- check a
> tb <- check b
> te <- supplyVar
> unify ta (TyFun tb te)
> return te

There’s a few alterations, but the gist of Saizan’s core which prompted this blog-post is all there, and I want to thank him for this great illustration of how to use the typermonad, since I did not think about it myself at all. Notice that the only code that would change in the case of a different type-checker is the code that came after the definition of the lambda-calculus. All the code that came before that were generic helper functions that I did not introduce in the prior blog post as then they would’ve not been clear as to why they are useful, but they -should- go into TypeChecker.hs.

Finally, let’s show some examples that Saizan originally showed, and see how nicely they typecheck :)

> id' = Lambda "x" (Var "x")
> flip' = Lambda "f" (Lambda "a" (Lambda "x" (App (App (Var "f") < font color="Green">(
Var "x")) (Var "a"))))
> run m = evalTyperT M.empty m
>
> -- *STLC> run $ typeCheck (App flip' id')
> -- b -> (b -> g) -> g

As usual, this blogpost is a literate haskell file, and if you have any comments, questions or suggestions, feel free to leave a comment on my blog :)

A Fractional Type for Haskell

In this short blog post, I introduce a utility module that I will use in another blog post. To keep the content there short, I decided to make a blogpost just for this module. As usual, the license for this module is BSD, and the author is the author of this blog post.

Basically, while working on continued fractions, I needed a way to compare fractions of arbitrary numbers to see if their integral part coincided. Before I explain what I mean by that (if it’s not already obvious), I will first show some notation that I use to represent fraction types:

a :∼: b represents a fraction ab

Since this is a rather short post, let’s dive straight into the code.

As usual, this will be a literate haskell post, and it will include the full comments from the original file :) So first, the header, which also specifies some details regarding the workings of this code

> module Fraction where
> import Data.Ratio
>
> data Fraction a = {-# UNPACK #-}!a :~: {-# UNPACK #-}!a
> deriving (Show)
>
> infix 7 :~:

As mentioned earlier, this code serves to allow comparing of fractions for just their integral part. Unlike Data.Ratio in Haskell, this type allows for having 0 in the denominator. The reason for this is that the code that uses this type needed to be able to store these numbers and only later filter them. As such, we have the following rules (where nan = not a number):

  • ∀ a. (a > 0 ⇔ (a :∼: 0) = ∞) ∧ (a < 0 ⇔ (a :∼: 0) = −∞)
  • (0 :∼: 0) = nan
  • ∞ ≠ nan, −∞ ≠ nan, ∞ ≠ −∞, −∞ < ∞
  • ∀ a b: b ≠ 0 . (a :∼: b) ≠ nan ∧ (a :∼: b) ≠ ∞ ∧ (a :∼: b) ≠ −∞
  • ∀ a b: b ≠ 0 . −∞ < (a :∼: b) < ∞
  • ∀ a b c d: b ≠ 0 . (a :∼: b) = (c :∼: d) ⇔ a `div` b = c `div `d
  • ∀ a b c d: b ≠ 0 . (a :∼: b) < (c :∼: d) ⇔ a `div` b < c `div `d

It is important to notice that ‘nan’ can not be compared to any other value. It can only be ‘compared’ for equality, but it is not part of the order defined on these numbers. Porting the following rules straight to code, and adding some simple functions to check whether a number is infinite or a nan, and some accessors, we get:

> unFraction :: Fraction a -> (a,a)
> unFraction (a :~: b) = (a,b)
>
> toIntegral (a :~: b) = a `div` b
>
> isInfinite (a :~: 0) = a /= 0
> isInfinite _ = False
>
> isNan (0 :~: 0) = True
> isNan _ = False
>
> instance (Eq a, Num a, Integral a) => Eq (Fraction a) where
> -- (0 :~: 0) == (0 :~: 0) = True -- See blog-comments
> (0 :~: 0) == _ = False
> _ == (0 :~: 0) = False
> (a :~: 0) == (c :~: 0) = signum a == signum c
> (_ :~: 0) == (_ :~: _) = False
> (_ :~: _) == (_ :~: 0) = False
> (a :~: b) == (c :~: d) = a `div` b == c `div` d
>
> instance (Ord a, Num a, Integral a) => Ord (Fraction a) where
> (0 :~: 0) `compare` _ = error "Can not compare NaN's"
> _ `compare` (0 :~: 0) = error "Can not compare NaN's"
> (a :~: 0) `compare` (c :~: 0) = compare (signum a) (signum c)
> (a :~: 0) `compare` (_ :~: _) = compare a 0
> (_ :~: _) `compare` (c :~: 0) = compare 0 c
> (a :~: b) `compare` (c :~: d) = compare (a `div` b) (c `div` d)

Defining arithmethic for this type is rather easy. Since I only care about equality of the final number, we can use plain old arithmetic like any old rational type. This includes the instance for Fractional, which defines division. Finally, it is also rather easy to define an instance of Real number for this fractional type, since it’s very easy to generate a rational number from this. The only problem, of course, would be when ‘toRational’ is called on an infinite or a nan.

> instance (Num a, Integral a) => Num (Fraction a) where
> (a :~: b) + (c :~: d) = (a*d + b*c) :~: (b*d)
> (a :~: b) - (c :~: d) = (a*d - b*c) :~: (b*d)
> (a :~: b) * (c :~: d) = (a*c) :~: (b*d)
> negate (a :~: b) = (negate a :~: b)
> abs (a :~: b) = (abs a :~: abs b)
> signum (a :~: b) = (signum a :~: 1)
> fromInteger x = fromInteger x :~: 1
>
> instance (Fractional a, Integral a) => Fractional (Fraction a) where
> (a :~: b) / (c :~: d) = (a*d) :~: (b*c)
> fromRational x = (fromInteger . numerator$ x) :~: (fromInteger . denominator $ x)
>
> instance (Real a, Integral a) => Real (Fraction a) where
> toRational (a :~: b) = toRational a / toRational b

Well that’s all folks, not really complicated stuff. Just thought I’d add a light blog in preparation for the entry on continued fractions which will be reasonably math intensive.

SImple Type Inference in Haskell

In this article I show how to build a simple Hindley-Milner type-inference engine in Haskell. I used this a while back in a MiniML frontend/interpreter. Due to the size of the full code, I will only show the type-inference engine and not the rest of the interpreter. I’ll show some simple uses and then in future articles I will show how this can be used more practically in a real compiler. Or potentially expand the type-checker with new concepts.

For this code I used three custom monads that I made which are actually quite useful in general. They will each go in their separate module. Since this means that this article is not one literate haskell file, I will not use literate style, except for the code belonging to the actual type checker module. Just copy paste the other three files in appropriately named .hs files. The first monad is very simple and was actually written by Cale Gibbard. It takes as input an infinite list of data (for instance variables), and then whenever asked it will give a new fresh symbol. The license of all the code is simple permissive license (I explicitly mention this because the first monad is Cale’s work). The original code comes from MonadSupply. I extended it with a few more monad instances. Of interest is the function ‘makeSupply’ which was also added so that it’s easy to generate an infinite list of unique symbols based on a list of prefixes and a list of characters that can be used to extend the symbols to make new symbols.



{-# OPTIONS_GHC -fglasgow-exts -fallow-undecidable-instances #-}
module MonadSupply where
import Control.Monad
import Control.Monad.State
import Control.Monad.Reader

newtype SupplyT s m a = SupplyT { unSupplyT :: StateT [s] m a}
deriving (Functor, Monad, MonadTrans, MonadIO)

newtype Supply s a = Supply (SupplyT s Maybe a)
deriving (Functor, Monad, MonadSupply s)

class Monad m => MonadSupply s m | m -> s where
supply :: m s

instance Monad m => MonadSupply s (SupplyT s m) where
supply = SupplyT $ do
(x:xs) <- get
put xs
return x

instance MonadState s m => MonadState s (SupplyT x m) where
get = SupplyT . lift $ get
put v = SupplyT . lift $ put v

instance MonadReader r m => MonadReader r (SupplyT x m) where
ask = SupplyT . lift $ ask
local f a = SupplyT . local f . unSupplyT $ a

evalSupplyT (SupplyT s) supp = evalStateT s supp
evalSupply (Supply s) supp = evalSupplyT s supp

runSupplyT (SupplyT s) supp = runStateT s supp
runSupply (Supply s) supp = runSupplyT s supp

--------------------------------------------------------------------------------
--- makeSupply
--- Makes an infinite list
--------------------------------------------------------------------------------
-- makeSupply :: [[a]] -> [[a]] -> [[a]]
-- makeSupply inits tails =
-- let vars = inits ++ (map concat . sequence $ [vars, tails]) in vars
--------------------------------------------------------------------------------
--- Cleaner version supplied by TuringTest
--------------------------------------------------------------------------------
makeSupply :: [[a]] -> [[a]] -> [[a]]
makeSupply inits tails =
let vars = inits ++ (liftM2 (++) vars tails) in vars


The second monad is an environment monad which I made. It’s basically a fancy wrapper around a state monad that stores key-value pairs.



{-# OPTIONS_GHC -fglasgow-exts -fallow-undecidable-instances #-}
module MonadEnv where
import Control.Monad
import Control.Monad.State
import Control.Monad.Reader
import qualified Data.Map as M

type Memory k v = M.Map k v

newtype EnvT k v m a = EnvT { unEnvT :: StateT (Memory k v) m a }
deriving (Functor, Monad, MonadTrans, MonadIO)

newtype Env k v a = Env (EnvT k v Maybe a)
deriving (Functor, Monad, MonadEnv k v)

class (Ord k, Monad m) => MonadEnv k v m | m -> k, m -> v where
getfor :: k -> m (Maybe v)
putfor :: k -> v -> m ()

instance (Ord k, Monad m) => MonadEnv k v (EnvT k v m) where
getfor k = EnvT $ do
s <- get
return $ M.lookup k s
putfor k v = EnvT $ do
modify (\s -> M.insert k v s)

instance MonadState s m => MonadState s (EnvT k v m) where
get = EnvT . lift $ get
put v = EnvT . lift $ put v

instance MonadReader r m => MonadReader r (EnvT k v m) where
ask = EnvT . lift $ ask
local f a = EnvT . local f . unEnvT $ a

evalEnvT (EnvT s) ctx = evalStateT s ctx
evalEnv (Env s) ctx = evalEnvT s ctx

The final monad which I used was actually to scope behaviour during type-checking. This is not required, perse, for the pure typechecker, as you could put it on top of the typechecker monad in your compiler monad. However I think that the three fit nicely together (and I admit for being too lazy to rewrite the code to have split monads). It is a scoping environment. I hope that this is not too much code for one blog article. I plan to release a few more monads I have made in separate articles, so this feels like a collosal article, but I’m rather intent on showing this type-checker :) .



{-# OPTIONS_GHC -fglasgow-exts -fallow-undecidable-instances #-}
module MonadScope where
import Control.Monad
import Control.Monad.State
import Control.Monad.Reader
import qualified Data.Map as M

type Context k v = M.Map k v
type Subst k v = Context k v-> Context k v

newtype ScopeT k v m a = ScopeT { unScopeT :: ReaderT (Context k v) m a }
deriving (Functor, Monad, MonadTrans, MonadIO)

newtype Scope k v a = Scope (ScopeT k v Maybe a)
deriving (Functor, Monad, MonadScope k v)

class (Ord k, Monad m) => MonadScope k v m | m -> k, m -> v where
find :: k -> m (Maybe v)
scope :: Subst k v -> m a -> m a

instance (Ord k, Monad m) => MonadScope k v (ScopeT k v m) where
find k = ScopeT $ do
s <- ask
return $ M.lookup k s
scope s act = ScopeT $ do
local s . unScopeT $ act

instance MonadState s m => MonadState s (ScopeT k v m) where
get = ScopeT . lift $ get
put v = ScopeT . lift $ put v

evalScopeT (ScopeT s) ctx = runReaderT s ctx
evalScope (Scope s) ctx = evalScopeT s ctx

Now that we have the above three modules behind the way, we can start looking at the typechecker. Obviously we start with the definition of the module and the import of these three module as well as a few other basic necessities.



> {-# LANGUAGE FlexibleContexts, GeneralizedNewtypeDeriving, TypeSynonymInstances, MultiParamTypeClasses #-}
> module TypeChecker where
>
> import MonadSupply
> import MonadScope
> import MonadEnv
> import Data.List(nub, (\\), intersperse)
> import qualified Data.Map as M
> import Control.Monad.Trans

Basic type definitions

Now that we have that in place, it is important to specify types. One should realize that a typechecker has two kinds of types inside: monotypes and polytypes. The difference is that any free variables in a mono-type may only be unified with 1 specific type, while a polytype has variables that are parametrically polymorphic. More specifically, if we take the function “map :: (a -> b) -> [a] -> [b]“, this is actually “map :: forall a b. (a -> b) -> [a] -> [b]“. Thus it has a polytype. All top-level definitions and let-bound variables in Haskell are poly-typed. If map were mono-typed, then the first use of map would unify the ‘a’ and ‘b’ to specific types and any other invocation would have to respect those types. So a polytype is a monotype that has been quantified over several variables. As for monotypes, there are two specific options. Either the type is purely a type variable (TyVar), or it is a type-constructor that has several parameters. For convenience sake, we also define a function type (TyFun). In essence it’s just a TyConst with as Const “->”, but it’s always nice to make special cases ;) . For the actual type-variables, we will be using strings.

Besides the above basic ‘types’, we also introduce a few useful type-classes. Additionally, we define a few std type creationers (I know, bad word, but ‘type constructors’ would be ambiguous) to define some std types. Some of the functions are a bit simplistic and could be replaced by a simple call to the data-constructor. These exist because originally my types were a bit more complicated (I had a typeclass for types since I wanted to be able to add extra information to types, as such the type of types was actually ‘MonoType mt’ and then I would tie the knot by fixing the type declaration over whatever record contained the extra info, ignore and just be glad that the functions all have nicely similar names :) .



> --- Type variable
> type Var = String
> --- Type constructor
> type Const = String
> --- MonoTypes
> data MonoType =
> TyVar Var
> | TyFun MonoType MonoType
> | TyConst Const [MonoType]
> deriving (Eq, Ord)
> --- PolyTypes
> data PolyType =
> TyPoly [Var] MonoType
> deriving (Eq, Ord)
>
> instance Show MonoType where
> show (TyVar x) = x
> show (TyFun ta tb) = "(" ++ show ta ++ ") -> " ++ show tb
> show (TyConst "(,)" tis) = "(" ++ (concat . intersperse ", " . map show $ tis) ++ ")"
> show (TyConst n []) = n
> show (TyConst x tis) = x ++ " " ++ (unwords . map show $ tis)
>
> instance Show PolyType where
> show (TyPoly ids mt) = (if null ids then "" else "forall " ++ unwords ids ++ ".") ++ show mt
>
> class HasVars a where
> freeVars :: a -> [Var]
> occurs :: Var -> a -> Bool
> occurs x t = x `elem` freeVars t
>
> instance HasVars MonoType where
> freeVars (TyVar a) = [a]
> freeVars (TyFun ta tb) = nub $ freeVars ta ++ freeVars tb
> freeVars (TyConst _ ts) = nub . concatMap freeVars $ ts
> occurs x (TyVar y) = x == y
> occurs x (TyFun ta tb) = occurs x ta || occurs x tb
> occurs x (TyConst _ ts) = or . map (occurs x) $ ts
>
> instance HasVars PolyType where
> freeVars (TyPoly vs t) = freeVars t \\ vs
>
> toPoly :: MonoType -> PolyType
> toPoly x = TyPoly (freeVars x) x
> fromPoly :: PolyType -> MonoType
> fromPoly (TyPoly fvs t) = t
>
> unitConstructor = "()"
> tupleConstructor = "(,)"
>
> mkTyVar :: Var -> MonoType
> mkTyVar x = TyVar x
> mkTyFun :: MonoType -> MonoType -> MonoType
> mkTyFun ta tb = TyFun ta tb
> mkTyConst :: Const -> [MonoType] -> MonoType
> mkTyConst c ts = TyConst c ts
>
> mkTupleType :: [MonoType] -> MonoType
> mkTupleType ts = mkTyConst tupleConstructor ts
> mkUnitType :: MonoType
> mkUnitType = mkTyConst unitConstructor []
> mkBoolType :: MonoType
> mkBoolType = mkTyConst "Bool" []
> mkIntType :: MonoType
> mkIntType = mkTyConst "Int" []
>
> mkFunType :: [MonoType] -> MonoType
> mkFunType (a:b:r) = mkTyFun a $ mkFunType (b:r)
> mkFunType [a] = a
> mkFunType [] = error "mkFunType: Trying to make a function with 0 args"

Type Checker Monad

Now that we’ve defined some standard functions and smart constructors, we could play around with it, but I will leave that to the reader. Instead, let’s move on to the meat of this blog entry. for this we define a new monad that is the typer monad. The typer monad is actual a stack of monad transformers. As bottom monad, we define the supply monad transformer that will ensure we have an unlimited supply of fresh names that the typer monad can use. On top of this, we define an environment monad (EnvT) that maps typevariables to appropriate MonoType’s. Finally, because we want to have let-binding in whatever language we may use, we define a scoping monad (ScopeT) so that whenever the language uses (let x = … in …) we can have a polytype for ‘x’ such that we do not need to worry about the momonomorphism restriction. With this stack, we define a custom monad (TyperMonad) that has two basic operations besides the standard operations that the stack we made gives and besides the regular monad interface. These two actions allow us to unify two types and allow us to normalize a type based on what has been unified so far. For instance, if we unify (TyVar “a”) with (TyConst “Int” []), then whenever we normalize a type that has (TyVar “a”) in it, we want to be sure that it becomes the Int type. We will show simple examples at the bottom on how this is used.



> -- Ident is the type for identifiers in a program
> type Ident = String
> -------------------------------------------------------------------------------
> --- TyperState:
> --- State of typer monad
> --- Keeps a map of tyvar -> MonoType substitutions
> --- Keeps a list of free tyvars
> --- Requires: tyvars used as keys do not appear in the values
> --- unify needs to ensure this at all times
> --------------------------------------------------------------------------------
> type TyperContext = M.Map Ident PolyType
> type TyperSubst = TyperContext -> TyperContext
>
> newtype TyperT m a = TyperT {
> runTyperT :: ScopeT Ident PolyType (EnvT Var MonoType (SupplyT Var m)) a
> } deriving (Functor, Monad, MonadIO)
>
> instance MonadTrans TyperT where
> lift = TyperT . lift . lift . lift
>
> instance (Monad m) => MonadSupply Var (TyperT m) where
> supply = TyperT . lift . lift $ supply
>
> instance (Monad m) => MonadScope Ident PolyType (TyperT m) where
> find = TyperT . find
> scope f act = TyperT . scope f . runTyperT $ act
>
> class (Monad m, MonadScope Ident PolyType m, MonadSupply Var m) => TyperMonad m where
> unify :: MonoType -> MonoType -> m ()
> normalize :: MonoType -> m MonoType

With the above interface for the TyperMonad given, it is time to actually define it. This is the real meat of the typer monad.



>
> problem :: (Monad m) => String -> String -> m ()
> problem phase message = fail $ phase ++ ": " ++ message
>
> instance (Monad m) => TyperMonad (TyperT m) where
> ------------------------------------------------------------------------------
> --- unify
> ------------------------------------------------------------------------------
> unify type1 type2 = TyperT $ do
> type1' <- runTyperT $ normalize type1
> type2' <- runTyperT $ normalize type2
> unifier type1' type2'
> where unifier (TyVar x) ty@(TyVar y) =
> if x == y
> then return ()
> else lift $ putfor x ty
> unifier (TyVar x) ty =
> if x `occurs` ty
> then problem "TyperChecker" ("Trying to unify recursive type " ++ show x ++ " = " ++ show ty)
> else lift $ putfor x ty
> unifier tx (TyVar y) =
> if y `occurs` tx
> then problem "TyperChecker" ("Trying to unify recursive type " ++ show y ++ " = " ++ show tx)
> else lift $ putfor y tx
> unifier tx@(TyConst nx px) ty@(TyConst ny py) =
> if nx == ny && length px == length py
> -- IMPORTANT TO use unify and not not unifier
> -- or the code will recurse for:
> -- foo x y = x y; bar x = foo bar bar
> then runTyperT . sequence_ $ zipWith unify px py
> else problem "TyperChecker" (show tx ++ " can not be inferred to " ++ show ty)
> unifier (TyFun tax tbx) (TyFun tay tby) = do
> runTyperT $ unify tax tay
> runTyperT $ unify tbx tby
> unifier tx ty =
> problem "TypeChecker" (show tx ++ " can not be inferred to " ++ show ty)
> ------------------------------------------------------------------------------
> --- normalize
> --- Normalizes a type by looking it up if it's a tyvar
> --- Applies a small optimization, it basically removes any extra unnecessary
> --- mappings. For instance:
> --- [a->b, b->Int]: normalize a
> --- [a->b, b->Int]: b' <- normalize b
> --- [a->Int, b->Int]: return b'
> ------- -----------------------------------------------------------------------
> normalize tx@(TyVar x) = TyperT $ do
> tx' <- lift $ getfor x
> case tx' of
> Nothing -> return tx
> Just ty -> do
> ty' <- runTyperT $ normalize ty
> if ty == ty'
> then return ty'
> else do
> lift $ putfor x ty'
> return ty'
> normalize tx@(TyConst n tl) = TyperT $ do
> tl' <- runTyperT $ mapM normalize tl
> return $ TyConst n tl'
> normalize tx@(TyFun ta tb) = TyperT $ do
> ta' <- runTyperT $ normalize ta
> tb' <- runTyperT $ normalize tb
> return $ TyFun ta' tb'
> ------------------------------------------------------------------------------
>
> evalTyperT :: (Monad m) => TyperContext -> TyperT m a -> m a
> evalTyperT ctx action =
> let vars = makeSupply (map return ['a'..'z']) ["'"] in
> evalSupplyT (evalEnvT (evalScopeT (runTyperT action) ctx) M.empty) vars

I will let you grok the code. If any bits are not clear, feel free to tell me so and I will expand upon them. Now we can easily do some experiments:


evalTyperT M.empty (do{unify (TyVar "a") mkIntType; normalize (mkFunType [TyVar "a", TyVar "a", TyVar "b"])})
=> (Int) -> (Int) -> b

You might notice that I included some extra machinery, namely the scoping and all that. In a future blog post I will show this is actually used to allow for typechecking a simple language (like MiniML). But for now, I will leave it at that as it has already grown to become quite a big blogpost.

If you have any questions or comments, please feel free to post them at the bottom and I will make the necessary changes if required to clarify or improve the presentation.

Higher Order Zippers

In this blog article we explore the meaning of zippers as well as higher order zippers. The idea for this blog article came while discussing with fasta on Freenode today about zippers for graphs. Out of the blue, the question popped to me, what does it mean to have higher order zippers. Not having thought it through completely, I hope this blog will offer some clarity, and perhaps some feedback.

[EDIT: This is a new version as of 2007-07-11 that takes some comments from reddit and the comments here into account, cleaning up a bit and adding some more content]


For those new to the concept of Zippers, I shall briefly explain what they are and how one can reason with them. The idea of a zipper is to provide an iterator that one can move through an arbitrary functor.

A functor is basically a container of elements. For instance, [] in Haskell is a functor. If you apply to it to a specific type, you get a container-type (in this case a list) of that type. Other typical examples include Maybe, Binary trees and the N-ary tree introduced in Flatten Benchmark.

Due to the fact that Haskell does not have mutability, at first it can seem inefficient to mutate an element inside such a Functor or container. That is why Huet invented the concept of a Zipper. A Zipper allows one to walk through such a container such that one specific element has O(1) access, namely the element that is currently in the ‘hole’. Then, typically, there will be functions that allow one to move the element we’re currently looking at.

First Order Zippers

To illustrate, I will demonstrate the Zipper for a list first.

> {-# OPTIONS_GHC -fglasgow-exts #-}
> module Zipper where
> import Data.Maybe(fromJust)
>
> -- A zipper is the current element and a context that stores where this
> -- element is.
> data Zipper d a = Zipper a (d a) deriving (Eq, Ord, Show)
>
> -- The context for a list is a combination of the elements before and the
> -- elements after the current element.
> data DList a = DList [a] [a]
> deriving (Eq, Ord, Show)
> type ZList a = Zipper DList a

The advantage of this zipper is that one can easily (with O(1) complexity) move the current hole we’re looking at back and forth. It also provides an O(1) complexity way of changing the current element. As last requirement is that it should be possible to reconstruct the entire data-type that has been ‘zipped’ from just the Zipper. This process is often referred to as ‘unzipping’ the data structure. The methods to perform these operations, as well as to create a zipper from a list are given here:

> enterList :: (Monad m) => [a] -> m (ZList a)
> enterList [] = fail "Can not zip an empty list"
> enterList (x:xs) = return $ Zipper x (DList [] xs)
>
> unzipList :: ZList a -> [a]
> unzipList (Zipper a (DList [] suf)) = a:suf
> unzipList z = unzipList . fromJust . prev $ z
>
> prev :: (Monad m) => ZList a -> m (ZList a)
> prev (Zipper a (DList [] tl)) = fail "Already at the first element"
> prev (Zipper a (DList (x:xs) tl)) = return $ Zipper x (DList xs (a:tl))
>
> next :: (Monad m) => ZList a -> m (ZList a)
> next (Zipper a (DList hd [])) = fail "Already at the last element"
> next (Zipper a (DList hd (x:xs))) = return $ Zipper x (DList (a:hd) xs)
>
> update :: (a -> a) -> Zipper d a -> Zipper d a
> update f (Zipper a d) = Zipper (f a) d

In The derivative of a
Regular Type is a Type of One-Hole Contests
Conor McBride shows us how it is possible to determine the context for any data-type using algebra. Basically, the context for a data-type is it’s derivative. How can one derive a data-type, however? Well this is done by using the more algebraic notation of a data type. If one takes a list, then the actual data type is: ‘List a = Nil | Cons a (List a)’. In an algebraic notation, this would be: L = 1 + a·L. Namely, a list is a sumtype of a constant (1) and a tuple of an element ‘a’ and the list again. Well, this is not fully correct, a list is actually the least-fixed-type that satisfies this equation (namely: L = 1 + a·L μ L.1 + a·L). However I will gloss over this. The context of a list is then the derivative of this equation using standard derivation as taught in algebra/calculus:

a L = ∂a a · L + a·∂a L = 1·L + a·∂a L = L + a·∂a L


=> data DList a = [a] | DCons a (DList a)

By factoring out the [a] (because any DList will contain exactly one), one gets “[a]*(mu dL.1 + a*dL)” or “[a]*[a]“. In general, I believe that in an equation “(mu x.S + Tx)” one can factor out the S (as long as it doesn’t contain a reference to x of course) to get “(S*(mu x.1 + Tx))”. For exercise’s sake, we will derive the context for a binary tree:

> data Tree a = Leaf | Node a (Tree a) (Tree a)
> deriving (Eq, Ord, Show)
> -- Tree a (or t for short)

a t = t2 + a·t·∂_ t = t2 × (μ x. 1 + 2·a·t·x) = t2·p where p = 1 + 2·a·t·p or p = 2·a·t

Looking at this from an intuitive point of view, this makes sense. The context of an element in a tree, are the left and right child-trees of the node this element is in, as well as the path that we took to get there by saving the trees that we skipped over along the way to the element.

> data DTree a = DTree {leftChild   :: (Tree a),
> rightChild :: (Tree a),
> path :: [SEither (Step a)]}
> deriving (Eq, Ord, Show)
> type SEither a = Either a a
> -- The path through a btree to the current node, saving those trees we did not enter.
> data Step a = Step a (Tree a)
> deriving (Eq, Ord, Show)
> type ZTree a = Zipper DTree a
>
> enterTree :: (Monad m) => Tree a -> m (ZTree a)
> enterTree Leaf = fail "Can not zip an empty btree"
> enterTree (Node x l r) = return $ Zipper x $ DTree l r []
>
> unzipTree :: (ZTree a) -> Tree a
> unzipTree (Zipper x (DTree l r [])) = Node x l r
> unzipTree dt = unzipTree . fromJust . up $ dt
>
> up :: (Monad m) => ZTree a -> m (ZTree a)
> up (Zipper x (DTree l r [])) = fail "Already at the top of a tree"
> up (Zipper x (DTree l r (p:pp))) =
> case p of
> Right (Step px pr) -> return $ Zipper px (DTree (Node x l r) pr pp)
> Left (Step px pl) -> return $ Zipper px (DTree pl (Node x l r) pp)
>
> left :: (Monad m) => ZTree a -> m (ZTree a)
> left (Zipper x (DTree Leaf pr pp)) = fail "Can not go further left"
> left (Zipper x (DTree (Node v l r) pr pp)) = return $ Zipper v $ DTree l r $ ((Right $ Step x pr):pp)
> right :: (Monad m) => ZTree a -> m (ZTree a)
> right (Zipper x (DTree pl Leaf pp)) = fail "Can not go further right"
> right (Zipper x (DTree pl (Node v l r) pp)) = return $ Zipper v $ DTree l r $ ((Left $ Step x pl):pp)

I will leave the implementation for an N-ary tree as an exercise for the reader.

Second Order Zippers

Now nothing introduced so far is really new. The question that arose to me is: what would a higher-order zipper be? What does it mean to have a double derivative of a data-type. I will first show what the structure for the double derivative of a list looks like by working it out and then give an intuition of what the meaning of this data-type might mean. To make sure that this intuition makes any sense, we will then work out the double derivative for a binary tree, to ascertain that the intuition we had for the list is valid for other data-types. So first we define the generic meaning of a second-order zipper:

> type Zipper2 d2 a = Zipper (Zipper d2) a
>
> update2 :: (a -> a) -> Zipper2 d2 a -> Zipper2 d2 a
> update2 f (Zipper x (Zipper y d)) = Zipper x (Zipper (f y) d)

A second-order zipper is simply the zipper of the zipper of a datatype parametrized with the second-order derivative of that data-type and a the element-type. So we can already see that a second-order zipper will be containing two ‘a’s as well as this second-order derivative. So what is the second-order derivative of a list? Well we had: “[a]‘ = [a]_h*[a]_t”. Applying simple derivation in the algebraic sense we get: “[a]” = [a]_h*[a]_t’ + [a]_h’*[a]_t”.

Second Order Zipper for a List

If we remember the meaning we gave to the two lists in the case of “[a]‘”, then we had the head part and the tail part of the list around the current element we’re looking at. Since we’re now either deriving one or the other, my intuition tells me that we’ll have either the prefix and suffix of the head part or the prefix and suffix of the tail part. If we take the definition of “[a]‘” and expand it in “[a]”” we get: “[a]*[a]*[a] + [a]*[a]*[a]“. Putting this in a Haskell data-type with names based on my intuition, we get:

> -- DDList a = Prev (reverse of prefix of prefix) 
> -- (suffix of prefix)
> -- suffix
> -- | Next (rever se prefix)
> -- (rever se of prefix of suffix)
> -- (suffix of suffix)
> data DDList a = Prev [a] [a] [a] | Next [a] [a] [a]
> deriving (Eq, Ord, Show)
> type ZZList a = Zipper2 DDList a
>
> openLeft :: (Monad m) => ZList a -> m (ZZList a)
> openLeft (Zipper r (DList [] tl)) = fail "Can not enter an empty list"
> openLeft (Zipper r (DList (l:hd) tl)) = return $ Zipper l (Zipper r (Prev hd [] tl))
>
> openRight :: (Monad m) => ZList a -> m (ZZList a)
> openRight (Zipper l (DList hd [])) = fail "Can not enter an empty list"
> openRight (Zipper l (DList hd (r:tl))) = return $ Zipper r (Zipper l (Next hd [] tl))
>
> unzipZList :: ZZList a -> ZList a
> unzipZList (Zipper l (Zipper r (Prev a [] c))) = Zipper r (DList (l:a) c)
> unzipZList z@(Zipper l (Zipper r (Prev a b c))) = unzipZList . fromJust . shrink $ z
> unzipZList (Zipper r (Zipper l (Next a [] c))) = Zipper l (DList a (r:c))
> unzipZList z@(Zipper r (Zipper l (Next a b c))) = unzipZList . fromJust . shrink $ z
>
> enlarge :: (Monad m) => ZZList a -> m (ZZList a)
> enlarge (Zipper l (Zipper r (Prev [] bs cs))) = fail "Can not move further to the left"
> enlarge (Zipper l (Zipper r (Prev (a:as) bs cs))) = return $ Zipper a (Zipper r (Prev as (l:bs) cs))
> enlarge (Zipper r (Zipper l (Next as bs []))) = fail "Can not move further to the right"
> enlarge (Zipper r (Zipper l (Next as bs (c:cs)))) = return $ Zipper c (Zipper l (Next as (r:bs) cs))
>
> shrink :: (Monad m) => ZZList a -> m (ZZList a)
> shrink (Zipper l (Zipper r (Prev as [] cs))) = fail "Can not further shrink"
> shrink (Zipper l (Zipper r (Prev as (b:bs) cs))) = return $ Zipper b (Zipper r (Prev (l:as) bs cs))
> shrink (Zipper r (Zipper l (Next as [] cs))) = fail "Can not further shrink"
> shrink (Zipper r (Zipper l (Next as (b:bs) cs))) = return $ Zipper b (Zipper l (Next as bs (r:cs)))
>
> switch :: ZZList a -> ZZList a
> switch (Zipper l (Zipper r (Prev as bs cs))) = Zipper r (Zipper l (Next as (reverse bs) cs))
> switch (Zipper r (Zipper l (Next as bs cs))) = Zipper l (Zipper r (Prev as (reverse bs) cs))
>
> splice :: ZZList a -> [a] -> ZZList a
> splice (Zipper l (Zipper r (Prev as _ cs))) bs = Zipper l (Zipper r (Prev as bs cs))
> splice (Zipper r (Zipper l (Next as _ cs))) bs = Zipper r (Zipper l (Next as bs cs))
>
> -- A more generic function (splice can be implemented in terms of this)
> modify :: ([a] -> [a]) -> ZZList a -> ZZList a
> modify f (Zipper l (Zipper r (Prev as bs cs))) = Zipper l (Zipper r (Prev as (f bs) cs))
> modify f (Zipper r (Zipper l (Next as bs cs))) = Zipper r (Zipper l (Next as (f bs) cs))
>

So what my intuitition tells me is that where a Zipper gives O(1) mutation of an element, a Zipper2 gives O(1) splicing. After all, we can directly access the part that is between the two singular elements stored in the Zipper2. Of course, to ascertain that this statement is valid for more than just lists, we should ascertain this is true for other data-types. In this case, we shall do the experiment for binary trees. Again, the exercise for N-ary trees is left as an exercise for the reader (feel free to put in a comment if you want to).

Deriving the rules for a tree

Note: I redid the math with a cleaner technique, and it seems I had made some mistakes in the original math, which is why my data-type was not as intuitive as I had hoped it to be. The correct version makes much more sense :) Namely: I was missing a “p” in the last term.

Flatten Benchmark

In this blog article, we look at the benchmarks as proposed in Kyle’s Smith’s blog regarding the flattening of lists in Scheme. However, we perform the same experiment in Haskell. Obviously, due to typing reasons, this will not be done on lists but N-ary trees. It should be interesting to see how these algorithms perform in Haskell, especially due to the very different semantics caused by laziness.

In fact, a very common idiom in Scheme, or even SML or O’Caml, namely ensuring tail-call recursion, is not always a good idea in Haskell when working with data-structures. They are too strict in a sense, and as such they do not work well on infinite data-structures.


The first thing to do in Haskell, of course, is to define a module. We also define the data-type that will hold a list to be flattened. In this case, it is an N-ary tree where the options for the data-type is sumtype of a child of a single element, or a parent of a list of this sum-type. To keep it concise, I will give the data-constructors short names.

> module Flatten where
> import Control.Monad(liftM, liftM2)
> import CPUTime(getCPUTime)
> import Data.List(foldl')
> import System(getArgs)
> data Tree a = C a | P [Tree a]

As example, we show the encoding of a one of the ‘lists’ from Kyle’s blog. The notation is a bit verbose, but one could easily add a read-instance to fix this. Since this is not crucial, I will not do so at the moment (let’s just say, yay for VIM and some regexp-fu to turn the data into Haskelly data).

(define abc ‘(a (b (c (d (e (f (g (h (i (j (k (l (m n) o) p) q) r) s) t) u) v) w) x) y) z)) ; would become:

> abc = P [C 'a', P [C 'b', P [C 'c', P [C 'd', P [C 'e', P [C 'f', P [C 'g', 
> P [C 'h', P [C 'i', P [C 'j', P [C 'k', P [C 'l', P [C 'm', C 'n'], C 'o'], C 'p'], C 'q'], C 'r'], C 's'],
> C 't'], C 'u'], C 'v'], C 'w'], C 'x'], C 'y'], C 'z']
> flat = P $ map C $ [1..26]
> flat_abc = P $ map C $ ['a'..'z']
> tree = P [C 'a', P [C 'b', P [C 'd', P [C 'i', C 'q', C 'r'], P [C 'j', C 's', C 't']],
> P [C 'f', P [C 'k', C 'u', C 'v'], P [C 'l', C 'w', C 'x']]], P [C 'c', P [C 'g', P [C 'm', C 'y', C 'z'],
> P [C 'n', C 'a', C 'b']], P [C 'h', P [C 'o', C 'c', C 'd'], P [C 'p', C 'e', C 'f']]]]
> treec = P [C 'a', P [C 'b', P [C 'd', P [C 'i', C 'q', C 'r'], P [C 'j', C 's', C 't']], P [C 'f', P [C 'k', C 'u', C 'v'],
> P [C 'l', C 'w', C 'x']]], P [C 'c', P [C 'g', P [C 'm', C 'y', C 'z'], P [C 'n', C 'a', C 'b']], P [C 'h', P [C 'o', C 'c', C 'd'], P [C 'p', C 'e', C 'f']]]]

All the algorithms will by definition be slightly different as we have one more case to check due to the design of our data-type. First of all, instead of checking on whether the input is null, we will instead check when we have a child element. And secondly, because each level of the tree is a pure list, we can use standard list operations like map and fold.

Looking through the algorithms, a lot use side-effects or reversing at the end. Obviously, side-effects are not a standard idiom in Haskell. Reversing is not a good idiom for Haskell programming, because reversing tends to destroy laziness. As such, the version that is most straightforward to code in Haskell is the one that uses ‘cons’ with an accumulator. The version in scheme required reversing at teh end. We do not need to reverse the list at the end because we use ‘foldr’ while the algorithms in scheme used a fold-left mechanism. The reason why we want foldr is because it respects laziness, while the reason why schemers and mlers want foldl is because it is tail-call recursive.

I will add type-declarations to the function but these are purely for documentation purposes and are not actually required for Haskell. The scheme version uses a mutation on the result variable. Instead of doing this, we will take a more Haskelly approach (I was going to say pure, in the purely functional, but that could be misconstrued to mean pure as in purity of algorithm) and thread this result through the calls.

> flatten :: Tree a -> [a]
> flatten t = f t [] -- Call helper with the tree and an empty list
> -- The case we have list of nodes
> where f (P l) r = foldr f r l
> -- The case where we have a single element
> f (C a) r = a:r

To test we simply run ‘ghci Flatten.lhs’ and then when we run ‘flatten abc’ we get “abcdefghijklmnopqrstuvwxyz. We also see that this definition respects lazyness in the horizontal (but therefore not perse the vertical) direction. Namely, we construct an infinite flat tree of elements and see whether it succeeds in flattening. We will also construct an infinite vertical tree (obviously with some elements at eachc level, or it will take an infinite amount of time to reach the first element.

> infinite_flat_tree = P $ map C [0..]
> infinite_vert_tree = build [0..]
> where build (x:xs) = P [C x, build xs]

Indeed, if we load Flatten.lhs in ghci and run flatten, everything works out fine (make sure to do something like: ‘take 10 $ flatten infinite_flat_tree’, or your terminal will spam a lot of numbers). Similarly, it also respects the infinitely vertical tree (which the reader should note, has been built up in a way to ensure the creation of the tree itself is also lazy).

Originally I had intended to try out all the different algorithms that were written in Kyle’s blog, but it seems most of the trade-off is between using set! as well as reversing and other techniques to circumvent this. However, when using foldr and lazy structures, as long as you make sure to respect laziness, this is not required and there’s only one way of coding this function, which is probably the way anyone would write it in Haskell. If any of the readers have feedback on other versions that might be applicable for Haskell, I am definitely interested in seeing their version.

Therefore, to give this article any meaningful content, we will add some benchmarks. My computer is not so powerful, it is a simple Dell Latitude D610 laptop with 1GB of memory and a Centrino of 1.6Ghz.

First we need to generate some data-sets besides the one above. The first one was far too small and infinite data-sets will have obvious results if computed completely. To ensure the calculation actually occurs, I will get th
e last element of the computed list to force the entire list to be generated. To measure how complicated an N-ary tree is, Kyle introduces the concept of complexity. I will translate this to Haskell (If anyone spots algorithmic differences, feel free to point them out).

> complexity :: Tree a -> Integer
> complexity (C x) = 1
> complexity (P l) = foldl' (\c e -> 1 + c + complexity e) 0 l
> buildTestTree :: [Tree a] -> Int -> Tree a
> buildTestTree ts n = P $ take n $ cycle ts -- Cycle through the different
> -- trees, take only 'n' in total
> -- and create a parent node
> -- Thanks apfelmus from #haskell (P.s: getCPUTime returns picoseconds)
> time m = liftM2 subtract getCPUTime (m >> getCPUTime)

Due to laziness, it is important that we force the creation of the input tree before actually timing the flattening of the tree. But since we need to know the complexity of the tree before we try to flatten it, we can let the complexity function force the creation of the tree. Therefore, to get a test,case, we simply get the following code:

> runTest :: (Show a) => Tree a -> IO ()
> runTest x = do
> putStr "Complexity: "
> t1 <- time $ print $ complexity $ x -- Force the creation of the tree
> putStr "Last element: "
> t2 <- time $ print $ last $ flatten x -- Time the flatten function
> putStrLn $ "Times: " ++ show t1 ++ ", " ++ show t2

Finally, we can tie it all together with a little main that will allow us to run this program to test different complexities. While the scheme version allowed the user to choose which subtrees to use to build up the big tree, I will not give this option as in the end, the only metric used was complexity. I would like to briefly point out, however, that it might be interesting to test deeper trees, as the trees seem to have been limited to the depth of trees defined at the beginning.

> main :: IO ()
> main = do
> n <- liftM (read . head) getArgs
> let t = buildTestTree [abc, flat_abc, treec] n
> sequence_ $ replicate 10 $ runTest t -- Run timing test 10 times

The results can be seen below in the figure. I hope this was useful.

Simplistic compiler in Haskell

Recently I gave a short intro course on functional programming languages to people at work, introducing some basic comments. At the end, I added a very very tiny compiler to show how easy it is to create a compiler in Haskell.

I thought it might be interesting for the people out there to see it as well. As mentioned, it is very minimalistic. Keeping with the trend of the previous post, I will ensure this blogpost is proper literal haskell code.


So first we create our module. We also import the Control.Monad for liftM and liftM2. Finally, we import QuickCheck so we can create some easy tests at the end.


> module Alg where
> import Control.Monad
> import Test.QuickCheck

Next, we define the domain of our compiler. Namely, our compiler will compile simple arithmetic expressions, that can be nested arbitrarily deep, to a stack machine. An expression consists of either a simple number, the addition of two expressions, the multiplication of two expressions, or the substraction of two expressions. We add some standard typeclasses that allow us to easily work with them in the GHC interpreter (for instance Show to show them).


> data Exp = Simple Integer
> | Mul Exp Exp
> | Add Exp Exp
> | Sub Exp Exp
> deriving (Eq, Ord, Show)

Without compiling, we can already write a mini interpreter that interprets an expression straight away. One option of making this more generic is abstracting away the specific binary operator instead of creating a specific data-constructor for each, but I will leave that as an excercise.


> interpretExp (Simple i) = i
> interpretExp (Mul a b) = interpretExp a * interpretExp b
> interpretExp (Add a b) = interpretExp a + interpretExp b
> interpretExp (Sub a b) = interpretExp a - interpretExp b

Next we define the codomain, or the target, of our compiler. For this I have opted for a very simple stack machine with only four instructions. Either one pushes a number, or one applies an operator to the top two numbers on the stack. As for the stack, it is simply a list of numbers.


> data Op = OpPush Integer | OpAdd | OpMul |OpSub
> deriving (Eq, Ord, Show)
> type Stk = [Integer]

We can also write an ‘interpreter’ for this stack-based language. First, we write the function that interprets a single stack operation with a given stack and returns a new stack. For clarity sake, I have not included error code for when the stack is empty but numbers are required.


> interpret :: Stk -> Op -> Stk
> interpret s (OpPush i) = i:s
> interpret (a:b:s) OpAdd = (a+b):s
> interpret (a:b:s) OpSub = (a-b):s
> interpret (a:b:s) OpMul = (a*b):s

To run a set operations, one can simply fold over the list of operations, starting with an empty stack:


> run :: [Op] -> Stk
> run = foldl interpret []

Next, we define the compiler function. This compiles algebraic expressions to a list of stack operations. Notice to do this, first we calculate the two sub expressions, and then compile the operation in question:


> compile :: Exp -> [Op]
> compile (Simple i) = [OpPush i]
> compile (Mul a b) = compile b ++ compile a ++ [OpMul]
> compile (Add a b) = compile b ++ compile a ++ [OpAdd]
> compile (Sub a b) = compile b ++ compile a ++ [OpSub]

The code is now done, and in fact, one can simply type ‘ghci Alg.lhs” and try it out. However, we will add a quickcheck instance so we can test the correctness of the compiler. Simply, we require that interpreting an expression yields the same result as the top of the stack after compiling and interpreting the stack operations. To enable this, we first need to define a quickcheck instance for the domain, namely algebraic expressions. The code is a bit more complicated as it makes sure that it never generates infinite expression trees, so I will not explain it in detail. I suggest for those interested to check The quickcheck manual, or the haskell documentation.


> instance Arbitrary Exp where
> arbitrary = sized tree'
> where tree' 0 = liftM Simple arbitrary
> tree' n | n > 0 =
> oneof[liftM Simple arbitrary,
> liftM2 Mul subtree subtree,
> liftM2 Add subtree subtree,
> liftM2 Sub subtree subtree]
> where subtree = tree' (n `div` 2)
> coarbitrary (Simple i) =
> variant 0 . coarbitrary i
> coarbitrary (Mul a b) =
> variant 1 . coarbitrary a . coarbitrary b
> coarbitrary (Add a b) =
> variant 2 . coarbitrary a . coarbitrary b
> coarbitrary (Sub a b) =
> variant 3 . coarbitrary a . coarbitrary b

Now that we have an implementation that generates arbitrary algebraic expressions, it’s time to write our test case. Namely we always require (True ==>), that the result of interpretation of the algebraic expression is the same as the top of the stack after compiling and interpreting the stack operations. We could add an additional requirement that the stack only has 1 element remaining in it.


> prop_compile tree = True ==> (head $ run $ compile tree) == interpretExp tree

Well, I hope that was useful :)

A friend of mine suggested I add some examples. Once you have saved the above in a file named Alg.lhs, load it up in the interpreter with ‘ghci Alg.lhs’. Then you try it out:


> interpretExp (Add (Mul (Simple 5) (Simple 4)) (Simple 3))
23
> compile (Add (Mul (Simple 5) (Simple 4)) (Simple 3))
[OpPush 3,OpPush 4,OpPush 5,OpMul,OpAdd]
> let x = [OpPush 3,OpPush 4,OpPush 5,OpMul,OpAdd] in run x
[23]

Cheers!

As final note, please feel free to leave comments or questions.