note to self: löb and möb

Working through the detail of Löb and möb: strange loops in Haskell and the related discussion on, in particular psygnisfive’s comment. There’s nothing much original in this post, I’m just working through the details.

The LHS source for this post is here:

> module Loeb where

In a spreadsheet one has a set of cells, and each cell can be defined in terms of values in the other cells. For example, let’s use four cells x0, x1, x2, and x3 with the following definition:

> f1 :: [Int]
> f1 = let xs0 = 1
>          xs1 = succ xs0
>          xs2 = succ xs1
>          xs3 = succ xs2
>          xs  = [xs0, xs1, xs2, xs3]
>          in xs

The variable xs0 appears in a few places but it can be factored out. Remove xs0 = 1 and substitute the value 1 in the definition for xs. Also, xs0 is the first element of the xs list, so refer to it using xs !! 0:

> f2 :: [Int]
> f2 = let xs1 = succ (xs !! 0)
>          xs2 = succ xs1
>          xs3 = succ xs2
>          xs = [1, xs1, xs2, xs3]
>          in xs

Now do the same for xs1:

> f3 :: [Int]
> f3 = let xs2 = succ (xs !! 1)
>          xs3 = succ xs2
>          xs = [1, succ (xs !! 0), xs2, xs3]
>          in xs

The pattern should be clear, so now factor out xs2 and xs3:

> f4 :: [Int]
> f4 = let xs = [ 1
>               , succ (xs !! 0)
>               , succ (xs !! 1)
>               , succ (xs !! 2)
>               ]
>          in xs

The common feature of the last three lines is that they are a function of xs. The first line is the constant 1, and we can make this a function of xs with something like

> _ -> 1

but the standard prelude provides const 1 for just this purpose. So now we have:

> f4_1 :: [Int]
> f4_1 = let xs = [ const 1 $ xs
>                 , succ (xs !! 0)
>                 , succ (xs !! 1)
>                 , succ (xs !! 2)
>                 ]
>          in xs

So each line is a function of xs. Can we factor it out, in a sense, so each line looks more like the first? Yes:

> f4_2 :: [Int]
> f4_2 = let xs = [ const 1 $ xs
>                 , succ . (h -> h !! 0) $ xs
>                 , succ . (h -> h !! 1) $ xs
>                 , succ . (h -> h !! 2) $ xs
>                 ]
>          in xs

The lambda expressions are a bit cumbersome. What we are doing is the succ function after selecting a certain element of a list. Haskell supports currying, and when one curries an operator, the left vs right arguments are respected:

*Main> :t (!!)
(!!) :: [a] -> Int -> a

*Main> :t (!! 3)
(!! 3) :: [a] -> a

So succ (xs !! 0) can be rewritten as succ . (!! 0) $ xs. Here is the next version:

> f5 :: [Int]
> f5 = let xs = [ const 1       $ xs
>               , succ . (!! 0) $ xs
>               , succ . (!! 1) $ xs
>               , succ . (!! 2) $ xs
>               ]
>         in xs

We can still ask if there is a way to generalise the definition of f5. Each line is of the form function $ xs so we could define a list of functions

> fs = [ const 1
>      , succ . (!! 0)
>      , succ . (!! 1)
>      , succ . (!! 2)
>      ]

and then xs = map (-> f xs) fs. In full:

> f6_1 :: [Int]
> f6_1 = let fs = [ const 1
>                 , succ . (!! 0)
>                 , succ . (!! 1)
>                 , succ . (!! 2)
>                 ]
>            xs = map (f -> f xs) fs
>            in xs

Finally, the lambda expression is a bit clunky and Haskell provides the dollar-sign operator for function application (which is all the lambda expression is actually doing). With currying we get an appropriate type:

*Main> :t ($)
($) :: (a -> b) -> a -> b

*Main> :t ($ [1, 2, 3])
($ [1, 2, 3]) :: Num t => ([t] -> b) -> b

so ($ xs) will be a function that takes a function that operates on a list and returns something (as long as xs is a list). This is just what we need:

> f6_2 :: [Int]
> f6_2 = let fs = [ const 1
>                 , succ . (!! 0)
>                 , succ . (!! 1)
>                 , succ . (!! 2)
>                 ]
>            xs = map ($ xs) fs
>           in xs

and this is the final form in psygnisfive’s comment.

