Applicative logic

Note: You can find the functions below in the module Control.Applicative.Logic (GitHub, Hackage).

The following is an exploration of a few functions I found while writing various Haskell programs over the years. Their names collide with some standard function in Prelude, which is unfortunate, and while the new functions cannot be used as drop-in replacements of the prelude functions, they are morally generalisations. Also, note that the order I present my insights here are almost the exact opposite of the order in which I “discovered” them. I say “discovered” because I am presumably not the first one to discover these as they are very general. In fact, some of them are already in the standard library (albeit under a different name).

tl;dr: Many functions involving booleans can be generalised to involve (Alternative f, Monoid a) => f a instead.

A boolean is maybe true

We will start our exploration with a very inane observation. It is essentially the observation that 1+1=2, which every child discover some time before the age of five. As mentioned, this is the final “insight” I had, which tied all the pieces together.

There it is! The equality sign with the squiggle over it means “isomorphic” which is a fancy way of saying “is essentially the same as” which for Haskell types mean that there are translation functions back and forth which are mutual inverses. So, in theory, any place you use a Bool you can use a Maybe () value. Just replace True with Just () and False with Nothing.

Digression: “Well, actually…” Alright, you clever little imp! I know what you want to say. Haskell semantics is Complicated™. And there are in fact differences between Bool and Maybe (). For instance, Just undefined does not really have a counterpart in Bool. An “isomorphism” could map it to either undefined :: Bool or True :: Bool, but they are both in a sense taken. But if your program depends on the exact structure of non-total elements of Bool, you deserve to live in the purgatory you have created.

But why?

Bool is a fine type. Very useful. In fact, it gets special treatment in by the compiler. Only Bools can be used in if-expressions and guards. So, this is not a suggestion to replace Bool with Maybe () if your program works well with Bool. The purpose is rather to recognise that some of the things done to booleans can be done to other structures as well. And the core of this stems from how Maybe () consists of two parts: Maybe which is an Applicative, Alternative functor and () which is a (admittedly trivial) Monoid. We wil now take some of the well-known functions involving Bool and bring them to this level of generality. Then by replacing Maybe and () with other Applicative, Alternative functors and Monoids, these functions will find new use cases.

Disjunction

Let us start by talking about disjunction, usually conceived as (||) :: Bool -> Bool -> Bool. But there is a typeclass called Alternative with an operator (<|>) :: (Alternative f) => f a -> f a -> f a which works like disjunction when we apply it to Maybe (): We get Just () <|> _ = Just () (true or anything is true) and likewise _ <|> Just () = Just () and finally Nothing <|> Nothing = Nothing (False or false is false). But the operator has many uses. For lists it is simply concatenation, and the operator is essential when writing parsers. The disjunctive unit (i.e. false) is called empty :: (Alternative f) => f a.

This is well-trodden stuff. But I think it is nice to highlight. For instance, if you have something where you get a lot of Maybe-values, perhaps in a list, and you just want to pick the first just value, you can use or = foldr (<|>) empty to convert [Maybe a] -> Maybe a.

or :: (Foldable t, Alternative f) => t (f a) -> f a
or = foldr (<|>) empty

This is clearly a generalisation of or :: (Foldable t) => t Bool -> Bool, but it is also a generalisation of concat :: [[a]] -> [a]. In Control.Applicative you will find this under the name asum and it is very useful!

any

While disjunction is useful, the reason I often end up using or to flatten something of type t (f b) to f b is because I first had t a and a predicate a -> f b. So, let us combine those two steps into a single, beautiful function:

any :: (Alternative f, Foldable t) => (a -> f b) -> t a -> f b
any = ($ empty) . foldr . ((<|>) .)

A very simple usage of this function is to convert from any foldable structure to any alternative functor using any pure. For instance a x <- any pure (Map.lookup i m) in a do-block will lookup a value in a map and rewrap it into your current monad (as long as it is Alternative). In fact any pure is a general conversion function which can convert from any of these:

Apropos the last entry in that list, any string ["foo","bar","bat"] is a parser which matches any of the words in the list. Over in ConcurrencyLand, any readTChan [chan0,chan1,chan2] will read the first value arriving in any of the three channels.

ghci> import Control.Applicative.Logic (any)
ghci> import Control.Monad (forever)
ghci> import Control.Concurrent (forkIO)
ghci> import Control.Concurrent.STM
ghci> import Control.Concurrent.STM.TChan

ghci> -- Create the channels
ghci> chan0 <- newTChanIO :: IO (TChan String)
ghci> chan1 <- newTChanIO :: IO (TChan String)
ghci> chan2 <- newTChanIO :: IO (TChan String)
ghci>
ghci> -- Create a thread reading from any chan:
ghci> forkIO $ forever
             $ atomically (readTChan `any` [chan0,chan1,chan2])
                 >>= putStrLn
ThreadId 689

