Planet Haskell

February 06, 2016

Douglas M. Auclair (geophf)

Graphing with Goats

Slides, presented comme ça! Links at the end. Presentation posted on youtube of the meetup.



1


2


3 (I am known for teh kittehs)


4 (graphs-я-borin' is another talk I gave at SanFran GraphConnect 2015)


5. The Beach (not Plastic)


6


7


8. ACID means something very important to DBMSes(eses)(eses)


9. neo4j Graph of Amino Acids (data table, Haskell code)


(geddit? links to linkurio.us? geddit?)


11. "sed-butt, sed-butt, sed-butt" my daughters chant around the house all day

Now: Graph-applications:


12. Social Media


13. The Markets


14. The Markets (again) / Managing Complexity


15. Search / (Fraud) Detection


16. Scoping / (Requirements) Analysis


17. Clustering


18. Errybody say: "YAAAAAAYYYYYY!"


19. Links, en-text-ified:

20. Buh-bay!

by geophf (noreply@blogger.com) at February 06, 2016 03:43 PM

servant

Announcing servant-swagger and swagger2

<section class="level2" id="swagger">

Swagger

Servant is not the first project to provide a unified way of documenting APIs. There is API Blueprint, RAML, Apiary, and finally swagger. While these Web API description languages are not also web frameworks , they are generally very mature, and have some amazing tooling. For example, take a look at what swagger-ui, a client-side HTML, CSS, and JS bundle, does with your swagger API description here.

As you can see, it’s a very convenient and approachable way of exploring your API. In addition to an easily-navigable structure, you can build up requests and send them to your server, and see its responses.

But it doesn’t end there. If you have a swagger specification of your API, you can also take advantage of the large variety of languages for which you can generate a client library automatically. You don’t even need to build the Java code - you can just use the “Generate Client” button in the beautiful swagger editor.

There are a wide array of other tools that support swagger. Obviously, having access to them would be a great boon. The problem so far has been that writing and maintaining a swagger specification, that you can be sure matches your service, is hard work.

</section> <section class="level2" id="swagger2-and-servant-swagger">

swagger2 and servant-swagger

Thankfully David Johnson and Nickolay Kudasov have written two Haskell libraries, swagger2 and servant-swagger, that automate nearly all of that process for servant APIs. They use the mechanism that guides most of the servant ecosystem — interpreters for the type-level DSL for APIs that is servant — to generate a swagger spec for that API.

Let’s see how it is used; as an example, we’re going to take the Gists part of the GitHub API v3. For the purpose of this post we will ignore authentication and consider only GET requests which do not require one. Furthermore, we’ll use simplified representation for the responses (i.e. we are also ignoring some fields of the response objects).

First the imports and pragmas (this is a literate haskell file):

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE TypeOperators #-}
module Gists where

import Control.Lens
import Data.Aeson
import Data.Aeson.Types (camelTo2)
import qualified Data.Aeson.Types as JSON
import qualified Data.ByteString.Lazy.Char8 as BL8
import Data.HashMap.Strict (HashMap)
import Data.Proxy
import Data.Swagger
import Data.Text (Text)
import Data.Time (UTCTime)
import GHC.Generics (Generic)
import Servant
import Servant.Swagger

The API:

type GitHubGistAPI
    = "users" :> Capture "username" Username :> "gists" :> QueryParam "since" UTCTime :> Get '[JSON] [Gist]
 :<|> "gists" :> GistsAPI

type GistsAPI
    = "public"  :> QueryParam "since" UTCTime :> Get '[JSON] [Gist]
 :<|> "starred" :> QueryParam "since" UTCTime :> Get '[JSON] [Gist]
 :<|> Capture "id" GistId :> GistAPI

type GistAPI
    = Get '[JSON] Gist
 :<|> Capture "sha" Revision :> Get '[JSON] Gist

api :: Proxy GitHubGistAPI
api = Proxy

Data types:

newtype Username = Username Text deriving (Generic, ToText, FromJSON)

newtype GistId = GistId Text deriving (Generic, ToText, FromJSON)

newtype SHA = SHA Text deriving (Generic, ToText)

type Revision = SHA

data Gist = Gist
  { gistId          :: GistId
  , gistDescription :: Text
  , gistOwner       :: Owner
  , gistFiles       :: HashMap FilePath GistFile
  , gistTruncated   :: Bool
  , gistComments    :: Integer
  , gistCreatedAt   :: UTCTime
  , gistUpdatedAt   :: UTCTime
  } deriving (Generic)

data OwnerType = User | Organization
  deriving (Generic)

data Owner = Owner
  { ownerLogin      :: Username
  , ownerType       :: OwnerType
  , ownerSiteAdmin  :: Bool
  } deriving (Generic)

data GistFile = GistFile
  { gistfileSize      :: Integer
  , gistfileLanguage  :: Text
  , gistfileRawUrl    :: Text
  } deriving (Generic)

FromJSON instances:

modifier :: String -> String
modifier = drop 1 . dropWhile (/= '_') . camelTo2 '_'

prefixOptions :: JSON.Options
prefixOptions = JSON.defaultOptions { JSON.fieldLabelModifier = modifier }

instance FromJSON OwnerType
instance FromJSON Owner    where parseJSON = genericParseJSON prefixOptions
instance FromJSON GistFile where parseJSON = genericParseJSON prefixOptions
instance FromJSON Gist     where parseJSON = genericParseJSON prefixOptions

So far this is what you would usually have when working with servant. Now to generate Swagger specification we need to define schemas for our types. This is done with ToParamSchema and ToSchema instances:

prefixSchemaOptions :: SchemaOptions
prefixSchemaOptions = defaultSchemaOptions { fieldLabelModifier = modifier }

instance ToParamSchema SHA
instance ToParamSchema Username
instance ToParamSchema GistId

instance ToSchema Username
instance ToSchema GistId
instance ToSchema OwnerType
instance ToSchema Owner    where declareNamedSchema = genericDeclareNamedSchema prefixSchemaOptions
instance ToSchema GistFile where declareNamedSchema = genericDeclareNamedSchema prefixSchemaOptions
instance ToSchema Gist     where declareNamedSchema = genericDeclareNamedSchema prefixSchemaOptions

These will give us a generically-derived Swagger schema (which is sort of a deterministic version of JSON Schema).

Part of the swagger2 package, Schema and ParamSchema can be quite useful in their own right if you want to e.g. respond with a schema in case of bad request bodies, or OPTIONS requests.

The next step will traverse the GitHubGistAPI, gathering information about it and swagger2 schemas to generate a Swagger value:

swaggerDoc1 :: Swagger
swaggerDoc1 = toSwagger api

Now we can generate the swagger documentation:

genSwaggerDoc1 :: IO ()
genSwaggerDoc1 = BL8.putStr $ encode swaggerDoc1

You can attach more information to your Swagger doc quite easily, using the lenses provided by swagger2:

swaggerDoc2 :: Swagger
swaggerDoc2 = swaggerDoc1
  & host ?~ "api.github.com"
  & info.title .~ "GitHub Gists API"
  & info.version .~ "v3"
main :: IO ()
main = BL8.putStr $ encode swaggerDoc2

Which results in this.

There’s a lot more you can do with both servant-swagger and swagger2 — write manual ToSchema instances for more detailed information, conveniently add tags or change responses of parts of your API, use convenient lenses to modify any part of your schema, generate automatic tests, etc.

Check out the servant-swagger and swagger2 docs for more.

These two new packages vastly expand the landscape of tools within easy reach of application developers using servant. Time to explore that landscape!

On a related note, Masahiro Yamauchi has recently added Servant codegen for Swagger. So not only can you generate a swagger description for your servant server, but you can also generate the servant description from a swagger one too!

</section>
Posted on February 6, 2016 by David Johnson, Nickolay Kudasov, Julian Arni

by servant developers at February 06, 2016 12:00 AM

Christopher Allen

Haskell is not trivial, but it's not unfair like Dark Souls either

Alternate title: Another brutal fisking for which I’ll forever be remembered as a monster

Don’t be a dick and don’t harass the original author please. They were just sharing their experience.

It took me five years to stop struggling with Haskell, I know a lot of the UX stuff sucks. I think there’s a lot of value in using Haskell for everyday work so it’s disappointing when things fall apart for a learner for unnecessary reasons.

I’ve since talked to the author of the original post and they’re cool with this post. Also they agree with me that wreq should get more airplay. On with the show.

Getting the ball rolling on talking to HTTP APIs

I want to collect some statistics from the GitHub API. Watch as I retrace my steps attempting the Tomb of the Dread HTTPS GET Request.

Okay, is there a reason we’re not going to use the Haskell Github client for that? Anyway, we’ll follow along with what the author’s doing for now.

Now I need to query the GitHub API. Not my first time to the rodeo, I generate a personal access token from GitHub and copy it to a local file. What query should I run first? How about the count for all ASM tetris repositories? Poking around the docs comes up with:

GET https://api.github.com/search/repositories?q=tetris+language:assembly&sort=stars&order=desc
User-Agent: victim
Authorization: token PUT_TOKEN_HERE

Cool so far. Think the author figured out Github’s docs more easily than I did.

Easy life. Now how do you GET a resource in Haskell? Ah, Network.HTTP! I copy the front page sample into src/Lib.hs

Okay first mistake. I know it sucks, but you want to be careful about using Hackage to find libraries for things unless you’re good at sniff-testing APIs. It’s generally better to ask what a good library to use is. The library named “HTTP” is a bit creaky and there are nicer, more up to date ways of doing HTTP in Haskell. Entirely not the author’s fault, but it’s pretty hard to get Hackage to do anything useful anyway. I know this is sucky implicit crap nobody should have to care about, but Haskell just doesn’t have the culture of design-focused self-promotion that other communities have. Not a value judgment, in the end it’s probably better for end-users if they can use design as a signal of how up to date or nice a library is, but that’s just how it is right now. It would probably help if there were more Haskellers that didn’t sneer at web devs.

Anyhoodle,

-- the article's version
module Lib
    ( someFunc
    ) where

x = simpleHTTP (getRequest "https://www.github.com/") >>= fmap (take 100) . getResponseBody

someFunc :: IO ()
someFunc =
   print x

Well. Yes that sucks. It’s also a weird way to write it. It’s like the code people write the first time they figure out how do syntax desugars into >>=, then they just start using >>= and point-free all over the place for the fuck of it. We’ll re-do it in wreq:

-- first.hs
-- this is my version

module FirstExample
  ( someFunc )
  where

-- Don't give me any shit about lens.
-- You don't need to understand lens
-- to know the ^. is for accessing a
-- record field. The wreq tutorial
-- lays out the common use-cases.

import Control.Lens
import qualified Data.ByteString.Lazy as BL
import Network.Wreq

-- Brand X
-- simpleHTTP (getRequest "https://www.github.com/") >>= fmap (take 100) . getResponseBody
-- someFunc :: IO ()
-- someFunc =
--    print x

-- our version
someFunc :: IO ()
someFunc = do
  response <- get "https://www.github.com/"
  print $ BL.take 100 (response ^. responseBody)

To load this beast up:

-- yes this'll take a moment, but then you won't
-- have to do it again because it's Stack.
$ stack build lens wreq
$ stack ghci
Prelude> :l first.hs 
[1 of 1] Compiling FirstExample     ( first.hs, interpreted )
Ok, modules loaded: FirstExample.
Prelude> someFunc
"<!DOCTYPE html>\n<html lang=\"en\" class=\"\">\n  <head prefix=\"og: http://ogp.me/ns# fb: http://ogp.me/ns"

Right-o, moving along.

Doesn’t compile. Durp, hackage is a package library, I need to add this to my cabal.

If you want to and you wanted a package for this, sure. I’ll typically use a stack template for new projects, but for initial exploration I’ll build the libraries as above I want and use them in stack ghci.

…author struggles with HTTP only supporting HTTP…

wreq and http-client-tls support HTTPS out of the box. YMMV. There’s a reason I don’t really recommend older Haskell libraries even if they’re maintained. The foundation of many libraries is http-client and it’s a pretty popular library to use. It’s used in http-conduit and pipes-http as well. The latter of which is a single 130 line module that has required almost zero maintenance in the past two years to add pipes streaming support to http-client. Things that use http-client are generally nice but you’ll often want to use something higher level than http-client itself, such as wreq.

Author moves on to use http-conduit, which uses http-client-tls under the hood

query :: IO String
query = do
    initReq <- parseUrl "https://api.github.com/search/repositories"
    let r = initReq
                   { method = "GET"
                    , requestHeaders = [(hUserAgent, "victim")
                                      , (hAuthorization, "token PUT_TOKEN_HERE")]}
    let request = setQueryString [("q", Just "tetris+language:assembly")
                                 ,("order", Just "desc")
                                 ,("sort", Just "stars")] r
    manager <- newManager tlsManagerSettings
    res <- httpLbs request manager
    return . show . responseBody $ res

someFunc :: IO ()
someFunc = do
  query >>= putStrLn

They’re not using the streaming, might as well use wreq. Normally you’d have, such as in a web framework, an HTTP client pool which gets initialized with the web app once and then shared with the handlers. So the initial setup code would happen once. I do think the API staging out the parseUrl part is a bit pointless for the common-case but w/e. For the record, I wouldn’t consider this code to be bad.

As it happens, wreq has an example of how to talk to Github’s API in the tutorial here if you ctrl-f “most popular implementations of Tetris” you’ll find it.

Prelude> let opts = defaults & param "q" .~ ["tetris"]
                             & param "language" .~ ["haskell"]
Prelude> r <- getWith opts "https://api.github.com/search/repositories"

As it happens, we can just skip past the explicit params thing and just do this:

Prelude> response <- get "https://api.github.com/search/repositories?q=tetris+language:assembly&sort=stars&order=desc"
Prelude> response ^. responseBody

But uh, we’ll get back to what they’re trying to do.

Time to parse this mega JSON string. Aeson seems to be the biggest contender. To use Aeson and get the total_count value from the return, I needed the following additions:

{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE DeriveGeneric #-}

import GHC.Generics
import Data.Aeson

data ResultCount = ResultCount {
  total_count :: Int }
  deriving (Generic, Show)

instance ToJSON ResultCount
instance FromJSON ResultCount

Huh? No you don’t! Int already has a FromJSON instance.

Just to make the point, I’ll do it in GHCi again with no module.

$ stack build aeson lens-aeson
$ stack ghci
Prelude> import Network.Wreq
Prelude> import Control.Lens
Prelude> import Data.Aeson
Prelude> import Data.Aeson.Lens
Prelude> :set -XOverloadedStrings
Prelude> response <- get "https://api.github.com/search/repositories?q=tetris+language:assembly&sort=stars&order=desc"

Prelude> response ^? responseBody . key "total_count"
Just (Number 354.0)
Prelude> response ^? responseBody . key "total_count" . _Number
Just 354.0

Don’t make it harder than it has to be. Ask for help!

I know this site is a bit of a disaster zone, but if you like my writing or think you could learn something useful from me, please take a look at the book I've been writing with my coauthor Julie. There's a free sample available too!

February 06, 2016 12:00 AM

February 05, 2016

Douglas M. Auclair (geophf)

January 2016 1HaskellADay Problems and Solutions

  • January 29th, 2016: Yesterday we monaded, for today's #haskell problem, we COMonad! ... with STREAMS! Oh, yeah! http://lpaste.net/2853437990695337984 onesies and twosies, duplicate to our solutionseis! http://lpaste.net/2531970919929217024
  • January 28th, 2016: Today: Monads. Tomorrow? COMonads! But today's #haskell problem: monads. http://lpaste.net/3895602141393321984 Todayed we Monaded! Oh, yeah! http://lpaste.net/8618821627204861952
  • January 27th, 2016: Today's #haskell problem: A Date-client! http://lpaste.net/3557542263343022080 Not what you're thinking, naughty children! *scold-scold*
  • January 26th, 2016: For today's #haskell problem we create a DayOfWeek web service! Woot! http://lpaste.net/5212178701889830912
  • January 25th, 2016: Per @SirElrik idea, this week we'll do #Haskell #µservices Today's problem is to JSONify a Day -> DayOfWeek function http://lpaste.net/150850 Date, JSONified http://lpaste.net/7633349000409645056
  • January 20th, 2016: Yesterday's problem showed us MLK-day was not a trading day, but WHAT WEEK DAY WAS IT? Today's #haskell problem: http://lpaste.net/3912063664412164096 The solutioneth giveth us the dayth of the weeketh! http://lpaste.net/703919211096834048
  • January 19th, 2016: Today's #haskell problem asks: Was yesterday a #trading day? http://lpaste.net/1968281888535609344 And a #haskell solution to the trading calendar? Monoids, of course! http://lpaste.net/1299918534133940224
  • January 18th, 2016: Today's #haskell problem is a mathematical conundrum concerning poetry ... yes, poetry http://lpaste.net/4733337870415167488 Langston Hughes and Rob't Frost give us the solution: http://lpaste.net/8014739098407272448
  • January 15th, 2016: Yesterday was the Repeatinator2000, for today's #haskell problem we have the GAPINATOR3004!! YES! http://lpaste.net/1481736263689043968 Well, we see HALF the stocks are only mentioned once. But minGaps are NOT telling! Hm. http://lpaste.net/5017845158461308928 
  • January 14th, 2016: In the sea of data we look for some repeaters for today's #haskell problem http://lpaste.net/781423227393015808 AN (H)istogram? A HISTogram? eh, whatevs. #haskell soln shows LOTS of low frequency mentions http://lpaste.net/8518180312847482880
  • January 13th, 2016: One chart to rule them all, one chart to find them, one chart to bring them all, and in the darkness bind them http://lpaste.net/161563874967945216 Big Up Chart ... in #haskell, ya! http://lpaste.net/2722111763528024064 
  • January 12th, 2016: Printing out buy/sell Orders for further analysis http://lpaste.net/2893303782647529472 The charts, ... with the #haskell program that generated them: http://lpaste.net/333157576608841728


  • January 11th, 2016: Prolog. Lists. *drops mic http://lpaste.net/8013339712162889728 For the solution we represent PrologList as a difference list http://lpaste.net/3349987882864476160
  • January 8th, 2016: '$NFLX and Chili?' is today's #haskell problem http://lpaste.net/3944517274819362816 What is this fascination with eating chili whilst watching movies? Case study: $NFLX a solution with several buy/sell scenarios and some open questions remaining http://lpaste.net/6187369537755676672
  • January 5th, 2016: We are Y2K16-compliance officers for today's #haskell problem http://lpaste.net/4805789218464858112
  • January 4th, 2016: Happy New Year! Today's #haskell problem looks at the World of WarCr–... Oops, I mean the World of Work-flow! http://lpaste.net/5383485916327182336

by geophf (noreply@blogger.com) at February 05, 2016 10:31 AM

February 04, 2016

Gabriel Gonzalez

From mathematics to map-reduce

There's more mathematics to programming than meets the eye. This post will highlight one such connection that explains the link between map-reduce and category theory. I will then conclude with some wild speculation about what this might imply for future programming paradigms.

This post assumes that you already know Haskell and explains the mathematics behind the map-reduce using Haskell concepts and terminology. This means that this post will oversimplify some of the category theory concepts in order to embed them in Haskell, but the overall gist will still be correct.

Background (Isomorphism)

In Haskell, we like to say that two types, s and t, are "isomorphic" if and only if there are two functions, fw and bw, of types

fw :: s -> t
bw :: t -> s

... that are inverse of each other:

fw . bw = id
bw . fw = id

We will use the symbol to denote that two types are isomorphic. So, for example, we would summarize all of the above by just writing:

s ≅ t

The fully general definition of isomorphism from category theory is actually much broader than this, but this definition will do for now.

Background (Adjoint functors)

Given two functors, f and g, f is left-adjoint to g if and only if:

f a -> b ≅ a -> g b

In other words, for them to be adjoint there must be two functions, fw and bw of types:

fw :: (f a -> b) -> (a -> g b)
bw :: (a -> g b) -> (f a -> b)

... such that:

fw . bw = id
bw . fw = id

These "functors" are not necessarily the same as Haskell's Functor class. The category theory definition of "functor" is more general than Haskell's Functor class and we'll be taking advantage of that extra generality in the next section.

Free functors

Imagine a functor named g that acted more like a type-level function that transforms one type into another type. In this case, g will be a function that erases a constraint named C. For example:

-- `g` is a *type-level* function, and `t` is a *type*
g (C t => t) = t

In other words, g "forgets" the C constraint on type t. We call g a "forgetful functor".

If some other functor, f is left-adjoint to g then we say that f is the "free C" (where C is the constraint that g "forgets").

In other words, a "free C" is a functor that is left-adjoint to another functor that forgets the constraint C.

Free monoid

The list type constructor, [], is the "free Monoid"

The "free Monoid" is, by definition, a functor [] that is left-adjoint to some other functor g that deletes Monoid constraints.

When we say that g deletes Monoid constraints we mean that:

g (Monoid m => m) = m

... and when we say that [] is left-adjoint to g that means that:

[] a -> b ≅ a -> g b

... and the type [a] is syntactic sugar for [] a, so we can also write:

[a] -> b ≅ a -> g b

Now substitute b with some type with a Monoid constraint, like this one:

b = Monoid m => m

That gives us:

[a] -> (Monoid m => m) ≅ a -> g (Monoid m => m)

... and since g deletes Monoid constraints, that leaves us with:

[a] -> (Monoid m => m) ≅ a -> m

The above isomorphism in turn implies that there must be two functions, fw and bw, of types:

fw :: ([a] -> (Monoid m => m)) -> (a -> m)
bw :: (a -> m) -> ([a] -> (Monoid m => m))

... and these two functions must be inverses of each other:

fw . bw = id
bw . fw = id

We can pull out the Monoid constraint to the left for both of those types to give us these more idiomatic types:

fw :: Monoid m => ([a] -> m) -> ( a  -> m)
bw :: Monoid m => ( a -> m) -> ([a] -> m)

Both of these types have "obvious" implementations:

fw :: Monoid m => ([a] -> m) -> (a -> m)
fw k x = k [x]

bw :: Monoid m => (a -> m) -> ([a] -> m)
bw k xs = mconcat (map k xs)

Now we need to prove that the fw and bw functions are inverse of each other. Here are the proofs:

-- Proof #1
fw . bw

-- eta-expand
= \k -> fw (bw k)

-- eta-expand
= \k x -> fw (bw k) x

-- Definition of `fw`
= \k x -> bw k [x]

-- Definition of `bw`
= \k x -> mconcat (map k [x])

-- Definition of `map`
= \k x -> mconcat [k x]

-- Definition of `mconcat`
= \k x -> k x

-- eta-reduce
= \k -> k

-- Definition of `id`
= id



-- Proof #2
bw . fw

-- eta-expand
= \k -> bw (fw k)

-- eta-expand
= \k xs -> bw (fw k) xs

-- Definition of `bw`
= \k xs -> mconcat (map (fw k) xs)

-- eta-expand
= \k xs -> mconcat (map (\x -> fw k x) xs)

-- Definition of `fw`
= \k xs -> mconcat (map (\x -> k [x]) xs)

-- map (f . g) = map f . map g
= \k xs -> mconcat (map k (map (\x -> [x]) xs))

-- ... and then a miracle occurs ...
--
-- In all seriousness this step uses a "free theorem" which says
-- that:
--
-- forall (k :: Monoid m => a -> m) . mconcat . map k = k . mconcat
--
-- We haven't covered free theorems, but you can read more about them
-- here: http://ttic.uchicago.edu/~dreyer/course/papers/wadler.pdf
= \k xs -> k (mconcat (map (\x -> [x]) xs)

-- This next step is a proof by induction, which I've omitted
= \k xs -> k xs

-- eta-reduce
= \k -> k

-- Definition of `id`
= id

Map reduce

Let's revisit the type and implementation of our bw function:

bw :: Monoid m => (a -> m) -> ([a] -> m)
bw k xs = mconcat (map k xs)

That bw function is significant because it is a simplified form of map-reduce:

  • First you "map" a function named k over the list of xs
  • Then you "reduce" the list using mconcat

In other words, bw is a pure "map-reduce" function and actually already exists in Haskell's standard library as the foldMap function.

The theory of free objects predict that all other functions of interest over a free object (like the free Monoid) can be reduced to the above fundamental function. In other words, the theory indicates that we can implement all other functions over lists in terms of this very general map-reduce function. We could have predicted the importance of "map-reduce purely from the theory of "free Monoids"!

However, there are other free objects besides free Monoids. For example, there are "free Monads" and "free Categorys" and "free Applicatives" and each of them is equipped with a similarly fundamental function that we can use to express all other functions of interest. I believe that each one of these fundamental functions is a programming paradigm waiting to be discovered just like the map-reduce paradigm.

by Gabriel Gonzalez (noreply@blogger.com) at February 04, 2016 06:32 AM

February 03, 2016

Roman Cheplyaka

Reducing boilerplate in finally tagless style

Introduction

Typed Tagless, a.k.a tagless-final or finally tagless, is an approach to embedding DSLs and modeling data in general, advocated by Oleg Kiselyov. Instead of defining a set of algebraic data types to describe data or terms, thus focusing on how data is constructed, the approach focuses on data consumption, defining a canonical eliminator for every constructor that we would otherwise define.

For instance, instead of defining lists as

data List a = Nil | Cons a (List a)

we would define a class

class List rep a where
  nil :: rep
  cons :: a -> rep -> rep

which of course corresponds to the Böhm-Berarducci (or Church) encoding of the above algebraic type.

Oleg has written extensively on the merits of this approach. In this article, I want to discuss a certain aspect of writing transformations in the finally tagless style.

The use case: language-integrated query

Oleg, together with Kenichi Suzuki and Yukiyoshi Kameyama, have published a paper Finally, Safely-Extensible and Efficient Language-Integrated Query. In this paper, they employ the finally tagless approach to embed, optimize, and interpret SQL queries in OCaml.

Here are some excerpts from their OCaml code:

(* Base Symantics *)
module type Symantics_base = sig
  ...
  (* lambda abstract *)
  val lam     : ('a repr -> 'b repr) -> ('a -> 'b) repr
  (* application *)
  val app     : ('a -> 'b) repr -> 'a repr -> 'b repr
  ...
end

(* Symantics with list operations *)
module type SymanticsL = sig
  include Symantics

  (* comprehension *)
  val foreach : (unit -> 'a list repr) ->
                ('a repr ->  'b list repr) -> 'b list repr
  (* condition *)
  val where   :  bool repr -> (unit -> 'a list repr) -> 'a list repr
  (* yield singleton list *)
  val yield   : 'a repr ->  'a list repr
  (* empty list *)
  val nil     :  unit -> 'a list repr
  (* not empty *)
  val exists  :  'a list repr ->  bool repr
  (* union list *)
  val (@%)    : 'a list repr -> 'a list repr -> 'a list repr

  (* the table constructor which take a table name and table contents *)
  val table : (string * 'a list) -> 'a list repr
end

(‘Symantics’ is not a typo; it’s a portmanteau of ‘syntax’ and ‘semantics’.)

Transformations

A SQL trasnformation (such as transforming a subquery to a join) is represented by an ML functor, i.e. a function mapping one SymanticsL to another, which interprets the term slightly differently than the original one. I say slightly, because normally a transformation touches only a few relevant methods. The others are transformed mechanically following the Reflection-Reification pattern (RR). Informally speaking, we leave the irrelevant methods unchanged, applying the minimal transformation that makes them typecheck.

The question is, how to avoid mentioning irrelevant methods when defining a transformation?

This question is not idle. The language-integrated query code contains about 40 methods and 13 transformations. Pause for a second and imagine the amount of boilerplate that would have to be written if we needed to define every single method for every transformation. As we will see below, ML modules make this a non-issue. In Haskell, however, it is an issue, exhibited in Oleg’s own Haskell example (although easy to miss for a class that only contains 3 methods).

In OCaml, the RR is defined as a transformation of the whole module:

module OL(X:Trans)
         (F:SymanticsL with type 'a repr = 'a X.from)  = struct
  include O(X)(F)
  open X

  let foreach src body =
    fwd (F.foreach (fun () -> bwd (src ())) (fun x -> bwd (body (fwd x))))
  let where test body  =
    fwd (F.where (bwd test) (fun () -> bwd (body ())))
  let yield e    = fmap F.yield e
  let nil ()     = fwd (F.nil ())
  let exists e   = fmap F.exists e
  let (@%) e1 e2 = fmap2 F.(@%) e1 e2

  let table (name,data) =
    fwd @@ F.table (name, data)
end

When they define a transformation, they first transform the module in this mechanical fashion, and then override the few relevant methods:

module AbsBeta_pass(F:SymanticsL) = struct
  module X0 = struct
    type 'a from = 'a F.repr
    type 'a term = Unknown : 'a from -> 'a term
             | Lam     : ('a term -> 'b term) -> ('a -> 'b) term
    let fwd x = Unknown x                              (* generic reflection *)
    let rec bwd : type a. a term -> a from = function  (* reification *)
      | Unknown e -> e
      | Lam f     -> F.lam (fun x -> bwd (f (fwd x)))
  end
  open X0
  module X = Trans_def(X0)
  open X
  (* optimization *)
  module IDelta = struct
    let lam f = Lam f
    let app e1 e2 =
      match e1 with
      | Lam f -> f e2
      | _ -> fmap2 F.app e1 e2
  end
end

(* Combine the concrete optimization with the default optimizer *)
module AbsBeta(F:SymanticsL) = struct
  module M = AbsBeta_pass(F)
  include OL(M.X)(F)        (* the default optimizer *)
  include M.IDelta          (* overriding `lam` and `app` *)
end

How can we do this in Haskell?

Explicit dictionaries

An explicit dictionariy (a data type containing methods as its fields) seems like a great fit for Symantics. The RR transformation would be a simple function mapping one record to another. To define a transformation, we would override the relevant methods via record update.

However, explicit dictionaries are not that well suited for the finally tagless style. In OCaml, you can include one module into another (notice include Symantics in the OCaml code above). This “unpacks” the contents of one module into another, so that when you open the second module, the contents of the first module is available, too.

This is important for the finally tagless style. One of its strength is extensibility, which is achieved through such inclusion. Consequently, deep inclusion chains are common. With Haskell’s data types, unpacking such chains manually at every use site will quickly become unwieldy.

Type classes

Type classes are better suited for inclusion. If we declare

class Symantics1 rep => Symantics2 rep where { ... }

and impose a Symantics2 rep constraint on a function definition, the methods of Symantics1 become available without any additional effort.

But then we don’t have good support for RR. Type class instances are not first class citizens; we can’t declare a function that transforms one instance into another. Nor can we create one instance from another by overriding a few methods… Or can we?

We can achieve our goal by using default method signatures.

We define the RR transformation simultaneously with the class itself:

class Symantics rep where
  lam :: (rep a -> rep b) -> rep (a -> b)
  default lam :: RR t rep => (t rep a -> t rep b) -> t rep (a -> b)
  lam f = fwd $ lam $ bwd . f . fwd

  app :: rep (a -> b) -> rep a -> rep b
  default app :: RR t rep => t rep (a -> b) -> t rep a -> t rep b
  app f x = fwd $ bwd f `app` bwd x

  foreach :: rep [a] -> (rep a -> rep [b]) -> rep [b]
  default foreach :: RR t rep => t rep [a] -> (t rep a -> t rep [b]) -> t rep [b]
  foreach a b = fwd $ foreach (bwd a) (bwd . b . fwd)

  ...

The implementation of RR is straightforward:

class RR t rep where
  fwd :: rep a -> t rep a
  bwd :: t rep a -> rep a

Now let’s define the AbsBeta pass in Haskell.

data AbsBeta rep a where
  Unknown :: rep a -> AbsBeta rep a
  Lam :: (AbsBeta rep a -> AbsBeta rep b) -> AbsBeta rep (a -> b)

instance Symantics rep => RR AbsBeta rep where
  fwd = Unknown
  bwd = \case
    Unknown t -> t
    Lam f -> lam (bwd . f . fwd)

instance Symantics rep => Symantics (AbsBeta rep) where
  lam = Lam
  app f x =
    case f of
      Unknown f' -> fwd $ app f' (bwd x)
      Lam b -> b x

All the methods not mentioned in the last instance get their default implementations based on RR, which is exactly what we wanted.

Associated types

Apart from methods, ML/OCaml modules can also define types. This is used in the Language-integrated query paper and code in the following way:

(* Base Symantics *)
module type Symantics_base = sig
  type 'a repr  (* representation type *)
  val observe : (unit -> 'a repr) -> 'a obs
  ...

In Haskell, we can replicate that with an associated type:

class SymanticsObs rep where
  type Obs rep :: * -> *

  observe :: rep a -> Obs rep a
  default observe :: RR t rep => t rep a -> Obs rep a
  observe = observe . bwd

The default definition for observe saves us from redefining it for derived representations, but what about Obs itself? We would like to write, in the spirit of default method signatures,

class SymanticsObs rep where
  type Obs rep :: * -> *
  type Obs (t rep) = rep

However, GHC would not let us to. Since recently, GHC does support default type declarations, but they need to be of the general form type Obs rep = ....

Nevertheless, we can create a type family that will extract the rep from t rep for us:

type family Peel (rep :: * -> *) :: (* -> *) where
  Peel (t rep) = rep

class SymanticsObs rep where
  type Obs rep :: * -> *
  type Obs rep = Obs (Peel rep)

  observe :: rep a -> Obs rep a
  default observe :: RR t rep => t rep a -> Obs rep a
  observe = observe . bwd

Now we can say

instance (Symantics rep, SymanticsObs rep) => SymanticsObs (AbsBeta rep)

without having to define either type Obs or observe explicitly.

Conclusion

Extensions such as default method signatures, default associated types, and type families can significantly reduce the boilerplate when defining transformations in the finally tagless style.

Update. Although I missed it on the first reading of the paper, /u/rpglover64 on reddit points out that the authors themselves acknowledge the boilerplate problem which this article addresses:

Haskell typeclasses made the encoding lightweight compared to OCaml modules. On the other hand, in OCaml we relied on the include mechanism to program optimizations by reusing the code for the identity transformation and overriding a couple of definitions. Haskell does not support that sort of code reuse among type classes. Therefore, programming tagless-final transformation in Haskell has quite a bit of boilerplate.

February 03, 2016 08:00 PM

Functional Jobs

OCaml server-side developer at Ahrefs Research (Full-time)

Who we are

Ahrefs Research is a San Francisco branch of Ahrefs Pte Ltd (Singapore), which runs an internet-scale bot that crawls whole Web 24/7, storing huge volumes of information to be indexed and structured in timely fashion. On top of that Ahrefs is building analytical services for end-users.

Ahrefs Research develops a custom petabyte-scale distributed storage to accommodate all that data coming in at high speed, focusing on performance, robustness and ease of use. Performance-critical low-level part is implemented in C++ on top of a distributed filesystem, while all the coordination logic and communication layer, along with API library exposed to the developer is in OCaml.

We are a small team and strongly believe in better technology leading to better solutions for real-world problems. We worship functional languages and static typing, extensively employ code generation and meta-programming, value code clarity and predictability, constantly seek out to automate repetitive tasks and eliminate boilerplate, guided by DRY and following KISS. If there is any new technology that will make our life easier - no doubt, we'll give it a try. We rely heavily on opensource code (as the only viable way to build maintainable system) and contribute back, see e.g. https://github.com/ahrefs . It goes without saying that our team is all passionate and experienced OCaml programmers, ready to lend a hand or explain that intricate ocamlbuild rule.

Our motto is "first do it, then do it right, then do it better".

What we need

Ahrefs Research is looking for backend developer with deep understanding of operating systems, networks and taste for simple and efficient architectural designs. Our backend is implemented mostly in OCaml and some C++, as such proficiency in OCaml is very much appreciated, otherwise a strong inclination to intensively learn OCaml in a short term will be required. Understanding of functional programming in general and/or experience with other FP languages (F#,Haskell,Scala,Scheme,etc) will help a lot. Knowledge of C++ and/or Rust is a plus.

The candidate will have to deal with the following technologies on the daily basis:

  • networks & distributed systems
  • 4+ petabyte of live data
  • OCaml
  • linux
  • git

The ideal candidate is expected to:

  • Independently deal with and investigate bugs, schedule tasks and dig code
  • Make argumented technical choice and take responsibility for it
  • Understand the whole technology stack at all levels : from network and userspace code to OS internals and hardware
  • Handle full development cycle of a single component, i.e. formalize task, write code and tests, setup and support production (devops)
  • Approach problems with practical mindset and suppress perfectionism when time is a priority

These requirements stem naturally from our approach to development with fast feedback cycle, highly-focused personal areas of responsibility and strong tendency to vertical component splitting.

What you get

We provide:

  • Competitive salary
  • Modern office in San Francisco SOMA (Embarcadero)
  • Informal and thriving atmosphere
  • First-class workplace equipment (hardware, tools)
  • No dress code

Get information on how to apply for this position.

February 03, 2016 07:36 PM

Tom Schrijvers

wren gayle romano

It's official, I'm off to Google

It's official, I'm heading to Google at the end of July to work with Mark Larson on the Chrome OS security team (of all things!). Seems an unlikely match, but Mark was pretty keen on my background (including the gender stuff!) and wasn't put off by my fusion of linguistics, type-theory, constructive logic/maths, et al. I guess the security team is more concerned with semantic models and constructive correctness than the other teams I talked with. Makes sense, I suppose, but it's sad that these are still thought of as "security" concerns rather than "everything in programming" concerns.

I'm totally looking forward to it, but I am still thinking of it as a bit of an experiment. I'm an academic at heart, so I could see myself heading back to academia in a few years. (Wanting to be a professor is, afterall, what motivated me to start gradschool in the first place.) Then again, I've never really thought of industry as being interested in the sorts of theory I work on. In any case, I'll still be around at the various conferences I've been frequenting; I won't just disappear into industry.

I know a bunch of y'all are in the bay area. I'd love to hear any pointers you have on apartment hunting or on what neighborhoods (nearish Mt View) are nice— i.e., places an artistic disabled radical queer woman might like. Feel free to comment below or get in touch by email, twitter, etc.



comment count unavailable comments

February 03, 2016 06:43 AM

February 01, 2016

Neil Mitchell

New HLint version and API features

Summary: In the new version of HLint, errors are warnings and warnings are suggestions. I plan to remove the old API very soon.

I've just released a new version of HLint, the tool for suggesting hints to improve your Haskell code. This version comes with two big changes.

Firstly, hints have been reclassified in severity. What used to be errors are now warnings, and hints that used to be warnings are now suggestions. As people have mentioned in the past, nothing HLint suggested was really an error, and now HLint matches that.

Secondly, there is now an hlint API entry point in Language.Haskell.HLint3 which captures the pattern of running HLint with command-line arguments, but in process as a library. With that, I don't think there are any API patterns that are better captured by the Language.Haskell.HLint API. If no one contacts me with issues, I will be making the module Language.Haskell.HLint a copy of Language.Haskell.HLint3 in the next release.

This release (like all minor releases) fixes a few bugs and adds a few new features. As a few random examples, HLint now warns on a redundant DefaultSignatures language extension, suggests fmap in preference to liftM and warns when otherwise is used as a pattern variable. There is a complete change log in the repo.

by Neil Mitchell (noreply@blogger.com) at February 01, 2016 09:30 PM

January 28, 2016

Joachim Breitner

Dreaming of role playing

Recently, at a summer-school-like event, we were discussing pen-and-paper role playing. I’m not sure if this was after a session of role-playing, but I was making the point that you don’t need much or any at all of the rules, and scores, and dice, if you are one of the story-telling role players, and it can actually be more fun this way.

As an example, I said, it can make sense if one of the players (and the game master, I suppose) reads up a lot about one aspect of the fantasy world, e.g. one geographical area, one cult, one person, and then this knowledge is used to create an exciting puzzle, even without any opponents.

I’m not quite sure, but I think I fell asleep shortly after, and I dreamed of such a role playing session. It was going roughly like this:

I (a human), and my fellows (at least a dwarf, not sure about the rest) went to some castle. It was empty, but scary. We crossed its hall, and went into a room on the other side. It was locked towards the hall by a door that covered the door frame only partly, and suddenly we could see a large Ogre, together with other foul folk not worth mentioning, hammered at the door. My group (which was a bit larger in that moment) all prepared shooting arrows at him the moment it burst through the door. I had the time to appreciate the ingenuity that we all waited for him to burst through, so that none of the arrows would bounce of the door, but it did not help, and we ran from the castle, over a field, through a forest, at the other side of which we could see, below a sleep slope, a house, so we went there.

The path towards that was filled with tracks that looked surprisingly like car tracks. When we reached the spot there was no house any more, but rather a cold camp side. We saw digging tools, and helmets (strangely, baseball helmets) were arranged in a circle, as if it was a burial site.

We set up camp there and slept.

It occurred to me that I must have been the rightful owner of the castle, and it was taken by me from my brother and his wife, who denied my existence or something treacherously like that. When we woke up at the camp side, she were there, together with what must be my niece. My sister in law mocked us for fighting unsuccessfully at the castle, but my niece was surprised to see me, as I must have a very similar appearance to my brother. She said that her mother forbid it, but she nevertheless sneakily takes out something which looks like a Gameboy with a camera attachment and a CompactFlash card from her mothers purse, puts it in and take a photo of me. This is when I realize that I will get my castle back.

At that moment, I woke up. I somewhat liked the story (and it was a bit more coherent in my mind than what I then wrote down here), so I wanted to write it down. I quickly fetched my laptop. My friends at the summer school were a bit worried, and I promised not to mention their names and concrete places, and started writing. They distracted me, so I searched for a place of my own, lied down (why? no idea), and continued writing. I had to to touch writing on my belly, because my laptop was not actually there.

I also noticed that I am back at the camp side, and that I am still wearing my back protector that I must have been wearing while fighting in the castle, and which I did not take off while sleeping at the camp side. Funnily, it was not a proper medieval amour, but rather my snowboarding back protector.

At that moment, I woke up. I somewhat liked the story (and it was a bit more coherent in my mind than what I then wrote down here), so I wanted to write it down. I quickly got up, started my laptop, and wrote it down. And this is what you are reading right now.

Off to bed again, let’s see what happens next.

by Joachim Breitner (mail@joachim-breitner.de) at January 28, 2016 07:26 AM

January 27, 2016

wren gayle romano

Finding hope

Many of us with disabilities have more than one. This multiplicity is invisiblized by the abled community. When our lives are already assumed to be defined by disability, admitting multiplicity risks the hazard of letting the complexities of disabled lives enter one's mind. But even among the disabled, there's a tendency to focus on the one or two things which most obviously impact our lives. This is a coping mechanism. To cope with lacking spoons, we are always prioritizing our energies, and there is never enough to solve all the things. But also, ableism being what it is, we must be careful never to "complain too much" lest we loose whatever ears we've gained; so we consign our suffering to silence, that we might grasp at crumbs of compassion for hope that when things worsen there may still be someone who'll listen.

I have my "one or two things": depression and cPTSD. And I've mentioned my migraines on occasion, though they're seldom of bloggable interest. But there's one I've never talked about, one I've still not come to terms with myself. That's the thing about chronic pain. Noone ever teaches us about all the things that shouldn't hurt, about all the pains most people don't have. And consequently we come to normalize them, to unsee the ways they make us choose —in small ways at first— to restrict our lives. Last week I met a fabulous girl and we got to talking about disability. And with one sentence she cut through me like a thunderbolt, cut through a silence I hadn't even realized I'd been spinning for years. Her words, so simple:

I have a connective tissue disease

I've suspected it for a couple decades, known it for nearly a decade, but it's never been something I've been allowed to talk about. When a teen complains about joint pain, it is dismissed as an insignificance. When a twentysomething does, everyone older jests and jeers; "just wait till you're my age," they say. Sit down. Shut up. Respect your elders. If you're resilient enough to keep at it, to endure the shame and go to a doctor... well, doctors have ways of silencing things they can't cure. When I first saw a doctor for my knees, he acted like it was nothing, like I was a stupid kid bitching about nothing— despite saying, with surprise in his voice, how my x-rays looked like someone 15–20 years older. When I pressed, when I refused to be cowed, he told me there was nothing modern science could do: I could use a splint, but that'd weaken the muscles and exacerbate the problem; I could try working out to strengthen the muscles —at least, for as long as I could stand the pain— but that'd only slow the inevitable by a couple years at best; it wasn't bad enough for surgery, besides that'd just cause even more damage. "You're young," he said in flat monotone, like words rehearsed without meaning. Like pointing out something broken or left behind, when you really don't care if they hear you. Your coffee. Your wallet. Your tail light. You're young.

The thing about genetic issues is that they pervade everything. It's never a singular problem, it's a cascade of them, a death by ten-thousand papercuts. In my childhood, my mother always had issues with her knees. It was almost a joke how often she went in for surgeries on them; the kind of joke people only mumble and noone laughs at but they tell it anyways because they don't know what else to do. During my early college years, her shoulders started going out. A few years back my sister died spontaneously, and within a few months a cousin joined her. Aortic ruptures. In the last year or so, my mother had an aortic dissection. She survived, but more from luck than anything. I happened to be in Maryland when she was in the hospital, and I visited. She'd also been having catastrophic spinal problems. My parents didn't even bother mentioning it until she went in for the first surgery. It didn't go well. Three followup surgeries later and who knows if any of it did any good. Sitting next to her as she lay in that bed, her hands all locked up in pain, held in mine, I could barely look on her. Because I know I'll live to be crippled and die twisted in pain. She's had enough in-patient PT to be released, and is back home now on out-patient PT. Noone talks about it. But at least noone jokes anymore.

I can't say if it was her heart or her back that somehow managed to convince some doctor to take a closer look. He'd thought she had Marfan syndrome and ordered a genetic screening. Tests came back negative. Followups found it's actually Loeys-Dietz, something that wasn't even discovered until ten years ago, and the docs only knew of it because she'd been admitted to the hospital where they discovered it. There's no point in testing the dead, but there's little doubt about what did my sister and cousin in. I've been checked for aortic problems, and show no symptoms as yet. I'll have to get checked again every couple years.

(One of the funniest things about transitioning is how it's been the healthiest decision I've ever made. If I'd've known all the minor health issues it'd cure, I would've fought harder to do it when I was 18. Among the things it helped was my back. While uncommon, HRT can cause corrections in one's hips and lower ribs. Thanks to the changes in my hips and my center of gravity, I no longer have chronic back pain. Growing up I could never attain correct posture: it caused pain and felt unnatural; whereas now it comes freely and without thinking.)

But the litany of little pains isn't what hurts the most. I used to draw. It used to be my life. The fire in my heart, as maths is the breath in my chest. I'd do it when I wasn't thinking. I'd do it to focus my thinking. I'd come home and spend hours at it. I'd ignore eating to finish a piece. I won awards. I thought I'd make a vocation of it. By halfway through undergrad I could barely finish a small sketch in the margins of my notes. Many of my friends are artists (e.g.), and while I love their work, a hateful demon grows in me every time I see their successes or hear them praised. These days I can barely hold a pencil. My script an ever more illegible shorthand as I try to eke out a few more pages before I resign to sitting behind a computer. (The most creative parts of doing math, for me, needs being written. It is only once I have the sketch of a thing can I put it to pixels.) Just bringing up my art, acknowledging it as something lost rather than as something I lost time for, crushes me.

That girl, that blessed fabulous girl. A few days after we'd met I asked her about her ring, a beautiful curious thing, like two rings locked together at an angle. Turns out it's a surgical splint for preventing hyperextension. She told me where to get one, and on the bus yesterday I decided to check out their website. Reading through the descriptions of the rings they offer —I don't even... How do you name that emotion when a pain you've had so long you've forgotten it exists is suddenly eased, that lift, that release, that letting go. Like when you find someone who shares your very same marginalization, that feeling where you can just talk, can let words free without censor knowing they have already been understood before they are spoken. That sudden finding oneself not alone. That slow creeping into existence of a future worth looking toward. I had to turn off my browser. Can't be crying on busses. Can't be weak in public.



comment count unavailable comments

January 27, 2016 05:35 AM

January 26, 2016

Oliver Charles

Monad transformers, free monads, mtl, laws and a new approach

If you’ve been following the hot topics of Haskell over the last few years, you’ll probably have noticed a lot of energy around the concepts of effects. By effects, we are generally talking about the types of computations we traditionally express using monads in Haskell – IO, non-determinism, exceptions, and so on. I believe the main reason that this has been a popular topic is that none of the existing solutions are particularly nice. Now “nice” isn’t a particularly well defined concept, but for something to fit in well with Haskell’s philosophy we’re looking for a system that is:

  1. Extensible. The approach we take should be open, allowing us to define new effects.
  2. Composable. It should be possible to mix different effects with well defined, predictable behaviour.
  3. Efficient. We should only have to pay a minimal cost for the use of the abstraction.
  4. Terse. Haskell is generally not verbose, and whatever system we use should allow us to avoid excessive verbosity. The system should work with us, we should not have to work for it.

I would also add in a 5th point

  1. Inferable. Type annotations should not be required for successful compilation.

With this list in mind, what are the current solutions, and how do they measure up?

Monad Transformers

Starting with the most basic, we can simply choose a concrete monad that does everything we need and work entirely in that – which is usually going to be IO. In a sense this is composable – certainly all programs in one monad compose together – but it’s composable in the same sense that dynamically typed languages fit together. Often choosing a single monad for each individual computation is too much, and it becomes very difficult to work out exactly what effects are being used in our individual functions: does this computation use IO? Will it throw exceptions? Fork threads? You don’t know without reading the source code.

Building a concrete monad can also be a lot of work. Consider a computation that needs access to some local state, a fixed environment and arbitrary IO. This has a type such as

newtype M a = M (Environment -> State -> IO (a, State))

However, to actually interact with the rest of the Haskell ecosystem we need to define (at least) instances of Functor, Applicative and Monad. This is boilerplate code and entirely determined by the choice of effects – and that means we should strive to have the compiler write it for us.

To combat this, we can make use of monad transformers. Unlike monads, monad transformers compose, which means we can build larger monads by stacking a collection of monad transformers together. The above monad M can now be defined using off-the-shelf components, but crucially we can derive all the necessary type classes in one fell swoop with the GeneralizedNewtypeDeriving language extension

{-# LANGUAGE GeneralizedNewtypeDeriving #-}

newtype M a = M (ReaderT Environment (StateT State IO) a)
  deriving (Functor, Applicative, Monad)

This saves typing considerably, and is a definite improvement. We’ve achieved more of points 1 and 2 (extenability and composability) by having both programs and effects compose. Point 4 (terseness) is improved by the use of GeneralizedNewtypeDeriving. There is a slight risk in terms of efficiency, but I believe if transformers would just INLINE a few more definitions, the cost can be entirely erased. All of this code will infer as we’d expect, as we’re working entirely with explicit types

However, while we had to type less to define the effects, we have to type more to use the effects! If we want to access the environment for example, we can use the ask operation from Control.Monad.Trans.Reader, but we have to wrap this up in the M newtype:

env :: M Environment
env = M ask

However, if we want to retrieve the current state in the computation, we can use get from Control.Monad.Trans.State, but we also have to lift that into the ReaderT monad that is wrapping StateT:

currentState :: M State
currentState = M (lift get)

This is unfortunate – lift is mostly noise that we don’t want to be concerned with. There is also the problem in that the amount of lifts to perform is tied directly to the underlying definition of M. If I later decide I want to layer in the chance of failure (perhaps with MaybeT), I now have to change almost all code using lift, by adding an extra one in!

lift is a mechanical operation that is determined by the type of monad transformer stack and the operation that we want to perform. As we noted, for different stacks, the amount of lifting will vary, but it is determined by the type of stack. This suggests that these lifts could be inferred by the use of type classes, and this is the purpose of the monad transformer library – mtl.

The Monad Transformer Library (mtl)

The mtl is a library consisting of type classes that abstract over the operations provided by each monad transformer. For ReaderT, we have the ask operation, and likewise for StateT we have get and put operations. The novelty in this library is that the instances for these type classes are defined inductively over monad transformer stacks. A subset of the instances for MonadReader for example, show

class MonadReader r m | m -> r where
  ask :: m r

instance Monad m => MonadReader r (ReaderT r m) where
  ask = Control.Monad.Trans.ReaderT.ask

instance (MonadReader r m) => MonadReader r (StateT s) where
  ask = lift ask

We can read this as:

  • a base case if the outermost transformer is ReaderT, in which case no lifting has to be performed.

  • an inductive case, stating that if we know there is a MonadReader instance somewhere within the stack (that is, somewhere in the stack we are using ReaderT), then the outer monad transformer (in this case StateT) is also an instance of MonadReader by simply passing those operations through to the underlying instance via one application of lift.

With these instances the lifting now becomes automatic entirely at the use of the respective operations. But not only does it become easier to use the operations, our programs also become more generic and easier to reason about. For example, while env previously had the type M Environment, it could now generalise to simply

env :: (MonadReader Environment m) => m Environment
env = ask

Stating that env is reusable in any computation that has access to Environment. This leads to both more options for composition (we’re not tied to working in M), but also types that are more expressive of what effects are actually being used by the computation. In this case, we didn’t use StateT, so we didn’t incur a MonadState type class constraint on m.

Type classes open up a risk of losing type inference, and the approach in mtl is to use functional dependencies. mtl makes use of functional dependencies in order to retain type inference, but this comes at a compositional cost – the selected effect proceeds by induction from the outer most monad transformer until we reach the first matching instance. This means that even if there are multiple possible matches, the first one encountered will be selected. The following program demonstrates this, and will fail to type check:

getTheString :: ReaderT Int (ReaderT String IO) String
getTheString = ask
    Couldn't match type ‘Int’ with ‘[Char]’
    arising from a functional dependency between:
      constraint ‘MonadReader String (ReaderT Int (ReaderT String IO))’
        arising from a use of ‘ask’

When we used ask induction proceeded from the outermost transformer - ReaderT Int. This is an instance of MonadReader, and due to the functional dependency will be selected even though it doesn’t contain the String that we’re looking for. This manifests as a type error, which can be frustrating.

In practice, I’m not convinced this is really a problem, but in the scenario where environments don’t match up we have a few options:

  1. Adapt the environment with tools like mapReaderT or magnify (from lens).

  2. Use monad-classes which uses a little more type level computation to allow this to work. I’m not entirely sure what the story for inference is here, but I think there may be a risk of less inference.

  3. Forgo the functional dependencies, as in mtl-unleashed. In this case you really do give up type inference, and I don’t consider it a viable option (it fails to satisfy point 5 in my criteria in the intro).

Interestingly, the generality we gained by being polymorphic over our choice of monad also opens the door to something we couldn’t do with monad transformers, which is to choose a different implementation of the type class. For example, here’s a different implementation of MonadReader for M:

instance MonadReader Environment M where
  ask = do
    env <- M ask
    liftIO (putStrLn "Requesting environment")
    liftIO (putStrLn ("It is currently " ++ show env)
    return env

While a slightly contrived example, we see that we now have the ability to provide a different interpretation for ask which makes use of the underlying IO in M by logging whenever a computation looks at the environment. This technique is even more useful when you start defining domain specific effects, as it gives you the option to provide a pure variant that uses mock data, which can be useful for unit testing.

Free monads

Let’s move away from monad transformer stacks and see what the other options are. One option that’s getting a lot of attention is the use of free monads. A free monad is essentially a type of construction that adds just enough structure over some data in order to have the structure of a monad – and nothing extra. We spend our days working with monads, and the reason the approach afforded by free monads is appealing is due to the way that we build them – namely, we just specify the syntax! To illustrate this, let me the consider the almost traditional example of free monads, the syntax of “teletype” programs.

To begin with, I have to define the syntax of teletype programs. These programs have access to two operations - printing a line to the screen, and reading a line from the operator.

data TeletypeF a = PrintLine String a
                 | GetLine (String -> a)
  deriving (Functor)

This functor defines the syntax of our programs - namely programs that read and write to the terminal. The parameter a allows us to chain programs together, such as this echo program that prints whatever the user types:

echo :: TeletypeF (TeletypeF ())
echo = GetLine (\line -> PrintLine line ())

However, this is kind of messy. The free monad construction allows us to generate a monad out of this functor, which provides the following presentation:

echo :: Free TeletypeF ()
echo = do
  l <- getLine
  printLine l

getLine :: Free TeletypeF String
getLine = liftF (GetLine return)

printLine :: String -> Free TeletypeF ()
printLine l = liftF (PrintLine l ())

This definition of echo looks much more like the programs we are used to writing.

The remaining step is to provide an interpretation of these programs, which means we can actually run them. We can interpret our teletype programs by using STDOUT and STDIN from IO:

runTeletype :: Free TeletypeF a -> IO a
runTeletype =
  iterM (\op ->
           case op of
             GetLine k -> readLine >>= k
             PrintLine l k -> putStrLn l >> k)

This rather elegant separation between syntax and semantics suggests a new approach to writing programs – rather than working under a specific monad, we can instead work under a free monad for some suitable functor that encodes all the operations we can perform in our programs.

That said, the approach we’ve looked at so far is not particularly extensible between different classes of effects, as everything is currently required to be in a single functor. Knowing that free monads are generated by functors, we can start to look at the constructions we can perform on functors. One very nice property of functors is that given any two functors, we can compose them. The following functors below witness three possible ways to compose functors:

data Sum f g a = InL (f a) | InR (g a) deriving (Functor)
data Product f g a = Product (f a) (g a) deriving (Functor)
data Compose f g a = g (f a) deriving (Functor)

Assuming f and g are Functors, all of these are also Functors - which means we can use them to build monads with Free.

The most interesting of these constructions (for our purposes) is Sum, which lets us choose between two different Functors. Taking a more concrete example, I’ll repeat part of John A. De Goes “Modern FP” article. In this, he defines two independent functors for programs that can access files in the cloud, and another for programs that can perform basic logging.

data CloudFilesF a
  = SaveFile Path Bytes a
  | ListFiles Path (List Path -> a)
  deriving (Functor)

data LoggingF a
  = Log Level String a
  deriving (Functor)

Both of these can now be turned into monads with Free as we saw before, but we can also combine both of these to write programs that have access to both the CloudFilesF API and LoggingF:

type M a = Free (Sum CloudFilesF LoggingF) a

However, in order to use our previous API, we’ll have to perform another round of lifting:

-- API specific to individual functors
log :: Level -> String -> Free LoggingF ()
log l s = liftF (Log l s ())

saveFile :: Path -> Bytes -> Free CloudFilesF ()
saveFile p b = lift (SaveFile p b ())

-- A program using multiple effects
saveAndLog :: Free (Sum CloudFilesF LoggingF) ()
saveAndLog = do
  liftLeft (log Info "Saving...")
  liftRight (saveFile "/data" "\0x42")

-- Lifting operations
liftLeft :: Free f a -> Free (Sum f g) a
liftLeft = hoistFree InL

liftRight :: Free g a -> Free (Sum f g) a
liftRight = hoistFree InR

This is a slightly unfortunate outcome - while we’ve witnessed that there is extensiblity, without more work the approaches don’t compose particularly well.

To solve the problem of having to lift everything leads us to the need for an mtl-like solution in the realm of free monads - that is, a system that automatically knows how to lift individual functors into our composite functor. This is essentially what’s happening in the extensible-effects library - as a user you define each individual Functor, and then extensible-effects provides the necessary type class magic to combine everything together.

We should also mention something on efficiency while we’re here. Free monads have at least two presentations that have different use cases. One of these is extremely easy to inspect (that is, write interpters) but has a costly implementation of >>=. We know how to solve this problem, but the trade off switches over to being costly to inspect. Recently, we learnt how to perform reads and binds in linear time, but the constant factors are apparently a little too high to be competative with raw transformers. So all in all, there is an efficiency cost of just working with a free monad approach.

mtl and laws

I want to now return to the monad transformer library. To recap, the definition of MonadReader is –

class MonadReader r m | m -> r where
  ask :: m r

But this alone makes me a little uneasy. Why? I am in the class of Haskellers who consider a type class without a law a smell, as it leaves us unable to reason about what the type class is even doing. For example, it doesn’t require much imagination to come up with nonsense implementations of ask:

newtype SomeM a = SomeM (StateT Int IO a)
  deriving (Functor, Applicative, Monad)

instance MonadReader Int SomeM where
  ask = SomeM $ do
    i <- get
    put (i + 1)
    return i

But then again – who’s to say this is nonsense? Given that we were never given a specification for what ask should do in the first place, this is actually perfectly reasonable! For this reason, I set out searching for a way to reason about mtl-style effects, such that we could at least get some laws.

A different approach

The transformers library also give us mtl-like type classes, one of which is MonadIO. However, this type class does have laws as well:

-- liftIO . return = return
-- liftIO (f >>= g) = liftIO f >>= liftIO . g
class MonadIO m where
  liftIO :: IO a -> m a

This law is an example of a homomorphism. To quote Wikipedia on the subject:

A homomorphism is a structure-preserving map between two algebraic structures (such as groups, rings, or vector spaces).

In this case the algebraic structure is the monad structure of IO. We see that any monad that is an instance of MonadIO has the ability to lift IO operations, and as this is a homomorphism, the laws state that it will preserve the underlying structure of IO.

It’s currently unclear how to apply this type of reasing to MonadReader, given its current definition – ask is just a value, it doesn’t even take an argument – so how can we even try and preserve anything?

Let’s take some inspiration from free monads, and consider the effect language for MonadReader. If we only have (Monad m, MonadReader r m), then the only thing we can do on top of the normal monad operations is ask the environment. This suggests a suitable functor would be:

data AskF r a = Ask (r -> a)
  deriving (Functor)

I can now wrap this up in Free in order to write programs with the ability to ask:

type Ask r a = Free (AskF r) a

Now we have an algebraic structure with properties (Ask r is a Monad) that we would like to preserve, so we can write this alternative form of MonadReader:

-- liftAsk . return = return
-- liftAsk (f >>= g) = liftAsk f >>= liftAsk . g
class Monad m => MonadReader r m | m -> r where
  liftAsk :: Ask r a -> m a

ask :: MonadReader r m => m r
ask = liftAsk (liftF (Ask id))

Et voilà! We now have an equally powerful MonadReader type class, except this time we have the ability to reason about it and its instances. If we return to the instance that I was questioning earlier, we can redefine it under the new API:

instance MonadReader Int SomeM where
  liftAsk askProgram = SomeM $ do
    x <- get
    out <- iterM (\(Ask k) -> return (k t)) askProgram
    put (x + 1)
    return out

Now that we have some laws, we can ask: is this a valid definition of MonadReader? To check, we’ll use equational reasoning. Working through the first law, we have

liftAsk (return a)
  = { definition of return for Free }
liftAsk (Pure a)
  = { definition of liftAsk for SomeM }
SomeM $ do
  x <- get
  out <- iterM (\(Ask k) -> return (k t)) (Pure a)
  put (x + 1)
  return out
  = { evaluate iterM for Pure a }
SomeM $ do
  x <- get
  out <- return a
  put (x + 1)
  return out
  = { monad laws }
SomeM $ do
  x <- get
  put (x + 1)
  return a

Already we have a problem. While we can see that this does return the original a it was given, it does so in a way that also incurred some side effects. That is, liftAsk (return a) is not the same as return a, so this isn’t a valid definition of MonadReader. Back to the drawing board… Now, it’s worth noting that there is an instance that is law abiding, but might still be considered as surprising:

instance MonadReader Int SomeM where
  liftAsk askProgram =
    iterM (\(Ask k) -> SomeM $ do
      x <- get
      put (x + 1)
      k x )

Applying the same equational reasoning to this is much easier, and shows that the first law is satisfied

liftAsk (return a)
  = { definition of liftAsk }
iterM (\(Ask k) -> SomeM $ do
  x <- get
  put (x + 1)
  k x)
  (return a)
  = { definition of return for Free }
iterM (\(Ask k) -> SomeM $ do
  x <- get
  put (x + 1)
  k x)
  (Pure a)
  = { definition of iterM given Pure}
return a

For the second law, I’ll omit the proof, but I want to demonstrate to sessions in GHCI:

> let runSomeM (M m) = evalState m 0

> runSomeM (liftAsk (ask >>= \r1 -> ask >>= \r2 -> return (r1, r2))
(1, 2)

> runSomeM (liftAsk ask >>= \r1 -> liftAsk >>= \r2 -> return (r1, r2)
(1, 2)

So while the answers agree - they probably don’t agree with your intuition! This is only surprising in that we have some assumption of how =Ask= programs should behave. Knowing more about =Ask=, we might seek this further law:

ask >> ask = ask

This law can also be seen as a reduction step in the classification of our Ask programs, but a Free monad is not powerful enough to capture that. Indeed, the documentation of Free mentions exactly this:

A free Monad is one that does no work during the normalisation step beyond simply grafting the two monadic values together. [] is not a free Monad (in this sense) because join [[a]] smashes the lists flat.

The law ask >> ask = ask follows by normalisation of our “reader” programs, so a free monad will be unable to capture that by construction – the best we can do is add an extra law to our type class. However, what we can also do is play a game of normalisation by evaluation. First, we write an evaluator for Free (AskF r) programs:

runAsk :: Free (AskF r) a -> (r -> a)
runAsk f r = iterM (\(AskF k) -> k r) f

and then witness that we can reify these r -> a terms back into Free (Ask r) a:

reify :: (r -> a) -> Free (Ask r) a
reify = AskF

You should also convince yourself that (r -> a) really is a normal form, and you may find the above linked article on this useful for formal proofs (search for “normalisation”). What we’ve essentially shown is that every Free (AskF r) a program can be expressed as a single r -> a function. The normal form of ask >> ask is now - by definition - a single ask, which is the law we were originally having to state.

As we’ve witnessed that r -> a is the normal form of Free (AskF r) a, this suggests that we could just as well write:

-- liftAsk . return = return
-- liftAsk (f >>= g) = liftAsk f >>= liftAsk . g
class MonadReader r m | m -> r where
  liftAsk :: (r -> a) -> m a

(The structure being preserved by the homomorphism is assuming that (r -> a) is a reader monad).

Our strange instance now becomes

instance MonadReader UTCTime SomeM where
  liftAsk f = SomeM $ do
    x <- get
    put (x + 1)
    return (f x)

With a little scrutiny, we can see that this is not going to satisfy the homomorphism laws. Not only does it fail to satisfy the return law (for the same reason), the second law states that liftAsk (f >>= g) = liftAsk f >>= liftAsk . g. Looking at our implementation this would mean that we would have to increase the state based on the amount of binds performed in f >>= g. However, we also know that >>= for r -> a simply reduces to another r -> a function - the implication being that it’s impossible to know how many binds were performed.

Here a counter example will help convince us that the above is wrong. First, we know

liftAsk (ask >> ask) = liftAsk ask

because ask >> ask = ask by definition.

By the homomorphism laws, we must also have

liftAsk (ask >> ask) = liftAsk ask >> liftAsk

Combining these, we expect

liftAsk ask = liftAsk (ask >> ask) = liftAsk ask >> liftAsk ask

However…

> runSomeM (liftAsk ask)
1

> runSomeM (liftAsk (ask >> ask))
1

> runSomeM (liftAsk ask >> liftAsk ask)
2

Now we can see that SomeM’s current definition of MonadReader fails. It’s much harder to write a law abiding form of MonadReader Int SomeM - but it will essentially require some fixed data throughout the scope of the computation. The easiest is of course to change the definition of SomeM:

newtype SomeM a = SomeM (ReaderT Int IO a)

instance MonadReader UTCTime SomeM where
  liftAsk f = SomeM (fmap f ask)

You should convince yourself that this instance is now law abiding - for example by considering the above counter-example, or by performing equational reasoning.

A pattern for effect design

The process we underwent to reach the new form of a =MonadReader= type class, extends well to many different type classes and suggests a new pattern for mtl-like type class operations. Here’s a rough framework that I’m having a lot of success with:

1. Define the operations as data

To begin, think about the language that your effect will talk about. For the reader monad, we defined the AskF functor, and the same can be done for the exception monad, the failure monad, the state monad, and so on. For more “domain specific” operations, a free monad also scales well - one could imagine a language for interacting with general relational databases, with operations to SELECT, UPDATE, DELETE, and so on.

2. Find a suitable way to compose operations

Individual operations are not enough, we also need a way to write programs using this language. This amounts to finding a suitable way to compose these operations together. An easy first approximation is to use a free structure, again – as we started with for the reader monad. In the case of the aforementioned domain specific relational database example, the free monad might be as far as we want to go.

It’s also worth exploring if there is a normal form that more succinctly captures the operations in your language along with equational reasoning. We saw that the normal form of Free (AskF r) a was r -> a, and the same process can be ran for Free (StateF s) a - reaching s -> (a, s) as a normal form. It’s important to note that if you go through the process of normalisation by evaluation, that you also make sure you can reify your evaluation result back into the original language. To illustrate why, consider the hypothetical relational database language:

data DatabaseF a = Query SqlQuery (Results -> a)

runDb :: Free DatabaseF a -> (DatabaseHandle -> IO a)
runDb h = iterM (\(Query q k) -> query h q >>= k)

This is fine for an interpreter, but DatabaseHandle -> IO a is not a normal form because we can’t reify these terms back into DatabaseF. This is important, because by working with a normal form it means that you can define a whole range of interpreters that see the necessary structure of the original programs. To illustrate one problem with DatabaseHandle -> IO a, if we attempted to write a pure interpreter, we would be unable to see which queries were performed in order to produce the data under a (not to mention the limitation that working in IO would cause).

3. Introduce a type class for homomorphisms

With your effect language defined, the next step is to define a type class for homomorphisms from this effect language into larger monad stacks. Often this will be a monad homomorphism – much as we saw with MonadReader and MonadIO – but the homomorphism need not be a monad homomorphism. For example, if your source effect language is a simple monoid, then the homomorphism will be a monoid homomorphism. We’ll see an example of this shortly.

4. Export polymorphic operations

With a type class of homomorphisms, we can now export a cleaner API. For MonadReader, this means exporting convenience ask operations that are defined in terms of liftAsk with the appropriate program in our AskF language.

5. Provide a reference implementation

I also suggest providing a “reference” implementation of this type class. For MonadReader, this reference implementation is ReaderT. The idea is that users can immediately take advantage of the effect we’re defining by introducing the appropriate monad transformer into their monad stack.

The type class allows them to more efficiently define the operations in terms of existing monadic capabilities (e.g., IO), but for many simply reusing a transformer will be sufficient.

A worked example for logging

To conclude this article I want to explore one more application of this pattern applied to building a logging effect. In fact, it is this very problem that motivated the research for this blog post, and so we’ll end up building the foundations of my logging-effect library.

The first step is to identify a language for programs that can perform logging. There’s not much involved here, simply the ability to append to the log at any point in time. Let’s formalise that idea with the appropriate functor:

data LoggingF message a = AppendLogMessage message a
  deriving (Functor)

This functor is parameterised by the type of log messages. The only constructor for LoggingF takes a log message and the rest of the computation to run. We could stop here and lift Free (LoggingF message) a programs, but I want to go a bit further and see are any other ways to express this. I’ll use normalisation by evaluation again, and see what happens.

runFreeLogging :: Free (LoggingF message) a -> (a, [message])
runFreeLogging (Pure a) = (a, [])
runFreeLogging (Free (AppendLogMessage m next)) =
  case runFreeLogging next of
    (a, messages) -> (a, m:messages)

We can also take a (a, [message]) and turn it back into the equivalent Free (LoggingF message) a, so (a, [message]) is another candidate for the language of our logging programs.

But this a bothers me. It occurs only in LoggingF message to capture the rest of the computation, but never does the result of logging affect the choice of what that next computation is. This suggests that it’s mostly noise, and maybe we can just erase it. This would lead us to have logging programs of the type [message]. This type is no longer the right kind for our lifting operation to be a monad homomorphism, which means we have to identify another algebraic structure. Well, lists are certainly a composable structure - they have all the properties of a monoid.

With that in mind, we need to consider what it means to be a monoid homomorphism into some monad. First, observe that monads also have a monoid-like operations:

monadMempty :: Monad m => ()
monadMempty = return ()

monadMappend :: Monad m => m () -> m () -> m ()
monadMappend l r = l >> r

We can now write our lifting type class with the laws of a monoid homomorphism:

liftLog mempty   = mempty                 -- = return ()
liftLog (x <> y) = liftLog x <> liftLog y -- = liftLog x >> liftLog y
class MonadLog message m | m -> message where
  liftLog :: [message] -> m ()

While we reached this type by normalisation-by-evaluation and then a little bit of fudging, there is another way we could have got here. In a sense, [] can be seen as another construction like Free - given any type a, [a] is a free monoid generated by a. An easier route to this type class would have been to describe the individual operations in our logging programs by:

data LoggingOp message = LogMessage message

and then using [] as our free construction. As LoggingOp message ~ Identity message ~ message, we know we could also use [message], and we’re back at the type class above.

(In my logging-effect library I chose a slightly different representation of the free monoid. Theoretically, this is a sounder way to talk about free monoids, but I’m mostly interested in the slight efficiency win by not having to build up lists only to immediately deconstruct them.)

The last steps are to provide polymorphic operations and a reference implementation that satisfies the laws:

logMessage :: (MonadLog message m) => message -> m ()
logMessage message = liftLog [message]

newtype LoggingT message m a = LoggingT (ReaderT (message -> IO ()) m a)

instance MonadIO m => MonadLog message (LoggingT message m) where
  liftLog messages = LoggingT (\dispatchLog -> liftIO (for_ messages dispatchLog))

Does this reference implementation satisfy the monoid homomorphism laws that is required by MonadLog?

liftLog mempty
  = { definition of mempty for lists }
liftLog []
  = { definition of liftLog for LoggingT }
LoggingT (\dispatchLog -> liftIO (for_ [] dispatchLog))
  = { definition of for_ for [] }
LoggingT (\dispatchLog -> liftIO (return ()))
  = { liftIO . return = return }
LoggingT (\dispatchLog -> return ())
  = { definition of return for LoggingT }
return ()

So far so good!

liftLog (x <> y)
  = { definition of liftLog for LoggingT }
LoggingT (\dispatchLog -> liftIO (for_ (x ++ y) dispatchLog))
  = { for_ distributes over ++ }
LoggingT (\dispatchLog -> liftIO (for_ x dispatchLog >> for_ y dispatchLog)
  = { liftIO (f >>= g) = liftIO f >>= liftIO . g }
LoggingT (\dispatchLog -> liftIO (for_ x dispatchLog) >> liftIO (for_ y dispatchLog))
  = { definition of (>>=) for LoggingT }
LoggingT (\dispatchLog -> liftIO (for_ x dispatchLog)) >>
LoggingT (\dispatchLog -> liftIO (for_ y dispatchLog)) >>
  = { definition of liftLog for LoggingT }
liftLog x >> liftLog y

Bingo!

Further thoughts

In this post I presented a pattern for building mtl-like type classes in a mechanical fashion, and this suggests that maybe some of the details can be automatically dealt with. In the next few days I’ll be presenting my algebraic-transformers library which will show exactly that.

by Oliver Charles at January 26, 2016 12:00 AM

January 25, 2016

Yesod Web Framework

Auto generate Docbook XML for the Yesod book

I just made a minor tweak to the yesodweb.com-content repository, which contains all of the content that gets displayed on this site, including this blog post and the entire Yesod book. This repo contains both the original asciidoc version of the content, as well as the XML docbook files that are generated from it. Though that's a slightly contentious decision, storing it this way avoids having to have the asciidoc tools installed on the server hosting the website.

Until now, I've had to manually generate the XML from time to time after making updates or merging pull requests. However, doing this kind of manual maintenance is annoying. Much better to use automated systems. And whenever possible, I like to go for Travis CI. The setup is pretty simple, but involves some finer points that I thought may be interesting to others (not to mention good documentation for myself in the future).

Encrypted deployment key

In order to push from Travis back to Github, we need to have an SSH key. Travis allows us to put encrypted content into the repo, which anyone can see themselves. Within Travis, this file can be decrypted and then placed in the ~/.ssh directory with the following commands:

mkdir -p $HOME/.ssh
openssl aes-256-cbc -K $encrypted_92ac0cbbb1f3_key -iv $encrypted_92ac0cbbb1f3_iv -in id_rsa.enc -out id_rsa -d
mv id_rsa $HOME/.ssh
chmod 400 $HOME/.ssh/id_rsa

If you want to create your own encrypted files for Travis, you'll want to use the Travis command line interface's encrypt-file command.

Get necessary prerequisites installed

In order to build the XML files, we need three tools: asciidoc, GHC, and Stack. The first two can be installed via apt, but until travis-ci/apt-source-whitelist#7 is merged, we need to install Stack more manually. This is all still pretty easy to get set up:

addons:
  apt:
    packages:
    - asciidoc
    - ghc-7.10.3
    sources:
    - hvr-ghc

install:
- export PATH=$HOME/.local/bin:/opt/ghc/7.10.3/bin:$PATH
- mkdir -p $HOME/.local/bin
- curl -L https://www.stackage.org/stack/linux-x86_64 | tar xz --wildcards --strip-components=1 -C ~/.local/bin '*/stack'

Generate the XML

This part's easy: we wipe out the original XML files and run the generate.sh script:

- rm -f book/generated-xml/*
- book/tools/generate.sh
- git diff

We run git diff at the end to provide some useful feedback during PRs of the resulting XML difference.

Commit and push

This is where the magic happens. Let's look at the code (a bash script inlined in the YAML for Travis):

- |
  if [ $TRAVIS_PULL_REQUEST != false ]
  then
    echo Not pushing diff for a pull request
  elif [ -n "$(git status --porcelain)" ]
  then
    mkdir -p $HOME/.ssh
    openssl aes-256-cbc -K $encrypted_92ac0cbbb1f3_key -iv $encrypted_92ac0cbbb1f3_iv -in id_rsa.enc -out id_rsa -d
    mv id_rsa $HOME/.ssh
    chmod 400 $HOME/.ssh/id_rsa
    git config --global user.email "michael+travis@snoyman.com"
    git config --global user.name "Travis job for yesodweb/yesodweb.com-content"
    git add -A
    git commit -m "Travis auto-generate XML files, $(date --utc --iso=sec)"
    git push git@github.com:yesodweb/yesodweb.com-content.git HEAD:$TRAVIS_BRANCH
  else
    echo No changes present
  fi

If we're looking at a pull request, we don't want to ever push to the branch. (Travis will also prevent us from making a silly mistake here, since the decryption key we need to get the SSH key won't be available.) We also check if there are any changes to the XML files. But in the case of a non-PR build that has changes, we:

  1. Set up the SSH key, as we described above
  2. Commit all changes locally
  3. Push the changes to the current branch (1$TRAVIS_BRANCH`)

Full file

You can look at the current version of the .travis.yml on Github. Here's the content at the time of writing:

language: c
sudo: false

cache:
  directories:
  - $HOME/.stack

addons:
  apt:
    packages:
    - asciidoc
    - ghc-7.10.3
    sources:
    - hvr-ghc

install:
- export PATH=$HOME/.local/bin:/opt/ghc/7.10.3/bin:$PATH
- mkdir -p $HOME/.local/bin
- curl -L https://www.stackage.org/stack/linux-x86_64 | tar xz --wildcards --strip-components=1 -C ~/.local/bin '*/stack'

script:
- rm -f book/generated-xml/*
- book/tools/generate.sh
- git diff
- |
  if [ $TRAVIS_PULL_REQUEST != false ]
  then
    echo Not pushing diff for a pull request
  elif [ -n "$(git status --porcelain)" ]
  then
    mkdir -p $HOME/.ssh
    openssl aes-256-cbc -K $encrypted_92ac0cbbb1f3_key -iv $encrypted_92ac0cbbb1f3_iv -in id_rsa.enc -out id_rsa -d
    mv id_rsa $HOME/.ssh
    chmod 400 $HOME/.ssh/id_rsa
    git config --global user.email "michael+travis@snoyman.com"
    git config --global user.name "Travis job for yesodweb/yesodweb.com-content"
    git add -A
    git commit -m "Travis auto-generate XML files, $(date --utc --iso=sec)"
    git push git@github.com:yesodweb/yesodweb.com-content.git HEAD:$TRAVIS_BRANCH
  else
    echo No changes present
  fi

There's nothing particularly complicated or earth-shattering about this approach, but hopefully putting it all together like this can help others implement this themselves more easily.

January 25, 2016 10:30 AM

January 24, 2016

Magnus Therning

Freer play with effects

In the previous posts on my playing with free I got stuck at combining APIs. I recalled reading a paper on extensible effects as an alternatve to monad transformers. I have to admit to not having finished the paper, and not quite understanding the part I did read. When looking it up again I found that the work had continued and that there is a paper on more extensible effects. (I got to it via http://okmij.org/ftp/Haskell/extensible/.)

A quick search of Hackage revealed the package extensible-effects with an implementation of the ideas, including the stuff in the latter paper. So, what would the examples from my previous posts look like using extensible effects?

Opening

The examples require a few extensions and modules:

{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE TypeOperators #-}

and

import Control.Eff
import Control.Eff.Lift
import Control.Eff.Operational
import Data.Typeable

Just an API

This part was greatly helped by the fact that there is a example in extensible-effects.

I start with defining the SimpleFile API using GADTs

data SimpleFileAPI a where
  LoadFile :: FilePath -> SimpleFileAPI String
  SaveFile :: FilePath -> String -> SimpleFileAPI ()

The usage of the constructors need to be wrapped up in singleton. To remember that I create two convenience functions

loadFile :: Member (Program SimpleFileAPI) r => FilePath -> Eff r String
loadFile = singleton . LoadFile

saveFile :: Member (Program SimpleFileAPI) r => FilePath -> String -> Eff r ()
saveFile fp = singleton . SaveFile fp

For withSimpleFile I only have to modify the type

withSimpleFile :: Member (Program SimpleFileAPI) r => (String -> String) -> FilePath -> Eff r ()
withSimpleFile f fp = do
  d <- loadFile fp
  let result = f d
  saveFile (fp ++ "_new") result

Now for the gut of it, the interpreter.

runSimpleFile :: (Member (Lift IO) r, SetMember Lift (Lift IO) r) => Eff (Program SimpleFileAPI :> r) a -> Eff r a
runSimpleFile = runProgram f
  where
    f :: (Member (Lift IO) r, SetMember Lift (Lift IO) r) => SimpleFileAPI a -> Eff r a
    f (LoadFile fp) = lift $ readFile fp
    f (SaveFile fp s) = lift $ writeFile fp s

Runnnig it is fairly simple after this

> :! cat test.txt 
Lorem ipsum dolor sit amet, consectetur adipiscing elit. Donec a diam lectus.
Sed sit amet ipsum mauris. Maecenas congue ligula ac quam viverra nec
consectetur ante hendrerit.
> runLift $ runSimpleFile $ withSimpleFile (map toUpper) "test.txt"
> :! cat test.txt_new 
LOREM IPSUM DOLOR SIT AMET, CONSECTETUR ADIPISCING ELIT. DONEC A DIAM LECTUS.
SED SIT AMET IPSUM MAURIS. MAECENAS CONGUE LIGULA AC QUAM VIVERRA NEC
CONSECTETUR ANTE HENDRERIT.

Now, that was pretty easy. It looks almost exactly like when using Free, only without the Functor instance and rather more complicated types.

Combining two APIs

Now I get to the stuff that I didn’t manage to do using Free; combining two different APIs.

I start with defining another API. This one is truly a play example, sorry for that, but it doesn’t really matter. The type with convenience function looks like this

data StdIoAPI a where
  WriteStrLn :: String -> StdIoAPI ()

writeStrLn :: Member (Program StdIoAPI) r => String -> Eff r ()
writeStrLn = singleton . WriteStrLn

The interpreter then is straight forward

runStdIo :: (Member (Lift IO) r, SetMember Lift (Lift IO) r) => Eff (Program StdIoAPI :> r) a -> Eff r a
runStdIo = runProgram f
  where
    f :: (Member (Lift IO) r, SetMember Lift (Lift IO) r) => StdIoAPI a -> Eff r a
    f (WriteStrLn s) = lift $ putStrLn s

Now I just need a program that combines the two APIs

verboseWithSimpleFile :: (Member (Program StdIoAPI) r, Member (Program SimpleFileAPI) r) =>
                         (String -> String) -> String -> Eff r ()
verboseWithSimpleFile f fp = writeStrLn ("verboseWithSimpleFile on " ++ fp) >> withSimpleFile f fp

That type is surprisingly clear I find, albeit a bit on the long side. Running it is just a matter of combining runStdIo and runSimpleFile.

> :! cat test.txt 
Lorem ipsum dolor sit amet, consectetur adipiscing elit. Donec a diam lectus.
Sed sit amet ipsum mauris. Maecenas congue ligula ac quam viverra nec
consectetur ante hendrerit.
> runLift $ runSimpleFile $ runStdIo $ verboseWithSimpleFile (map toUpper) "test.txt"
verboseWithSimpleFile on test.txt
> :! cat test.txt_new 
LOREM IPSUM DOLOR SIT AMET, CONSECTETUR ADIPISCING ELIT. DONEC A DIAM LECTUS.
SED SIT AMET IPSUM MAURIS. MAECENAS CONGUE LIGULA AC QUAM VIVERRA NEC
CONSECTETUR ANTE HENDRERIT.

Oh, and it doesn’t matter in what order the interpreters are run!

At this point I got really excited about Eff because now it’s obvious that I’ll be able to write the logging “decorator”, in fact it’s clear that it’ll be rather simple too.

The logging

As before I start with a data type and a convenience function

data LoggerAPI a where
  Log :: String -> LoggerAPI ()

logStr :: Member (Program LoggerAPI) r => String -> Eff r ()
logStr = singleton . Log

For the decorating I can make use of the fact that APIs can be combined like I did above. That is, I don’t need to bother with any coproduct (Sum) or anything like that, I can simply just push in a call to logStr before each use of SimpleFileAPI

logSimpleFileOp :: (Member (Program SimpleFileAPI) r, Member (Program LoggerAPI) r) => SimpleFileAPI a -> Eff r a
logSimpleFileOp op@(LoadFile fp) = logStr ("LoadFile " ++ fp) *> singleton op
logSimpleFileOp op@(SaveFile fp _) = logStr ("SaveFile " ++ fp) *> singleton op

Of course an interpreter is needed as well

runLogger :: (Member (Lift IO) r, SetMember Lift (Lift IO) r) => Eff (Program LoggerAPI :> r) a -> Eff r a
runLogger = runProgram f
  where
    f :: (Member (Lift IO) r, SetMember Lift (Lift IO) r) => LoggerAPI a -> Eff r a
    f (Log s) = lift $ putStrLn s

Running is, once again, a matter of stacking interpreters

> :! cat test.txt
Lorem ipsum dolor sit amet, consectetur adipiscing elit. Donec a diam lectus.
Sed sit amet ipsum mauris. Maecenas congue ligula ac quam viverra nec
consectetur ante hendrerit.
> runLift $ runLogger $ runSimpleFile $ runProgram logSimpleFileOp $ withSimpleFile (map toUpper) "test.txt"
LoadFile test.txt
SaveFile test.txt_new
> :! cat test.txt_new 
LOREM IPSUM DOLOR SIT AMET, CONSECTETUR ADIPISCING ELIT. DONEC A DIAM LECTUS.
SED SIT AMET IPSUM MAURIS. MAECENAS CONGUE LIGULA AC QUAM VIVERRA NEC
CONSECTETUR ANTE HENDRERIT.

Closing thoughts

With Eff I’ve pretty much arrived where I wanted, I can

  • define APIs of operations in a simple way (simpler than when using Free even).
  • write a definitional interpreter for the operations.
  • combine two different APIs in the same function.
  • translate from one API to another (or even to a set of other APIs).

On top, I can do this without having to write a ridiculous amount of code.

I’m sure there are drawbacks as well. There’s a mention of some of them in the paper. However, for my typical uses of Haskell I haven’t read anything that would be a deal breaker.

January 24, 2016 12:00 AM

January 23, 2016

Richard Eisenberg

Haskell as a gradually typed dynamic language

I spent a few days this week at POPL (one day too short due to a massive blizzard currently pounding Philadelphia). As always at conferences, I had a great time and left full of new ideas.

This time, I sat in on a series of talks on gradual typing. Forgive me as I’m nowhere near an expert on gradual typing, but I took away this gist: with a gradual typing system, a type-checker does the best it can to assign static types; anything it can’t do is deferred to runtime in a dynamic type check.

As I nearly always do when considering a type system concept, I thought about how this might apply to Haskell. And I realized with a start that Haskell is only a stone’s throw away from a very spiffy gradually typed dynamic language! Let’s explore how this is the case.

(Disclaimer: I have no plans to implement any idea in this post. I also apologize, specifically, if I’m misusing the term “gradual typing”, which I’m not deeply versed in. This is all meant to be a bit tongue-in-cheek, though I think there’s a proper good idea in all of this.)

First, I wish to address a common fallacy about an existing feature in GHC:

Deferred type errors do not make Haskell a dynamic language

Recent versions of GHC come with a flag -fdefer-type-errors. (Naturally, this feature comes with its own published paper from ICFP’12.) With this flag enabled, type errors become warnings. When you try to run the code that contains a type error, you get a runtime exception. To wit:

> {-# OPTIONS_GHC -fdefer-type-errors #-}
> module GradualHaskell where
> 
> import Data.Typeable
> 
> ex1 = not 'x'

Compiling produces

/Users/rae/work/blog/011-dynamic/post.lhs:32:13: warning:
    • Couldn't match expected type ‘Bool’ with actual type ‘Char’
    • In the first argument of ‘not’, namely ‘'x'’
      In the expression: not 'x'
      In an equation for ‘ex1’: ex1 = not 'x'

Running produces

*** Exception: /Users/rae/work/blog/011-dynamic/post.lhs:32:13: error:
    • Couldn't match expected type ‘Bool’ with actual type ‘Char’
    • In the first argument of ‘not’, namely ‘'x'’
      In the expression: not 'x'
      In an equation for ‘ex1’: ex1 = not 'x'
(deferred type error)

What’s nice about deferred type errors is that they let you compile a program even with errors. You can then test the type-correct parts of your program while you’re still developing the type-incorrect parts.

However, deferred type errors don’t make Haskell a dynamic language.

Consider

> silly :: a -> b
> silly True  = False
> silly False = "Howdy!"
> silly 'x'   = 42

This, of course, compiles with lots of warnings. But you can’t successfully call silly, even at one of the values matched against. Running silly True produces a runtime type error. This is not what one would expect in a dynamic language, where silly True is perfectly False. The problem in Haskell is that we have no way to know if the type silly is called at is really Bool: all types are erased. All deferred type errors do is to take the normal compile-time type errors and stuff them into thunks that get evaluated when you force the ill-typed expression. Haskell still never does a runtime type check.

Preserving type information to runtime

The way to make Haskell into a proper dynamic language must be to retain type information to runtime. But we already have a way of doing runtime type checks: Typeable and friends.

The constraint Typeable a means that we know a’s type at runtime. The Typeable interface (from Data.Typeable) includes, for example, the function

cast :: (Typeable a, Typeable b) => a -> Maybe b

which does a runtime type equality test and, if the test succeeds, casts an expression’s type.

As of GHC 7.10, all statically-known types are Typeable. (Saying deriving Typeable is a no-op.) But type variables might still have a type unrecoverable at runtime.

So, all of this adds up to an interesting idea. I propose a new language extension -XDynamicTypes with two effects:

  1. All type variables automatically get a Typeable constraint.
  2. The type-checker behaves quite like it does with -fdefer-type-errors, but instead of putting an unconditional type error in an expression, it does a runtime type check. If the check succeeds, the expression evaluates normally; otherwise, a runtime error is thrown.

Change (1), coupled with the fact that all non-variable types are already Typeable, means that all types are known at runtime. Then, change (2) enabled runtime typing. Under this scenario, my silly function above would elaborate to

> forceCast :: (Typeable a, Typeable b) => a -> b
> forceCast x = case cast x of
>   Just y  -> y
>   Nothing -> error "type error" -- could even print the types if we wanted
> 
> notSilly :: (Typeable a, Typeable b) => a -> b
> notSilly true  | Just True  <- cast true  = forceCast False
> notSilly false | Just False <- cast false = forceCast "Howdy!"
> notSilly x     | Just 'x'   <- cast x     = forceCast (42 :: Int)

This definition works just fine. It does do a lot of casting, though. That’s because of silly’s very general type, a -> b, which is necessary due to the differing types of silly’s equations. However, if all the equations of a function have the same type, then the function is inferred with a precise type, and no casting is necessary. Indeed, in a program that is type-correct without -XDynamicTypes, no runtime checks would ever take place.

This idea seems to give you get the flexibility of dynamic types with the speed of static types (if your program is statically type-correct). And this general model seems to fit exactly in the space of possibilities of gradual type systems.

I’ve heard it said that Haskell is the best imperative programming language. Could it also become the best dynamic language?


by Richard Eisenberg at January 23, 2016 03:38 AM

January 20, 2016

Dominic Steinitz

Particle Smoothing

Introduction

The equation of motion for a pendulum of unit length subject to Gaussian white noise is

\displaystyle   \frac{\mathrm{d}^2\alpha}{\mathrm{d}t^2} = -g\sin\alpha + w(t)

We can discretize this via the usual Euler method

\displaystyle   \begin{bmatrix}  x_{1,i} \\  x_{2,i}  \end{bmatrix}  =  \begin{bmatrix}  x_{1,i-1} + x_{2,i-1}\Delta t \\  x_{2,i-1} - g\sin x_{1,i-1}\Delta t  \end{bmatrix}  +  \mathbf{q}_{i-1}

where q_i \sim {\mathcal{N}}(0,Q) and

\displaystyle   Q  =  \begin{bmatrix}  \frac{q^c \Delta t^3}{3} & \frac{q^c \Delta t^2}{2} \\  \frac{q^c \Delta t^2}{2} & {q^c \Delta t}  \end{bmatrix}

The explanation of the precise form of the covariance matrix will be the subject of another blog post; for the purpose of exposition of forward filtering / backward smoothing, this detail is not important.

Assume that we can only measure the horizontal position of the pendulum and further that this measurement is subject to error so that

\displaystyle   y_i = \sin x_i + r_k

where r_i \sim {\mathcal{N}}(0,R).

Particle Filtering can give us an estimate of where the pendulum is and its velocity using all the observations up to that point in time. But now suppose we have observed the pendulum for a fixed period of time then at times earlier than the time at which we stop our observations we now have observations in the future as well as in the past. If we can somehow take account of these future observations then we should be able to improve our estimate of where the pendulum was at any given point in time (as well as its velocity). Forward Filtering / Backward Smoothing is a technique for doing this.

Haskell Preamble

> {-# OPTIONS_GHC -Wall                     #-}
> {-# OPTIONS_GHC -fno-warn-name-shadowing  #-}
> {-# OPTIONS_GHC -fno-warn-type-defaults   #-}
> {-# OPTIONS_GHC -fno-warn-unused-do-bind  #-}
> {-# OPTIONS_GHC -fno-warn-missing-methods #-}
> {-# OPTIONS_GHC -fno-warn-orphans         #-}
> {-# LANGUAGE MultiParamTypeClasses        #-}
> {-# LANGUAGE TypeFamilies                 #-}
> {-# LANGUAGE ScopedTypeVariables          #-}
> {-# LANGUAGE ExplicitForAll               #-}
> {-# LANGUAGE DataKinds                    #-}
> {-# LANGUAGE FlexibleInstances            #-}
> {-# LANGUAGE MultiParamTypeClasses        #-}
> {-# LANGUAGE FlexibleContexts             #-}
> {-# LANGUAGE TypeFamilies                 #-}
> {-# LANGUAGE BangPatterns                 #-}
> {-# LANGUAGE GeneralizedNewtypeDeriving   #-}
> {-# LANGUAGE TemplateHaskell              #-}
> {-# LANGUAGE DataKinds                    #-}
> {-# LANGUAGE DeriveGeneric                #-}
> module PendulumSamples ( pendulumSamples
>                        , pendulumSamples'
>                        , testFiltering
>                        , testSmoothing
>                        , testFilteringG
>                        , testSmoothingG
>                        ) where
> import           Data.Random hiding ( StdNormal, Normal )
> import           Data.Random.Source.PureMT ( pureMT )
> import           Control.Monad.State ( evalState, replicateM )
> import qualified Control.Monad.Loops as ML
> import           Control.Monad.Writer ( tell, WriterT, lift,
>                                         runWriterT
>                                       )
> import           Numeric.LinearAlgebra.Static
>                  ( R, vector, Sym,
>                    headTail, matrix, sym,
>                    diag
>                  )
> import           GHC.TypeLits ( KnownNat )
> import           MultivariateNormal ( MultivariateNormal(..) )
> import qualified Data.Vector as V
> import           Data.Bits ( shiftR )
> import           Data.List ( transpose )
> import           Control.Parallel.Strategies
> import           GHC.Generics (Generic)

Simulation

Let’s first plot some typical trajectories of the pendulum.

> deltaT, g :: Double
> deltaT = 0.01
> g  = 9.81
> type PendulumState = R 2
> type PendulumObs = R 1
> pendulumSample :: MonadRandom m =>
>                   Sym 2 ->
>                   Sym 1 ->
>                   PendulumState ->
>                   m (Maybe ((PendulumState, PendulumObs), PendulumState))
> pendulumSample bigQ bigR xPrev = do
>   let x1Prev = fst $ headTail xPrev
>       x2Prev = fst $ headTail $ snd $ headTail xPrev
>   eta <- sample $ rvar (MultivariateNormal 0.0 bigQ)
>   let x1= x1Prev + x2Prev * deltaT
>       x2 = x2Prev - g * (sin x1Prev) * deltaT
>       xNew = vector [x1, x2] + eta
>       x1New = fst $ headTail xNew
>   epsilon <-  sample $ rvar (MultivariateNormal 0.0 bigR)
>   let yNew = vector [sin x1New] + epsilon
>   return $ Just ((xNew, yNew), xNew)

Let’s try plotting some samples when we are in the linear region with which we are familiar from school \sin\alpha \approx \alpha.

\displaystyle   \frac{\mathrm{d}^2\alpha}{\mathrm{d}t^2} = -g\alpha + w(t)

In this case we expect the horizontal displacement to be approximately equal to the angle of displacement and thus the observations to be symmetric about the actuals.

> bigQ :: Sym 2
> bigQ = sym $ matrix bigQl
> qc1 :: Double
> qc1 = 0.0001
> bigQl :: [Double]
> bigQl = [ qc1 * deltaT^3 / 3, qc1 * deltaT^2 / 2,
>           qc1 * deltaT^2 / 2,       qc1 * deltaT
>         ]
> bigR :: Sym 1
> bigR  = sym $ matrix [0.0001]
> m0 :: PendulumState
> m0 = vector [0.01, 0]
> pendulumSamples :: [(PendulumState, PendulumObs)]
> pendulumSamples = evalState (ML.unfoldrM (pendulumSample bigQ bigR) m0) (pureMT 17)

But if we work in a region in which linearity breaks down then the observations are no longer symmetrical about the actuals.

> bigQ' :: Sym 2
> bigQ' = sym $ matrix bigQl'
> qc1' :: Double
> qc1' = 0.01
> bigQl' :: [Double]
> bigQl' = [ qc1' * deltaT^3 / 3, qc1' * deltaT^2 / 2,
>            qc1' * deltaT^2 / 2,       qc1' * deltaT
>          ]
> bigR' :: Sym 1
> bigR'  = sym $ matrix [0.1]
> m0' :: PendulumState
> m0' = vector [1.6, 0]
> pendulumSamples' :: [(PendulumState, PendulumObs)]
> pendulumSamples' = evalState (ML.unfoldrM (pendulumSample bigQ' bigR') m0') (pureMT 17)

Filtering

We do not give the theory behind particle filtering. The interested reader can either consult Särkkä (2013) or wait for a future blog post on the subject.

> nParticles :: Int
> nParticles = 500

The usual Bayesian update step.

> type Particles a = V.Vector a
> oneFilteringStep ::
>   MonadRandom m =>
>   (Particles a -> m (Particles a)) ->
>   (Particles a -> Particles b) ->
>   (b -> b -> Double) ->
>   Particles a ->
>   b ->
>   WriterT [Particles a] m (Particles a)
> oneFilteringStep stateUpdate obsUpdate weight statePrevs obs = do
>   tell [statePrevs]
>   stateNews <- lift $ stateUpdate statePrevs
>   let obsNews = obsUpdate stateNews
>   let weights       = V.map (weight obs) obsNews
>       cumSumWeights = V.tail $ V.scanl (+) 0 weights
>       totWeight     = V.last cumSumWeights
>   vs <- lift $ V.replicateM nParticles (sample $ uniform 0.0 totWeight)
>   let js = indices cumSumWeights vs
>       stateTildes = V.map (stateNews V.!) js
>   return stateTildes

The system state and observable.

> data SystemState a = SystemState { x1  :: a, x2  :: a }
>   deriving (Show, Generic)
> instance NFData a => NFData (SystemState a)
> newtype SystemObs a = SystemObs { y1  :: a }
>   deriving Show

To make the system state update a bit more readable, let’s introduce some lifted arithmetic operators.

> (.+), (.*), (.-) :: (Num a) => V.Vector a -> V.Vector a -> V.Vector a
> (.+) = V.zipWith (+)
> (.*) = V.zipWith (*)
> (.-) = V.zipWith (-)

The state update itself

> stateUpdate :: Particles (SystemState Double) ->
>                 Particles (SystemState Double)
> stateUpdate xPrevs = V.zipWith SystemState x1s x2s
>   where
>     ix = V.length xPrevs
> 
>     x1Prevs = V.map x1 xPrevs
>     x2Prevs = V.map x2 xPrevs
> 
>     deltaTs = V.replicate ix deltaT
>     gs = V.replicate ix g
>     x1s = x1Prevs .+ (x2Prevs .* deltaTs)
>     x2s = x2Prevs .- (gs .* (V.map sin x1Prevs) .* deltaTs)

and its noisy version.

> stateUpdateNoisy :: MonadRandom m =>
>                     Sym 2 ->
>                     Particles (SystemState Double) ->
>                     m (Particles (SystemState Double))
> stateUpdateNoisy bigQ xPrevs = do
>   let xs = stateUpdate xPrevs
> 
>       x1s = V.map x1 xs
>       x2s = V.map x2 xs
> 
>   let ix = V.length xPrevs
>   etas <- replicateM ix $ sample $ rvar (MultivariateNormal 0.0 bigQ)
> 
>   let eta1s, eta2s :: V.Vector Double
>       eta1s = V.fromList $ map (fst . headTail) etas
>       eta2s = V.fromList $ map (fst . headTail . snd . headTail) etas
> 
>   return (V.zipWith SystemState (x1s .+ eta1s) (x2s .+ eta2s))

The function which maps the state to the observable.

> obsUpdate :: Particles (SystemState Double) ->
>              Particles (SystemObs Double)
> obsUpdate xs = V.map (SystemObs . sin . x1) xs

And finally a function to calculate the weight of each particle given an observation.

> weight :: forall a n . KnownNat n =>
>           (a -> R n) ->
>           Sym n ->
>           a -> a -> Double
> weight f bigR obs obsNew = pdf (MultivariateNormal (f obsNew) bigR) (f obs)

The variance of the prior.

> bigP :: Sym 2
> bigP = sym $ diag 0.1

Generate our ensemble of particles chosen from the prior,

> initParticles :: MonadRandom m =>
>                  m (Particles (SystemState Double))
> initParticles = V.replicateM nParticles $ do
>   r <- sample $ rvar (MultivariateNormal m0' bigP)
>   let x1 = fst $ headTail r
>       x2 = fst $ headTail $ snd $ headTail r
>   return $ SystemState { x1 = x1, x2 = x2}

run the particle filter,

> runFilter :: Int -> [Particles (SystemState Double)]
> runFilter nTimeSteps = snd $ evalState action (pureMT 19)
>   where
>     action = runWriterT $ do
>       xs <- lift $ initParticles
>       V.foldM
>         (oneFilteringStep (stateUpdateNoisy bigQ') obsUpdate (weight f bigR'))
>         xs
>         (V.fromList $ map (SystemObs . fst . headTail . snd)
>                           (take nTimeSteps pendulumSamples'))

and extract the estimated position from the filter.

> testFiltering :: Int -> [Double]
> testFiltering nTimeSteps = map ((/ (fromIntegral nParticles)). sum . V.map x1)
>                                (runFilter nTimeSteps)

Smoothing

If we could calculate the marginal smoothing distributions \{p(x_t \,|\, y_{1:T})\}_{i=1}^T then we might be able to sample from them. Using the Markov assumption of our model that x_i is independent of y_{i+1:N} given x_{i+1}, we have

\displaystyle   \begin{aligned}  \overbrace{p(x_i \,|\, y_{1:N})}^{\mathrm{smoother}\,\mathrm{at}\, i} &=  \int p(x_i, x_{i+1} \,|\, y_{1:N}) \,\mathrm{d}x_{i+1} & \text{marginal distribution} \\  &=  \int p(x_{i+1} \,|\, y_{1:N}) \,p(x_{i} \,|\, y_{1:N}, x_{i+1}) \,\mathrm{d}x_{i+1} & \text{conditional density} \\  &=  \int p(x_{i+1} \,|\, y_{1:N}) \,p(x_{i} \,|\, y_{1:i}, x_{i+1}) \,\mathrm{d}x_{i+1} & \text{Markov model} \\  &=  \int p(x_{i+1} \,|\, y_{1:N}) \,  \frac{p(x_{i}, x_{i+1} \,|\, y_{1:i})}{p(x_{i+1} \,|\, y_{1:i})}  \,\mathrm{d}x_{i+1}  & \text{conditional density} \\  &=  \int p(x_{i+1} \,|\, y_{1:N}) \,  \frac{p(x_{i+1} \,|\, x_{i}, y_{1:i})  \,p(x_{i} \,|\, y_{1:i})}{p(x_{i+1} \,|\, y_{1:i})}  \,\mathrm{d}x_{i+1}  & \text{conditional density} \\  &=  \int \overbrace{p(x_{i+1} \,|\, y_{1:N})}^{\text{smoother at }i+1} \,  \underbrace{  \overbrace{p(x_{i} \,|\, y_{1:i})}^{\text{filter at }i}  \frac{p(x_{i+1} \,|\, x_{i})}       {p(x_{i+1} \,|\, y_{1:i})}  }  _{\text{backward transition }p(x_{i} \,|\, y_{1:i},\,x_{i+1})}  \,\mathrm{d}x_{i+1}  & \text{Markov model}  \end{aligned}

We observe that this is a (continuous state space) Markov process with a non-homogeneous transition function albeit one which goes backwards in time. Apparently for conditionally Gaussian linear state-space models, this is known as RTS, or Rauch-Tung-Striebel smoothing (Rauch, Striebel, and Tung (1965)).

According to Cappé (2008),

  • It appears to be efficient and stable in the long term (although no proof was available at the time the slides were presented).

  • It is not sequential (in particular, one needs to store all particle positions and weights).

  • It has numerical complexity proportional O(n^2) where N is the number of particles.

We can use this to sample paths starting at time i = N and working backwards. From above we have

\displaystyle   p(x_i \,|\, X_{i+1}, Y_{1:N}) =  \frac{p(X_{i+1} \,|\, x_{i})  \,p(x_{i} \,|\, Y_{1:i})}{p(X_{i+1} \,|\, Y_{1:i})}  =  Z  \,p(X_{i+1} \,|\, x_{i})  \,p(x_{i} \,|\, Y_{1:i})

where Z is some normalisation constant (Z for “Zustandssumme” – sum over states).

From particle filtering we know that

\displaystyle   {p}(x_i \,|\, y_{1:i}) \approx \hat{p}(x_i \,|\, y_{1:i}) \triangleq \sum_{j=1}^M w_i^{(j)}\delta(x_i - x_i^{(j)})

Thus

\displaystyle   \hat{p}(x_i \,|\, X_{i+1}, Y_{1:i})  =  Z  \,p(X_{i+1} \,|\, x_{i})  \,\hat{p}(x_{i} \,|\, Y_{1:i})  =  \sum_{j=1}^M w_i^{(j)}\delta(x_i - x_i^{(j)})  \,p(X_{i+1} \,|\, x_{i})

and we can sample x_i from \{x_i^{(j)}\}_{1 \leq j \leq M} with probability

\displaystyle   \frac{w_k^{(i)}  \,p(X_{i+1} \,|\, x_{i})}  {\sum_{i=1}^N w_k^{(i)}  \,p(X_{i+1} \,|\, x_{i})}

Recalling that we have re-sampled the particles in the filtering algorithm so that their weights are all 1/M and abstracting the state update and state density function, we can encode this update step in Haskell as

> oneSmoothingStep :: MonadRandom m =>
>          (Particles a -> V.Vector a) ->
>          (a -> a -> Double) ->
>          a ->
>          Particles a ->
>          WriterT (Particles a) m a
> oneSmoothingStep stateUpdate
>                  stateDensity
>                  smoothingSampleAtiPlus1
>                  filterSamplesAti = do it
>   where
>     it = do
>       let mus = stateUpdate filterSamplesAti
>           weights =  V.map (stateDensity smoothingSampleAtiPlus1) mus
>           cumSumWeights = V.tail $ V.scanl (+) 0 weights
>           totWeight     = V.last cumSumWeights
>       v <- lift $ sample $ uniform 0.0 totWeight
>       let ix = binarySearch cumSumWeights v
>           xnNew = filterSamplesAti V.! ix
>       tell $ V.singleton xnNew
>       return $ xnNew

To sample a complete path we start with a sample from the filtering distribution at at time i = N (which is also the smoothing distribution)

> oneSmoothingPath :: MonadRandom m =>
>              (Int -> V.Vector (Particles a)) ->
>              (a -> Particles a -> WriterT (Particles a) m a) ->
>              Int -> m (a, V.Vector a)
> oneSmoothingPath filterEstss oneSmoothingStep nTimeSteps = do
>   let ys = filterEstss nTimeSteps
>   ix <- sample $ uniform 0 (nParticles - 1)
>   let xn = (V.head ys) V.! ix
>   runWriterT $ V.foldM oneSmoothingStep xn (V.tail ys)
> oneSmoothingPath' :: (MonadRandom m, Show a) =>
>              (Int -> V.Vector (Particles a)) ->
>              (a -> Particles a -> WriterT (Particles a) m a) ->
>              Int -> WriterT (Particles a) m a
> oneSmoothingPath' filterEstss oneSmoothingStep nTimeSteps = do
>   let ys = filterEstss nTimeSteps
>   ix <- lift $ sample $ uniform 0 (nParticles - 1)
>   let xn = (V.head ys) V.! ix
>   V.foldM oneSmoothingStep xn (V.tail ys)

Of course we need to run through the filtering distributions starting at i = N

> filterEstss :: Int -> V.Vector (Particles (SystemState Double))
> filterEstss n = V.reverse $ V.fromList $ runFilter n
> testSmoothing :: Int -> Int -> [Double]
> testSmoothing m n = V.toList $ evalState action (pureMT 23)
>   where
>     action = do
>       xss <- V.replicateM n $
>              snd <$> (oneSmoothingPath filterEstss (oneSmoothingStep stateUpdate (weight h bigQ')) m)
>       let yss = V.fromList $ map V.fromList $
>                 transpose $
>                 V.toList $ V.map (V.toList) $
>                 xss
>       return $ V.map (/ (fromIntegral n)) $ V.map V.sum $ V.map (V.map x1) yss

By eye we can see we get a better fit

and calculating the mean square error for filtering gives 1.87\times10^{-2} against the mean square error for smoothing of 9.52\times10^{-3}; this confirms the fit really is better as one would hope.

Unknown Gravity

Let us continue with the same example but now assume that g is unknown and that we wish to estimate it. Let us also assume that our apparatus is not subject to noise.

Again we have

\displaystyle   \frac{\mathrm{d}^2\alpha}{\mathrm{d}t^2} = -g\sin\alpha + w(t)

But now when we discretize it we include a third variable

\displaystyle   \begin{bmatrix}  x_{1,i} \\  x_{2,i} \\  x_{3,i}  \end{bmatrix}  =  \begin{bmatrix}  x_{1,i-1} + x_{2,i-1}\Delta t \\  x_{2,i-1} - x_{3,i-1}\sin x_{1,i-1}\Delta t \\  x_{3,i-1}  \end{bmatrix}  +  \mathbf{q}_{i-1}

where q_i \sim {\mathcal{N}}(0,Q)

\displaystyle   Q  =  \begin{bmatrix}  0 & 0 & 0 \\  0 & 0 & 0 \\  0 & 0 & \sigma^2_g  \end{bmatrix}

Again we assume that we can only measure the horizontal position of the pendulum so that

\displaystyle   y_i = \sin x_i + r_k

where r_i \sim {\mathcal{N}}(0,R).

> type PendulumStateG = R 3
> pendulumSampleG :: MonadRandom m =>
>                   Sym 3 ->
>                   Sym 1 ->
>                   PendulumStateG ->
>                   m (Maybe ((PendulumStateG, PendulumObs), PendulumStateG))
> pendulumSampleG bigQ bigR xPrev = do
>   let x1Prev = fst $ headTail xPrev
>       x2Prev = fst $ headTail $ snd $ headTail xPrev
>       x3Prev = fst $ headTail $ snd $ headTail $ snd $ headTail xPrev
>   eta <- sample $ rvar (MultivariateNormal 0.0 bigQ)
>   let x1= x1Prev + x2Prev * deltaT
>       x2 = x2Prev - g * (sin x1Prev) * deltaT
>       x3 = x3Prev
>       xNew = vector [x1, x2, x3] + eta
>       x1New = fst $ headTail xNew
>   epsilon <-  sample $ rvar (MultivariateNormal 0.0 bigR)
>   let yNew = vector [sin x1New] + epsilon
>   return $ Just ((xNew, yNew), xNew)
> pendulumSampleGs :: [(PendulumStateG, PendulumObs)]
> pendulumSampleGs = evalState (ML.unfoldrM (pendulumSampleG bigQg bigRg) mG) (pureMT 29)
> data SystemStateG a = SystemStateG { gx1  :: a, gx2  :: a, gx3 :: a }
>   deriving Show

The state update itself

> stateUpdateG :: Particles (SystemStateG Double) ->
>                 Particles (SystemStateG Double)
> stateUpdateG xPrevs = V.zipWith3 SystemStateG x1s x2s x3s
>   where
>     ix = V.length xPrevs
> 
>     x1Prevs = V.map gx1 xPrevs
>     x2Prevs = V.map gx2 xPrevs
>     x3Prevs = V.map gx3 xPrevs
> 
>     deltaTs = V.replicate ix deltaT
>     x1s = x1Prevs .+ (x2Prevs .* deltaTs)
>     x2s = x2Prevs .- (x3Prevs .* (V.map sin x1Prevs) .* deltaTs)
>     x3s = x3Prevs

and its noisy version.

> stateUpdateNoisyG :: MonadRandom m =>
>                      Sym 3 ->
>                      Particles (SystemStateG Double) ->
>                      m (Particles (SystemStateG Double))
> stateUpdateNoisyG bigQ xPrevs = do
>   let ix = V.length xPrevs
> 
>   let xs = stateUpdateG xPrevs
> 
>       x1s = V.map gx1 xs
>       x2s = V.map gx2 xs
>       x3s = V.map gx3 xs
> 
>   etas <- replicateM ix $ sample $ rvar (MultivariateNormal 0.0 bigQ)
>   let eta1s, eta2s, eta3s :: V.Vector Double
>       eta1s = V.fromList $ map (fst . headTail) etas
>       eta2s = V.fromList $ map (fst . headTail . snd . headTail) etas
>       eta3s = V.fromList $ map (fst . headTail . snd . headTail . snd . headTail) etas
> 
>   return (V.zipWith3 SystemStateG (x1s .+ eta1s) (x2s .+ eta2s) (x3s .+ eta3s))

The function which maps the state to the observable.

> obsUpdateG :: Particles (SystemStateG Double) ->
>              Particles (SystemObs Double)
> obsUpdateG xs = V.map (SystemObs . sin . gx1) xs

The mean and variance of the prior.

> mG :: R 3
> mG = vector [1.6, 0.0, 8.00]
> bigPg :: Sym 3
> bigPg = sym $ matrix [
>     1e-6, 0.0, 0.0
>   , 0.0, 1e-6, 0.0
>   , 0.0, 0.0, 1e-2
>   ]

Parameters for the state update; note that the variance is not exactly the same as in the formulation above.

> bigQg :: Sym 3
> bigQg = sym $ matrix bigQgl
> qc1G :: Double
> qc1G = 0.0001
> sigmaG :: Double
> sigmaG = 1.0e-2
> bigQgl :: [Double]
> bigQgl = [ qc1G * deltaT^3 / 3, qc1G * deltaT^2 / 2, 0.0,
>            qc1G * deltaT^2 / 2,       qc1G * deltaT, 0.0,
>                            0.0,                 0.0, sigmaG
>          ]

The noise of the measurement.

> bigRg :: Sym 1
> bigRg  = sym $ matrix [0.1]

Generate the ensemble of particles from the prior,

> initParticlesG :: MonadRandom m =>
>                  m (Particles (SystemStateG Double))
> initParticlesG = V.replicateM nParticles $ do
>   r <- sample $ rvar (MultivariateNormal mG bigPg)
>   let x1 = fst $ headTail r
>       x2 = fst $ headTail $ snd $ headTail r
>       x3 = fst $ headTail $ snd $ headTail $ snd $ headTail r
>   return $ SystemStateG { gx1 = x1, gx2 = x2, gx3 = x3}

run the particle filter,

> runFilterG :: Int -> [Particles (SystemStateG Double)]
> runFilterG n = snd $ evalState action (pureMT 19)
>   where
>     action = runWriterT $ do
>       xs <- lift $ initParticlesG
>       V.foldM
>         (oneFilteringStep (stateUpdateNoisyG bigQg) obsUpdateG (weight f bigRg))
>         xs
>         (V.fromList $ map (SystemObs . fst . headTail . snd) (take n pendulumSampleGs))

and extract the estimated parameter from the filter.

> testFilteringG :: Int -> [Double]
> testFilteringG n = map ((/ (fromIntegral nParticles)). sum . V.map gx3) (runFilterG n)

Again we need to run through the filtering distributions starting at i = N

> filterGEstss :: Int -> V.Vector (Particles (SystemStateG Double))
> filterGEstss n = V.reverse $ V.fromList $ runFilterG n
> testSmoothingG :: Int -> Int -> ([Double], [Double], [Double])
> testSmoothingG m n = (\(x, y, z) -> (V.toList x, V.toList y, V.toList z))  $
>                      mkMeans $
>                      chunks
>   where
> 
>     chunks =
>       V.fromList $ map V.fromList $
>       transpose $
>       V.toList $ V.map (V.toList) $
>       chunksOf m $
>       snd $ evalState (runWriterT action) (pureMT 23)
> 
>     mkMeans yss = (
>       V.map (/ (fromIntegral n)) $ V.map V.sum $ V.map (V.map gx1) yss,
>       V.map (/ (fromIntegral n)) $ V.map V.sum $ V.map (V.map gx2) yss,
>       V.map (/ (fromIntegral n)) $ V.map V.sum $ V.map (V.map gx3) yss
>       )
> 
>     action =
>       V.replicateM n $
>       oneSmoothingPath' filterGEstss
>                         (oneSmoothingStep stateUpdateG (weight hG bigQg))
>                         m

Again by eye we get a better fit but note that we are using the samples in which the state update is noisy as well as the observation so we don’t expect to get a very good fit.

Notes

Helpers for Converting Types

> f :: SystemObs Double -> R 1
> f = vector . pure . y1
> h :: SystemState Double -> R 2
> h u = vector [x1 u , x2 u]
> hG :: SystemStateG Double -> R 3
> hG u = vector [gx1 u , gx2 u, gx3 u]

Helpers for the Inverse CDF

That these are helpers for the inverse CDF is delayed to another blog post.

> indices :: V.Vector Double -> V.Vector Double -> V.Vector Int
> indices bs xs = V.map (binarySearch bs) xs
> binarySearch :: (Ord a) =>
>                 V.Vector a -> a -> Int
> binarySearch vec x = loop 0 (V.length vec - 1)
>   where
>     loop !l !u
>       | u <= l    = l
>       | otherwise = let e = vec V.! k in if x <= e then loop l k else loop (k+1) u
>       where k = l + (u - l) `shiftR` 1

Vector Helpers

> chunksOf :: Int -> V.Vector a -> V.Vector (V.Vector a)
> chunksOf n xs = ys
>   where
>     l = V.length xs
>     m  = 1 + (l - 1) `div` n
>     ys = V.unfoldrN m (\us -> Just (V.take n us, V.drop n us)) xs

Bibliography

Cappé, Olivier. 2008. “An Introduction to Sequential Monte Carlo for Filtering and Smoothing.” http://www-irma.u-strasbg.fr/~guillou/meeting/cappe.pdf.

Rauch, H. E., C. T. Striebel, and F. Tung. 1965. “Maximum Likelihood Estimates of Linear Dynamic Systems.” Journal of the American Institute of Aeronautics and Astronautics 3 (8): 1445–50.

Särkkä, Simo. 2013. Bayesian Filtering and Smoothing. New York, NY, USA: Cambridge University Press.


by Dominic Steinitz at January 20, 2016 06:17 PM

January 19, 2016

Neil Mitchell

One Bag of Huel

I've been a fan of the idea of meal replacement products for a while - the Matrix gruel always seemed simple and appealing. One such product is Huel, which is available in the UK, seems fairly sensibly thought out, and isn't cadim-yummy. When having lunch at home, I found myself eating stuff that was nutritionally garbage, inconvenient and time consuming to get and not very nice. Given the downsides, Huel seemed worth a try. Having gone through one bag, it seems to be working nicely, and I intend to continue this as my default lunch-at-home plan.

General random thoughts on Huel:

  • My wife pronounces Huel with a strong and long 'u', huuuuuuel, to imitate the sound of someone vomiting. Soylent is probably a better name.
  • I bought a first bag, and they threw in a free flask/shaker and t-shirt. I've been using the flask they supplied, and the t-shirt is very nice.
  • I like that it has all the vitamins and minerals required, so I'm not likely to be missing anything.
  • The taste is OK. Not horrid, perfectly drinkable, but not too nice, so unlikely to go overboard. They got the balance right.
  • Most of the flavouring suggestions seem like someone trolling. The default vanilla flavour works fine for me.
  • The taste/consistency depends a lot on exactly how much water goes in, so experiment a bit (I find 420ml and 3 scoops works for me).
  • By the end of the flask, it's significantly more dense, so I add a little bit of water with about 40ml to go.
  • If you add the powder before the water it's a bit of a disaster and you get clumped powder at the bottom.
  • Wash the flask as soon as you finish, or it sets quite hard.
  • I think I spend about 3 mins preparation time making the mixture and washing up after, which isn't bad.
  • The pouches come sealed at the top with a resealable strip that is initially unsealed. Cut the top of the strip, don't tear it, or you bump into the resealable strip. Before starting, you have to clean the resealable strip out with a knife (which gives a bad first impression, but otherwise is unproblematic).
  • The powder has a habit of escaping a bit when filling up the flask. If it gets on clothes, it stays there until you wash them, and a gentle brushing down has little effect. A little annoying, but not fatal.
  • It's sufficiently filling that I think I'm probably going under the number of calories I should be getting at lunch. I'm experimenting with trying to start my lunch Huel a bit earlier, and then have another Huel or snack in the afternoon - splitting lunch in two.

Since this is a post about a specific product, I should probably mention I have no relationship with the company other than having spent £45 on Huel.

by Neil Mitchell (noreply@blogger.com) at January 19, 2016 12:25 PM

Dan Burton

Stackage is reverting to aeson-0.9

Starting immediately, Stackage nightly builds will be stepping back from aeson-0.10.0.0 to aeson-0.9.0.1. Due to issues with aeson-0.10, we are planning to discontinue LTS 4. Next Sunday (2016-01-24) we will begin LTS 5, which will ship with aeson-0.9. Under normal circumstances, the support … Continue reading

by Dan Burton at January 19, 2016 03:56 AM

January 18, 2016

Darcs

darcs hacking sprint 10 report

Last weekend we had our tenth Darcs sprint, and our first one in Spain. This time indeed, the sprint was organised in the University of Seville, ETSII (Technical Superior School of Informatics Engineering), on January 15th to 17th.



We were 3 participants: Florent Becker, Guillaume Hoffmann and Ganesh Sittampalam. We also had Pierre-Étienne Meunier on video call and Simon Michael on IRC.


Darcs and Pijul integration


One major topic during the whole sprint was the possible integration of Darcs with Pijul. Pijul is a new version control system based on a different patch theory, whose main author is Pierre-Étienne Meunier. Florent also contributes to Pijul and announced its first release last October.

Pijul is promising in terms of how it handles conflicts in a better way than Darcs (better as: better presentation to the user and better performance). There may be a future where Darcs uses Pijul patches by default.  We had many conversations with Florent to understand the internals of Pijul and how it manages patches.

On the first day of the sprint we did a video call with Pierre-Étienne Meunier, to discuss integration of Pijul core with Darcs. It happens that the Darcs code is modular enough to handle Pijul patches (with some work). That afternoon Florent started to work on a Haskell binding for libpijul (through a C binding maintained by Pierre-Étienne, Pijul being implemented in Rust).

Ganesh, Florent and Pierre-Étienne are going to work towards a better integration of both systems. Pierre-Étienne plans to release a 0.2 version of Pijul soon.


Ganesh and Florent with Pierre-Étienne on video call

Renaming Patch/RealPatch to RepoPatchV1/RepoPatchV2

The code of Darcs contains many different layers of patch types. One of them is represented by the two types Patch and RealPatch, and specifies the behaviour of named patch when they are commuted and in case of conflicts. The "Patch" type is the behaviour of patches in repositories with the darcs-1 patch semantics (which can still be created by Darcs) and "RealPatch" is for darcs-2 semantics (the current default of Darcs). I sent a patch to rename these types into something less confusing: RepoPatchV1 and RepoPatchV2.


Interactive selection performance and refactoring

Even if we wrote a patch that improved greatly performance during the last sprint (and we now have a unit test for it), the command "darcs rollback -p ." still remains much slower than "darcs rollback" before presenting the first choice of patch to the user. Florent determined that this was because the action of matching patches within interactive selection is not lazy, ie, the whole list of patches has to be scanned and classified before the first prompt is shown to the user. Florent unearthed a refactor he had of the patch selection code and started rebasing it against the current code.


User manual and developer handbook

We want Darcs to have a user manual again, and a developer handbook that would compile documentation for programmers and computer scientists. We decided the manual should live in darcs' repository itself (so that it stays up-to-date) and the developer handbook on the wiki.

Darcs on Stackage

On IRC, Simon Michael (after an initial request by Joachim Breitner) committed himself to maintain a stack.yaml file for Darcs, and during the weekend Darcs was added to stackage for easier building.


Cleanup, fixes and refactorings

Ganesh tracked down bugs in rebase and sent a few cleanup patches. Moreover he's improving the code of "darcs test" (formerly called "darcs trackdown") so that uncompilable states are neither considered as Passing nor Failing, and bisect is going to be more efficient.


What happens next

I am going to release Darcs 2.10.3 within a couple of weeks, and Darcs 2.12 within a couple of months. This new major version will have optimizations (some of them are already backported to the 2.10 branch) and code refactorings. It may contain the stash feature currently developed by Ganesh. 

This year we hope to have another sprint, and to have more developers participating. Please consult the How to Help, Developer's Getting Started and Projects page on the wiki to get involved!

Ganesh, Florent and Guillaume



by guillaume (noreply@blogger.com) at January 18, 2016 04:57 PM

Don Stewart (dons)

Haskell developer roles at Standard Chartered [London, Singapore]

The Strats team at Standard Chartered has three open positions for typed functional programming developers, based in London and Singapore. Strats are a specialized software engineering and quantitative analysis team who build a broad range of software for financial markets users at Standard Chartered.

You will work on the trading floor, directly with traders, building software to automate their work and improve their efficiency. The focus of these role will be on market pricing feed automation and algorithmic pricing.

You will use Haskell for almost all tasks: data analysis, market data publishing, database access, web services, desktop GUIs, large parallel tasks, quantitative models, solvers, everything. This is a fast paced role – code you write today will be deployed within hours to hundreds of users and has to work. 

These are permanent, associate director and director positions, in London and Singapore as part of the Strats global team. Demonstrated experience in typed FP (Haskell, OCaml, F# etc) is required. We have around 3 million lines of Haskell, and our own Haskell compiler. In this context we look for skill and taste in typed functional programming to capture and abstract over complex, messy systems.

Experience writing typed APIs to external systems such as databases, web services, pub/sub platforms is very desirable. We like working code, so if you have Hackage or github libraries, we definitely want to see them. We also like StackOverflow answers, blog posts, academic papers, or other arenas where you can show broad FP ability. A PhD in computer science is a strong advantage.

The role requires physical presence on the trading floor in Singapore or London. Remote work is not an option. You will have some project and client management skills — you will talk to users, understand their problems and then implement and deliver what they really need. No financial background is required. These positions have attractive remuneration for the right candidates. Relocation support will also be provided. Contracting-based positions are also possible if desired.

Applicants who don’t necessarily meet all criteria but have an interest in working in Singapore in particular, and have an FP background, are encouraged to apply.

More info about our development process is in the 2012 PADL keynote, and a 2013 HaskellCast interview.

If this sounds exciting to you, please send your resume to me – donald.stewart <at> sc.com.


Tagged: jobs

by Don Stewart at January 18, 2016 01:25 PM

January 17, 2016

wren gayle romano

A week of "P"s

The next week+ I'll be in St. Petersburg Florida for PEPM, PADL, POPL, PPS, and PPAML PI (also CPP and OBT). Would've mentioned it sooner, but it's a bit of a last minute thing. I love reconnecting with old friends and meeting new folks, so feel free to come say hi. If you want to meet up for dinner or such, leave a comment with when/where to find you, or just look for the tall gal with the blue streak in her hair.



comment count unavailable comments

January 17, 2016 06:34 PM

Gabriel Gonzalez

How to contribute to the Haskell ecosystem

I wanted to share a few quick ways that beginning Haskell programmers can contribute to the Haskell ecosystem. I selected these tasks according to a few criteria:

  • They are fun! These tasks showcase enjoyable tricks
  • They are easy! They straightforwardly apply existing libraries
  • They are useful! You can probably find something relevant to your project

For each task I'll give a brief end-to-end example of what a contribution might look like and link to relevant educational resources.

This post only assumes that you have the stack build tool installed, which you can get from haskellstack.com. This tool takes care of the rest of the Haskell toolchain for you so you don't need to install anything else.

Contribution #1: Write a parser for a new file format

Writing parsers in Haskell is just about the slickest thing imaginable. For example, suppose that we want to parse the PPM "plain" file format, which is specified like this [Source]:

Each PPM image consists of the following:

  1. A "magic number" for identifying the file type. A ppm image's magic number is the two characters "P3".
  2. Whitespace (blanks, TABs, CRs, LFs).
  3. A width, formatted as ASCII characters in decimal.
  4. Whitespace.
  5. A height, again in ASCII decimal.
  6. Whitespace.
  7. The maximum color value (Maxval), again in ASCII decimal. Must be less than 65536 and more than zero.
  8. A single whitespace character (usually a newline).
  9. A raster of Height rows, in order from top to bottom. Each row consists of Width pixels, in order from left to right. Each pixel is a triplet of red, green, and blue samples, in that order. Each sample is represented as an ASCII decimal number.

The equivalent Haskell parser reads almost exactly like the specification:

{-# LANGUAGE OverloadedStrings #-}

import Control.Monad (guard)
import Data.Attoparsec.Text

data PPM = PPM
{ width :: Int
, height :: Int
, maximumColorValue :: Int
, image :: [[RGB]]
} deriving (Show)

data RGB = RGB
{ red :: Int
, green :: Int
, blue :: Int
} deriving (Show)

ppm3 :: Parser PPM
ppm6 = do
"P3"
skipMany1 space
w <- decimal
skipMany1 space
h <- decimal
skipMany1 space
maxVal <- decimal
guard (maxVal < 65536)
space
let sample = do
lo <- decimal
skipMany1 space
return lo
let pixel = do
r <- sample
g <- sample
b <- sample
return (RGB r g b)

rows <- count h (count w pixel)
return (PPM w h maxVal rows)

We can try to test our parser out on the following example file:

$ cat example.ppm
P6
4 4
255
0 0 0 100 0 0 0 0 0 255 0 255
0 0 0 0 255 175 0 0 0 0 0 0
0 0 0 0 0 0 0 15 175 0 0 0
255 0 255 0 0 0 0 0 0 255 255 255

We don't even have to compile a program to test our code. We can load our code into the Haskell REPL for quick feedback on whether or not our code works:

$ stack ghci attoparsec --resolver=lts-3.14
...
Prelude> :load ppm.hs
[1 of 1] Compiling Main ( ppm.hs, interpreted )
Ok, modules loaded: Main.
*Main> txt <- Data.Text.IO.readFile "example.ppm"
*Main> parseOnly ppm3 txt
Right (PPM {width = 4, height = 4, maximumColorValue = 255,
image = [[RGB {red = 0, green = 0, blue = 0},RGB {red = 100,
green = 0, blue = 0},RGB {red = 0, green = 0, blue = 0},RGB
{red = 255, green = 0, blue = 255}],[RGB {red = 0, green =
0, blue = 0},RGB {red = 0, green = 255, blue = 175},RGB {red
= 0, green = 0, blue = 0},RGB {red = 0, green = 0, blue = 0
}],[RGB {red = 0, green = 0, blue = 0},RGB {red = 0, green =
0, blue = 0},RGB {red = 0, green = 15, blue = 175},RGB {red
= 0, green = 0, blue = 0}],[RGB {red = 255, green = 0, blue
= 255},RGB {red = 0, green = 0, blue = 0},RGB {red = 0, gre
en = 0, blue = 0},RGB {red = 255, green = 255, blue = 255}]]
})

Works like a charm!

You can very quickly get your hands dirty with Haskell by writing a parser that converts a file format you know and love into a more structured data type.

To learn more about parser combinators in Haskell, I highly recommend this "functional pearl":

... as well as this attoparsec tutorial:

To see a "long form" example of attoparsec, check out this HTTP request parser written using attoparsec:

I use "long form" in quotes because the entire code is around 60 lines long.

Contribution #2: Write a useful command-line tool

Haskell's turtle library makes it very easy to write polished command-line tools in a tiny amount of code. For example, suppose that I want to build a simple comand-line tool for managing a TODO list stored in a todo.txt file. First I just need to provide a subroutine for displaying the current list:

{-# LANGUAGE OverloadedStrings #-}

import Turtle

todoFile = "TODO.txt"

todoItem = d%": "%s

display :: IO ()
display = sh (do
(n, line) <- nl (input todoFile)
echo (format todoItem n line) )

... a subroutine for adding an item to the list:

add :: Text -> IO ()
add txt = runManaged (do
tempfile <- mktempfile "/tmp" "todo"
output tempfile (input todoFile <|> pure txt)
mv tempfile todoFile )

... and a subroutine for removing an item from the list:

remove :: Int -> IO ()
remove m = runManaged (do
tempfile <- mktempfile "/tmp" "todo"
output tempfile (do
(n, line) <- nl (input todoFile)
guard (m /= n)
return line )
mv tempfile todoFile )

... then I can just wrap them in a command line API. I create a command line parser that runs display by default if the command line is empty:

parseDisplay :: Parser (IO ())
parseDisplay = pure display

... then a command line parser for the add subcommand:

parseAdd :: Parser (IO ())
parseAdd =
fmap add
(subcommand "add" "Add a TODO item"
(argText "item" "The item to add to the TODO list") )

... and a command line parser for the remove subcommand:

parseRemove :: Parser (IO ())
parseRemove =
fmap remove
(subcommand "rm" "Remove a TODO item"
(argInt "index" "The numeric index of the TODO item to remove") )

Finally, I combine them into a single composite parser for all three subcommands:

parseCommand :: Parser (IO ())
parseCommand = parseDisplay <|> parseAdd <|> parseRemove

... and run the parser:

main = do
command <- options "A TODO list manager" parseCommand
exists <- testfile todoFile
when (not exists) (touch todoFile)
command

... and I'm done! That's the full program:

{-# LANGUAGE OverloadedStrings #-}

import Turtle

todoFile = "TODO.txt"

todoItem = d%": "%s

display :: IO ()
display = sh (do
(n, line) <- nl (input todoFile)
echo (format todoItem n line) )

add :: Text -> IO ()
add txt = runManaged (do
tempfile <- mktempfile "/tmp" "todo"
output tempfile (input todoFile <|> pure txt)
mv tempfile todoFile )

remove :: Int -> IO ()
remove m = runManaged (do
tempfile <- mktempfile "/tmp" "todo"
output tempfile (do
(n, line) <- nl (input todoFile)
guard (m /= n)
return line )
mv tempfile todoFile )

parseDisplay :: Parser (IO ())
parseDisplay = pure display

parseAdd :: Parser (IO ())
parseAdd =
fmap add
(subcommand "add" "Add a TODO item"
(argText "item" "The item to add to the TODO list") )

parseRemove :: Parser (IO ())
parseRemove =
fmap remove
(subcommand "rm" "Remove a TODO item"
(argInt "index" "The numeric index of the TODO item to remove") )

parseCommand :: Parser (IO ())
parseCommand = parseDisplay <|> parseAdd <|> parseRemove

main = do
command <- options "A TODO list manager" parseCommand
exists <- testfile todoFile
when (not exists) (touch todoFile)
command

We can compile that program into an native binary on any platform (i.e. Windows, OS X, or Linux) with a fast startup time:

$ stack build turtle --resolver=lts-3.14
$ stack ghc --resolver=lts-3.14 -- -O2 todo.hs

... and verify that the program works:

$ ./todo add "Brush my teeth"
$ ./todo add "Shampoo my hamster"
$ ./todo
0: Brush my teeth
1: Shampoo my hamster
$ ./todo rm 0
$ ./todo
0: Shampoo my hamster

The program also auto-generates the usage and help information:

$ ./todo --help
A TODO list manager

Usage: todo ([add] | [rm])

Available options:
-h,--help Show this help text

Available commands:
add
rm
$ ./todo add
Usage: todo add ITEM
$ ./todo rm
Usage: todo rm INDEX

Amazingly, you can delete all the type signatures from the above program and the program will still compile. Try it! Haskell's type inference and fast type-checking algorithm makes it feel very much like a scripting language. The combination of type inference, fast startup time, and polished command line parsing makes Haskell an excellent choice for writing command-line utilities.

You can learn more about scripting in Haskell by reading the turtle tutorial, written for people who have no prior background in Haskell programming:

Contribution #3: Client bindings to a web API

Haskell's servant library lets you write very clean and satisfying bindings to a web API. For example, suppose that I want to define a Haskell client to to the JSONPlaceholder test API. We'll use two example endpoints that the API provides.

A GET request against the /posts endpoint returns a list of fake posts:

[
{
"userId": 1,
"id": 1,
"title": "sunt aut facere repellat ..."
"body": "quia et suscipit\nsuscipit ..."
},
{
"userId": 1,
"id": 2,
"title": "qui est esse",
"body": "est rerum tempore vitae\nsequi ..."
},
...

... and a POST request against the same endpoint accepts a list of posts and returns them back as the response.

To write a client binding to this API, we just need to define a record representing APost:

data APost = APost
{ userId :: Int
, id :: Int
, title :: Text
, body :: Text
} deriving (Show, Generic, FromJSON, ToJSON)

The last line instructs the Haskell compiler to auto-derive conversion functions between APost and JSON.

Now we just encode the REST API as a type:

-- We can `GET` a list of posts from the `/posts` endpoint
type GetPosts = "posts" :> Get '[JSON] [APost]

-- We can `POST` a list of posts to the `/posts` endpoint
-- using the request body and get a list of posts back as
-- the response
type PutPosts = ReqBody '[JSON] [APost] :> "posts" :> Post '[JSON] [APost]

type API = GetPosts :<|> PutPosts

... and then the compiler will "automagically" generate API bindings:

getPosts :<|> putPosts =
client (Proxy :: Proxy API) (BaseUrl Http "jsonplaceholder.typicode.com" 80)

Now anybody can use our code to GET or POST lists of posts. We can also quickly test out our code within the Haskell REPL to verify that everything works:

$ stack ghci servant-server servant-client --resolver=lts-3.14
ghci> :load client.hs
[1 of 1] Compiling Main ( httpbin.hs, interpreted )
Ok, modules loaded: Main.
*Main> import Control.Monad.Trans.Either as Either
*Main Either> -- Perform a `GET` request against the `/posts` endpoint
*Main Either> runEitherT getPosts
Right [APost {userId = 1, id = 1, title = "sunt aut facere ...
*Main Either> -- Perform a `POST` request against the `/posts` endpoint
*Main Either> runEitherT (putPosts [APost 1 1 "foo" "bar"])
Right [APost {userId = 1, id = 1, title = "foo", body = "bar"}]

Here's the full code with all the extensions and imports that enable this magic:

{-# LANGUAGE DataKinds         #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE TypeOperators #-}

import Data.Aeson (FromJSON, ToJSON)
import Data.Text (Text)
import GHC.Generics (Generic)
import Servant
import Servant.Client

data APost = APost
{ userId :: Int
, id :: Int
, title :: Text
, body :: Text
} deriving (Show, Generic, FromJSON, ToJSON)

type GetPosts = "posts" :> Get '[JSON] [APost]
type PutPosts = ReqBody '[JSON] [APost] :> "posts" :> Post '[JSON] [APost]
type API = GetPosts :<|> PutPosts

getPosts :<|> putPosts =
client (Proxy :: Proxy API) (BaseUrl Http "jsonplaceholder.typicode.com" 80)

To learn more about how this works, check out the servant tutorial here:

Note that servant is both a client and server library so everything you learn about auto-generating client side bindings can be reused to auto-generate a server, too!

To see a more long-form example of bindings to the Google Translate API, check out this code:

Conclusion

Suppose that you write up some useful code and you wonder: "What's next? How do I make this code available to others?". You can learn more by reading the stack user guide which contains complete step-by-step instructions for authoring a new Haskell project, including beginning from a pre-existing project template:

by Gabriel Gonzalez (noreply@blogger.com) at January 17, 2016 05:40 PM

Magnus Therning

Free play, part three

The code in the previous post can do with a bit of cleaning up. I start with introducing a type class for an API that can be run

class RunnableF f where
  runOp :: f a -> IO a

and a function that actually runs iteFile

runF :: (RunnableF o) => Free o a -> IO a
runF = foldFree runOp

A coproduct (Sum) of two runnable APIs can itself be runnable

instance (RunnableF f, RunnableF g) => RunnableF (Sum f g) where
  runOp (InL op) = runOp op
  runOp (InR op) = runOp op

After this all I have to do is to move the guts of runSimpleF and runLogging into implementations for SimpleFil and LogF respectively

instance RunnableF SimpleFileF where
  runOp (LoadFile fp f') = liftM f' $ readFile fp
  runOp (SaveFile fp d r) = writeFile fp d >> return r

instance RunnableF LogF where
  runOp (Log s a)= putStrLn s >> return a

The rest is left as is. Running now looks like this

> :! cat test.txt
Lorem ipsum dolor sit amet, consectetur adipiscing elit. Donec a diam lectus.
Sed sit amet ipsum mauris. Maecenas congue ligula ac quam viverra nec
consectetur ante hendrerit.
> runF $ withSimpleFile (map toUpper) "test.txt"
> :! cat test.txt_new
LOREM IPSUM DOLOR SIT AMET, CONSECTETUR ADIPISCING ELIT. DONEC A DIAM LECTUS.
SED SIT AMET IPSUM MAURIS. MAECENAS CONGUE LIGULA AC QUAM VIVERRA NEC
CONSECTETUR ANTE HENDRERIT.
> runF $ foldFree loggingSimpleFileI $ withSimpleFile (map toLower) "test.txt"
** load file test.txt
** save file test.txt_new
> :! cat test.txt_new
lorem ipsum dolor sit amet, consectetur adipiscing elit. donec a diam lectus.
sed sit amet ipsum mauris. maecenas congue ligula ac quam viverra nec
consectetur ante hendrerit.

What else?

With these changes it becomes slightly esier to create new basic API types. but there are still a few things I think could be useful:

  • More generic decorators. logSimpleFileI is tied to decorating only SimpleFileF. I’m fairly sure this could be dealt with by a type class LoggableF and have APIs implement it. I also think there’s a rather natural implementation of LoggableF for Sum f g.
  • Combining decorators (and other interpreters). I’m guessing this is what John refers to as “generalizing interpreters.”
  • Combining APIs. I’d prefer making small APIs of related operations, but then that also means I need a nice way of combining APIs. I had a go at using FreeT but simply gave up on bending the types to my will. In any case I’m not completely sure that a stack of various FreeT is a good direction to go.

January 17, 2016 12:00 AM

January 15, 2016

Well-Typed.Com

Efficient Amortised and Real-Time Queues in Haskell

A queue is a datastructure that provides efficient—O(1)—operations to remove an element from the front of the queue and to insert an element at the rear of the queue. In this blog post we will discuss how we can take advantage of laziness to implement such queues in Haskell, both with amortised and with worst-case O(1) bounds.

The results in this blog post are not new, and can be found in Chris Okasaki’s book “Purely Functional Data Structures”. However, the implementation and presentation here is different from Okasaki’s. In particular, the technique we use for real-time datastructures is more explicit and should scale to datastructures other than queues more easily than Okasaki’s.

Non-solution: Lists

To set the stage, consider this first attempt at implementing queues:

class Queue q where
  empty :: q a
  head  :: q a -> a
  tail  :: q a -> q a
  snoc  :: q a -> a -> q a

data Queue0 a = Q0 [a]

instance Queue Queue0 where
  empty              = Q0 []
  head (Q0 (x:_ ))   = x
  tail (Q0 (_:xs))   = Q0 xs
  snoc (Q0 xs    ) x = Q0 (xs ++ [x])

What is the complexity of head and snoc in this representation? Your first instinct might be to say that head has O(1) complexity (after all, it doesn’t do anything but a pattern match) and that snoc has O(n) complexity, because it needs to traverse the entire list before it can append the element.

However, Haskell is a lazy language. All that happens when we call snoc is that we create a thunk (a suspended computation), which happens in O(1) time. Consider adding the elements [1..5] into an empty queue, one at a time:

Q0      []
Q0     ([] ++ [1])
Q0    (([] ++ [1]) ++ [2])
Q0   ((([] ++ [1]) ++ [2]) ++ [3])
Q0  (((([] ++ [1]) ++ [2]) ++ [3]) ++ [4])
Q0 ((((([] ++ [1]) ++ [2]) ++ [3]) ++ [4]) ++ [5])

Now when we call head on the resulting queue, (++) needs to traverse this entire chain before it can find the first element; since that chain has O(n) length, the complexity of head is O(n).

Strict, Non-Persistent Queues

Thinking about complexity in a lazy setting can be confusing, so let’s first think about a spine strict queue. In order to define it, we will need a spine-strict list:

data StrictList a = SNil | SCons a !(StrictList a)

A bang annotation here means each evaluating an SCons node to weak-head normal form (for instance by pattern matching on it) will also force its tail to weak head normal form, and hence the entire spine of the list; we cannot have an SCons node with a pointer to an unevaluated tail.

We will also need a few operations on strict lists:

-- | Append two strict lists
app :: StrictList a -> StrictList a -> StrictList a
app SNil ys         = ys
app (SCons x xs) ys = SCons x (app xs ys)

-- | Reverse a strict list
rev :: StrictList a -> StrictList a
rev = go SNil
  where
    go :: StrictList a -> StrictList a -> StrictList a
    go acc SNil         = acc
    go acc (SCons x xs) = go (SCons x acc) xs

The definition of strict lists in hand, we can attempt our next queue implementation:

data Queue1 a = Q1 !Int !(StrictList a) !Int !(StrictList a)

Instead of using a single list, we split the queue into two parts: the front of the queue and the rear of the queue. The front of the queue will be stored in normal order, so that we can easily remove elements from the front of the queue; the rear of the queue will be stored in reverse order, so that we can also easily insert new elements at the end of the queue.

In addition, we also record the size of both lists. We will use this to enforce the following invariant:

Queue Invariant: The front of the queue cannot be shorter than the rear.

(Simpler invariants are also possible, but this invariant is the one we will need later so we will use it throughout this blogpost.)

When the invariant is violated, we restore it by moving the elements from the rear of the queue to the front; since the rear of the queue is stored in reverse order, but the front is not, the rear must be reversed:

inv1 :: Queue1 a -> Queue1 a
inv1 q@(Q1 f xs r ys)
  | f < r     = Q1 (f+r) (xs `app` rev ys) 0 SNil
  | otherwise = q

The invariant can be violated when we shrink the front or grow the rear, so we end up with this implementation of the Queue interface:

instance Queue Queue1 where
  empty                           = Q1 0 SNil 0 SNil
  head (Q1 _ (SCons x _ ) _ _ )   = x
  tail (Q1 f (SCons _ xs) r ys)   = inv1 $ Q1 (f-1) xs r ys
  snoc (Q1 f xs           r ys) y = inv1 $ Q1 f xs (r+1) (SCons y ys)

Worst-Case versus Amortised Complexity

Since we don’t have to think about laziness, the complexity of this queue implementation is a bit easier to determine. Clearly, head is O(1), and both tail and snoc have worst case O(n) complexity because rev has O(n) complexity. However, consider what happens when we insert [1..7] into an empty queue:

Q1 0 []     0 []
Q1 1 [1]    0 []       -- invariant restored
Q1 1 [1]    1 [2]
Q1 3 [1..3] 0 []       -- invariant restored
Q1 3 [1..3] 1 [4]
Q1 3 [1..3] 2 [5,4]
Q1 3 [1..3] 3 [6,5,4]
Q1 7 [1..7] 0 []       -- invariant restored

Notice what happens: we only need to reverse n elements after having inserted n elements; we therefore say that the amortised complexity (the complexity averaged over all operations) of the reverse is in fact O(1)—with one proviso, as we shall see in the next section.

Amortisation versus Persistence

The analysis in the previous section conveniently overlooked one fact: since values are immutable in Haskell, nothing is stopping us from reusing a queue multiple times. For instance, if we started from

Q1 3 [1..3] 3 [6,5,4]

we might attempt to insert 7, then 8, then 9, and finally 10 into this (same) queue:

Q1 7 [1,2,3,4,5,6,7]  0 []  -- invariant restored
Q1 7 [1,2,3,4,5,6,8]  0 []  -- invariant restored
Q1 7 [1,2,3,4,5,6,9]  0 []  -- invariant restored
Q1 7 [1,2,3,4,5,6,10] 0 []  -- invariant restored

Notice that each of these single insertions incurs the full cost of a reverse. Thus, claiming an amortised O(1) complexity is only valid if we use the queue linearly (i.e., never reusing queues). If we want to lift this restriction, we need to take advantage of laziness.

Amortised Complexity for Persistent Queues

In order to get amortised constant time bounds even when the queue is not used linearly, we need to take advantage of lazy evaluation. We will change the front of the queue back to be a lazy list:

data Queue2 a = Q2 !Int [a] !Int !(StrictList a)

The remainder of the implementation is the same as it was for Queue1, except that reverse now needs to take a strict list as input and return a lazy list as result:

rev' :: StrictList a -> [a]
rev' = go []
  where
    go :: [a] -> StrictList a -> [a]
    go acc SNil         = acc
    go acc (SCons x xs) = go (x:acc) xs

All the other changes are just changing the operations on strict lists to operations on lazy lists:

inv2 :: Queue2 a -> Queue2 a
inv2 q@(Q2 f xs r ys)
  | f < r     = Q2 (f+r) (xs ++ rev' ys) 0 SNil
  | otherwise = q

instance Queue Queue2 where
  empty                     = Q2 0 [] 0 SNil
  head (Q2 _ (x:_ ) _ _ )   = x
  tail (Q2 f (_:xs) r ys)   = inv2 $ Q2 (f-1) xs r ys
  snoc (Q2 f xs     r ys) y = inv2 $ Q2 f xs (r+1) (SCons y ys)

The genius of this representation lies in two facts. First, notice that when we construct the thunk (xs ++ rev' ys), we know that the rev' ys will not be forced until we have exhausted xs. Since we construct this thunk only when the rear is one longer than the front, we are indeed justified in saying that the cost of the reverse is amortised O(1).

But what about reusing the same queue twice? This is where we rely crucially on laziness. Suppose we have a sequence of operations

Q2 4 [1,2,3,4] 4 [8,7,6,5]               -- initial queue
Q2 9 ([1..4] ++ rev' [9,8,7,6,5]) 0 []   -- snoc (invariant restored)
Q2 5 (rev' [9,8,7,6,5]) 0 []             -- tail 4 times

While it is true that we might call tail on this resulting queue any number of times, they will not each incur the full cost of rev': since these thunks will all be shared, laziness will make sure that once this rev' has been evaluated (“forced”) once, it will not be forced again.

Of course, if we started from that initial queue and inserted various elements, then each of those would create a separate (not shared) thunk with a call to rev': but those calls to rev' will only be forced if for each of those separate queues we first do f calls to tail (in this case, 4 calls).

From Amortised to Worst-Case Bounds

The queues from the previous section will suffice for lots of applications. However, in some applications amortised complexity bounds are not good enough. For instance, in real time systems having normally-cheap operations occassionally take a long time is not acceptable; each operation should take approximately the same amount of time, even if that means that the overall efficiency of the system is slightly lower.

There are two sources of delays in the implementation from the previous section. The first is that when we come across the call to reverse, that whole reverse needs to happen in one go. The second source comes from the fact that we might still chain calls to append; consider what happens when we insert the elements [1..7]:

Q2 0 [] 0 []
Q2 1 r1 0 []  -- invariant restored, r1 = [] ++ rev' [1]
Q2 1 r1 1 [2]
Q2 3 r2 0 []  -- invariant restored, r2 = r1 ++ rev' [3,2]
Q2 3 r2 1 [4]
Q2 3 r2 2 [5,4]
Q2 3 r2 3 [6,5,4]
Q2 7 r3 0 []  -- invariant restored, r3 = r2 ++ rev' [7,6,5,4]

This is similar to the behaviour we saw for the queues based on a single list, except we now have a maximum of O(log n) calls rather than O(n), because the distance between two calls to reverse doubles each time.

Intuitively, we can solve both of these problems by doing a little bit of the append and a little bit of the reverse each time we call tail or snoc. We need to reestablish the invariant when r = f + 1. At this point the append will take f steps, and the reverse r steps, and we will not need to reestablish the invariant again until we have added r + f + 2 elements to the rear of the queue (or added some to the rear and removed some from the front). This therefore gives us plenty of time to do the append and the reverse, if we take one step on each call to tail and snoc.

Progress

How might we “do one step of a reverse”? This is where we diverge from Okasaki, and give a more direct implementation of this idea. We can implement a datatype that describes the “progress” of an operation:

data Progress = Done | NotYet Progress

The idea is that we can execute one step of an operation by pattern matching on an appropriate value of type Progress:

step :: Progress -> Progress
step Done       = Done
step (NotYet p) = p

For (++) it is easy to construct a Progress value which will execute the append; all we need to do is force (part of) the spine of the resulting list:

forceSpine :: Int -> [a] -> Progress
forceSpine 0 _      = Done
forceSpine _ []     = Done
forceSpine n (_:xs) = NotYet (forceSpine (n-1) xs)

For other operations this is more difficult. We need some way to express a computation split into multiple steps. We can use the following datatype for this purpose:

data Delay a = Now a | Later (Delay a)

Delay a is a computation of an a, but we mark the various steps of the computation using the Later constructor (this datatype is variously known as the delay monad or the partiality monad, but we will not need the fact that it is a monad in this blog post). For example, here is reverse:

revDelay :: StrictList a -> Delay [a]
revDelay = go []
  where
    go :: [a] -> StrictList a -> Delay [a]
    go acc SNil         = Now acc
    go acc (SCons x xs) = Later $ go (x:acc) xs

We then need to be able to execute one step of such a computation. For this purpose we can introduce

runDelay :: Delay a -> (a, Progress)

which returns the final value, as well as a Progress value which allows us to execute the computation step by step. The definition of runDelay is somewhat difficult (see appendix, below), but the idea hopefully is clear: evaluating the resulting Progress n steps will execute precisely n steps of the computation; if you look at the resulting a value before having stepped the entire Progress the remainder of the computation will run at that point.

Finally, we can execute two operations in lockstep by pattern matching on two Progress values at the same time:

par :: Progress -> Progress -> Progress
par !p         Done        = p
par Done       !p'         = p'
par (NotYet p) (NotYet p') = NotYet (par p p')

Real-Time Queues

We can use the Progress datatype to implement real-time queues: queues where both insertion and deletion has O(1) worst case complexity. The representation is much like we used in the previous section, but we add a Progress field (Progress is an example implementation of what Okasaki calls a “schedule”):

data Queue3 a = Q3 !Int [a] !Int !(StrictList a) !Progress

Re-establishing the invariant happens much as before, except that we record the resulting Progress on the queue:

inv3 :: Queue3 a -> Queue3 a
inv3 q@(Q3 f xs r ys _)
  | f < r     = let (ys', p1) = runDelay $ revDelay ys
                    xs'       = xs ++ ys'
                    p2        = forceSpine f xs'
                in Q3 (f+r) xs' 0 SNil (par p1 p2)
  | otherwise = q

All that is left to do now is make sure we take a step of the background reverse and append actions on each call to tail and snoc:

instance Queue Queue3 where
  empty = Q3 0 [] 0 SNil Done
  head (Q3 _ (x:_ ) _ _  _)   = x
  tail (Q3 f (_:xs) r ys p)   = inv3 $ Q3 (f-1) xs r ys (step p)
  snoc (Q3 f xs     r ys p) y = inv3 $ Q3 f xs (r+1) (SCons y ys) (step p)

Conclusions

It is difficult to develop data structures with amortised complexity bounds in strict but pure languages; laziness is essential for making sure that operations don’t unnecessarily get repeated. For applications where amortised bounds are insufficient, we can use an explicit schedule to make sure that operations get executed bit by bit; we can use this to develop a pure and persistent queue with O(1) insertion and deletion.

In his book, Okasaki does not introduce a Progress datatype or any of its related functionality; instead he makes very clever use of standard datatypes to get the same behaviour somehow implicitly. Although this is very elegant, it also requires a lot of ingenuity and does not immediately suggest how to apply the same techniques to other datatypes. The Progress datatype we use here is perhaps somewhat cruder, but it might make it easier to implement other real-time data structures.

Random access to (any of the variations on) the queue we implemented is still O(n); if you want a datastructure that provides O(1) insertion and deletion as well as O(log n) random access you could have a look at Data.Sequence; be aware however that this datatype provides amortised, not real-time bounds. Modifying Sequence to provide worst-case complexity bounds is left an exercise for the reader ;-)

Appendix: Implementation of runDelay

The definition of runDelay is tricky. The most elegant way we have found is to use the lazy ST monad:

runDelay :: Delay a -> (a, Progress)
runDelay = \xs -> runST $ do  
    r <- newSTRef xs
    x <- unsafeInterleaveST $ readSTRef r
    p <- next r
    return (runNow x, p)
  where
    next :: STRef s (Delay a) -> ST s Progress
    next r = do
      xs <- readSTRef r
      case xs of
        Now _   -> return Done
        Later d -> do writeSTRef r d
                      p' <- next r
                      return $ NotYet p'

    runNow :: Delay a -> a
    runNow (Now   a) = a
    runNow (Later d) = runNow d

In the lazy ST monad effects are only executed when their results are demanded, but are always executed in the same order. We take advantage of this to make sure that the calls to next only happen when pattern matching on the resulting Progress value. However, it is crucial that for the value of x we read the contents of the STRef only when the value of x is demanded, so that we can take advantage of any writes that next will have done in the meantime.

This does leave us with a proof obligation that this code is safe; in particular, that the value of x that we return does not depend on when we execute this readSTRef; in other words, that invoking next any number of times does not change this value. However, hopefully this is relatively easy to see. Indeed, it follows from parametricity: since runDelay is polymorphic in a, the only a it can return is the one that gets passed in.

To see that pattern matching on the resulting Progress has the intended effect, note that the ST ref starts with “cost n”, where n is the number of Later constructors, and note further that each call to next reduces n by one. Hence, by the time we reach Done, the computation has indeed been executed (reached the Now constructor).

Note that for the case of the queue implementation, by the time we demand the value of the reversed list, we are sure that we will have fully evaluated it, so the definition

runNow (Later d) = runNow d

could actually be replaced by

runNow (Later _) = error "something went horribly wrong!"

Indeed, this can be used to debug designing these real time data structures to ensure that things are indeed fully evaluated by the time you expect them to. In general however it makes the runDelay combinator somewhat less general, and strictly speaking it also breaks referential transparency because now the value of x does depend on how much of the Progress value you evaluate.

For more information about the (lazy) ST monad, see Lazy Functional State Threads, the original paper introducing it. Section 7.2, “Interleaved and parallel operations” discusses unsafeInterleaveST.

by edsko at January 15, 2016 10:58 AM

Chris Smith

Help 25 to 30 girls learn computer programming in Mountain View, CA!

If you live around Mountain View, CA, and love kids, programming, and/or Haskell, read on!

Empoder is a non-profit organization established to teach computer science to underprivileged kids.  They are looking for volunteers to help with a coding club called Empower Girls Through Code, at Graham Middle School in Mountain View, CA.  This will be 25 to 30 girls, of middle school ages.  The club is led by a teacher at Graham, and we have some teaching assistants already there to help.  Empoder would like a couple more volunteers, to make sure there are enough people to give one-on-one help when it’s needed.

  • Who: A teacher, some fellow TAs, you, and 25 to 30 middle school girls excited about learning to code.
  • Where: Graham Middle School, Mountain View, CA
  • When: Wednesdays, 7:50 to 9:20 am, starting January 27
  • Why: Because it’s amazing… easily the most fun thing I have ever done.

The class will use CodeWorld, a web-based programming environment using a dialect of Haskell.  But you don’t need to know that to volunteer.  We can all learn together.

Hope to see you there!  If interested, email marissa.yanez@empoder.org.


by cdsmith at January 15, 2016 03:35 AM

Comonad Reader

Adjoint Triples

A common occurrence in category theory is the adjoint triple. This is a pair of adjunctions relating three functors:

F ⊣ G ⊣ H
F ⊣ G, G ⊣ H

Perhaps part of the reason they are so common is that (co)limits form one:

colim ⊣ Δ ⊣ lim

where Δ : C -> C^J is the diagonal functor, which takes objects in C to the constant functor returning that object. A version of this shows up in Haskell (with some extensions) and dependent type theories, as:

∃ ⊣ Const ⊣ ∀
Σ ⊣ Const ⊣ Π

where, if we only care about quantifying over a single variable, existential and sigma types can be seen as a left adjoint to a diagonal functor that maps types into constant type families (either over * for the first triple in Haskell, or some other type for the second in a dependently typed language), while universal and pi types can be seen as a right adjoint to the same.

It's not uncommon to see the above information in type theory discussion forums. But, there are a few cute properties and examples of adjoint triples that I haven't really seen come up in such contexts.

To begin, we can compose the two adjunctions involved, since the common functor ensures things match up. By calculating on the hom definition, we can see:

Hom(FGA, B)     Hom(GFA, B)
    ~=              ~=
Hom(GA, GB)     Hom(FA, HB)
    ~=              ~=
Hom(A, HGB)     Hom(A, GHB)

So there are two ways to compose the adjunctions, giving two induced adjunctions:

FG ⊣ HG,  GF ⊣ GH

And there is something special about these adjunctions. Note that FG is the comonad for the F ⊣ G adjunction, while HG is the monad for the G ⊣ H adjunction. Similarly, GF is the F ⊣ G monad, and GH is the G ⊣ H comonad. So each adjoint triple gives rise to two adjunctions between monads and comonads.

The second of these has another interesting property. We often want to consider the algebras of a monad, and coalgebras of a comonad. The (co)algebra operations with carrier A have type:

alg   : GFA -> A
coalg : A -> GHA

but these types are isomorphic according to the GF ⊣ GH adjunction. Thus, one might guess that GF monad algebras are also GH comonad coalgebras, and that in such a situation, we actually have some structure that can be characterized both ways. In fact this is true for any monad left adjoint to a comonad; [0] but all adjoint triples give rise to these.

The first adjunction actually turns out to be more familiar for the triple examples above, though. (Edit: [2]) If we consider the Σ ⊣ Const ⊣ Π adjunction, where:

Σ Π : (A -> Type) -> Type
Const : Type -> (A -> Type)

we get:

ΣConst : Type -> Type
ΣConst B = A × B
ΠConst : Type -> Type
ΠConst B = A -> B

So this is the familiar adjunction:

A × - ⊣ A -> -

But, there happens to be a triple that is a bit more interesting for both cases. It refers back to categories of functors vs. bare type constructors mentioned in previous posts. So, suppose we have a category called Con whose objects are (partially applied) type constructors (f, g) with kind * -> *, and arrows are polymorphic functions with types like:

 
forall x. f x -> g x
 

And let us further imagine that there is a similar category, called Func, except its objects are the things with Functor instances. Now, there is a functor:

U : Func -> Con

that 'forgets' the functor instance requirement. This functor is in the middle of an adjoint triple:

F ⊣ U ⊣ C
F, C : Con -> Func

where F creates the free functor over a type constructor, and C creates the cofree functor over a type constructor. These can be written using the types:

 
data F f a = forall e. F (e -> a) (f e)
newtype C f a = C (forall r. (a -> r) -> f r)
 

and these types will also serve as the types involved in the composite adjunctions:

FU ⊣ CU : Func -> Func
UF ⊣ UC : Con -> Con

Now, CU is a monad on functors, and the Yoneda lemma tells us that it is actually the identity monad. Similarly, FU is a comonad, and the co-Yoneda lemma tells us that it is the identity comonad (which makes sense, because identity is self-adjoint; and the above is why F and C are often named (Co)Yoneda in Haskell examples).

On the other hand, UF is a monad on type constructors (note, U isn't represented in the Haskell types; F and C just play triple duty, and the constraints on f control what's going on):

 
eta :: f a -> F f a
eta = F id
 
transform :: (forall x. f x -> g x) -> F f a -> F g a
transform tr (F g x) = F g (tr x)
 
mu :: F (F f) a -> F f a
mu (F g (F h x)) = F (g . h) x
 

and UC is a comonad:

 
epsilon :: C f a -> f a
epsilon (C e) = e id
 
transform' :: (forall x. f x -> g x) -> C f a -> C g a
transform' tr (C e) = C (tr . e)
 
delta :: C f a -> C (C f) a
delta (C e) = C $ \h -> C $ \g -> e (g . h)
 

These are not the identity (co)monad, but this is the case where we have algebras and coalgebras that are equivalent. So, what are the (co)algebras? If we consider UF (and unpack the definitions somewhat):

 
alg :: forall e. (e -> a, f e) -> f a
alg (id, x) = x
alg (g . h, x) = alg (g, alg (h, x))
 

and for UC:

 
coalg :: f a -> forall r. (a -> r) -> f r
coalg x id = x
coalg x (g . h) = coalg (coalg x h) g
 

in other words, (co)algebra actions of these (co)monads are (mangled) fmap implementations, and the commutativity requirements are exactly what is required to be a law abiding instance. So the (co)algebras are exactly the Functors. [1]

There are, of course, many other examples of adjoint triples. And further, there are even adjoint quadruples, which in turn give rise to adjoint triples of (co)monads. Hopefully this has sparked some folks' interest in finding and studying more interesting examples.

[0]: Another exmaple is A × - ⊣ A -> - where the A in question is a monoid. (Co)monad (co)algebras of these correspond to actions of the monoid on the carrier set.

[1]: This shouldn't be too surprising, because having a category of (co)algebraic structures that is equivalent to the category of (co)algebras of the (co)monad that comes from the (co)free-forgetful adjunction is the basis for doing algebra in category theory (with (co)monads, at least). However, it is somewhat unusual for a forgetful functor to have both a left and right adjoint. In many cases, something is either algebraic or coalgebraic, and not both.

[2]: Urs Schreiber informed me of an interesting interpretation of the ConstΣ ⊣ ConstΠ adjunction. If you are familiar with modal logic and the possible worlds semantics thereof, you can probably imagine that we could model it using something like P : W -> Type, where W is the type of possible worlds, and propositions are types. Then values of type Σ P demonstrate that P holds in particular worlds, while values of type Π P demonstrate that it holds in all worlds. Const turns these types back into world-indexed 'propositions,' so ConstΣ is the possibility modality and ConstΠ is the necessity modality.

by Dan Doel at January 15, 2016 01:16 AM

Dominic Steinitz

Inferring Parameters for ODEs using Stan

Introduction

The equation of motion for a pendulum of unit length subject to Gaussian white noise is

\displaystyle  \frac{\mathrm{d}^2\alpha}{\mathrm{d}t^2} = -g\sin\alpha + w(t)

We can discretize this via the usual Euler method

\displaystyle  \begin{bmatrix} x_{1,i} \\ x_{2,i} \end{bmatrix} = \begin{bmatrix} x_{1,i-1} + x_{2,i-1}\Delta t \\ x_{2,i-1} - g\sin x_{1,i-1}\Delta t \end{bmatrix} + \mathbf{q}_{i-1}

where q_i \sim {\mathcal{N}}(0,Q) and

\displaystyle  Q = \begin{bmatrix} \frac{q^c \Delta t^3}{3} & \frac{q^c \Delta t^2}{2} \\ \frac{q^c \Delta t^2}{2} & {q^c \Delta t} \end{bmatrix}

The explanation of the precise form of the covariance matrix will be the subject of another blog post; for the purpose of exposition of using Stan and, in particular, Stan’s ability to handle ODEs, this detail is not important.

Instead of assuming that we know g let us take it to be unknown and that we wish to infer its value using the pendulum as our experimental apparatus.

Stan is a probabilistic programming language which should be welll suited to perform such an inference. We use its interface via the R package rstan.

A Stan and R Implementation

Let’s generate some samples using Stan but rather than generating exactly the model we have given above, instead let’s solve the differential equation and then add some noise. Of course this won’t quite give us samples from the model the parameters of which we wish to estimate but it will allow us to use Stan’s ODE solving capability.

Here’s the Stan

functions {
  real[] pendulum(real t,
                  real[] y,
                  real[] theta,
                  real[] x_r,
                  int[] x_i) {
    real dydt[2];
    dydt[1] <- y[2];
    dydt[2] <- - theta[1] * sin(y[1]);
    return dydt;
  }
}
data {
  int<lower=1> T;
  real y0[2];
  real t0;
  real ts[T];
  real theta[1];
  real sigma[2];
}
transformed data {
  real x_r[0];
  int x_i[0];
}
model {
}
generated quantities {
  real y_hat[T,2];
  y_hat <- integrate_ode(pendulum, y0, t0, ts, theta, x_r, x_i);
  for (t in 1:T) {
    y_hat[t,1] <- y_hat[t,1] + normal_rng(0,sigma[1]);
    y_hat[t,2] <- y_hat[t,2] + normal_rng(0,sigma[2]);
  }
}

And here’s the R to invoke it

library(rstan)
library(mvtnorm)

qc1 = 0.0001
deltaT = 0.01
nSamples = 100
m0 = c(1.6, 0)
g = 9.81
t0 = 0.0
ts = seq(deltaT,nSamples * deltaT,deltaT)

bigQ = matrix(c(qc1 * deltaT^3 / 3, qc1 * deltaT^2 / 2,
                qc1 * deltaT^2 / 2,       qc1 * deltaT
                ),
              nrow = 2,
              ncol = 2,
              byrow = TRUE
              )

samples <- stan(file = 'Pendulum.stan',
                data = list (
                    T  = nSamples,
                    y0 = m0,
                    t0 = t0,
                    ts = ts,
                    theta = array(g, dim = 1),
                    sigma = c(bigQ[1,1], bigQ[2,2]),
                    refresh = -1
                ),
                algorithm="Fixed_param",
                seed = 42,
                chains = 1,
                iter =1
                )

We can plot the angle the pendulum subtends to the vertical over time. Note that this is not very noisy.

s <- extract(samples,permuted=FALSE)
plot(s[1,1,1:100])

Now let us suppose that we don’t know the value of g and we can only observe the horizontal displacement.

zStan <- sin(s[1,1,1:nSamples])

Now we can use Stan to infer the value of g.

functions {
  real[] pendulum(real t,
                  real[] y,
                  real[] theta,
                  real[] x_r,
                  int[] x_i) {
    real dydt[2];
    dydt[1] <- y[2];
    dydt[2] <- - theta[1] * sin(y[1]);
    return dydt;
  }
}
data {
  int<lower=1> T;
  real y0[2];
  real z[T];
  real t0;
  real ts[T];
}
transformed data {
  real x_r[0];
  int x_i[0];
}
parameters {
  real theta[1];
  vector<lower=0>[1] sigma;
}
model {
  real y_hat[T,2];
  real z_hat[T];
  theta ~ normal(0,1);
  sigma ~ cauchy(0,2.5);
  y_hat <- integrate_ode(pendulum, y0, t0, ts, theta, x_r, x_i);
  for (t in 1:T) {
    z_hat[t] <- sin(y_hat[t,1]);
    z[t] ~ normal(z_hat[t], sigma);
  }
}

Here’s the R to invoke it.

estimates <- stan(file = 'PendulumInfer.stan',
                  data = list (
                      T  = nSamples,
                      y0 = m0,
                      z  = zStan,
                      t0 = t0,
                      ts = ts
                  ),
                  seed = 42,
                  chains = 1,
                  iter = 1000,
                  warmup = 500,
                  refresh = -1
                  )
e <- extract(estimates,pars=c("theta[1]","sigma[1]","lp__"),permuted=TRUE)

This gives an estiamted valeu for g of 9.809999 which is what we would hope.

Now let’s try adding some noise to our observations.

set.seed(42)
epsilons <- rmvnorm(n=nSamples,mean=c(0.0),sigma=bigR)

zStanNoisy <- sin(s[1,1,1:nSamples] + epsilons[,1])

estimatesNoisy <- stan(file = 'PendulumInfer.stan',
                       data = list (T  = nSamples,
                                    y0 = m0,
                                    z  = zStanNoisy,
                                    t0 = t0,
                                    ts = ts
                                    ),
                       seed = 42,
                       chains = 1,
                       iter = 1000,
                       warmup = 500,
                       refresh = -1
                       )
eNoisy <- extract(estimatesNoisy,pars=c("theta[1]","sigma[1]","lp__"),permuted=TRUE)

This gives an estiamted value for g of 8.5871024 which is ok but not great.

Postamble

To build this page, download the relevant files from github and run this in R:

library(knitr)
knit('Pendulum.Rmd')

And this from command line:

pandoc -s Pendulum.md --filter=./Include > PendulumExpanded.html

by Dominic Steinitz at January 15, 2016 12:02 AM

Magnus Therning

Free play, part two

This post on Free play builds on my previous one. It was John A De Goes’ post that finally got me started on playing with Free and his post contian the following:

Moreover, not only do algebras compose (that is, if you have algebras f and g, you can compose them into a composite algebra Coproduct f g for some suitable definition of Coproduct), but interpreters also compose — both horizontally and vertically.

And a little bit later he offers a few types and some details, but not all details. How could something like that look in Haskell?

Starting from the code in the previous post I first created a new type for a logging action

data LogF a = Log String a

This type has to be a Functor

instance Functor LogF where
  fmap f (Log s a) = Log s (f a)

The logging should basically decorate a SimpleFileF a action, so I need a function to map one into a Free LogF a

logSimpleFileI :: SimpleFileF a -> Free LogF ()
logSimpleFileI (LoadFile fp _) = liftF $ Log ("** load file " ++ fp) ()
logSimpleFileI (SaveFile fp _ _) = liftF $ Log ("** save file " ++ fp) ()

Now I needed a Coproduct for Functor. Searching hackage only offered up one for Monoid (in monoid-extras) so I first translated one from PureScript, but later I got some help via Twitter and was pointed to two in Haskell, Data.Functor.Coproduct from comonad and Data.Functor.Sum from transformers, I decided on the one from transformers because of its shorter name and the fact that it was very different from my translated-from-PureScript version.

Following John’s example I use Applicative to combine the logging with the file action

loggingSimpleFileI :: SimpleFileF a -> Free (Sum LogF SimpleFileF) a
loggingSimpleFileI op = toLeft (logSimpleFileI op) *> toRight (liftF op)

with toLeft and toRight defined like this

toLeft :: (Functor f, Functor g) => Free f a -> Free (Sum f g) a
toLeft = hoistFree InL
toRight :: (Functor f, Functor g) => Free g a -> Free (Sum f g) a
toRight = hoistFree InR

With all of this in place I can decorate the program from the last post like this foldFree loggingSimpleFileI (withSimpleF toUpper "FreePlay.hs"). What’s left is a way to run it. The function for that is a natural extension of runsimpleFile


runLogging :: Free (Sum LogF SimpleFileF) a -> IO a
runLogging = foldFree f
  where
    f :: (Sum LogF SimpleFileF) a -> IO a
    f (InL op) = g op
    f (InR op) = h op

    g :: LogF a -> IO a
    g (Log s a)= putStrLn s >> return a

    h :: SimpleFileF a -> IO a
    h (LoadFile fp f') = liftM f' $ readFile fp
    h (SaveFile fp d r) = writeFile fp d >> return r

Running the decorated program

runLogging $ foldFree loggingSimpleFileI (withSimpleF toUpper "FreePlay.hs")

does indeed result in the expected output

** load file FreePlay.hs
** save file FreePlay.hs_new

and the file FreePlay.hs_new contains only uppercase letters.

My thoughts

This ability to decorate actions (or compose algebras) is very nice. There’s probably value in the “multiple interpreters for a program” in some domains, but I have a feeling that it could be a hard sell. However, combining it with this kind of composability adds quite a bit of value in my opinion. I must say I don’t think my code scales very well for adding more decorators (composing more algebras), but hopefully some type wizard can show me a way to improve on that.

The code above is rather crude though, and I have another version that cleans it up quite a bit. That’ll be in the next post.

January 15, 2016 12:00 AM

January 14, 2016

Neil Mitchell

A simple Haskell function

Summary: An example of a small function I recently wrote - from type signature to tests.

When writing a build system there are lots of nasty corner cases to consider. One is that command line limits combined with lots of arguments sometimes requires splitting a single command up into multiple commands, each of which is under some maximum length. In this post I'll describe a function that was required, my implementation, and how I tested it.

Type signature and documentation

Before I even got to the function, it already had a type signature and some Haddock documentation:

-- | @chunksOfSize size strings@ splits a given list of strings into chunks not
-- exceeding @size@ characters. If that is impossible, it uses singleton chunks.
chunksOfSize :: Int -> [String] -> [[String]]

As an example:

chunksOfSize 5 ["this","is","a","test"] == [["this"],["is","a"],["test"]]

Implementation

My implementation was:

chunksOfSize n = repeatedly $ \xs ->
let i = length $ takeWhile (<= n) $ scanl1 (+) $ map length xs
in splitAt (max 1 i) xs

First we use the repeatedly function from the extra library. This has the signature:

repeatedly :: ([a] -> (b, [a])) -> [a] -> [b]

Given a list of input, you supply a function that splits off an initial piece and returns the rest. One of the examples in the documentation is:

repeatedly (splitAt 3) xs  == chunksOf 3 xs

So we can see how repeatedly lets us focus on just the "next step" of this list, ignoring the recursion. For the function argument we have two tasks - first decide how many items to put in this chunk, then to split the chunks. Splitting the chunks is the easy bit, and can be written:

splitAt (max 1 i) xs

If we know the next i elements will be at or below the limit, then we can use splitAt to divide the elements. As a special case, if no elements would be allowed, we allow one, using max 1 to ensure we never pass 0 to splitAt (and thus enter an infinite loop). That leaves us with:

i = length $ takeWhile (<= n) $ scanl1 (+) $ map length xs

Reading from right to left, we reduce each element to it's length, then use scanl1 to produce a running total - so each element represents the total length up to that point. We then use takeWhile (<= n) to keep grabbing elements while they are short enough, and finally length to convert back to something we can use with splitAt.

Tests

When testing, I tend to start with a few concrete examples then move on to QuickCheck properties. As an initial example we can do:

quickCheck $
chunksOfSize 3 ["a","b","c","defg","hi","jk"] ==
[["a","b","c"],["defg"],["hi"],["jk"]]

Here we are explicitly testing some of the corner cases - we want to make sure the full complement of 3 get into the first chunk (and we haven't got an off-by-one), we also test a singleton chunk of size 4. Now we move on to QuickCheck properties:

quickCheck $ \n xs ->
let res = chunksOfSize n xs
in concat res == xs &&
all (\r -> length r == 1 || length (concat r) <= n) res

There are really two properties here - first, the chunks concat together to form the original. Secondly, each chunk is either under the limit or a singleton. These properties capture the requirements in the documentation.

A final property we can check is that it should never be possible to move the first piece from a chunk to the previous chunk. We can write such a property as:

all (> n) $ zipWith (+)
(map (sum . map length) res)
(drop 1 $ map (length . head) res)

This property isn't as important as the other invariants, and is somewhat tested in the example, so I didn't include it in the test suite.

Performance and alternatives

The complexity is O(n) in the number of Char values, which is as expected, since we have to count them all. Some observations about this point in the design space:

  • In a strict language this would be an O(n^2) implementation, since we would repeatedly length and scanl the remainder of the tail each time. As it is, we are calling length on the first element of each chunk twice, so there is minor constant overhead.
  • Usually in Haskell, instead of counting the number of elements and then doing splitAt we would prefer to use span - something like span ((<= n) . fst) .... While possible, it makes the special singleton case more difficult, and requires lots of tuples/contortions to associate each element with its rolling sum.
  • For a build system, the entire input will be evaluated before, and the entire output will be kept in memory afterwards. However, if we think about this program with lazy streaming inputs and outputs, it will buffer each element of the output list separately. As a result memory would be bounded by the maximum of the longest string and the Int argument to chunksOfSize.
  • It is possible to write a streaming version of this function, which returns each String as soon as it is consumed, with memory bounded by the longest string alone. Moreover, if the solution above was to use lazy naturals, it would actually come quite close to being streaming (albeit gaining a quadratic complexity term from the takeWhile (<= n)).
  • The type signature could be generalised to [a] instead of String, but I would suspect in this context it's more likely for String to be replaced by Text or ByteString, rather than to be used on [Bool]. As a result, sticking to String seems best.

Refactoring the previous version

The function already existed in the codebase I was working on, so below is the original implementation. This implementation does not handle the long singleton special case (it loops forever). We can refactor it to support the singleton case, which we do in several steps. The original version was:

chunksOfSize _    [] = []
chunksOfSize size strings = reverse chunk : chunksOfSize size rest
where
(chunk, rest) = go [] 0 strings
go res _ [] = (res, [])
go res chunkSize (s:ss) =
if newSize > size then (res, s:ss) else go (s:res) newSize ss
where
newSize = chunkSize + length s

Refactoring to use repeatedly we get:

chunksOfSize size = repeatedly $ second reverse . go [] 0
where
go res _ [] = (res, [])
go res chunkSize (s:ss) =
if newSize > size then (res, s:ss) else go (s:res) newSize ss
where
newSize = chunkSize + length s

Changing go to avoid the accumulator we get:

chunksOfSize size = repeatedly $ go 0
where
go _ [] = ([], [])
go chunkSize (s:ss) =
if newSize > size then ([], s:ss) else first (s:) $ go newSize ss
where
newSize = chunkSize + length s

It is then reasonably easy to fix the singleton bug:

chunksOfSize size = repeatedly $ \(x:xs) -> first (x:) $ go (length x) xs
where
go _ [] = ([], [])
go chunkSize (s:ss) =
if newSize > size then ([], s:ss) else first (s:) $ go newSize ss
where
newSize = chunkSize + length s

Finally, it is slightly simpler to keep track of the number of characters still allowed, rather than the number of characters already produced:

chunksOfSize size = repeatedly $ \(x:xs) -> first (x:) $ go (size - length x) xs
where
go n (x:xs) | let n2 = n - length x, n2 >= 0 = first (x:) $ go n2 xs
go n xs = ([], xs)

Now we have an alternative version that is maximally streaming, only applies length to each element once, and would work nicely in a strict language. I find the version at the top of this post more readable, but this version is a reasonable alternative.

Acknowledgements: Thanks to Andrey Mokhov for providing the repo, figuring out all the weird corner cases with ar, and distilling it down into a Haskell problem.

by Neil Mitchell (noreply@blogger.com) at January 14, 2016 11:03 PM

Dan Burton

What to do with aeson-0.10?

aeson-0.10.0.0 has been out since September 2015. Aeson is widely used, and adoption of the new version was fairly slow. The changelog claims, “the API changes below should be upwards compatible from older versions of aeson. If you run into … Continue reading

by Dan Burton at January 14, 2016 10:34 PM

Theory Lunch (Institute of Cybernetics, Tallinn)

Second-order theories should not be taken lightly

First-order formal logic is a standard topic in computer science. Not so for second-order logic: which, though used the default in fields of mathematics such as topology and analysis, is usually not treated in standard courses in mathematical logic. For today’s Theory Lunch I discussed some classical theorems that hold for first-order logic, but not for second-order logic: my talk was based on Boolos’ classical textbook.

We consider languages made of symbols that represents either objects, or functions, or relations: in particular, unary relations, or equivalently, sets. A sentence on such a language is a finite sequence of symbols from the language and from the standard logical connectives and quantifiers (\wedge for conjunction, \vee for disjunction, \sim for negation, etc.) according to the usual rules, such that every variable is bounded by some quantifier. A first-order sentence only has quantifiers on objects, while a second-order sentence can have quantifiers on functions and relations (in particular, sets) as well.

For example, the set \mathbf{Q} is made of the following first-order sentences on the language \{ \mathbf{0}, {}', +, \cdot, < \}:

  1. \forall x . \sim (x' = \mathbf{0})
  2. \forall x y . x' = y' \to x = y
  3. \forall x . x + \mathbf{0} = x
  4. \forall x y . x + y' = (x + y) '
  5. \forall x . x \cdot \mathbf{0} = 0
  6. \forall x y . x \cdot y' = x \cdot y + x
  7. \forall x . \sim (x < \mathbf{0})
  8. \forall x y. x < y' \iff (x < y \vee x = y)
  9. \forall x . \mathbf{0} < x \iff \sim (x = \mathbf{0})
  10. \forall x y . x' < y \iff (x < y \wedge y \neq x')

Of course, second-order logic is much more expressive than first order logic. The natural question is: how much?

The answer is: possibly, too much more than we would like.

To discuss how it is so, we recall the notion of model. Informally, a model of a set of sentences is a “world” where all the sentences in the set are true. For instance, the set \mathbb{N} of natural numbers with the usual zero, successor, addition, multiplication, and ordering is a model of \mathbf{Q}. A model for a set of sentences is also a model for every theorem of that set, i.e., every sentence that can be derived in finitely many steps from those of the given set by applying the standard rules of logic.

For sets of first-order sentences, the following four results are standard:

Compactness theorem. (Tarski and Mal’tsev) Given a set \Gamma of first-order sentences, if every finite subset of \Gamma has a model, then \Gamma has a model.

Upwards Löwenheim-Skolem theorem. If a set of first-order sentences has a model of infinite cardinality \alpha, then it also has models of every cardinality \beta>\alpha.

Downwards Löwenheim-Skolem theorem. If a set of first-order sentences on a finite or countable language has a model, then it also has a finite or countable model.

Completeness theorem. (Gödel) Given a set \Gamma of first-order sentences, if a first-order sentence A is true in every model of \Gamma, then A is a theorem of \Gamma.

All of these facts fail for second-order theories. Let us see how:

We start by considering the following second-order sentence:

\mathbf{Denum} \equiv \exists x \exists f \forall S . ( S(x) \wedge \forall y . (S(y) \to S(f(y))) ) \to \forall y . S(y)

Lemma 1. The sentence \mathbf{Denum} is true in a model \mathcal{M} if and only if the universe of \mathcal{M} is at most countable.

The informal reason is that \mathbf{Denum} intuitively means:

the universe is a monoid on a single generator

Let us now consider the following second-order sentence:

\mathbf{Infin} \equiv \exists x \exists f . (\forall y . x \neq f(y)) \wedge (\forall y z . f(y) = f(z) \to y = z)

Lemma 2. The sentence \mathbf{Infin} is true in a model \mathcal{M} if and only if the universe of \mathcal{M} is infinite.

The informal reason is that \mathbf{Infin} intuitively means:

the universe contains a copy of the natural numbers

Theorem 1. Both Löwenheim-Skolem theorems fail for sets of second-order sentences.

Proof. \mathbf{Infin} \wedge \mathbf{Denum} only has countably infinite models. \mathbf{Infin} \wedge \sim \mathbf{Denum} only has uncountably infinite models. \Box

Let us now consider the set \mathbf{PA2} of all the sentences of \mathbf{Q} together with the following second-order sentence:

\mathbf{Ind} \equiv \forall S . (S(\mathbf{0}) \wedge \forall x. (S(x) \to S(x'))) \to \forall x . S(x)

Clearly, \mathbf{Ind} is the induction principle: which is an axiom in second-order Peano arithmetics, but only an axiom scheme in first-order PA.

Lemma 3. Every model of \mathbf{PA2} is isomorphic to the set of natural numbers with zero, successor, addition, multiplication, and ordering.

The informal reason is that \mathbf{Q}, though finite, is powerful enough to tell numbers from each other: therefore, in every model of \mathbf{PA2}, each numeral \mathbf{n} (nth iteration of the successor, starting from \mathbf{0}) can be denoted by at most one item in the universe of the model. On the other hand, \mathbf{Ind} is powerful enough to reconstruct every numeral.

Theorem 2. The compactness theorem fails for sets of second-order sentences.

Proof. Let c be a constant outside the language of \mathbf{PA2}. Consider the set \Gamma made of all the sentences from \mathbf{PA2} and all the sentences of the form X_n \equiv c \neq \mathbf{n}. Then every finite subset \Gamma_0 of \Gamma has a model, which can be obtained from the set of natural numbers by interpreting c as some number M strictly greater than all of the values n such that X_n \in \Gamma_0. However, a model of \Gamma is also a model of \mathbf{PA2}, and must be isomorphic to the set of natural numbers: but no interpretation of the constant c is possible within such model. \Box

We can now prove

Theorem 3. The completeness theorem does not hold for second-order sentences.

In other words, second-order logic is semantically inadequate: it is not true anymore that all “inequivocably true” sentences are theorems. The proof will be based on the following two facts:

Fact 1. (Gödel) The set of the first-order formulas which are true in every model of \mathbf{Q} is recursively enumerable.

Fact 2. (Tarski) The set of first-order formulas which are true in \mathbb{N} is not recursively enumerable.

Fact 1 is actually a consequence of the completeness theorem: the set of first-order formulas which are true in every model of \mathbf{Q} is the same as the set of first-order sentences that are provable from \mathbf{Q}, and that set is recursively enumerable by producing every possible proof! To prove Theorem 3 it will thus be sufficient to prove that Fact 1 does not hold for second-order sentences.

Proof of Theorem 3. We identify \mathbf{PA2} with the conjunction of all its formulas, which are finitely many.

Let A be a first-order sentence in the language of \mathbf{Q}. Because of what we saw while discussing the compactness theorem, A is true in \mathbb{N} if and only if it is true in every model of \mathbf{PA2}: this, in turn, is the same as saying that \mathbf{PA2} \to A is true in every model of \mathbf{Q}. Indeed, let \mathcal{M} be a model of \mathbf{Q}: if \mathcal{M} is isomorphic to \mathbb{N}, then \mathbf{PA2} \to A is true in \mathcal{M} if and only if A is true in \mathcal{M}; if \mathcal{M} is not isomorphic to \mathbb{N}, then \mathbf{PA2} is false in \mathcal{M}, which makes \mathbf{PA2} \to A true in \mathcal{M}. This holds whatever A is.

Fix a Gödel numbering for sentences. There exists a recursive function that, for every sentence A, transforms the Gödel number of the first-order sentence A into the Gödel number of the second-order sentence \mathbf{PA2} \to A.

Suppose now, for the sake of contradiction, that the set of second-order sentences that are true in every model of \mathbf{Q} is recursively enumerable. Then we could get a recursive enumeration of the set of first-order sentences which are true in the standard model of \mathbf{Q} by taking the Gödel number of such a sentence A, turning it into that of \mathbf{PA2} \to A via the aforementioned recursive function, and feeding the latter number to the semialgorithm for second-order sentences that are true in every model of \mathbf{Q}. But because of Tarski’s result, no such recursive enumeration exists. \Box

Bibliography:

  1. George S. Boolos et al. Computability and Logic. Fifth Edition. Cambridge University Press, 2007

by Silvio Capobianco at January 14, 2016 12:14 PM

Functional Jobs

Haskell Engineer at Elevence Digital Finance (Full-time)

Elevence reinvents how software helps financial firms do business.

We build our solution on formal methods and functional programming. We care about open-source, distributed systems and cryptography. We are growing our core software engineering team in Zurich.

You are a developer with expert functional programming skills in one of the following domains:

  • Compiler development
  • Formal methods and theorem provers
  • Cryptography
  • Distributed systems
  • Algorithmic trading

You have 2+ years experience in functional programming (preferrably Haskell), and care about delivering high-quality code within an agile team.

Get information on how to apply for this position.

January 14, 2016 09:49 AM

January 13, 2016

Magnus Therning

Free play, part one

When I read John A De Goes post A Modern Architecture for FP I found it to be a bit too vague for me, but the topic was just interesting enough to finally push me to play a little with free monads. It’s not the first post I’ve read on the topic, there have been many before. None have quite managed to push me into actually doing something though!

A file API

To make it concrete but still short enough to not bore readers I came up with a small API for working with files:

data SimpleFileF a =
  LoadFile FilePath (String -> a)
  | SaveFile FilePath String a

The free monad wraps a functor, so here’s an implementation of that

instance Functor SimpleFileF where
  fmap f (LoadFile fp f')= LoadFile fp (f . f')
  fmap f (SaveFile fp d a) = SaveFile fp d (f a)

Now for some convenient functions to work with the API type

loadFile :: FilePath -> Free SimpleFileF String
loadFile fp = liftF $ LoadFile fp id

saveFile :: FilePath -> String -> Free SimpleFileF ()
saveFile fp d = liftF $ SaveFile fp d ()

With this in place I can write a somewhat more complex one

withSimpleFile :: (String -> String) -> FilePath -> Free SimpleFileF ()
withSimpleFile f fp = do
  d <- loadFile fp
  let result = f d
  saveFile (fp ++ "_new") result

Now I need a way to run programs using the API

runSimpleFile :: Free SimpleFileF a -> IO a
runSimpleFile = foldFree f
  where
    f (LoadFile fp f') = liftM f' $ readFile fp
    f (SaveFile fp d r) = writeFile fp d >> return r

If this code was save in the file FreePlay.hs I can now convert it all to upper case by using

runSimpleFile $ withSimpleFile toUpper "FreePlay.hs"

which of course will create the file FreePlay.hs_new.

What have I bought so far?

Well, not much really.

So far it’s not much more than a rather roundabout way to limit what IO actions are available. In other words it’s not much more than what can be done by creating a limited IO, as in my earlier posts here and here.

Of course it would be possible to write another run function, e.g. one that doesn’t actually perform the file actions but just says what it would do. The nice thing though is, to use that same metaphor as John does, that I can add a layer to the onion. In other words, I can decorate each use of my SimpleFileF API with some other API. I think it was John’s description of this layering that pushed me to play with Free.

January 13, 2016 12:00 AM

January 12, 2016

Well-Typed.Com

Haskell courses in New York City

Well-Typed is happy to announce that once again we will be running Haskell training courses in New York alongside

C◦mp◦se conference

Thursday, February 4 – Sunday, February 7, 2016, New York City

This conference is focused on typed functional programming and features a keynote by Eugenia Cheng and an excellent line-up of talks including one by our own Austin Seipp on Cryptography and verification with Cryptol. There’s also an “unconference” with small workshops and tutorials as well as the opportunity to get your hands dirty and try things out yourself.

For several years now, we have been running successful Haskell courses in collaboration in Skills Matter. The New York courses will be taught by Duncan Coutts, co-founder and partner at Well-Typed. He’s an experienced teacher and is involved in lots of commercial Haskell development projects at Well-Typed.

You can participate in our Haskell courses directly before or directly after C◦mp◦se in February, or if that doesn’t suit we are running two of the courses in London this April:

Fast Track to Haskell

Tuesday, February 2 – Wednesday, February 3, 2016, New York City
(and Monday, April 4 – Tuesday, April 5, 2016, London)

Find out more or register here.

This course is for developers who want to learn about functional programming in general or Haskell in particular. It introduces important concepts such as algebraic datatypes, pattern matching, type inference, polymorphism, higher-order functions, explicit effects and, of course, monads and provides a compact tour with lots of hands-on exercises that provide a solid foundation for further adventures into Haskell or functional programming.

Guide to Haskell Performance and Optimization

Monday, February 8 – Tuesday, February 9, 2016, New York City
(and Wednesday, April 6 – Thursday, April 7, 2016, London)

Find out more or register here.

This brand-new course looks under the surface of Haskell at how things are implemented, including how to reason about performance and optimize your programs, so that you can write beautiful programs that scale. It covers the internal representation of data on the heap, what exactly lazy evaluation means and how it works, how the compiler translates Haskell code to a target language via several internal representations, what you can and cannot reasonably expect the compiler to do, and how you can tweak the optimizer behaviour by using compiler pragmas such as inlining annotations and rewrite rules.

Guide to the Haskell Type System

Wednesday, February 10, 2016, New York City

Find out more or register here.

This course is a one-day introduction to various type-system extensions that GHC offers, such as GADTs, rank-n polymorphism, type families and more. It assumes some familiarity with Haskell. It does not make use of any other advanced Haskell concepts except for the ones it introduces, so it is in principle possible to follow this course directly after Fast Track. However, as this course focuses on the extreme aspects of Haskell’s type system, it is particularly recommended for participants who are enthusiastic about static types and perhaps familiar with a strong static type system from another language.

Well-Typed training courses

In general, our courses are very practical, but don’t shy away from theory where necessary. Our teachers are all active Haskell developers with not just training experience, but active development experience as well. In addition to the courses in New York, we regularly offer courses in London.

We also provide on-site training on requests nearly anywhere in the world. If you want to know more about our training or have any feedback or questions, have a look at our dedicated training page or just drop us a mail.

by adam at January 12, 2016 09:45 PM

January 11, 2016

Bill Atkins

GCD and Parallel Collections in Swift

One of the benefits of functional programming is that it's straightforward to parallelize operations. Common FP idioms like map, filter and reduce can be adapted so they run on many cores at once, letting you get instant parallelization wherever you find a bottleneck.

The benefits of these parallel combinators are huge. Wherever you find a bottleneck in your program, you can simply replace your call to map with a call to a parallel map and your code will be able to take advantage of all the cores on your system. On my eight-core system, for example, simply using a parallel map can theoretically yield an eight-fold speed boost. Of course, there are a few reasons you might not see that theoretical speed improvement: namely, the overhead of creating threads, splitting up the work, synchronizing data between the threads, etc. Nevertheless, if you profile your code and focus on hotspots, you can see tremendous improvements with simple changes.

Swift doesn't yet come with parallel collections functions, but we can build them ourselves, using Grand Central Dispatch:
// requires Swift 2.0 or higher
extension Array {
    public func pmap<t>(transform: (Element -> T)) -> [T] {</t>
        guard !self.isEmpty else {
            return []
        }
        
        var result: [(Int, [T])] = []
        
        let group = dispatch_group_create()
        let lock = dispatch_queue_create("pmap queue for result", DISPATCH_QUEUE_SERIAL)
        
        let step: Int = max(1, self.count / NSProcessInfo.processInfo().activeProcessorCount) // step can never be 0
        
        for var stepIndex = 0; stepIndex * step < self.count; stepIndex++ {
            let capturedStepIndex = stepIndex

            var stepResult: [T] = []
            dispatch_group_async(group, dispatch_get_global_queue(DISPATCH_QUEUE_PRIORITY_DEFAULT, 0)) {
                for i in (capturedStepIndex * step)..<((capturedStepIndex + 1) * step) {
                    if i < self.count {
                        let mappedElement = transform(self[i])
                        stepResult += [mappedElement]
                    }
                }

                dispatch_group_async(group, lock) {
                    result += [(capturedStepIndex, stepResult)]
                }
            }
        }
        
        dispatch_group_wait(group, DISPATCH_TIME_FOREVER)
        
        return result.sort { $0.0 < $1.0 }.flatMap { $0.1 }
   }
}

pmap takes the same arguments as map but runs the function across all of your system's CPUs. Let's break the function down, step by step.
  1. In the case of an empty array, pmap returns early, since the overhead of splitting up the work and synchronizing the results is non-trivial. We might take this even further by falling back to standard map for arrays with a very small element count.
  2. Create a Grand Central Dispatch group that we can associate with the GCD blocks we'll run later on. Since all of these blocks will be in the same group, the invoking thread can wait for the group to be empty at the end of the function and know for certain that all of the background work has finished before returning to the caller.
  3. Create a dedicated, sequential lock queue to control access to the result array. This is a common pattern in GCD: simulating a mutex with a sequential queue. Since a sequential queue will never run two blocks simultaneously, we can be sure that whatever operations we perform in this queue will be isolated from one another.
  4. Next, pmap breaks the array up into "steps", based on the host machine's CPU count (since this is read at runtime from NSProcessInfo, this function will automatically scale up to use all available cores). Each step is dispatched to one of GCD's global background queues. In the invoking thread, this for loop will run very, very quickly, since all it does is add closures to background queues.
  5. The main for loop iterates through each "step," capturing the stepIndex in a local variable, capturedStepIndex. If we don't do this, the closures passed to dispatch_group_async will all refer to the same storage location - as the for loop increments, all of the workers will see stepIndex increase by one and will all operate on the same step. By capturing the variable, each worker has its own copy of stepIndex, which never changes as the for loop proceeds.
  6. We calculate the start and end indices for this step. For each array element in that range, we call transform on the element and add it to this worker's local stepResult array. Because it's unlikely that the number of elements in the array will be exactly divisible by a given machine's processor count, we check that i never goes beyond the end of the array, which could otherwise happen in the very last step.
  7. After an entire step has been processed, we add this worker's results to the master result array. Since the order in which workers will finish is nondeterministic, each element of the result array is a tuple containing the stepIndex and the transformed elements in that step's range. We use the lock queue to ensure that all changes to the result array are synchronized. 
      • Note that we only have to enter this critical section once for each core - an alternative implementation of pmap might create a single master result array of the same size as the input and set each element to its mapped result as it goes. But this would have to enter the critical section once for every array element, instead of just once for each CPU, generating more memory and processor contention and benefiting less from spatial locality. 
      • We use dispatch_sync instead of dispatch_async because we want to be sure that the worker's changes have been applied to the masterResults array before declaring this worker to be done. If we were to use dispatch_async, the scheduler could very easily finish all of the step blocks but leave one or more of these critical section blocks unprocessed, leaving us with an incomplete result.
  8. Back on the original thread, we call dispatch_group_wait, which waits until all blocks in the group have completed. At this point, we know that all work has been done and all changes to the master results array have been made.
  9. The final line sorts the master array by stepIndex (since steps finish in a nondeterministic order) and then flattens the master array in that order.
To see how this works, let's create a simple profile function:

func profile(desc: String, block: () -> A) -> Void {
    let start = NSDate().timeIntervalSince1970
    block()
    
    let duration = NSDate().timeIntervalSince1970 - start
    print("Profiler: completed \(desc) in \(duration * 1000)ms")

}
We'll test this out using a simple function called slowCalc, which adds a small sleep delay before each calculation, to ensure that each map operation does enough work. In production code, you should never sleep in code submitted to a GCD queue - this is purely to simulate a slow calculation for demonstration purposes. Without this little delay, the overhead of parallelization would be too great to see a speedup:

func slowCalc(x: Int) -> Int {
    NSThread.sleepForTimeInterval(0.1)
    return x * 2
}

let smallTestData: [Int] = [Int](0..<10)
let largeTestData = [Int](0..<300)

profile("large dataset (sequential)") { largeTestData.map { slowCalc($0) } }
profile("large dataset (parallel)") { largeTestData.pmap { slowCalc($0) } }

On my eight-core machine, this results in:

Profiler: completed large dataset (sequential) in 31239.7990226746ms
Profiler: completed large dataset (parallel) in 4005.04493713379ms

an 7.8-fold increase, which is about what you'd expect.

It's important thing to remember that if each iteration doesn't do enough work, the overhead of splitting up work, setting up worker blocks and synchronizing data access will far outweigh the time savings of parallelization. The amount of overhead involved can be surprising. This code is identical to the above, except that it doesn't add the extra delay.

profile("large dataset (sequential, no delay)") { largeTestData.map { $0 * 2 } }
profile("large dataset (parallel, no delay)") { largeTestData.pmap { $0 * 2 } }

On my machine, it results in:

Profiler: completed large dataset (sequential, no delay) in 53.4629821777344ms
Profiler: completed large dataset (parallel, no delay) in 161.548852920532ms

The parallel version is three times slower than the sequential version! This is a really important consideration when using parallel collection functions:
  1. Make sure that each of your iterations does enough work to make parallelization worth it.
  2. Parallel collections are not a panacea - you can't just sprinkle them throughout your code and assume you'll get a performance boost. You still need to profile for hotspots, and it's important to focus on bottlenecks found through profiling, rather than hunches about what parts of your code are slowest.
  3. Modern CPUs are blindingly fast - basic operations like addition or multiplication are so fast that it's not worth parallelizing these, unless your array is very large.
You can use the same techniques to implement a parallel filter function:

// requires Swift 2.0 or higher
extension Array {
    public func pfilter(includeElement: Element -> Bool) -> [Element] {
        guard !self.isEmpty else {
            return []
        }
        
        var result: [(Int, [Element])] = []
        
        let group = dispatch_group_create()
        let lock = dispatch_queue_create("pmap queue for result", DISPATCH_QUEUE_SERIAL)
        
        let step: Int = max(1, self.count / NSProcessInfo.processInfo().activeProcessorCount) // step can never be 0
        
        for var stepIndex = 0; stepIndex * step < self.count; stepIndex++ {
            let capturedStepIndex = stepIndex
            
            var stepResult: [Element] = []
            dispatch_group_async(group, dispatch_get_global_queue(DISPATCH_QUEUE_PRIORITY_DEFAULT, 0)) {
                for i in (capturedStepIndex * step)..<((capturedStepIndex + 1) * step) {
                    if i < self.count && includeElement(self[i]) {
                        stepResult += [self[i]]
                    }
                }
                
                dispatch_group_async(group, lock) {
                    result += [(capturedStepIndex, stepResult)]
                }
            }
        }
        
        dispatch_group_wait(group, DISPATCH_TIME_FOREVER)
        
        return result.sort { $0.0 < $1.0 }.flatMap { $0.1 }
    }
}

This code is almost exactly identical to pmap - only the logic in the inner for loop is different.

We can now start using these combinators together (again, we have to use a slowed-down predicate function in order to see the benefit from parallelization):

func slowTest(x: Int) -> Bool {
    NSThread.sleepForTimeInterval(0.1)
    return x % 2 == 0
}

profile("large dataset (sequential)") { largeTestData.filter { slowTest($0) }.map { slowCalc($0) } }
profile("large dataset (sequential filter, parallel map)") { largeTestData.filter { slowTest($0) }.pmap { slowCalc($0) } }
profile("large dataset (parallel filter, sequential map)") { largeTestData.pfilter { slowTest($0) }.map { slowCalc($0) } }
profile("large dataset (parallel filter, parallel map)") { largeTestData.pfilter { slowTest($0) }.pmap { slowCalc($0) } }

which results in:

Profiler: completed large dataset (sequential) in 1572.28803634644ms
Profiler: completed large dataset (sequential filter, parallel map) in 1153.90300750732ms
Profiler: completed large dataset (parallel filter, sequential map) in 642.061948776245ms
Profiler: completed large dataset (parallel filter, parallel map) in 231.456995010376ms

Using one parallel combinator gives a slight improvement; combining the two parallel operations gives us an almost sevenfold performance improvement over the basic sequential implementation.

Here are some other directions to pursue:
  1. Implement parallel versions of find, any/exists and all. These are tricky because their contracts stipulate that processing stops as soon as they have a result. So you'll have to find some way to stop your parallel workers as soon as the function has its answer.
  2. Implement a parallel version of reduce. The benefit of doing this is that reduce is a "primitive" higher-order function - you can easily implement pmap and pfilter given an existing parallel reduce function.
  3. Generalize these functions to work on all collections (not just arrays), using Swift 2's protocol extensions.

by More Indirection (noreply@blogger.com) at January 11, 2016 01:39 PM

NSNotificationCenter, Swift and blocks

The conventional way to register observers with NSNotificationCenter is to use the target-action pattern. While this gets the job done, it's inherently not type-safe.

For example, the following Swift snippet will compile perfectly:

    NSNotificationCenter.defaultCenter().addObserver(self, selector: Selector("itemAdded:"),
      name: MyNotificationItemAdded, object: nil)

even though at runtime it will fail unless self has a method named itemAdded that takes exactly one parameter (leaving off that last colon in the selector will turn this line into a no-op). Plus, this method gives you no way to take advantages of Swift's closures, which would allow the observer to access local variables in the method that adds the observer and would eliminate the need to create a dedicated method to handle the event.

A better way to do this is to use blocks. And NSNotificationCenter does include a block-based API:

    NSNotificationCenter.defaultCenter().addObserverForName(MyNotificationItemAdded, object: nil, queue: nil) { note in
      // ...
    }

This is much nicer, especially with Swift's trailing closure syntax. There are no method names to be looked up at runtime, we can refer to local variables in the method that registered the observer and we can perform small bits of logic in reaction to events without having to create and name dedicated methods.

The catch comes in resource management. It's very important that an object remove its event observers when it's deallocated, or else NSNotificationCenter will try to invoke methods on invalid pointers.

The traditional target-action method has the one advantage that we can easily handle this requirement with a single call in deinit:

  deinit {
    NSNotificationCenter.defaultCenter().removeObserver(self)
  }

With the block API, however, since there is no explicit target object, each call to addObserverForName returns "an opaque object to act as observer." So your observer class would need to track all of these objects and then remove them all from the notification center in deinit, which is a pain.

In fact, the hassle of having to do bookkeeping on the observer objects almost cancels out the convenience of using the block API. Frustrated by this situation, I sat down and created a simple helper class, NotificationManager:

class NotificationManager {
  private var observerTokens: [AnyObject] = []

  deinit {
    deregisterAll()
  }

  func deregisterAll() {
    for token in observerTokens {
      NSNotificationCenter.defaultCenter().removeObserver(token)
    }

    observerTokens = []
  }

  func registerObserver(name: String!, block: (NSNotification! -> Void)) {
    let newToken = NSNotificationCenter.defaultCenter().addObserverForName(name, object: nil, queue: nil, usingBlock: block)

    observerTokens.append(newToken)
  }
  
  func registerObserver(name: String!, forObject object: AnyObject!, block: (NSNotification! -> Void)) {
    let newToken = NSNotificationCenter.defaultCenter().addObserverForName(name, object: object, queue: nil, usingBlock: block)
    
    observerTokens.append(newToken)
  }
}

First, this simple class provides a Swift-specialized API around NSNotificationCenter.  It provides an additional convenience method without an object parameter (rarely used, in my experience) to make it easier to use trailing-closure syntax. But most importantly, it keeps track of the observer objects generated when observers are registered, and removes them when the object is deinit'd.

A client of this class can simply keep a member variable of type NotificationManager and use it to register its observers. When the parent class is deallocated, the deinit method will automatically be called on its NotificationManager member variable, and its observers will be properly disposed of:

class MyController: UIViewController {
  private let notificationManager = NotificationManager()
  
  override init() {
    notificationManager.registerObserver(MyNotificationItemAdded) { note in
      println("item added!")
    }
    
    super.init()
  }
  
  required init(coder: NSCoder) {
    fatalError("decoding not implemented")
  }
}

When the MyController instance is deallocated, its NotificationManager member variable will be automatically deallocated, triggering the call to deregisterAll that will remove the dead objects from NSNotificationCenter.

In my apps, I add a notificationManager instance to my common UIViewController base class so I don't have to explicitly declare the member variable in all of my controller subclasses.

Another benefit of using my own wrapper around NSNotificationCenter is that I can add useful functionality, like group observers: an observer that's triggered when any one of a group of notifications are posted:

struct NotificationGroup {
  let entries: [String]
  
  init(_ newEntries: String...) {
    entries = newEntries
  }

}

extension NotificationManager {
  func registerGroupObserver(group: NotificationGroup, block: (NSNotification! -> ()?)) {
    for name in group.entries {
      registerObserver(name, block: block)
    }
  }
}

This can be a great way to easily set up an event handler to run when, for example, an item is changed in any way at all:

   let MyNotificationItemsChanged = NotificationGroup(
      MyNotificationItemAdded,
      MyNotificationItemDeleted,
      MyNotificationItemMoved,
      MyNotificationItemEdited
    )

    notificationManager.registerGroupObserver(MyNotificationItemsChanged) { note in
      // ...
    }

by More Indirection (noreply@blogger.com) at January 11, 2016 01:32 PM

January 09, 2016

Douglas M. Auclair (geophf)

December 2015 1HaskellADay Problems and Solutions

December 2015

  • December 30th, 2015: For today's #haskell problem we convert valid airport IATA codes to ints and back http://lpaste.net/9126537884587786240 And a Happy New Year solution: http://lpaste.net/2748656525433110528 Safe travels should you be Haskelling by air!
  • December 28th, 2015: So, remember ADVENT? What happens when your INV becomes full? Today's #haskell problem looks at that http://lpaste.net/5153847668711096320
  • December 23rd, 2015: Warm and fuzzy December, so we have a warm and fuzzy #haskell problem for today http://lpaste.net/6855091060834566144
  • December 21st, 2015: For today's #haskell problem we are to deduce stock splits using LOGIC and SCIENCE http://lpaste.net/7920293407518359552
  • December 18th, 2015: Today's #haskell problem... 'may' be thematic with that 'Star ...' what was the name of that movie? http://lpaste.net/7186856307830292480 Gosh! Star ... something! eh, whatevs: just let the Wookie win (always the best policy) http://lpaste.net/4229765238565634048 
  • December 17th, 2015: For today's #haskell problem we look at reporting out periodically on an investment and, BONUS! charting it! http://lpaste.net/638111979885559808 And we've charted our AAPL investment growth, too! http://lpaste.net/5472780506909114368 
  • December 16th, 2015: For (coming onto) today's #haskell problem we demask the masked data to unmaskify it, yo! http://lpaste.net/3793517022239784960 And then the solution unmasked that masked data! (that's convenient.) http://lpaste.net/5286190256939335680
  • December 15th, 2015: So yesterday we masked some rows, but what happened to the masking dictionary? Today's #haskell problem we save it http://lpaste.net/7703498271758483456 Ah! So that's where that cipher went! http://lpaste.net/2548817005729808384
  • December 14th, 2015: We look at a way of masking data for today's #haskell problem http://lpaste.net/4428582328419221504 And the solution gives us some lovely masked rows http://lpaste.net/7169250386480463872
  • December 11th, 2015: Today's #haskell problem asks: WHAT DOES THE TRANSFORMED JSON SAY! http://lpaste.net/5253460432890363904 (okay, that was weaksauce)
  • December 10th, 2015: For today's #Haskell problem we try to find relevancy in our daily lives http://lpaste.net/4994238781251911680 ...well, in #JSON, which is the same thing.
  • December 9th, 2015: Today's #haskell problem asks you to read in some rows of #JSON http://lpaste.net/3949063995918385152 We'll be looking into this data set through the week "Watcha readin'?" "JSON." "Cool! ... No, ... wait." http://lpaste.net/218583096285462528
  • December 8th, 2015: My main man, magic Mike (m^5 to his friends) said: "You're doing it wrong."Do it right for today's #haskell problem http://lpaste.net/6186236014281883648 A first stab at the solution, not taking into account splits, is posted at http://lpaste.net/6854975053767901184 And the split-adjusted solution here: http://lpaste.net/2656933684896071680 ~3700%-gain. It's time for me to sing the "You're the Top"-song to @MacNN_Mike
  • December 7th, 2015: In today's #haskell problem we cry «On y va!» and have at it! http://lpaste.net/5243343693259210752 En garde, you pesky investment problem, you! The solution shows Dr. Evil does NOT get ONE MILLION DOLLARS! http://lpaste.net/177540921380831232 Nor piranhas with laser beams on their heads, either.
  • December 4th, 2015: We write a web-proxy to help out poor, little Ajax go cross domain for today's #haskell problem http://lpaste.net/5120963316033781760
  • December 3rd, 2015: We meet the Ip-man for today's #haskell problem. Hiya! http://lpaste.net/8926203451507998720 Today's solution shares a little-known fact http://lpaste.net/5525895581479731200 AND ALSO uses <$> as well! Is there a weekly limit on these thingies?
  • December 2nd, 2015: Synthetic data generation for today's #haskell problem http://lpaste.net/4208367754446635008 NOT ONLY did we write a Synthetic data generator in a day http://lpaste.net/6059310371951345664 but we learned all 50 states AND used <$> and <*> – BONUS!
  • December 1st, 2015: In today's #haskell problem, we see @geophf lose his cool. http://lpaste.net/6645397898311761920 No... wait... That's not news now, is it. (RID analysis). Unwordin' down-low on the arrr-eye-dee, LIKE A GANGSTA! http://lpaste.net/7371239202307964928

by geophf (noreply@blogger.com) at January 09, 2016 09:17 PM

January 07, 2016

Edward Z. Yang

ghc-shake: Reimplementing ghc -​-make

ghc --make is a useful mode in GHC which automatically determines what modules need to be compiled and compiles them for you. Not only is it a convenient way of building Haskell projects, its single-threaded performance is good too, by reusing the work of reading and deserializing external interface files. However, the are a number of downsides to ghc --make:

  1. Projects with large module graphs have a hefty latency before recompilation begins. This is because ghc --make (re)computes the full module graph, parsing each source file's header, before actually doing any work. If you have a preprocessor, it's even worse.
  2. It's a monolithic build system, which makes it hard to integrate with other build systems if you need something more fancy than what GHC knows how to do. (For example, GHC's painstakingly crafted build system knows how to build in parallel across package boundaries, which Cabal has no idea how to do.)
  3. It doesn't give you any insight into the performance of your build, e.g. what modules take a long time to build or what the big "blocker" modules are.

ghc-shake is a reimplementation of ghc --make using the Shake build system. It is a drop-in replacement for ghc. ghc-shake sports the following features:

  1. Greatly reduced latency to recompile. This is because Shake does not recompute the module graph by parsing the header of every file; it reuses cached information and only re-parses source files which have changed.
  2. If a file is rebuilt (and its timestamp updated) but the build output has not changed, we don't bother recompiling anything that depended on it. This is in contrast to ghc --make, which has to run the recompilation check on every downstream module before concluding there is nothing to do. In fact, ghc-shake never runs the recompilation test, because we reimplemented this dependency structure natively in Shake.
  3. Using -ffrontend-opt=--profile, you can get nice profiling information about your build, including how long it took to build each module, and how expensive it is to change one of the modules.
  4. It's as fast as ghc --make on single-threaded builds. Compare this to ghc-make, another build system which uses Shake to build Haskell. ghc-make does not use the GHC API and must use the (slow) ghc -M to get initial dependency information about your project.
  5. It's accurate. It handles many edge-cases (like -dynamic-too) correctly, and because it is written using the GHC API, it can in principle be feature-for-feature compatible with ghc --make. (It's not currently, but only because I haven't implemented them yet.)

There are some downsides:

  1. Shake build systems require a .shake directory to actual store metadata about the build. This is in contrast to ghc --make, which operates entirely off of the timestamps of build products in your directory.
  2. Because it is directly implemented with the GHC API, it only works with a specific version of GHC (the upcoming GHC 8.0 release).
  3. It needs a patched version of the Shake library, because we have custom rule for building modules based off of Shake's (not exported) file representation. I've reported it here.
  4. There are still some missing features and bugs. The ones I've run into are that (1) we forget to relink in some cases, and (2) it doesn't work for building profiled code.

If you want to use ghc-shake today (not for the faint of heart), try git clone https://github.com/ezyang/ghc-shake and follow the instructions in the README. But even if you're not interested in using it, I think the code of ghc-shake has some good lessons for anyone who wants to write a build system involving Haskell code. One of the most important architectural decisions was to make the rules in ghc-shake not be organized around output files (e.g. dist/build/Data/Foo.hi, as in make) but around Haskell modules (e.g. Data.Foo). Semantic build systems work a lot better than forcing everything into a "file abstraction" (although Shake doesn't quite support this mode of use as well as I would like.) There were some other interesting lessons... but that should be the subject for another blog post!

Where is this project headed? There are a few things I'm considering doing in the not-so-immediate future:

  1. To support multiple GHC versions, we should factor out the GHC specific code into a separate executable and communicate over IPC (hat tip Duncan Coutts). This would also allow us to support separate-process parallel GHC builds which still get to reuse read interface files. In any case, ghc-shake could serve as the blueprint for what information GHC needs to make more easily accessible to build systems.
  2. We could consider moving this code back to GHC. Unfortunately, Shake is a bit too big of a dependency to actually have GHC depend on, but it may be possible to design some abstract interface (hello Backpack!) which represents a Shake-style build system, and then have GHC ship with a simple implementation for --make (but let users swap it out for Shake if they like.)
  3. We can extend this code beyond ghc --make to understand how to build entire Cabal projects (or bigger), ala ToolCabal, a reimplementation of Cabal using Shake. This would let us capture patterns like GHC's build system, which can build modules from all the boot packages in parallel (without waiting for the package to completely finish building first.

P.S. ghc-shake is not to be confused with shaking-up-ghc, which is a project to replace GHC's Makefile-based build system with a Shake based build system.

by Edward Z. Yang at January 07, 2016 05:59 PM

January 06, 2016

FP Complete

Status of School of Haskell 2.0

Status of School of Haskell 2.0

Earlier this year, I wrote a blogpost about our plans for the next version of the School of Haskell. SoH is a community service and project to make it possible to use interactive snippets of Haskell on any website, in particular on schoolofhaskell.com. Today, we are open sourcing the SoH 2.0 repositories! We've also retired FP Haskell Center, and SoH pages that were previously on fpcomplete.com now redirect to schoolofhaskell.com.

Here's the current status of the different parts:

Here's the repo main SoH code, which includes the browser client and API service. Once the service side of things is ready, they will allow you to embed interactive Haskell snippets in any website!

The soh-client is written using GHCJS, and provides a code editing widget. It uses ghcjs-react to separate the view from the model / controller. It utilizes some of GHCJS's fancier features, such as fully supporting concurrency and STM.

The soh-runner runs within a container, and hooks up stack-ide to a websocket for communication with soh-client.

The soh-scheduler provides a REST API for requesting that a container running soh-runner gets spun up. We ran into some issues with deployment to ECS, likely due to our huge docker images. Our plan is to rework / rewrite the service code to instead target Kubernetes. Since the initial implementation of SoH 2.0, we've had a lot of positive experiences with kubernetes, and would prefer to use it.

The schoolofhaskell.com repo repo contains code based on code for the fpcomplete.com site. It is served from schoolofhaskell.com. The contents of the site is not yet interactive, as the kubernetes based version of soh-scheduler still needs to be written and deployed.

Future Improvements

There are quite a few immediate things to work on in SoH, in particular, the switch to kubernetes, and integrating the new client with schoolofhaskell.com. Once these things are resolved, there are also some interesting possibilities. Ever since the client code was initially written, a number of developments have occurred that it might leverage:

One such development is haskell-ide-engine, a project to centralize our efforts on providing Haskell tools (particularly those that use GHC), as a service to text editors and IDEs. We'd like to focus our efforts in this direction on haskell-ide-engine, rather than stack-ide. This means that in the future, SoH may be based on haskell-ide-engine, along with some selection of its plugins. I encourage people to dive into helping with HIE, to bring it to a point where it makes Haskell development excellent, and to make it fit for usage SoH 2.0.

Another interesting development is Ryan Trinkle's excellent reflex library for reactive UI. While using react was quite nice overall, I ended up hacking around some of the paradigm. I think things would work out cleaner with reflex / reflex-dom, and this way SoH development can benefit that project!

January 06, 2016 08:00 AM

Functional Jobs

Software Engineer at Capital Match (Full-time)

Overview

Capital Match is the leading peer-to-peer lending platform in Singapore. Our in-house platform, mostly developed in Haskell, currently manages more than S$ 4 million in different type of facilities and is growing fast. We have closed our series A funding round about 6 months ago and are looking forward to a new round, most probably for middle of 2016. We are now embarking on the next stage of tech development to extend our set of features, strengthen our platform and develop new products. We are hiring an experienced backend software engineer to join the team.

Responsibilities

We are looking for an experienced (5+ years) software engineer interested in all aspects of the creation, growth and operations of a secure web-based platform: front-to-back features development, distributed deployment and automation in the cloud, build and test automation etc. Like all team members you will be in charge of development of new features from early design and prototyping to maintenance in production, and of exploring innovative solutions to answer current and future business needs.

Requirements

Our platform is primarily developed in Haskell with an Om/ClojureScript frontend. This job's focus being primarily on backend we are expecting our candidate to have experience working with a functional programming language, e.g. Scala/OCaml/F#/Clojure/Lisp/Erlang. Of course, demonstrable experience in Haskell would definitely be a plus.

Deployment and production is managed with Docker containers using standard cloud infrastructure so familiarity with Linux systems, command-line environment and cloud-based deployment is mandatory.

Experience in web-based software development is essential and minimum exposure to and understanding of XP practices (TDD, CI, Emergent Design, Refactoring, Peer review and programming, Continuous improvement) is expected. These are standard practices within the team. We therefore favour candidates who value simplicity and respect, accept and give feedback and who are generally team player.

Our team is distributed so ability to work comfortably in a distributed setting is essential. We will favor candidates that are living in or willing to relocate to Singapore, but we are also open to candidates willing to work remotely provided they can demonstrate solid experience with such a setting.

Offer

We offer a combination of salary and equity depending on experience and skills:

Salary: USD 4,000-8,000 / month

Equity: 0.3-1% (subject to vesting)

European citizens who relocate to Singapore do not have to pay their home country taxes and the local tax rate in Singapore is around 2-5% (effective on the proposed salary range). Visa sponsorship will be provided.

Singapore is a great place to live, a vibrant city rich with diverse cultures, a very strong financial sector and a central position in Southeast Asia.

Get information on how to apply for this position.

January 06, 2016 06:29 AM

January 05, 2016

Douglas M. Auclair (geophf)

December 2015 1HaskellADay 1-Liners

One-liners
  • December 30th, 2015: You have a string of 'digits' in base whatever to convert to an Int
    debase :: [Int] -> Int -> Int
    debase [12,21,3] 26 ~> 8661
    Define debase
    • Gautier DI FOLCO @gautier_difolco
      import Data.Bifunctor
      debase = curry (sum . uncurry (zipWith (*)) . bimap reverse (flip iterate 1 . (*)))
    • bazzargh @bazzargh
      debase a b = sum $ zipWith (*) (reverse a) (map (b^) [0..])
    • obadz @obadzz
      or debase l b = foldl (\ p n -> p * b + n) 0 l
    • bazzargh @bazzargh
      that's better than mine. how about:
      flip (foldl1 . ((+) .) . (*))
  • December 12th, 2015: #math You have this sequence: [1,1,1,1,1,1,2,1,1,1,3,3] What is this pattern? Is there one? Write #haskell to generate this list.
  • December 3rd, 2015: Lens-y again Points-free-itize the following correctName :: Row -> Row correctName r = set lastName (init (view lastName r)) r
  • December 3rd, 2015: Let's get a little lens-y with this one: accumer :: Getter a t a -> t -> [a] -> [a] accumer f s acc = ans where ans = view f s:acc
    • Define the curried-accumer function that curries away the acc-argument.
    • What would the curried definition be if the function type were: accumer :: Getter a t a -> t -> Set a -> Set a
  • December 3rd, 2015: define minimax :: Ord eh => eh -> (eh, eh) -> (eh, eh) such that, e.g.: minimax 1 (2,3) ~> (1,3) minimax 10 (2,3) ~> (2,10)
    • Thomas Dietert @thomasdietert In that case, minimax n (x,y) = (minimum [n,x,y], maximum [n,x,y])
    • joomy @cattheory minimax = liftM2 (***) min max
  • December 1st, 2015: define (->>) :: (a -> m ()) -> (a -> m ()) -> a -> m () All monadic effects must be evaluated.
    • Jérôme @phollow (->>) f g a = f a >> g a 
      • then liftM2 (>>)
      • Nicoλas @BeRewt but the full applicative is: liftA2 (*>)

by geophf (noreply@blogger.com) at January 05, 2016 12:47 PM

January 04, 2016

apfelmus

FRP — Release of reactive-banana version 1.1

Happy New Year, everyone! I’m pleased to announce the release of version 1.1.0.0 of my reactive-banana library on hackage.

This is essentially a maintenance release that fixes an important type mistake. Atze van der Ploeg has kindly pointed out to me that the switchB and switchE combinators need to be in the Moment monad

switchB :: Behavior a -> Event (Behavior a) -> Moment (Behavior a)
switchE :: Event (Event a) -> Moment (Event a)

This is necessary to make their efficient implementation match the semantics.

Apart from that, I have mainly improved the API documentation, adding graphical figures to visualize the main types and adding an introduction to recursion in FRP. Atze has also contributed a simplified implementation of the model semantics, it should now be much easier to digest and understand. Thanks!

The full changelog can be found in the repository. Happy hacking!

January 04, 2016 09:07 PM

January 02, 2016

Philip Wadler

Joy of Coding

I will be keynoting at Joy of Coding, 17 June, De Doelen, Rotterdam. Thank you to Felienne Hermans for the invite. Looking forward to it!

by Philip Wadler (noreply@blogger.com) at January 02, 2016 01:48 PM

Felipe Almeida Lessa

Announcing serversession

I’m pleased to announce the serversession family of packages.

Background

HTTP is a stateless protocol. Cookies are used to create sessions out of otherwise independent requests made by the browser to the server. There are many ways of managing sessions via cookies, but they can be mostly separated into two big camps:

Client-side sessions
The cookie data contains the session data. For example, it could contain a shopper’s login and cart contents.
Server-side sessions
The cookie data contains a session identifier, and the session data is kept on a database indexed by the session identifiers.

The clientsession package has existed for many years already. It’s both Yesod‘s and Snap‘s de facto session backend. It performs well and is battle tested by many different people and companies.

However, there are many reasons why one may want to favor server-side sessions over client-side ones:

  • Saving arbitrary amounts of session data without being constrained by cookie size limits. Even if your data fits on a cookie, you may want to spare having to bounce all that data around on every request and response.
  • Securely invalidating a session. User logout with client-side sessions erases the cookie from the user’s browser but doesn’t invalidate its data. The old cookie is still valid until its expiration. Server-side sessions, however, can be securely invalidate by simply erasing them from your session database. This can be a critical feature depending on your needs.

The biggest disadvantage of server-side sessions is that they need more server-side resources. Not only it needs space for sessions storage, but it also incurs the overhead of zero to two DB transactions per HTTP request.

One solution isn’t inherently better than the other. It all depends on your use case. And if your use case needs server-side sessions, this is your lucky day.

The serversession packages

I’d like to fill the gap that currently exists on the Haskell ecosystem with respect to server-side session support. Preferably once and for all. That’s why there are many serversession packages.

The main one, aptly called serversession, contains the core logic about server-side sessions. It’s abstracted over a backend which will store the session’s data (usually a database). And it’s meant to be used by a frontend, such as Yesod or Snap. Besides having a nice test suite, it’s also unencumbered by the minutia of dealing with databases and thus is easier to review. It also defines a standard test suite that every backend needs to pass.

Out-of-the-box you’ll find support for many different backends:

We also already officially support the most popular frontends:

Adding a new backend is very straightforward, specially because there’s already a test suite for free. Adding a new frontend is a bit more complicated depending on how well your frontend’s concept of sessions maps to serversession’s. If you’d like to support your favorite backend/frontend, please send your contributions back upstream so they become official packages as well!

Usage example

If you have an Yesod app, you’re probably using persistent. Changing your app to support serversession is just a matter of setting up the session storage entities and changing Yesod’s default session backend (not to be confused with a serversession backend).

To setup the entities, you’ll have to teach persistent how to set them up on your database. Please check serversession-backend-persistent’s docs for details, but it all boils down to changing your migration Template Haskell code from:

-- On Model.hs
share [mkPersist sqlSettings, mkMigrate "migrateAll"]

to:

-- On Model.hs
share [mkPersist sqlSettings, mkSave "entityDefs"]

-- On Application.hs
mkMigrate "migrateAll" (serverSessionDefs (Proxy :: Proxy SessionMap) ++ entityDefs)

Changing the default session backend is even easier. Again, please read the docs, but you’ll just add the following to your instance Yesod App:

    makeSessionBackend = simpleBackend id . SqlStorage . appConnPool

And you’re set! Please take a look at the included example project to see how everything fits together.

Final words

One of clientsession’s biggest success was in being used by many different projects. This is desirable both for reducing duplicate community efforts and for increasing the number of eyeballs over a security-related piece of code. I’d like to make serversession equally successful in the same way, which is why it supports from the get-go both the major Haskell web frameworks that today use clientsession by default.

I’d like to invite your criticism and feedback. And your success stories as well!

Happy New Year!

by Felipe Lessa at January 02, 2016 03:06 AM

December 30, 2015

Gabriel Gonzalez

Compile-time memory safety using Liquid Haskell

When indexing into a vector, you usually have one of two options:

  • enable bounds-checking to throw an exception if you index out of bounds or:
  • disable bounds-checking to improve performance.

Both of these options are still unsatisfactory, though. Even if your program fails fast with an exception, your program still failed.

Fortunately, Haskell programmers can now select a third option:

  • verify at compile time that you never index a vector out of bounds.

A new tool named Liquid Haskell makes this sort of verification possible. Liquid Haskell is a customizable static analysis tool for the Haskell language that eliminates a wide variety of programming errors at compile time that would normally be difficult to eliminate using Haskell's ordinary type system.

However, the Liquid Haskell tool still needs a lot of polish. I've been using Liquid Haskell for the last couple of months and in my experience the tool is just starting to become "usable in anger". I'm saying this as somebody who has reported eight issues with the tool so far and encountered a ninth issue while writing up this post.

I'll illustrate how Liquid Haskell works by:

  • implementing a binary search algorithm for Haskell's Vector type,
  • using Liquid Haskell to statically verify the complete absence of out-of-bound indexing, and then:
  • safely disabling bounds checking since I've proven the algorithm correct.

Along the way I'll highlight both the ups and downs of using Liquid Haskell so that you can preview what it's like to use the tool.

Let's begin with the following Haskell code for binary search over a sorted Vector. I've included a real mistake I made when first implementing this algorithm. See if you can spot the mistake:

import Data.Vector as Vector

{-| Postconditions:

* If the result is `Just i`, then `0 <= i < length v`
-}
binarySearch :: Ord a => a -> Vector a -> Maybe Int
binarySearch x v = loop x v 0 (Vector.length v - 1)

{-| Preconditions:

* `0 <= lo < length v`
* `lo <= hi < length v`
-}
loop :: Ord a => a -> Vector a -> Int -> Int -> Maybe Int
loop x v lo hi = do
let mid = (lo + hi) `div` 2
if x < v ! mid
then do
let hi' = mid - 1
if lo <= hi'
then loop x v lo hi'
else Nothing
else if v ! mid < x
then do
let lo' = mid + 1
if lo' <= hi
then loop x v lo' hi
else Nothing
else Just mid

Let's try this out on a few values:

$ stack ghci --resolver=lts-3.19 vector
...
Prelude> :load binarysearch.hs
...
*Main> let v = Vector.fromList [1, 4, 5, 10]
*Main> binarySearch 4 v
Just 1
*Main> binarySearch 3 v
Nothing
*Main> binarySearch 1 v
Just 0
*Main> binarySearch 0 v
Nothing
*Main> binarySearch 10 v
Just 3
*Main> binarySearch 11 v
Nothing

Liquid Haskell

We can run this code through the Liquid Haskell tool in order to locate all potential out-of-bounds indexes. In order to install the tool we must have some SMT solver on our $PATH which Liquid Haskell uses to automate the deduction process. In my case, I installed the Z3 solver by downloading the latest stable release from this page (Version 4.4.1 at the time of this writing):

Then I installed Liquid Haskell using stack:

$ cat stack.yaml 
resolver: lts-3.19
packages: []
extra-deps:
- intern-0.9.1.4
- liquid-fixpoint-0.4.0.0
$ stack build liquidhaskell

... and then I run the liquid tool over my code like this:

$ stack exec liquid binarysearch.hs
LiquidHaskell Copyright 2009-15 Regents of the University of California. All Rights Reserved.


**** DONE: Extracted Core using GHC *******************************************


**** DONE: generateConstraints ************************************************


**** START: fixpoint ***********************************************************



========================================================
© Copyright 2009 Regents of the University of California.
All Rights Reserved.
========================================================
............../Unsatisfied Constraints:
{snip}
UNSAT

**** DONE: fixpoint ***********************************************************


**** DONE: solve **************************************************************


**** DONE: annotate ***********************************************************


**** UNSAFE ********************************************************************


binarysearch.hs:18:16-18: Error: Liquid Type Mismatch
Inferred type
VV : {VV : Int | VV == mid}

not a subtype of Required type
VV : {VV : Int | VV >= 0 && VV < vlen v}

In Context
VV : {VV : Int | VV == mid}
v : {v : (Vector a) | 0 <= vlen v}
?a : {?a : Int | ?a == lo + hi}
hi : Int
mid : {mid : Int | mid == ?a / ?b && (?a >= 0 && ?b >= 0 => mid >= 0) &&
(?a >= 0 && ?b >= 1 => mid <= ?a)}
?b : {?b : Int | ?b == 2}
lo : Int


binarysearch.hs:22:23-24: Error: Liquid Type Mismatch
Inferred type
VV : {VV : Int | VV == lo}

not a subtype of Required type
VV : {VV : Int | VV < lo && VV >= 0}

In Context
VV : {VV : Int | VV == lo}
lo : Int


binarysearch.hs:24:17-19: Error: Liquid Type Mismatch
Inferred type
VV : {VV : Int | VV == mid}

not a subtype of Required type
VV : {VV : Int | VV >= 0 && VV < vlen v}

In Context
VV : {VV : Int | VV == mid}
v : {v : (Vector a) | 0 <= vlen v}
?a : {?a : Int | ?a == lo + hi}
hi : Int
mid : {mid : Int | mid == ?a / ?b && (?a >= 0 && ?b >= 0 => mid >= 0) &&
(?a >= 0 && ?b >= 1 => mid <= ?a)}
?b : {?b : Int | ?b == 2}
lo : Int


binarysearch.hs:28:23-25: Error: Liquid Type Mismatch
Inferred type
VV : {VV : Int | VV == lo'}

not a subtype of Required type
VV : {VV : Int | VV < lo && VV >= 0}

In Context
VV : {VV : Int | VV == lo'}
?a : {?a : Int | ?a == lo + hi}
?c : {?c : Int | ?c == 2}
hi : Int
mid : {mid : Int | mid == ?a / ?c && (?a >= 0 && ?c >= 0 => mid >= 0) &&
(?a >= 0 && ?c >= 1 => mid <= ?a)}
?b : {?b : Int | ?b == 1}
lo : Int
lo' : {lo' : Int | lo' == mid + ?b}

Okay, so we got four errors on our first check. How concerned should we be?

Usually these errors fall into three categories:

  • Missing preconditions

    We fix these by formally documenting the preconditions of our own functions using Liquid Haskell's type system

  • Missing postconditions

    We fix these by formally documenting the postconditions of functions we use, also using Liquid Haskell's type system

  • Genuine bugs (i.e. your code is wrong even when all preconditions and postconditions are correctly documented)

    We fix these by correcting our code

When we first begin most of the errors will fall into the first two categories (missing preconditions or postconditions) and as things progress we may discover errors in the third category (genuine bugs).

Preconditions

Liquid Haskell documents the preconditions and postconditions of many Haskell functions "out-of-the-box" by providing "refined" type signatures for these functions. You can find all of the built-in refined type signatures here:

... and here's an example refined type from the Data.Vector module (slightly modified from the original):

assume ! :: v : Vector a -> { i : Int | 0 <= i && i < vlen v } -> a

(!) is Haskell's infix operator for indexing into a vector. Normally, the ordinary Haskell type signature for this operator would look like this:

(!) :: Vector a -> Int -> a

... which you can read roughly as saying: "The first (left) argument to this infix operator is a Vector containing elements of type a (where a can be any type). The second (right) argument to this infix operator is the index you want to retrieve. The result is the retrieved element.

Here is an example use of the operator:

$ stack ghci --resolver=lts-3.19 vector
Prelude> import Data.Vector as Vector
Prelude Vector> let v = Vector.fromList [1, 4, 5, 10]
Prelude Vector> v ! 0
1
Prelude Vector> v ! 3
10
Prelude Vector> v ! 2
5
Prelude Vector> v ! 4
*** Exception: ./Data/Vector/Generic.hs:249 ((!)): index out of bounds (4,4)

Oops! This operator is not safe because indexing can fail at runtime with an exception if you index out of bounds.

This is where Liquid Haskell comes into play. Liquid Haskell lets you write richer type signatures that document preconditions and postconditions. These type signatures resemble Haskell type signatures except that you can decorate them with logical predicates, like this:

assume ! :: v : Vector a -> { i : Int | 0 <= i && i < vlen v } -> a

This is an example of a precondition. The above refined type says: "The index, i, must be non-negative and must be less than the length of the vector, v, that you supplied for the first argument".

So how does Liquid Haskell know what the length of the vector is? Remember that Liquid Haskell needs to somehow verify this precondition at compile time even though we don't necessarily know what the input will be at compile time. In fact, Liquid Haskell actually doesn't know anything about Vectors at all, let alone their lengths, unless we teach it!

Postconditions

We can teach Liquid Haskell about Vector lengths by introducing a new "measure" named vlen:

measure vlen :: Vector a -> Int

The only thing we provide is the type of vlen, but there is no code associated with vlen. Just treat vlen as an abstract type-level placeholder for the length of the Vector. We can use vlen to give a more refined type to Vector.length:

assume Vector.length :: v : Vector a -> { n : Int | n == vlen v }

This is an example of a postcondition. You can read this type signature as saying: "We know for sure that whatever Int that length returns must be the length of the Vector".

The assume keyword indicates that we haven't proven this the correctness of this refined type. Instead we are asserting that the type is true. Any time you study a Liquid Haskell program you need to stare really hard at any part of the code that uses assume since that's an escape hatch that might compromise any safety guarantees.

Not all postconditions require the use of assume. In fact, Liquid Haskell can automatically promote a restricted subset of Haskell safely to the type level. Unfortunately, this subset does not include operations on Vectors, which is why we must assert the correctness of the above refined type.

Safety

Let's verify that the refined types for (!) and length work correctly using a small test example. We'll begin with a program that is not necessarily safe:

import Data.Vector as Vector

example :: Vector a -> a
example v = v ! 2

We run the above program through the liquid type-checker and get a type error (as expected) since the type-checker cannot verify that the input Vector has at least three elements:

$ stack exec example.hs
...
UNSAT

**** UNSAFE ********************************************************************


safe.hs:4:17: Error: Liquid Type Mismatch
Inferred type
VV : {VV : Int | VV == ?a}

not a subtype of Required type
VV : {VV : Int | VV >= 0 && VV < vlen v}

In Context
VV : {VV : Int | VV == ?a}
v : {v : (Vector a) | 0 <= vlen v}
?a : {?a : Int | ?a == 2}

Don't worry if you don't understand the type error just yet. Right now all we care about is the line and column number, which point directly at the 2 in the source code:

import Data.Vector as Vector

example :: Vector a -> a
example v = v ! 2
-- ERROR HERE ^

There are two ways we can fix our program. The best solution is to add a precondition to the type of our example function. We can specify that our function only works for Vectors that have at least 3 elements:

import Data.Vector as Vector

{-@ example :: { v : Vector a | 3 <= vlen v } -> a @-}
example :: Vector a -> a
example v = v ! 2

We document this in a second parallel type signature embedded within a Haskell comment. Liquid Haskell is designed to be backwards compatible with the Haskell language and is not yet a formal language extension supported by ghc, which is why Liquid Haskell types have to live inside comments.

Once we add that precondition then the liquid Haskell type-checker verifies that our program is correct:

$ stack exec liquid example.hs
...
SAT

**** DONE: fixpoint ***********************************************************


**** DONE: solve **************************************************************


**** DONE: annotate ***********************************************************


**** SAFE **********************************************************************

WARNING: Once you begin using this tool you will quickly grow addicted to that SAFE message. Using Liquid Haskell feels very much like a fun game where the reward is correct code!

Another way we can satisfy the type-checker is to check the Vector's length at runtime and return Nothing if the Vector is too small. We wrap successful results in Just if the Vector is large enough:

import Data.Vector as Vector

example :: Vector a -> Maybe a
example v =
if 3 <= Vector.length v
then Just (v ! 2)
else Nothing

Notice how this program requires no Liquid Haskell type signature or type annotation. Liquid Haskell is smart enough to figure out that the precondition for (!) was already satisfied by the runtime check:

$ stack exec liquid example.hs
...
**** SAFE **********************************************************************

However, we prefer to avoid runtime checks if possible. Type-level refinements improve on runtime checks in two important ways:

  • Refinements are "free" - they incur no runtime cost
  • Refinements encourage pushing fixes upstream (by constraining the input) instead of propagating problems downstream (by returning a Maybe output)

Binary search - Continued

Let's revisit our binary search algorithm and study the first error message more closely:

 binarysearch.hs:18:16-18: Error: Liquid Type Mismatch
Inferred type
VV : {VV : Int | VV == mid}

not a subtype of Required type
VV : {VV : Int | VV >= 0 && VV < vlen v}

In Context
VV : {VV : Int | VV == mid}
v : {v : (Vector a) | 0 <= vlen v}
?a : {?a : Int | ?a == lo + hi}
hi : Int
mid : {mid : Int | mid == ?a / ?b && (?a >= 0 && ?b >= 0 => mid >= 0) &&
(?a >= 0 && ?b >= 1 => mid <= ?a)}
?b : {?b : Int | ?b == 2}
lo : Int

Your first reflex should be to jump to the line and column numbers, which point to this location:

{-| Invariants:

* `0 <= lo < length v`
* `lo <= hi < length v`
-}
loop :: Ord a => a -> Vector a -> Int -> Int -> Maybe Int
loop x v lo hi = do
let mid = (lo + hi) `div` 2
if x < v ! mid
-- ^^^ ERROR HERE
then do
let hi' = mid - 1
if lo <= hi'
then loop x v lo hi'
else Nothing
else if v ! mid < x
then do
let lo' = mid + 1
if lo' <= hi
then loop x v lo' hi
else Nothing
else Just mid

This suggests that we provided an index that might be out of bounds and the error message confirms that:

   Inferred type
VV : {VV : Int | VV == mid}

not a subtype of Required type
VV : {VV : Int | VV >= 0 && VV < vlen v}

This is Liquid Haskell's way of saying: "I can't prove that mid is within the vector bounds". Liquid Haskell will even explain its reasoning process, showing what refinements were in scope for that expression:

   In Context
VV : {VV : Int | VV == mid}
v : {v : (Vector a) | 0 <= vlen v}
?a : {?a : Int | ?a == lo + hi}
hi : Int
mid : {mid : Int | mid == ?a / ?b && (?a >= 0 && ?b >= 0 => mid >= 0) &&
(?a >= 0 && ?b >= 1 => mid <= ?a)}
?b : {?b : Int | ?b == 2}
lo : Int

This is an example of the first class of errors: missing preconditions. Liquid Haskell can't read our comment so Liquid Haskell has no way of knowing that lo and hi are within the vector bounds. Therefore, Liquid Haskell can't conclude that their midpoint, mid, is also within the vector bounds.

This is very easy to fix. We can transform our unstructured comment describing preconditions into a refined type for the loop function:

{-@
loop
:: Ord a
=> x : a
-> v : Vector a
-> lo : { lo : Int | 0 <= lo && lo < vlen v }
-> hi : { hi : Int | lo <= hi && hi < vlen v }
-> Maybe Int
@-}
loop :: Ord a => a -> Vector a -> Int -> Int -> Maybe Int

Now our documentation is machine-checked and will never go out of date!

Refining our input

Now we get several new errors when we run our code through the liquid type-checker. I've only included the first error message for brevity:

 binarysearch.hs:8:29: Error: Liquid Type Mismatch
Inferred type
VV : {VV : Int | VV == ?a}

not a subtype of Required type
VV : {VV : Int | 0 <= VV && VV < vlen v}

In Context
VV : {VV : Int | VV == ?a}
v : {v : (Vector a) | 0 <= vlen v}
?a : {?a : Int | ?a == 0}

This points to a new subexpression:

binarySearch :: Ord a => a -> Vector a -> Maybe Int
binarySearch x v = loop x v 0 (Vector.length v - 1)
-- ERROR HERE ^

Liquid Haskell incorporated the new information we supplied through the refined type. The type-checker then worked backwards from loop's preconditions and found a problem in our code via the following reasoning process:

  • The type of loop says that the lo argument must be less than the length of the vector
  • We supplied 0 for the lo argument to loop
  • Therefore the Vector v needs to be at least length 1
  • But we never proved that the Vector has at least one element!

This is an example of the third class of errors: a genuine bug. I introduced this bug when I first wrote up this algorithm and Liquid Haskell caught my mistake. I never thought about the case where the Vector was empty. Many programmers smarter than me would carefully consider the corner case where the Vector was empty, but I use tools like Liquid Haskell so that I don't need to be smart (or careful).

In this case we don't want to refine the type of binarySearch to require non-empty Vector inputs since we want to support binary searches for Vectors of all sizes. Instead, we will add a special case to handle an empty Vector input:

binarySearch :: Ord a => a -> Vector a -> Maybe Int
binarySearch x v =
if Vector.length v == 0
then Nothing
else loop x v 0 (Vector.length v - 1)

Refining our output

Now the type-checker gives a new error message:

 binarysearch.hs:25:16-18: Error: Liquid Type Mismatch
Inferred type
VV : {VV : Int | VV == mid}

not a subtype of Required type
VV : {VV : Int | VV >= 0 && VV < vlen v}

In Context
VV : {VV : Int | VV == mid}
v : {v : (Vector a) | 0 <= vlen v}
?a : {?a : Int | ?a == lo + hi}
hi : {hi : Int | lo <= hi && hi < vlen v}
mid : {mid : Int | mid == ?a / ?b && (?a >= 0 && ?b >= 0 => mid >= 0) &&
(?a >= 0 && ?b >= 1 => mid <= ?a)}
lo : {lo : Int | 0 <= lo && lo < vlen v}
?b : {?b : Int | ?b == 2}

Let's see where this points:

loop :: Ord a => a -> Vector a -> Int -> Int -> Maybe Int
loop x v lo hi = do
let mid = (lo + hi) `div` 2
if x < v ! mid
-- ^^^ ERROR HERE
then do
let hi' = mid - 1
if lo <= hi'
then loop x v lo hi'
else Nothing
else if v ! mid < x
then do
let lo' = mid + 1
if lo' <= hi
then loop x v lo' hi
else Nothing
else Just mid

This is the same as the first error message! WHAT GIVES?!?!

Liquid Haskell already knows that both lo and hi are within the Vector bounds, but cannot deduce that their midpoint must also lie within the Vector bounds.

This is an example of the second class of errors: missing postconditions. In this case the issue here is a deficiency of Liquid Haskell's built-in Prelude. Without going into too many details, the built-in refinement for the div function uses integer division, but for some reason type-level division does not provide sufficient information for Liquid Haskell to deduce that the midpoint lies between lo and hi. I'm actually still in the process of narrowing downthe precise problem before reporting this on the Liquid Haskell issue tracker, so I may be interpreting this problem incorrectly.

Edit: Rhanjit Jhala explained that you can fix this by supplying the --real flag or adding this pragma to the top of the file:

{-@ LIQUID "--real" @-}

import Data.Vector as Vector

...

Once you supply this flag then the postcondition for div correctly satisfies the type-checker. The previous version of this post used an assume to enforce the relevant postcondition, which is no longer necessary with this flag.

Termination checking

We're now down to two error messages, the first of which is:

 binarysearch.hs:31:23-24: Error: Liquid Type Mismatch
Inferred type
VV : {VV : Int | VV == lo}

not a subtype of Required type
VV : {VV : Int | 0 <= VV && VV < vlen v && VV < lo && VV >= 0}

In Context
VV : {VV : Int | VV == lo}
v : {v : (Vector a) | 0 <= vlen v}
lo : {lo : Int | 0 <= lo && lo < vlen v}

This one took me an hour to figure out and the error message originates from Liquid Haskell's termination checker! I only figured this error out because I already knew that Liquid Haskell had a built-in termination checker and even then I had to first minimize the code example before I fully understood the problem.

Liquid Haskell supports termination checking by default, which is actually pretty awesome despite the confusing error. Termination checking means that Liquid Haskell verifies that our code never endlessly loops. Or in other words, Liquid Haskell transforms Haskell into a "total" programming language (i.e. a programming language where computation always halts). You can also disable the termination checker completely or disable the checker for selected functions if you find the check too restrictive.

The termination checker proves termination by looking for some sort of "well-founded metric" that shows that the function will eventually terminate. This "well-founded metric" is usually an Int that decreases each time the function recurses and the recursion halts when the Int reaches 0.

By default, Liquid Haskell guesses and tries to use the first Int argument to the recursive function as the well-founded metric, which was the lo argument in our example. You get an error message like the above when Liquid Haskell guesses wrong. In our case, lo is not a suitable "well-founded" metric because lo does not decrease every time the function recurses. Quite the opposite: lo either stays the same or increases.

loop x v lo hi = do
let mid = (lo + hi) `div` 2
if x < v ! mid
then do
let hi' = mid - 1
if lo <= hi'
then loop x v lo hi' -- `lo` stays the same
else Nothing
else if v ! mid < x
then do
let lo' = mid + 1
if lo' <= hi
then loop x v lo' hi -- `lo` increases
else Nothing
else Just mid

The hi argument is also not a suitable well-founded metric. hi never increases, but hi does not necessarily decrease either:

loop x v lo hi = do
let mid = (lo + hi) `div` 2
if x < v ! mid
then do
let hi' = mid - 1
if lo <= hi'
then loop x v lo hi' -- `hi` decreases
else Nothing
else if v ! mid < x
then do
let lo' = mid + 1
if lo' <= hi
then loop x v lo' hi -- `hi` stays the same
else Nothing
else Just mid

However, we are not limited to using arguments as well-founded metrics. We can create our own custom metric that is a composite of the given arguments. In this case we do know that hi - lo always decreases on every iteration and we can instruct Liquid Haskell to use that as the well-founded metric using the following syntax:

{-@
loop
:: Ord a
=> x : a
-> v : Vector a
-> lo : { lo : Int | 0 <= lo && lo < vlen v }
-> hi : { hi : Int | lo <= hi && hi < vlen v }
-> Maybe Int
/ [hi - lo] -- The well-founded metric
@-}

SAFE

Once we add the well-founded metric the type-checker accepts our program!!!

stack exec liquid binarysearch.hs 
LiquidHaskell Copyright 2009-15 Regents of the University of California. All Rights Reserved.


**** DONE: Extracted Core using GHC *******************************************


**** DONE: generateConstraints ************************************************


**** START: fixpoint ***********************************************************



========================================================
© Copyright 2009 Regents of the University of California.
All Rights Reserved.
========================================================
........................../
SAT

**** DONE: fixpoint ***********************************************************


**** DONE: solve **************************************************************


**** DONE: annotate ***********************************************************


**** SAFE **********************************************************************

That's it! We're done. Liquid Haskell analyzed the flow of our program and statically verified two properties about our program:

  • Our program will never fail from an out-of-bounds index error
  • Our program will never loop endlessly

The only assistance we had to provide was to document preconditions and postconditions in the types and the type-checker automated the rest of the proof.

This means that we can safely disable bounds checking by replacing (!) with Vector.unsafeIndex. Compile-time memory safety already rocks, but getting a free speed improvement is icing on the cake.

Edit: /u/f2u on /r/haskell points out that there is still a bug: the code can fail due to integer overflow.

You can further eliminate the possibility of integer overflow through the use of refinement types, but Liquid Haskell does not provide these extra refinements to protect against overflow by default. Instead you must opt-in to them by adding your own refinements.

The solution to prevent overflow is to replace this:

(lo + hi) `div` 2

... with this:

lo + (hi - lo) `div` 2

Exercise

If you remember correctly, our original code had a postcondition:

{-| Postconditions:

* If the result is `Just i`, then `0 <= i < length v`
-}
binarySearch :: Ord a => a -> Vector a -> Maybe Int
binarySearch x v = loop x v 0 (Vector.length v - 1)

Try modifying the final code example (See the Appendix) to add this postcondition as a refinement to the type of binarySearch. Hint: you will also need to further refine the type of loop as well.

You will not need to assume any additional information if you do this correctly. The type-checker should be able to verify the newly added postcondition from the existing preconditions.

Conclusion

If you would like to learn more about Liquid Haskell, I highly recommend the official Liquid Haskell tutorial. This tutorial is well-written, comprehensive, and packed with practical examples:

Liquid Haskell is designed in the same spirit as Haskell: check as much as possible with as little input from the programmer. Despite all the bugs I run into, I keep coming back to this tool because of the very high power-to-weight ratio for formal verification.

Also note that the final program is still valid Haskell code so we don't sacrifice any compatibility with the existing Haskell toolchain by using Liquid Haskell.

Appendix

Here is the complete final program that type-checked, for reference:

{-@ LIQUID "--real" @-}

import Data.Vector as Vector

{-| Postconditions:

* If the result is `Just i`, then `0 <= i < length v`
-}
binarySearch :: Ord a => a -> Vector a -> Maybe Int
binarySearch x v =
if Vector.length v == 0
then Nothing
else loop x v 0 (Vector.length v - 1)

{-@
loop
:: Ord a
=> x : a
-> v : Vector a
-> lo : { lo : Int | 0 <= lo && lo < vlen v }
-> hi : { hi : Int | lo <= hi && hi < vlen v }
-> Maybe Int
/ [hi - lo]
@-}
loop :: Ord a => a -> Vector a -> Int -> Int -> Maybe Int
loop x v lo hi = do
let mid = (lo + hi) `div` 2
if x < v ! mid
then do
let hi' = mid - 1
if lo <= hi'
then loop x v lo hi'
else Nothing
else if v ! mid < x
then do
let lo' = mid + 1
if lo' <= hi
then loop x v lo' hi
else Nothing
else Just mid

by Gabriel Gonzalez (noreply@blogger.com) at December 30, 2015 07:26 PM

Philip Wadler

Ada Lovelace Symposium, Oxford

I was fortunate to attend a celebration of Ada Lovelace's 200th birthday at Oxford, featuring fantastic talks by Sydney Padua, Bernard Sufrin, Judith Grabiner, and many others. After the first session of three talks I thought "I wish all of those were longer", something I cannot remember thinking ever before! It's all online, so you can see it too.

by Philip Wadler (noreply@blogger.com) at December 30, 2015 01:43 PM

Halmos on refereeing


Paul Halmos offers excellent advice on refereeing, two tenets that he formed as a young referee and confirmed as an experienced editor: "be Boolean; be prompt".


From "I want to be a mathematician: an automathography" by P. R. Halmos.

by Philip Wadler (noreply@blogger.com) at December 30, 2015 01:13 PM

December 29, 2015

Philip Wadler

Impredicative images

Three images, spotted by Ohad Kammar (@aleph_kappa). Ohad suggests they illustrate recursion, but I think they represent impredicativity. Impredicativity is a category error, when a predicate applies to itself, as in Russell's paradox; but also a defining feature of polymorphic lambda calculus, where a function abstracted over a type may be applied to its own type.



by Philip Wadler (noreply@blogger.com) at December 29, 2015 12:39 PM

December 28, 2015

ERDI Gergo

Hacks of 2015

Encsé writes in his blog that one of the reasons he created a tiny CPS-based Scheme interpreter was because he realized he hasn't done any fun side projects all year. So I thought I'd make an inventory of fun hacks I've done in 2015.

Bit-fiddling

  • An FPGA implementation of the Commodore PET. This is still not fully finished: although I managed to hunt down the bug mentioned at the end of the blog post, I still haven't gotten around to implementing Datasette (tape) I/O.
  • Viki & I put together a prototype for an AVR-based CHIP-8 handheld. This one has no web presence yet; we're hoping to finalize the design into a PCB-based one, before releasing the schematics and the code.

    CHIP-328

  • Went to a hackerspace.sg workshop/hackathon for the Fernvale platform. Not much came out of that, I think I was the only person who at least got as far as running my own code on the device (reusing the low-level bitbanging from Fernly of course). I ended up doing some lame but colourful animations on the screen that would have gotten me boo'd off the stage in a 1986 demo compo.

Games

  • I wanted to do some old-school 8-bit hacking, and ended up reverse-engineering and then reimplementing in Inform 6 the classic Hungarian text adventure game Időrégész. This even got me my fifteen minutes on Hungarian retro-gaming blog IDDQD.
  • I managed to convince Viki to join me in participating in MiniLD #56. We decided early on to go with only 2 keyboard keys, 4 colours, one game mechanic, and a dancing theme — so, a rhythm game! To make deployment easy, we wanted it to be playable via just a web browser, and ended up choosing Elm as our development platform. The end result, after a frantic weekend of hacking, is Two-Finger Boogie.

Talks

Functional programming

  • Fixed a long-standing bug in MetaFun, the "Haskell"-to-C++ template metaprogram compiler: patterns in function definitions are now tried for matching in the correct order.
  • Wrote a Bison summary parser that a co-worker wanted to use to generate exhaustive test cases for Bison-generated parsers. That project ended up not going anywhere as far as I know.
  • If you use every GHC extension and then some, you can write a fairly nifty untyped-to-typed embedding of STLC that is almost as nice as doing it in a proper dependently typed language!

Stack Overflow highlights

Some of the answers I wrote this year on Stack Overflow required me to learn just enough of something new to be able to answer the question:

Then, there were those where it turned out there was a bug to be found by scratching the surface of the question deep enough:

Then there were the answers that were just too much fun to write:

All in all, it seems this has been quite a productive year for me out of the office, even if you exclude the Stack Overflow part. I was actually surprised how long this list was while compiling it for this blog post. Maybe I should write a list like this every year from now...

December 28, 2015 09:33 PM

December 26, 2015

Audrey Tang

期待已久的意外派對

<article lang="zh-Hant" xml:lang="zh-Hant">

Camelia-small

哈囉。叮、叮、叮,注意!……注意!

謝謝。

嗨,如果你不認識我(就算認識也一樣),我是 Camelia。人們叫我在 Perl 6 正式現身的派對上發表談話,所以我就在這囉。有其他人負責燒烤,我只是來敬酒的。他們跟我說這次說話要認真一點。哈,說得好像我知道怎麼認真講話一樣。認真的嗎?

好吧。認真說來,我要謝謝你們大家今天一起出櫃。

啊,那好像有點雙關。抱歉。呃,也沒什麼好抱歉的啦……

但還是謝謝你們來這裡,這是 Perl 6 的大日子。她這下可正式成年了。嗯……差不多啦。總之她駕照已經到手了。當心了,世界!

[從後面桌子傳來聽不見的議論]

喔,我不該提到這個嗎?我都還沒真的談到那些小事故耶,當時她……好吧,算了。我們繼續。我相信她會是個好駕駛的。從現在開始。

總之,我真的對 Perl 6 非常感同身受,因為我是隻蝴蝶。我也不得不在蛹裡忍住很久的時間,等到出來的那一天。我真的是非出櫃不可。哈,應該說是飛出櫃吧!

呃,唉呀。我又來了,是吧。

總之,請對 Perl 6 有點耐心。雖然我們今天宣稱她長大了,但你也知道,她還只是青少年。當我們很小的時候,就只是那年紀的小鬼,但當我們成為青少年,歷經賀爾蒙的變化時,這個嘛,我們就會開始不穩定了。這種不穩定的程度,有一陣子會顯得更嚴重。在 15 歲的時候,這種不穩定的幅度可能是正負 10 年。某天的舉止就像是 25 歲,隔天又像是 5 歲一樣。

所以 Perl 6 還需要再更加成熟,這當然囉。我的意思不是在她亂發脾氣把我們逼瘋的日子裡我們就比較不愛她,我的意思是,呃,我想我的意思是她就是家人,而不論甘苦你都會愛著家人的。因為你相信,總有一天會苦盡甘來。

而我們都是她的大家族,今天在這裡相聚。人們說撫養一個小孩需要一座村莊,但從來沒有過這樣的小孩或這樣的村莊!如果你明天宿醉消退後,有機會看看程式碼,也請看看背後的貢獻者列表。超過 800 人積極地為 Perl 6 的開發提供協助,以各種方式。當然一定還有些名字沒列在上面。

你們是很重要的一群人,你們所有人都是,不只是家族中親近的那些人。我們家族從很久以前就知道,成長中的電腦語言所能得到的最珍貴指引,有些來自於直系親屬之外。朋友和熟人,有時比朝夕相處的人能擁有更大的視野。這就是為什麼會需要一座村莊。

「成熟」這件事就像碎形,會在許多尺度下進行。Perl 6 透過你們認識她即將進入的寬廣世界,外頭的世界充滿挑戰。Perl 6 對其中某些情況已做好準備,這多虧了你們。

當然,她還只有 15 歲。某些事情她已經做得很好了。她的溝通技巧非常棒,當不懂你的意思時也很有禮貌。她可以同時進行許多對話。她數學很好,也相當擅長處理各種物件。她熱愛外語,以及那些奇妙的字符。

但她仍是個慎重的孩子,在學習事物時有時似乎思考得太努力了。沒關係,在接下來幾年她會變得更快並更有效率,因為她的腦袋正在重組成完全的大人。她會學到新的東西,關於這個世界和自己。但我不認為她的性格會有太大的變化,這點是很明顯的。

而這是因為她的性格其實來自於大家。是你們的愛讓她誕生,而現在她準備要把這些愛,傳達給還不認識她的人。

火箭升空時我們都會很興奮。TimToady 告訴我在凌晨起床看水星號、雙子星號和阿波羅火箭升空的事。我還太小不記得那些,但我們有自己的刺激進展可以追蹤。我的話,我很高興看到這禮拜 SpaceX 成功降落。在經過一些小事故後……

[又一陣聽不見的議論]

我不理你。小心了,我們已經非常非常擅長不理會某些人。別成為他們之中的一份子。

真的,我為那些只在不開心的事出現時才開心的人感到遺憾。

總之,向世界推出 Perl 6 就像火箭升空。倒數時非常興奮,還有不知道會升空還是爆炸的屏息時刻。我們現在就是如此。主推進器已經點著了,固定器也鬆開了。這些都很戲劇化,主要是因為此刻看來並沒有真的發生什麼事。

不過火箭本來就跟這些無關,戲劇性並不是火箭想要的。火箭想要的是升空,更快更快再更快。這跟位置無關,甚至也跟速率無關。重要的是,一切都在加速進行中。

[舉杯]

那麼,在此獻上 Perl 6。她將自由高飛。祝她為存在而歡喜,祝她為發現世界而歡喜,祝她只要願意就能不斷加速!乾杯!

</article>

by audreyt at December 26, 2015 01:53 AM

December 24, 2015

Bill Atkins

Working on the Swift compiler with Jetbrains AppCode

Just a few weeks ago, Apple open-sourced the Swift compiler and standard library. This is exciting news for the Swift community: not only will Swift development now be done in the open, but the availability of Swift's source makes it possible to port Swift to other platforms.

The Swift codebase is very large (approaching 400k lines of C++ code, including test cases) so an IDE to help you navigate through it would be ideal. I'm partial to the Jetbrains tools, but wasn't sure if I could use them to browse the Swift source tree. I had some difficulty getting CLion to use the CMake scripts in the Swift repo and was about to give up. Fortunately, I noticed in the bottom of Swift's README that there's a script to generate an Xcode project from the Swift repo.

So here's how I generated the Xcode project and was able to work on Swift using AppCode:

1. Create a new parent directory, cd into it and clone the Swift repo:

$ mkdir Swift
$ cd Swift
$ git clone https://github.com/apple/swift.git

2.  Prep the Swift repo, per the instructions in the README. This will import other tools that Swift depends on (like cmark and some LLVM tools)

$ cd swift
./utils/update-checkout --clone

3.  Generate the Xcode project:

$ utils/build-script -X --skip-build -- --reconfigure

4. Now open AppCode and click File | Open...

5. Find the outer Swift directory you created in step 1 (the one that holds the Swift repo and all its associated tools).

6. Open the build folder, then open Xcode-DebugAssert. You'll see a folder that looks like swift-macosx-x86_64 (the exact name may differ based on your system).

Just open this folder in AppCode, wait for indexing to complete, and you'll be able to browse and Edit the Swift source from AppCode!

by More Indirection (noreply@blogger.com) at December 24, 2015 01:17 PM

December 22, 2015

Philip Wadler

John Finnemore on Paris



From The Now Show, Series 47, Episode 6, Friday 18 December 2015.
Good news, globally 2015 is likely to be the hottest year ever recorded. And if it is the hottest year ever recorded then it will beat the previous record holder, last year.  ...

There is genuinely, genuinely good news about the environment this week, the Paris climate deal has been signed, a global agreement made by 195 countries to try and keep temperature rise below 1.5 degrees as we move away from fossil fuels. President Orlande said "History is coming. In fact, history is here." Which I'm not sure is quite how history works. I take his point. And the Prime Minister himself said "This global deal now means the whole world has signed up to play its part in halting climate change." And what inspiring words those are. And with those inspiring words, he beetled off home to see what part he could play in this global effort. And only a few days later he managed to change the law about fracking under Britain's national parks. I know what's happened though, it's a simple misunderstanding. They've heard everyone in Paris talking about how we must move to a fossil-fuel free future and said to themselves "Hang on, there's a bit of fossil fuel left under the Lake District. Better dig that up pronto and burn it." I assume that's what happened. Either that, or it's just like when you go to the gym, and then on the way home you say to yourself "Well, I've earned myself some fish and chips". Except of course the Paris agreement is actually a collection of largely non-binding aspirations for the future, so this is more like saying "I really must go the gym more often. Well that's earned me some fish and chips."

by Philip Wadler (noreply@blogger.com) at December 22, 2015 04:23 PM

December 21, 2015

Neil Mitchell

Solving the GCHQ puzzle "by hand"

The GCHQ 2015 Christmas puzzle is a Nonogram puzzle, which involves filling in squares on a grid to reveal a picture, guided by constraints on the rows and columns. For a computer, a nice way to solve this problem is using a SAT solver. But humans aren't great at SAT solving, and I was given a print-out of this puzzle while on holiday, with no computer. I'd never encountered such a puzzle before, so working with a friend (and some wine) we came up with an approach, and set about applying it. Alas, robustly applying an algorithm with many steps is not easy for a human, and we eventually ended up with contradictions. On returning from holiday, I automated our approach, and tested it. Our approach worked, and the code is below.

The Problem

The puzzle is:

It comprises a 25x25 grid, some filled in squares, and alongside each row/column are the number of consecutive squares that must be filled in each line. For example, the 8th row down must have two runs of three filled squares, with a gap in between, and potentially gaps before or after.

Our Approach

Our approach was to take each line and compute the number of "free" gaps - how many spaces could be inserted with choice. For one row (4 from the bottom) the entire grid is constrained, with no free gaps. Starting with the most constrained lines, we tried to figure out where the pieces could go, based on the existing squares. We quickly realised that negative information was important, so tagged each square with "don't know" (left blank), must be filled (we shaded it in) or must be unfilled (we drew a circle in it). For each line in isolation, looking at the constraints, we inferred squares to be filled or unfilled by examining the possible locations of each run.

The Code

I implemented our approach in Haskell, complete code is available here.

Our constraint system works over a grid where each square is in one of three states. We can encode the grid as [[Maybe Bool]]. The [[.]] is a list of lists, where the outer list is a list of rows, and the inner list is a list of squares. Each of the inner lists must be the same length, and for the GCHQ puzzle, they must all be 25 elements long. For the squares we use Maybe Bool, with Nothing for unknown and Just for known, using True as filled and False as unfilled.

Given the [[Maybe Bool]] grid and the constraints, our approach was to pick a single line, and try to layout the runs, identifying squares that must be True/False. To replicate that process on a computer, I wrote a function tile that given the constraints and the existing line, produces all possible lines that fit. The code is:

tile :: [Int] -> [Maybe Bool] -> [[Bool]]
tile [] xs = maybeToList $ xs ~> replicate (length xs) False
tile (c:cs) xs = concat [map (\r -> a ++ b ++ c ++ r) $ tile cs xs
| gap <- [0 .. length xs - (c + sum cs + length cs)]
, (false,xs) <- [splitAt gap xs]
, (true,xs) <- [splitAt c xs]
, (space,xs) <- [splitAt 1 xs]
, Just a <- [false ~> replicate gap False]
, Just b <- [true ~> replicate c True]
, Just c <- [space ~> replicate (length space) False]]

The first equation (second line) says that if there are no remaining constraints we set all remaining elements to False. We use the ~> operator to check our desired assignment is consistent with the information already in the line:

(~>) :: [Maybe Bool] -> [Bool] -> Maybe [Bool]
(~>) xs ys | length xs == length ys &&
and (zipWith (\x y -> maybe True (== y) x) xs ys)
= Just ys
(~>) _ _ = Nothing

This function takes a line of the grid (which may have unknowns), and a possible line (which is entirely concrete), and either returns Nothing (inconsistent) or Just the proposed line. We first check the sizes are consistent, then that everything which is concrete (not a Nothing) matches the proposed value.

Returning to the second equation in tile, the idea is to compute how many spaces could occur at this point. Taking the example of a line 25 long, with two runs of size 3, we could have anywhere between 0 and 18 (25-3-3-1) spaces first. For each possible size of gap, we split the line up (the splitAt calls), then constrain each piece to match the existing grid (using ~>).

Given a way of returning all possible lines, we then collapse that into a single line, by marking all squares which could be either True or False as Nothing:

constrainLine :: [Int] -> [Maybe Bool] -> Maybe [Maybe Bool]
constrainLine cs xs = if null xs2 then Nothing else mapM f $ transpose xs2
where xs2 = tile cs xs
f (x:xs) = Just $ if not x `elem` xs then Nothing else Just x

If there are no satisfying assignments for the line, we return Nothing - that implies the constraints are unsatisfiable. Next, we scale up to a side of constraints, by combining all the constraints and lines:

constrainSide :: [[Int]] -> [[Maybe Bool]] -> Maybe [[Maybe Bool]]
constrainSide cs xs = sequence $ zipWith constrainLine cs xs

Finally, to constrain the entire grid, we constrain one side, then the other. To simplify the code, we just transpose the grid in between, so we can treat the rows and columns identically:

constrainGrid :: [[Int]] -> [[Int]] -> [[Maybe Bool]] -> Maybe [[Maybe Bool]]
constrainGrid rows cols xs =
fmap transpose . constrainSide cols .
transpose =<< constrainSide rows xs

To constrain the whole problem we apply constrainGrid repeatedly, until it returns Nothing (the problem is unsatisfiable), we have a complete solution (problem solved), or nothing changes. If nothing changes then there might be two solutions, or our approach might not be powerful enough without using search.

The Result

After four iterations we end up with a fully constrained answer. To see the progress, after one iteration we have:

..XXXXX...X.OO..X.XXXXX..
..OOOOX.X.O.....O.XOOOO..
..XXX.X....O...OX.X.XX...
X.XXX.X....XXXXXX.X.XX...
X.XXX.X..XXXX..XX.X.XX..X
X.OOOOX...XO...OO.XOOO..X
XXXXXXXOXOXOXOXOXOXXXXXXX
..OOO.OO..XOOOX.XOOOOO.O.
..XX..XX.OXOXOXXXOXO...X.
..XO..OO....OXX.O.O....X.
..X...X......X..X......O.
..O...O......XO.X........
..XX..X.X....O.OO.X......
..OXX.O.X....XXXX.X......
..XX..XXXXX..O.OO........
..X...O.X..O..O.X...O....
..X...X.X.OXO.O.X...X....
..OOO.O.X..O..O.X...X..X.
X.XXXXX.......O.X...X..X.
X.OOO.X.....XOO.X...X..X.
X.XXX.X.....XXOOX...X...O
XOXXXOXOXXXOXXXXXXXXXXOXX
..XXX.X.....XXXXX..XXXX.O
..OOOOX......OOOO...O.X..
..XXXXX......XOXX.O.X.X..

Here a . stands for Nothing. After four iterations we reach the answer in a total of 0.28s:

XXXXXXXOXXXOOOXOXOXXXXXXX
XOOOOOXOXXOXXOOOOOXOOOOOX
XOXXXOXOOOOOXXXOXOXOXXXOX
XOXXXOXOXOOXXXXXXOXOXXXOX
XOXXXOXOOXXXXXOXXOXOXXXOX
XOOOOOXOOXXOOOOOOOXOOOOOX
XXXXXXXOXOXOXOXOXOXXXXXXX
OOOOOOOOXXXOOOXXXOOOOOOOO
XOXXOXXXOOXOXOXXXOXOOXOXX
XOXOOOOOOXXXOXXOOOOXOOOXO
OXXXXOXOXXXXOXXOXOOOOXXOO
OXOXOOOXOOOXOXOXXXXOXOXXX
OOXXOOXOXOXOOOOOOXXOXXXXX
OOOXXXOXXOXXOXXXXXXOXXXOX
XOXXXXXXXXXOXOXOOXXOOOOXO
OXXOXOOXXOOOXXOXXXOOOOOXO
XXXOXOXOXOOXOOOOXXXXXOXOO
OOOOOOOOXOOOXXOXXOOOXXXXX
XXXXXXXOXOOXXOOOXOXOXOXXX
XOOOOOXOXXOOXOOXXOOOXXOXO
XOXXXOXOOOXXXXOOXXXXXOOXO
XOXXXOXOXXXOXXXXXXXXXXOXX
XOXXXOXOXOOXXXXXXOXXXXXXO
XOOOOOXOOXXOOOOOOXOXOXXOO
XXXXXXXOXXOOOXOXXOOOXXXXX

Update: On the third attempt, my friend managed to solve it manually using our technique, showing it does work for humans too.

by Neil Mitchell (noreply@blogger.com) at December 21, 2015 09:25 PM

Roman Cheplyaka

Fixing Permission denied (publickey). after an SSH upgrade

This weekend I upgraded my laptop from Fedora 22 to 23. Today, when I tried to push to github, I suddenly got

% git push     
Permission denied (publickey).
fatal: Could not read from remote repository.

Please make sure you have the correct access rights
and the repository exists.

To debug this, I ran (according to these instructions)

% ssh -vT git@github.com
OpenSSH_7.1p1, OpenSSL 1.0.2e-fips 3 Dec 2015
debug1: Reading configuration data /home/feuerbach/.ssh/config
debug1: Reading configuration data /etc/ssh/ssh_config
debug1: /etc/ssh/ssh_config line 56: Applying options for *
debug1: Connecting to github.com [192.30.252.129] port 22.
debug1: Connection established.
debug1: identity file /home/feuerbach/.ssh/id_rsa type 1
debug1: key_load_public: No such file or directory
debug1: identity file /home/feuerbach/.ssh/id_rsa-cert type -1
debug1: identity file /home/feuerbach/.ssh/id_dsa type 2
debug1: key_load_public: No such file or directory
debug1: identity file /home/feuerbach/.ssh/id_dsa-cert type -1
debug1: key_load_public: No such file or directory
debug1: identity file /home/feuerbach/.ssh/id_ecdsa type -1
debug1: key_load_public: No such file or directory
debug1: identity file /home/feuerbach/.ssh/id_ecdsa-cert type -1
debug1: key_load_public: No such file or directory
debug1: identity file /home/feuerbach/.ssh/id_ed25519 type -1
debug1: key_load_public: No such file or directory
debug1: identity file /home/feuerbach/.ssh/id_ed25519-cert type -1
debug1: Enabling compatibility mode for protocol 2.0
debug1: Local version string SSH-2.0-OpenSSH_7.1
debug1: Remote protocol version 2.0, remote software version libssh-0.7.0
debug1: no match: libssh-0.7.0
debug1: Authenticating to github.com:22 as 'git'
debug1: SSH2_MSG_KEXINIT sent
debug1: SSH2_MSG_KEXINIT received
debug1: kex: server->client chacha20-poly1305@openssh.com <implicit> none
debug1: kex: client->server chacha20-poly1305@openssh.com <implicit> none
debug1: kex: curve25519-sha256@libssh.org need=64 dh_need=64
debug1: kex: curve25519-sha256@libssh.org need=64 dh_need=64
debug1: expecting SSH2_MSG_KEX_ECDH_REPLY
debug1: Server host key: ssh-rsa SHA256:nThbg6kXUpJWGl7E1IGOCspRomTxdCARLviKw6E5SY8
debug1: Host 'github.com' is known and matches the RSA host key.
debug1: Found key in /home/feuerbach/.ssh/known_hosts:19
debug1: SSH2_MSG_NEWKEYS sent
debug1: expecting SSH2_MSG_NEWKEYS
debug1: SSH2_MSG_NEWKEYS received
debug1: Roaming not allowed by server
debug1: SSH2_MSG_SERVICE_REQUEST sent
debug1: SSH2_MSG_SERVICE_ACCEPT received
debug1: Authentications that can continue: publickey
debug1: Next authentication method: publickey
debug1: Offering RSA public key: /home/feuerbach/.ssh/id_rsa
debug1: Authentications that can continue: publickey
debug1: Skipping ssh-dss key /home/feuerbach/.ssh/id_dsa for not in PubkeyAcceptedKeyTypes
debug1: Trying private key: /home/feuerbach/.ssh/id_ecdsa
debug1: Trying private key: /home/feuerbach/.ssh/id_ed25519
debug1: No more authentication methods to try.
Permission denied (publickey).

The important line is this one

debug1: Skipping ssh-dss key /home/feuerbach/.ssh/id_dsa for not in PubkeyAcceptedKeyTypes

It turns out that Fedora 23 ships with OpenSSH 7.1p1 which has disabled DSS (aka DSA) keys by default.

A short term solution is to add

Host *
PubkeyAcceptedKeyTypes=+ssh-dss

to ~/.ssh/config. A long-term solution is to replace the DSS keys with, say, RSA keys.

December 21, 2015 08:00 PM

FP Complete

Using Stack on Travis CI

Using Stack for build of Haskell code on Travis CI has number of benefits. For those unfamiliar with it, Travis is a cloud-base continuous integration system, which will build and test your code automatically. It integrates with Github and is free for open-source projects (but also has paid plans for private projects). Stack's use of cached packages built from Stackage snapshots means builds will be much shorter than without, and reduces the guesswork of whether a build failure was introduced by your own code or something that changed on Hackage. It's also easy to use multiple environment configurations to test against multiple snapshots, including the latest nightly, as a way to ensure that your code builds against a known-to-work set of the latest packages.

Stack works very nicely on Travis, but until recently the documentation for how to set it up languished in semi-obscurity on the Stack wiki. Hereby, we are lifting it out of obscurity. Rather than repeat ourselves, go look at:

  • The Travis with caching section of the user's guide, which should be sufficient for most use cases.
  • The Travis CI document, which has more information and a slightly different approach.

December 21, 2015 05:20 PM

Mark Jason Dominus

A message to the aliens, part 23/23 (wat)

Earlier articles: Introduction Common features Page 1 (numerals) Page 2 (arithmetic) Page 3 (exponents) Page 4 (algebra) Page 5 (geometry) Page 6 (chemistry) Page 7 (mass) Page 8 (time and space) Page 9 (physical units) Page 10 (temperature) Page 11 (solar system) Page 12 (Earth-Moon system) Page 13 (days, months, and years) Page 14 (terrain) Page 15 (human anatomy) Page 16 (vital statistics) Page 17 (DNA chemistry) Page 18 (cell respiration and division) Pages 19-20 (map of the Earth) Page 21 (the message) Page 22 (cosmology)

This is page 23 (the last) of the Cosmic Call message. An explanation follows.

This page is a series of questions for the recipients of the message. It is labeled with the glyph , which heretofore appeared only on page 4 in the context of solving of algebraic equations. So we might interpret it as meaning a solution or a desire to solve or understand. I have chosen to translate it as “wat”.

I find this page irritating in its vagueness and confusion. Its layout is disorganized. Glyphs are used inconsistent with their uses elsewhere on the page and elsewhere in the message. For example, the mysterious glyph , which has something to do with the recipients of the message, and which appeared only on page 21 is used here to ask about both the recipients themselves and also about their planet.

The questions are arranged in groups. For easy identification, I have color-coded the groups.

Starting from the upper-left corner, and proceeding clockwise, we have:

Kilograms, meters, and seconds, wat. I would have used the glyphs for abstract mass, distance, and time, and , since that seems to be closer to the intended meaning.

Alien mathematics, physics, and biology, wat. Note that this asks specifically about the recipients’ version of the sciences. None of these three glyphs has been subscripted before. Will the meaning be clear to the recipients? One also wonders why the message doesn't express a desire to understand human science, or science generally. One might argue that it does not make sense to ask the recipients about the human versions of mathematics and physics. But a later section expresses a desire to understand males and females, and the recipients don't know anything about that either.

Aliens wat. Alien [planet] mass, radius, acceleration wat. The meaning of shifts here from meaning the recipients themselves to the recipients’ planet. “Acceleration” is intended to refer to the planet's gravitational acceleration as on page 14. What if the recipients don't live on a planet? I suppose they will be familiar with planets generally and with the fact that we live on a planet, which explained back on pages 11–13, and will get the idea.

Fucking speed of light, how does it work?

Planck's constant, wat. Universal gravitation constant, wat?

Males and females, wat. Alien people, wat. Age of people, wat. This group seems to be about our desire to understand ourselves, except that the third item relates to the aliens. I'm not quite sure what is going on. Perhaps “males and females” is intended to refer to the recipients? But the glyphs are not subscripted, and there is no strong reason to believe that the aliens have the same sexuality.

The glyph , already used both to mean the age of the Earth and the typical human lifespan, is even less clear here. Does it mean we want to understand the reasons for human life expectancy? Or is it intended to continue the inquiry from the previous line and is asking about the recipients’ history or lifespan?

Land, water, and atmosphere of the recipients’ planet, wat.

Energy, force, pressure, power, wat. The usage here is inconsistent from the first group, which asked not about mass, distance, and time but about kilograms, meters, and seconds specifically.

Velocity and acceleration, wat. I wonder why these are in a separate group, instead of being clustered with the previous group or the first group. I also worry about the equivocation in acceleration, which is sometimes used to mean the Earth's gravitational acceleration and sometimes acceleration generally. We already said we want to understand mass , , and the size of the Earth. The Earth's surface gravity can be straightforwardly calculated from these, so there's nothing else to understand about that.

Alien planet, wat. The glyph has heretofore been used only to refer to the planet Earth. It does not mean planets generally, because it was not used in connection with Jupiter . Here, however, it seems to refer to the recipients’ planet.

The universe, wat. HUH???

That was the last page. Thanks for your kind attention.

[ Many thanks to Anna Gundlach, without whose timely email I might not have found the motivation to finish this series. ]

by Mark Dominus (mjd@plover.com) at December 21, 2015 12:39 PM

Ken T Takusagawa

[igptrdec] Encoding arbitrary precision integers in binary

Unary can encode arbitrarily large non-negative integers.  Adding a trailing 0 allows encoding a sequence of numbers by concatenating their representations.  Let's call the following encoding Encoding 1.

xEncoding 1Bit length
001
1102
21103
311104
4111105
51111106
611111107
7111111108
81111111109
9111111111010

Unary takes up a lot of space; binary is better.  For arbitrary sized integers (and especially, to encode a collection of integers), we need a way of encoding the length of the binary portion.  This can be done by prefixing a header which denotes the length of the following binary portion, with the header encoded in Encoding 1.  The header is highlighted in bold below. We form all possible bit strings of this format and line them up with the natural numbers to yield a bijection.  Let's call this combined scheme Encoding 2.

xEncoding 2Bit length
001
11003
21013
3110005
4110015
5110105
6110115
711100007
811100017
911100107
1011100117
1111101007
1211101017
1311101107
1411101117
151111000009
301111011119
311111100000011
63111111000000013
12711111110000000015
2551111111100000000017

Because we reset the binary portion back to 000...0 for each new length, converting back and forth from a number x to its encoding is a little bit tricky.

Encoding 2 still takes up quite a bit of space, with the header consuming over half the length of an encoded number.  We can improve this by recursion: encode the header (highlighted in bold below) in Encoding 2 (instead of Encoding 1), then follow it with a binary portion as before.  Let's call this combined scheme Encoding 3.

xEncoding 3Bit length
001
110004
210014
3101005
4101015
5101105
6101115
7110000008
8110000018
9110000108
10110000118
11110001008
12110001018
13110001108
14110001118
151100100009
31110100000010
631101100000011
1271110000000000014
25511100010000000015

We can recurse until infinity, with Encoding N having its header encoded in Encoding N-1.  There is always an integer large enough such that Encoding N saves space over N-1.  (Practically, there is no benefit beyond Encoding 4.). Translating back and forth efficiently from a (large) number and its encoding continues to be a little tricky.

This scheme is similar to encoding the length of the length of a number in decimal.

Next, we can recurse "beyond infinity".  For each bit string in Encoding N, prefix it with N encoded in Encoding 1.  This prefix is highlighted in bold below, demonstrating prefixing on Encoding 1, 2, and 3.  (We had arbitrarily chosen for the Encoding indices to start from 1 not 0 to preserve the elegance of encoding 0 as just 0.)

[100 1010 10110 101110 1011110 10111110 ...]
[1100 110100 110101 11011000 11011001 11011010 ...]
[11100 11101000 11101001 111010100 111010101 111010110 ...]
...

Sort the elements of this infinite list of infinite lists of bit strings first by bit length then lexicographically.  Call this Encoding Omega (inspired by ordinal numbers, where omega is the first number beyond all the finite numbers).

xEncoding OmegaBit length
001
11003
210104
311004
4101105
5111005
61011106
71101006
81101016
91111006
1010111107
1111111007
12101111108
13110110008
14110110018
15110110108
16110110118
17111010008
18111010018
19111111008
201011111109
211110101009
221110101019
231110101109
241110101119
251111111009
26101111111010
27110111000010
28110111000110
29110111001010
30110111001110
31110111010010
32110111010110
33110111011010
34110111011110
35111101000010
36111101000110
37111111110010
381011111111011
391111010010011
401111010010111
411111010011011
421111010011111
431111111110011
4410111111111012
4511011110000012
4611011110000112
4711011110001012
4811011110001112
4911011110010012
5011011110010112
5111011110011012
5211011110011112
5311011110100012
5411011110100112
5511011110101012
5611011110101112
5711011110110012
5811011110110112
5911011110111012
6011011110111112
6111101100000012
6211101100000112
6311101100001012
6411101100001112
6511101100010012
6611101100010112
6711101100011012
6811101100011112
6911111010000012
7011111010000112
7111111111110012
72101111111111013
73111011001000013
74111011001000113
75111011001001013
76111011001001113
77111011001010013
78111011001010113
79111011001011013
80111011001011113
81111011001100013
82111011001100113
83111011001101013
84111011001101113
85111011001110013
86111011001110113
87111011001111013
88111011001111113
89111101010000013
90111101010000113
91111101010001013
92111101010001113
93111101010010013
94111101010010113
95111101010011013
96111101010011113
97111110100010013
98111110100010113
99111110100011013
100111110100011113
101111111111110013
1021011111111111014
1031101111100000014
1041101111100000114
1841111110100000114
1851111111111110014
18610111111111111015
18711101101100000015
29411111101000011115
29511111111111110015
296101111111111111016
4441011111111111111017
49010111111111111111018
830101111111111111111019
11321011111111111111111020
211210111111111111111111021
3566101111111111111111111022
69781011111111111111111111023
1278410111111111111111111111024
25412101111111111111111111111025
486261011111111111111111111111026
6432610111111111111111111111111027
91636101111111111111111111111111028
1503441011111111111111111111111111029
25957410111111111111111111111111111030
518986101111111111111111111111111111031
9886641011111111111111111111111111111032
197716410111111111111111111111111111111033
3888634101111111111111111111111111111111034
77771021011111111111111111111111111111111035
1545574010111111111111111111111111111111111036

Efficiently translating between a number x and its Encoding Omega seems so difficult that Encoding Omega is probably practically useless.

Going beyond Encoding Omega is possible, choosing a different encoding (instead of Encoding 1) to express the header.  Encoding Omega Plus One uses Encoding 2 as the header, and Encoding Omega Plus Omega, i.e., Encoding Two-Omega, uses Encoding Omega for the header.

Here is some Haskell code to (inefficiently) compute these encodings up to and including Encoding Omega.  Encoding Omega required merge sorting an infinite list of infinite lists, which would be normally be impossible (when scanning the heads, you never know if you have found the smallest item).  However, all bit strings originating from Encoding N (and above) have length at least N+2, so finding all bit strings of a given length can be done in finite time.

by Ken (noreply@blogger.com) at December 21, 2015 09:49 AM

December 19, 2015

Christopher Done

A philosophical difference between Haskell and Lisp

One difference in philosophy of Lisp (e.g. Common Lisp, Emacs Lisp) and Haskell is that the latter makes liberal use of many tiny functions that do one single task. This is known as composability, or the UNIX philosophy. In Lisp a procedure tends to accept many options which configure its behaviour. This is known as monolithism, or to make procedures like a kitchen-sink, or a Swiss-army knife.

Which one is better can be discussed in another post. I just want to make the simple case that there is indeed a difference in philosophy and practice. Having written my fair share of non-trivial Emacs Lisp (and a small share of Common Lisp; I’ve maintained Common Lisp systems) and my fair share of non-trivial Haskell I think I’m in a position to judge.

Full disclosure: We’ll just look at some trivial examples anyone can understand, with the (unproven but asserted) implication that these examples are representative of the general way software is written in these languages.

An example which should be readily familiar to any programmer of any background is working on lists. For example, CL has the remove-if-not procedure. Its documentation signature is like this:

(REMOVE-IF-NOT predicate seq :key :count :start :end :from-end)

It packs a number of ideas into one procedure.

By comparison, Haskell has the filter function:

filter :: (a -> Bool) -> [a] -> [a]

Given a problem statement “take all elements from the list–except the first three–that satisfy predicate p, and take only the first five of those”, in Common Lisp you’d express it quite concisely as this:

(remove-if-not #'p xs :count 5 :start 3)

The same in Haskell would be expressed as this:

take 5 . filter p . drop 3

The difference which should be obvious whether you know Haskell or Lisp is that in the Lisp code the function does a few behaviours and accepts arguments to configure them. In the Haskell code, we use three different functions which do one task:

take  Int -> [a] -> [a]
filter  (a -> Bool) -> [a] -> [a]
drop  Int -> [a] -> [a]

The . operator composes functions together, just like pipes in UNIX. We might express this in UNIX something like:

bash-3.2$ cat | tail -n '+4' | grep -v '^p' | head -n 5
1
2
3
4
5
6
7
8
9
10

Press Ctrl-d here we get:

4
5
6
7
8

Like pipes in UNIX, the functions are clever enough to be performant when composed together–we don’t traverse the whole list and generate a new list each time, each item is generated on demand. In fact, due to stream fusion, the code will be compiled into one fast loop.

If we want things that don’t satisfy the predicate, we just compose again with not:

take 5 . filter (not . p) . drop 3

In Common Lisp composition is a bit wordier because it’s rarely if ever used, so instead there is another function for that:

(remove-if #'p xs :count 5 :start 3)

(Probably a more Lispy approach would’ve been to have a :not keyword argument to the remove-if function.)

The most pathological example of such a kitchen sink in Lisp is the well known LOOP macro.

Problem: get all elements greater than 5, then just the even ones of that set.

With the LOOP macro this can be expressed quite readily:

> (loop for i in '(1 2 3 4)
        when (evenp i)
        collect i
        when (> i 5) do (return))
(2 4)

In Haskell this is expressed with two separate functions:

λ> (filter even . takeWhile (< 5)) [1..4]
[2,4]

In Haskell the same applies to vector libraries and text libraries and bytes libraries, which can be fused. Fusion is chiefly an advantage of purity – you can fuse n loops together into one loop if you know that they don’t do side-effects. Such an advantage can also be applied to other pure languages like Idris or PureScript or Elm.

December 19, 2015 12:00 AM

December 18, 2015

Mark Jason Dominus

Math.SE report 2015-08

I only posted three answers in August, but two of them were interesting.

  • In why this keeps apearing in my group theory book? (cycle decomposition) the querent asked about the “conjugation” operation that keeps cropping up in group theory. Why is it important? I sympathize with this; it wasn't adequately explained when I took group theory, and I had to figure it out a long time later. Unfortunately I don't think I picked the right example to explain it, so I am going to try again now.

    Consider the eight symmetries of the square. They are of five types:

    1. Rotation clockwise or counterclockwise by 90°.
    2. Rotation by 180°.
    3. Horizontal or vertical reflection
    4. Diagonal reflection
    5. The trivial (identity) symmetry

    What is meant when I say that a horizontal and a vertical reflection are of the same ‘type’? Informally, it is that the horizontal reflection looks just like the vertical reflection, if you turn your head ninety degrees. We can formalize this by observing that if we rotate the square 90°, then give it a horizontal flip, then rotate it back, the effect is exactly to give it a vertical flip. In notation, we might represent the horizontal flip by , the vertical flip by , the clockwise rotation by , and the counterclockwise rotation by ; then we have

    $$ \rho H \rho^{-1} = V$$

    and similarly

    $$ \rho V \rho^{-1} = H.$$

    Vertical flips do not look like diagonal flips—the diagonal flip leaves two of the corners in the same place, and the vertical flip does not—and indeed there is no analogous formula with replaced with one of the diagonal flips. However, if and are the two diagonal flips, then we do have

    $$ \rho D_1 \rho^{-1} = D_2.$$

    In general, When and are two symmetries, and there is some symmetry for which

    $$xax^{-1} = b$$

    we say that is conjugate to . One can show that conjugacy is an equivalence relation, which means that the symmetries of any object can be divided into separate “conjugacy classes” such that two symmetries are conjugate if and only if they are in the same class. For the square, the conjugacy classes are the five I listed earlier.

    This conjugacy thing is important for telling when two symmetries are group-theoretically “the same”, and have the same group-theoretic properties. For example, the fact that the horizontal and vertical flips move all four vertices, while the diagonal flips do not. Another example is that a horizontal flip is self-inverse (if you do it again, it cancels itself out), but a 90° rotation is not (you have to do it four times before it cancels out.) But the horizontal flip shares all its properties with the vertical flip, because it is the same if you just turn your head.

    Identifying this sameness makes certain kinds of arguments much simpler. For example, in counting squares, I wanted to count the number of ways of coloring the faces of a cube, and instead of dealing with the 24 symmetries of the cube, I only needed to deal with their 5 conjugacy classes.

    The example I gave in my math.se answer was maybe less perspicuous. I considered the symmetries of a sphere, and talked about how two rotations of the sphere by 17° are conjugate, regardless of what axis one rotates around. I thought of the square at the end, and threw it in, but I wish I had started with it.

  • How to convert a decimal to a fraction easily? was the month's big winner. OP wanted to know how to take a decimal like and discover that it can be written as . The right answer to this is of course to use continued fraction theory, but I did not want to write a long treatise on continued fractions, so I stripped down the theory to obtain an algorithm that is slower, but much easier to understand.

    The algorithm is just binary search, but with a twist. If you are looking for a fraction for , and you know , then you construct the mediant and compare it with . This gives you a smaller interval in which to search for , and the reason you use the mediant instead of using as usual is that if you use the mediant you are guaranteed to exactly nail all the best rational approximations of . This is the algorithm I described a few years ago in your age as a fraction, again; there the binary search proceeds down the branches of the Stern-Brocot tree to find a fraction close to .


I did ask a question this month: I was looking for a simpler version of the dogbone space construction. The dogbone space is a very peculiar counterexample of general topology, originally constructed by R.H. Bing. I mentioned it here in 2007, and said, at the time:

[The paper] is on my desk, but I have not read this yet, and I may never.

I did try to read it, but I did not try very hard, and I did not understand it. So my question this month was if there was a simpler example of the same type. I did not receive an answer, just a followup comment that no, there is no such example.

by Mark Dominus (mjd@plover.com) at December 18, 2015 09:50 PM