(Embarrassingly for myself, I had assumed that the type of (!! xs) would be the result of currying on its left-hand parameter, not the right, which made the map ($ xs) fs form incomprehensible.)

To finish things off, we’d like to write a function that computes the result f6_2 given the list fs. Here’s a first attempt:

> loeb1 fs = let xs = map ($ xs) fs in xs

An alternative to using a let definition is to use a where (this brings us closer to the form given by quchen):

> loeb2 fs = go where go = map ($ go) fs

Looking at the type of loeb2,

> loeb2 :: [[b] -> b] -> [b]

shows the fact that we used a list as the starting point for the derivation. The first parameter is a list of functions that take a list and produce a value (of the same type), and the result is list. The final remark in psygnisfive’s comment is “rinse and repeat for your favourite functor.” What this refers to is the fact that map is specialised for lists. Functors generalise the idea of being able to “map over” something, and fmap generalises map:

*Main> :t map
map :: (a -> b) -> [a] -> [b]

*Main> :t fmap
fmap :: Functor f => (a -> b) -> f a -> f b

*Main> map (+2) [1, 2, 3]

*Main> fmap (+2) [1, 2, 3]

*Main> :m Data.Maybe

Prelude Data.Maybe> fmap (+1) (Just 3)
Just 4

Prelude Data.Maybe> fmap (+1) Nothing

Changing map to fmap in the definition of loeb2 gets us the actual definition of loeb:

> loeb :: Functor f => f (f b -> b) -> f b
> loeb fs = go where go = fmap ($ go) fs

For what it’s worth, putting f = [] specialises to the type signature of the earlier loeb2:

> loeb :: [] ([] b -> b) -> [] b

which can be rewritten in the usual form

> loeb :: [[b] -> b] -> [b]

It doesn’t end! You can then abstract out the fmap by making it a parameter, which gives the moeb function:

> moeb :: t -> (((a -> b) -> b) -> t -> a) -> a
> moeb fs x = go where go = x ($ go) fs

See the discussion on reddit for motivation and possible uses of moeb.

Tic-tac-toe and Haskell type classes