ghci> -- Now we can write to any of the channels:
ghci> atomically $ writeTChan chan1 "Foo"
Foo
ghci> atomically $ writeTChan chan0 "Bar"
Bar
ghci> atomically $ writeTChan chan2 "Baz"
Baz

The moral is that you can use this generalised any in many places where the word any would fall natural to use informally.

Conjunction

Having gone on and on about disjuntion, I should talk about conjunction. There might some wiggle room for what notion of conjunction best fits, but my experience from a lot of examples suggest that the following is practical:

(&&) :: (Applicative f, Monoid a)
     => f a -> f a -> f a
(&&) = liftA2 (<>)

Why Monoid? The idea is that && combines two generalised truth values. The a argument to f represents evidence of truth (say, a set of solutions, or results from a search or something). Thus, if a conjunction is true we must take into account the evidence from both sides. One option would be to instead use liftA2 (,) :: f a -> f b -> f (a,b), in a kind I-know-Curry–Howard way. But that will not really generalise to a function similar to any, where we collect evidence from a whole structure of elements. Thus, the Monoid alternative seems more useful in practice.

You can probably imagine uses for && yourself, so let us get off the ground by defining and:

and :: (Foldable t, Applicative f, Monoid a)
    => t (f a) -> f a
and = foldr (&&) (pure mempty)

As you can see pure mempty is the new True, otherwise only the type signature changed from the Bool definition. But what can we do with it? Let us start with a combinatorics example: Say we want to generate all sentences of the form “Harry/Sue loves/hates kale/honey”. Here is a solution:

Alright, I could not resist sneaking in an early “all”s in that. Stay tuned for it the next subsection, but ignore it for the moment, and let us focus on “and”. This example is standard list monad stuff, but the and function lets us easily generate combinations from lists of alternatives.

all

We have already seen one use of the generalised all, namely applying an IO function to every element of a list: all print [1..10]. But there already exists plenty of functions doing that. Can we do something else? Just pick your faviourite Applicative and start experimenting. Picking STM for instance, we can wait until a moment when all channels have something ready and get that using all ((singleton <$>) . readTChan) [chan0,chan1,chan2] :: STM [a]. Or for IO one can all readFile :: [FilePath] -> IO String to read list of files into a single string.

all :: (Applicative f, Monoid b, Foldable t)
    => (a -> f b) -> t a -> f b
all = ($ pure mempty) . foldr . ((&&) .)

Notice that guard :: (Alternative f) => Bool -> f () converts a standard bool to an applicative truth value. Hence all guard :: (Alternative f, Foldable t) => t Bool -> f () can be used where one would use and normally. For instance, here is a function which checks if a list is sorted:

ascending :: (Alternative f, Ord b) => [b] -> f ()
ascending l = all guard $ zipWith (<=) l (tail l)

Extended example

Here is a simple example where you can see a few usages of the applicative logic functions in context. It is simply a game of tic-tac-toe, but it demonstrates a few usages and the general intuition of any, or, all, and and convert.

import Control.Monad (guard)
import Control.Applicative
import qualified Data.Map as Map
import Data.Map (Map)
import Data.Functor (($>))

import System.Random (randomRIO)

import Prelude hiding (any, all, or)
import Control.Applicative.Logic (any, all, or, convert)

-- Game data
data Mark = X | O
  deriving (Eq,Show)

type Position = (Integer,Integer)

type Board = Map Position Mark

isValidMove :: Board -> Position -> Bool
isValidMove board (x,y) =  0 <= x && x <= 2
                        && 0 <= y && y <= 2
                        && null (Map.lookup (x,y) board)

-- All positions on the board
allPositions :: [Position]
allPositions = liftA2 (,) [0..2] [0..2]

-- Make a move on the board
move :: Board -> Position -> Mark -> Maybe Board
move board pos m = guard (isValidMove board pos)
                $> Map.insert pos m board

-- Verify who has won
won :: Board -> Maybe Mark
won board = any filled streaks where
    -- Generate all streaks
    streaks = do
          x <- allPositions
          y <- filter (x<) allPositions
          z <- filter (y<) allPositions
          check [x,y,z]
          pure [x,y,z]
    -- Check that three positions form a streak
    check l = do
              guard (mod (sum (fst <$> l)) 3 == 0)
              guard (mod (sum (snd <$> l)) 3 == 0)
              ascending (snd <$> l) <|> decending (snd <$> l)
    -- Verify that a player has filled a streak
    filled streak = do
        marks <- traverse (`Map.lookup` board) streak
        m <- any pure marks
        all (guard . (==m)) marks
        pure m
    -- Utility functions
    ascending l = all guard $ zipWith (<=) l (tail l)
    decending l = all guard $ zipWith (>=) l (tail l)

-- Game playing logic

main :: IO ()
main = gameLoop X (Map.empty :: Board)