(Literate Haskell source for this post is here:

In a blog post in 2011 Tony Morris set an exercise to write an API for the game tic-tac-toe that satisfies these requirements:

  1. If you write a function, I must be able to call it with the same arguments and always get the same results, forever.
  2. If I, as a client of your API, call one of your functions, I should always get a sensible result. Not null or an exception or other backdoors that cause the death of millions of kittens worldwide.
  3. If I call move on a tic-tac-toe board, but the game has finished, I should get a compile-time type-error. In other words, calling move on inappropriate game states (i.e. move doesn’t make sense) is disallowed by the types.
  4. If I call takeMoveBack on a tic-tac-toe board, but no moves have yet been made, I get a compile-time type-error.
  5. If I call whoWonOrDraw on a tic-tac-toe board, but the game hasn’t yet finished, I get a compile-time type-error.
  6. I should be able to call various functions on a game board that is in any state of play e.g. isPositionOccupied works for in-play and completed games.
  7. It is not possible to play out of turn.

I remember when I first saw this list of rules that numbers 3 and 4 stood out to me. How on earth could it be possible to make these compile-time errors?

In Python the standard implementation for a tic-tac-toe game would use a class containing the board state along with methods move, takeMoveBack, and so on. Calling one of these functions with an invalid state would throw an exception:

class TicTacToe:

    def move(self, position):
        if self.game_finished():
            raise ValueError, "Can't move on a finished board."

    def takeMoveBack(self, position):
        if self.is_empty_board():
            raise ValueError, "Can't take back a move on an empty board."

A crazy user of the TicTacToe API might write code like this (intentionally or not):

t = TicTacToe()

t.move('NW') # player 1 marks the North-West square

if random.random() < 1e-10:
    print t.whoWonOrDraw() # raises an exception as the game is not finished

There are ways to solve this problem in C#, F#, OCaml, Java, Scala, and Haskell. Of those langauges I am most familiar with Haskell so the following will focus exclusively on a solution using Haskell’s type classes.

Solving the tic-tac-toe problem requires a bit of code for dealing with the rules of the game itself, but what I want to focus on is how to enforce rules like 3 and 4 in a small system. So here is a reduced problem:

  1. The system has two states: 0 and 1.
  2. In either state, the system stores a single Integer.
  3. The only valid transition is from state 0 to state 1. Attempting to move from state 1 to state 0 should be a compile-time error.
  4. In either state, we can call pprint to get a String representation of the state.

First, define data types for the two states:

> {-# LANGUAGE MultiParamTypeClasses, FunctionalDependencies #-}
> module TicTacToe where
> data State0 = State0 Int deriving Show
> data State1 = State1 Int deriving Show

Now create a class StateLike to enforce the definition of a pretty-printing function pprint:

> class StateLike b where
>     pprint :: b -> String
> instance StateLike State0 where
>     pprint (State0 n) = "Initial state; " ++ show n
> instance StateLike State1 where
>     pprint (State1 n) = "Final state; " ++ show n

In ghci:

*TicTacToe> pprint $ State0 42
"Initial state; 42"
*TicTacToe> pprint $ State1 59
"Final state; 59"

There’s nothing too fancy so far.

Next we need to enforce rule 3, which says that the only transition is from state 0 to state 1. We would like to write

> class Transition where
>   move :: Int -> State0 -> State1

but this does not define a class and ghci complains accordingly:

    No parameters for class `Transition'
    In the class declaration for `Transition'

We can make this a class by replacing State0 and State1 with variables:

> class Transition a b where
>   move :: Int -> a -> b

but this still doesn’t make ghci happy. Previously we had no free variable and now we have two, so being a little bit psychic we can can add a functional dependency to indicate that b is completely determined by a:

> class Transition a b | a -> b where
>   move :: Int -> a -> b

This code will now compile. Finally, we provide an instance for Transition State0 State1:

> instance Transition State0 State1 where
>     move i (State0 n) = State1 (n + i)

where the new state’s integer component is just the addition of the previous state and the parameter i supplied to move.

Now we check each of the rules:

  1. Rule: The system has two states: 0 and 1.

    We defined the two data constructors State0 and State1:

    *TicTacToe> State0 10
    State0 10
    *TicTacToe> State1 20
    State1 20
  2. Rule: In either state, the system stores a single Integer.

    We stored 10 and 20 in the previous answer.

  3. Rule: The only valid transition is from state 0 to state 1. Attempting to move from state 1 to state 0 should be a compile-time error.

    Attempting to make a move from State0 is acceptable, and returns a State1:

    *TicTacToe> :t move 3 (State0 42)
    move 3 (State0 42) :: State1
    *TicTacToe> pprint $ move 3 (State0 42)
    "Final state; 45"

    Attempting to make a transition from State1 results in a type error which can be picked up at compile-time:

    *TicTacToe> move 4 (move 3 (State0 42))
        No instance for (Transition State1 to0)
          arising from a use of `move'
        Possible fix:
          add an instance declaration for (Transition State1 to0)
        In the expression: move 4 (move 3 (State0 42))
        In an equation for `it': it = move 4 (move 3 (State0 42))
  4. Rule: In either state, we can call pprint to get a String representation of the state.

    Yes, for example:

    *TicTacToe> pprint $ State0 10
    "Initial state; 10"
    *TicTacToe> pprint $ State1 20
    "Final state; 20"

If I’m correct, this is the way that we can enforce rules 3 and 4 of the tic-tac-toe problem. This idea may be useful in other situations. For example, a scientific workflow system could enforce, at compile time, the constraint that a node is connected to a data source and a data sink. Or a shopping cart API could make sure that you could not go to the checkout on an empty cart.

Here is the full source code for my two state example:

> {-# LANGUAGE FunctionalDependencies, FlexibleInstances #-}
> data State0 = State0 Int deriving Show
> data State1 = State1 Int deriving Show
> class StateLike b where
>     pprint :: b -> String
> instance StateLike State0 where
>     pprint (State0 n) = "Initial state; " ++ show n
> instance StateLike State1 where
>     pprint (State1 n) = "Final state; " ++ show n
> initialState = State0 34
> class Transition from to | from -> to where
>   move :: Int -> from -> to
> instance Transition State0 State1 where
>     move i (State0 n) = State1 (n + i)

Thinking more generally, we can encode a finite state system using type classes. Here is code for a system with states 0, 1, 2, 3, 4, and admissible transitions

  • 0 → 1
  • 0 → 2
  • 0 → 3
  • 1 → 4
  • 4 → 1
> data FState0 = FState0 Int deriving Show
> data FState1 = FState1 Int deriving Show
> data FState2 = FState2 Int deriving Show
> data FState3 = FState3 Int deriving Show
> data FState4 = FState4 Int deriving Show
> class FStateLike b where
>     fsPPrint :: b -> String
> instance FStateLike FState0 where
>     fsPPrint (FState0 n) = "FState0; " ++ show n
> instance FStateLike FState1 where
>     fsPPrint (FState1 n) = "FState1; " ++ show n
> instance FStateLike FState2 where
>     fsPPrint (FState2 n) = "FState2; " ++ show n
> instance FStateLike FState3 where
>     fsPPrint (FState3 n) = "FState3; " ++ show n
> instance FStateLike FState4 where
>     fsPPrint (FState4 n) = "FState4; " ++ show n
> class Transition1 a b | a -> b where
>     transition1 :: a -> b
> class Transition2 a b | a -> b where
>     transition2 :: a -> b
> class Transition3 a b | a -> b where
>     transition3 :: a -> b
> class Transition4 a b | a -> b where
>     transition4 :: a -> b
> class Transition5 a b | a -> b where
>     transition5 :: a -> b
> instance Transition1 FState0 FState1 where
>     transition1 (FState0 n) = FState1 n
> instance Transition2 FState0 FState2 where
>     transition2 (FState0 n) = FState2 n
> instance Transition3 FState0 FState3 where
>     transition3 (FState0 n) = FState3 n
> instance Transition4 FState1 FState4 where
>     transition4 (FState1 n) = FState4 n
> instance Transition5 FState4 FState1 where
>     transition5 (FState4 n) = FState1 n
> -- OK:
> test1 :: FState1
> test1 = transition5 $ transition4 $ transition1 $ FState0 42
> -- Not ok, compile-time error:
> -- test2 = transition4 $ transition2 $ FState0 42

You can do a lot with Haskell’s type system. In Issue 8 of The Monad.Reader Conrad Parker wrote a complete type-level program for the Instant Insanity game. Wow.

One final comment. Referring to the tic-tac-toe exercise, Tony wrote:

Recently I set a task, predicted how difficult it would be, then was astonished to find that it appears to be significantly more difficult than I had originally predicted. I’m still not sure what is going on here, however, I think there are some lessons to be taken.

Personally, I would have found the tic-tac-toe exercise easy if was prefaced with “Haskell’s type classes can enforce the permissible transitions of a finite state system.” But most tutorials on type classes use fairly benign examples like adding an Eq instance for a new Color class. It’s a novel idea to deliberately not provide an instance for a certain class to stop an end-user of an API from making certain transitions in a state diagram. It’s novel to even think of encoding a state diagram using a language’s type system, especially after spending years working with languages with relatively weak type systems.

Further reading:

Archived Comments

Date: 2017-01-31 08:38:03.281378 UTC

Author: Nick Hamilton

I like your demonstration of encoding state with type classes, but it seems using this mechanism to solve Tony’s challenge will result in a tonne of boilerplate? Over a hundred if you find a way to encode mirrored states, otherwise… thousands. Further to that, do you have any thoughts how the ‘api’ user would know which transition function (of the hundred+) to call?

I had a crack at solving the challenge, but I used the undecidable instances and flexible contexts extensions to create recursively unwrap a nested type containing each of the states.

Debian Wheezy on X1 Carbon

This would be a chef/puppet recipe if I had to do this kind of installation
more frequently.

Kernel configuration:

Installation notes: The copy on github will be the latest, not this blog post.

# Notes for building Debian Wheezy from scratch
# on my Lenovo Carbon X1 ultrabook.

# Put a copy of the iwlwifi package on a USB stick
# so that the installation program can get onto the
# network:

# Do a normal install using the amd64 DVD-1 ISO image, copied
# to a USB stick using dd. Set the boot methods in the BIOS
# to "legacy only". Beware that changing this option can break
# an existing installation!


echo 'source $HOME/work/bin/bash-aliases-x1' >> $HOME/.bashrc

# edit /etc/apt/sources.list as follows:

deb stable main contrib non-free
deb wheezy-updates main contrib non-free
deb wheezy/updates main contrib non-free
deb wheezy contrib

# Virtualbox key.
wget -q -O- | sudo apt-key add -

# Commonly used packages.
sudo apt-get update
sudo apt-get install unison2.32.52-gtk meld vim-gtk build-essential git colordiff ghc rsync sshfs xinput virtualbox-4.3 ipython python-nose python-networkx python-setuptools python-numpy python-scipy graphviz ecryptfs-utils cryptsetup pavucontrol screen durep baobab keepassx xinput htop transmission-gtk gnupg vlc mplayer gstreamer0.10-plugins-base gstreamer0.10-plugins-good gstreamer0.10-fluendo-mp3 gstreamer0.10-ffmpeg calibre conky-all gqview libjpeg-progs tcsh inkscape

sudo adduser carlo vboxusers

sudo apt-get install apt-file
sudo apt-file update

# Encrypt home directory if installer didn't do so.
ecryptfs-migrate-home -u carlo

# Google chrome.
sudo dpkg -i Downloads/google-chrome-stable_current_amd64.deb

# Skype.
sudo dpkg --add-architecture i386
sudo apt-get update
sudo dpkg -i Downloads/skype-debian_4.2.0.11-1_i386.deb
sudo apt-get -f install

# Skype headset configuration. Start a test call, set
# recording and output of the Skype application (in pavucontrol)
# to the Plantronics headset.
pavucontrol &
skype &

# Thunderbird binary tarball
sudo apt-get install ia32-libs-gtk # otherwise errors about xul library

# Why I can't change this setting, I have no idea:
#     $ grep firefox .thunderbird/l3fwjt8m.default/*js
#     user_pref("", "/opt/firefox/firefox");
#     user_pref("", "/opt/firefox/firefox");
#     user_pref("", "/opt/firefox/firefox");
# so here's an ugly hack:

sudo mkdir -p /opt/firefox
sudo ln -s /usr/bin/google-chrome /opt/firefox/firefox

# Dropbox
sudo dpkg -i d/dropbox_1.6.0_amd64.deb

# GHC and Haskell Platform:

sudo apt-get install ghc libncurses5 libncurses5-dev
cd ~/opt
rm -fr ghc-7.6.3_build/*
cd ghc-7.6.3
make clean
./configure --prefix=$HOME/opt/ghc-7.6.3_build
make && make install
echo 'export PATH=$HOME/opt/ghc-7.6.3_build/bin:$PATH' >> $HOME/.bashrc
# Get a new shell or set the $PATH manually.
cd ..

sudo apt-get install libgl1-mesa-dev                    
                     libglw1-mesa libglw1-mesa-dev
sudo apt-get install happy alex
sudo rm -fr haskell-platform-2013.2.0.0_build/*
cd haskell-platform-2013.2.0.0
make clean
./configure --prefix=$HOME/opt/haskell-platform-2013.2.0.0_build/
make && make install
echo 'export PATH=$HOME/opt/haskell-platform-2013.2.0.0_build/bin:$PATH' >> $HOME/.bashrc
# get a new shell or set the $PATH manually

# Cabal:
cabal update
cabal install cabal-install
echo 'export PATH=$HOME/.cabal/bin:$PATH' >> ~/.bashrc
# get a new shell...

# XMonad
sudo apt-get install libxrandr-dev trayer
cabal update
cabal install xmonad xmonad-contrib xmonad-extras xmonad-utils

# Edit /usr/share/xsessions/xmonadcarlo.desktop

[Desktop Entry]
Comment=This session starts xmonad

# As normal user:
xmonad --recompile

# Newer kernel:
sudo apt-get install libncurses5 libncurses5-dev kernel-package
cd ~/opt
wget -c
cd /usr/src
sudo su -
tar Jxf /home/carlo/opt/linux-3.11.6.tar.xz
cd linux-3.11.6
make mrproper
make clean
wget -O .config
make oldconfig
make-kpkg --rootcmd fakeroot --config menuconfig --initrd --us --uc -j 4 kernel_image
cd ..
dpkg -i linux-image-3.11.6_3.11.6-10.00.Custom_amd64.deb

# Reboot, check that the built-in webcam works.


## minc toolkit
# git clone FIXME
sudo apt-get install cmake cmake-curses-gui
cd minc-toolkit
rm -fr build
mkdir build
cd build
ccmake ..  # hit 'c'
           # go down to MT_BUILD_SHARED_LIBS, hit enter to turn 'ON'
           # hit 'c'
           # hit 'g'
sudo make install

## pyminc
# git clone FIXME
cd pyminc
sudo python install

## nipype
sudo pip install nibabel
sudo pip install traits traitsui
cd nipype
sudo rm -fr build && sudo python install

# Python things

sudo python
sudo pip install youtube-dl