gameLoop :: Mark -> Board -> IO ()
gameLoop currentMark board = do
    putStrLn "Current board:"
    printBoard board
    or
      [ do mark <- convert (won board)
           putStrLn $ "Player " ++ show mark ++ " wins!"
      , guard (Map.size board == 9) *> putStrLn "It's a draw!"
      , guard (currentMark == X)    *> moveIO board X userMove
                                   >>= gameLoop O
      , guard (currentMark == O)    *> moveIO board O computerMove
                                   >>= gameLoop X ]

moveIO :: Board -> Mark -> (Board -> IO Position) -> IO Board
moveIO board mark play = do
   pos <- play board
   convert (move board pos mark)
       <|> (do putStrLn "Position not in range!"
               moveIO board mark play)

userMove :: Board -> IO Position
userMove board = do
    putStrLn "Enter your move (row column):"
    input <- getLine
    case words input >>= reads :: [(Integer,String)] of
       [(x,""),(y,"")] -> pure (x,y)
       _ -> do
              putStrLn "Invalid input, please use the format 'row column'."
              userMove board

randomValidMove :: Board -> IO Position
randomValidMove board = do
    let validMoves = filter (isValidMove board) allPositions
    idx <- randomRIO (0, length validMoves - 1)
    pure $ validMoves !! idx

computerMove :: Board -> IO Position
computerMove board = do
    pos <- randomValidMove board
    putStrLn $ "Computer places " ++ show O ++ " at " ++ show pos
    pure pos

printBoard :: Board -> IO ()
printBoard board
  = all putStrLn [ unwords [ maybe "." show
                                   $ Map.lookup (x,y) board
                   | y <- [0..2]]
                   | x <- [0..2]]

Highlights of the extended example

Let me highlight a few usages of applicative logical function in the above code. The first and most striking part is the check-if-board-is-won function:

won :: Board -> Maybe Mark
won board = any filled streaks

This uses Maybe Mark as a proof-relevant truth value for any. Instead of just True when the board is won we get Just X or Just O, depending on which player won. And the code simply says that the board is won if there are any filled streaks (of three board positions in a row).

filled :: [Position] -> Maybe Mark
filled streak = do
    marks <- traverse (`Map.lookup` board) streak
    m <- any pure marks
    all (guard . (==m)) marks
    pure m

The filled function uses both any and and to check that a list of board possitions are filled with the same mark. First it uses traverse to check that all the positions of streak are filled with something on the current boar and collects them in a list. Then m <- any pure marks picks out the first mark of the streak and all (guard . (==m)) marks verifies that the remaining marks of the streak are all the same.

While it does not use any of the applicative logic functions directly, the code for generating all streaks is a nice example of thinking of applicative values as propositions:

streaks :: [[Position]]
streaks = do
        x <- allPositions
        y <- filter (x<) allPositions
        z <- filter (y<) allPositions
        check [x,y,z]
        pure [x,y,z]

This all happens in do-syntax for lists, and the first three lines are self-explanatory. The check function however is a predicate which checks if three positions form a streak (are in a row on the board). It is converted from Bool with heavy usage of guards:

check l = do
            guard (mod (sum (fst <$> l)) 3 == 0)
            guard (mod (sum (snd <$> l)) 3 == 0)
            ascending (snd <$> l) <|> decending (snd <$> l)

gameLoop :: Mark -> Board -> IO ()
gameLoop currentMark board = do
    putStrLn "Current board:"
    printBoard board
    or
      [ do mark <- convert (won board)
           putStrLn $ "Player " ++ show mark ++ " wins!"
      , guard (Map.size board == 9) *> putStrLn "It's a draw!"
      , guard (currentMark == X)    *> moveIO board X userMove
                                   >>= gameLoop O
      , guard (currentMark == O)    *> moveIO board O computerMove
                                   >>= gameLoop X ]

I am not sure this is actually a sane way do conditionals in IO, but it works. The or [⋯] part is interesting because it attempts to execute the elements of the list in order and stops once one of the steps succeeds. So, for instance:

do mark <- convert (won board)
   putStrLn $ "Player " ++ show mark ++ " wins!"

Will fail if no player has won yet. The Applicative.Logic.convert function converts the Maybe Mark into IO Mark, throwing an exception on Nothing, so the putStrLn part will only run if someone actually won. Otherwise, it will continue with checking for a draw, or letting one of the players move.

The move :: Board -> Position -> Mark -> Maybe Board function integrates the check of validity with the updating of the board. In the IO part again we use convert (aka any pure) to get an IO value of the updated board, and use disjunction for error handling:

moveIO :: Board -> Mark -> (Board -> IO Position) -> IO Board
moveIO board mark play = do
   pos <- play board
   convert (move board pos mark)
       <|> (do putStrLn "Position not in range!"
               moveIO board mark play)

The final little bit of niceness is to use all instead of mapM_ to print each row of the board on a separate line: