Planet Haskell without Tom Moertel's postsPipes Output
http://pipes.yahoo.com/pipes/pipe.info?_id=Jti_id1G3hGa1KrxdPQQIA
Sat, 25 Oct 2014 09:29:20 +0000http://pipes.yahoo.com/pipes/GHC Weekly News - 2014/10/24
http://ghc.haskell.org/trac/ghc/blog/weekly20141024
thoughtpolicehttp://ghc.haskell.org/trac/ghc/blog/weekly20141024Fri, 24 Oct 2014 23:43:39 +0000Update on Old Projects
http://jozefg.bitbucket.org/posts/2014-10-24-github.html
http://jozefg.bitbucket.org/posts/2014-10-24-github.htmlFri, 24 Oct 2014 00:00:00 +0000Postdoc Position in Functional and Constraint Programming
http://tomschrijvers.blogspot.com/2014/10/postdoc-position-in-functional-and.html
Postdoctoral position in Functional and Constraint Programming at KU LeuvenThe Declarative Languages and Artificial Intelligence (DTAI) group of KU Leuven (Belgium) invites applicants for a postdoctoral position in the area of functional and constraint programming. The position revolves around domain-specific languages (DSLs) embedded in Haskell for constraint programming. It is part of the EU project GRACeFUL whose overarching theme is tools for collective decision making. The KU Leuven part of the project is under the direction of prof. Tom Schrijvers.To apply you must hold a recent PhD (or be about to graduate) related to either functional or constraint programming. Experience in both areas is an advantage.You will work closely with prof. Schrijvers and his PhD students at KU Leuven, as well as with the GRACeFUL project partners across Europe.The position is for 3 years. The salary is competitive and the starting date negotiable (but no later than February 1). Moreover, KU Leuven's policy of equal opportunities and diversity applies to this position.Application procedure: http://people.cs.kuleuven.be/~tom.schrijvers/postdocposition2.htmlTom Schrijverstag:blogger.com,1999:blog-5844006452378085451.post-7283376461621649602Tue, 21 Oct 2014 08:08:00 +0000Upcoming talk
http://winterkoninkje.dreamwidth.org/99975.html
http://winterkoninkje.dreamwidth.org/99975.htmlTue, 21 Oct 2014 02:39:32 +0000GHC Weekly News - 2014/10/20
http://ghc.haskell.org/trac/ghc/blog/weekly20141020
thoughtpolicehttp://ghc.haskell.org/trac/ghc/blog/weekly20141020Mon, 20 Oct 2014 14:14:23 +0000Dijkstra quotes from EWD1284
http://therning.org/magnus/posts/2014-10-20-000-dijkstra-ewd1284.html
http://therning.org/magnus/posts/2014-10-20-000-dijkstra-ewd1284.htmlMon, 20 Oct 2014 00:00:00 +0000New Stackage features
https://www.fpcomplete.com/blog/2014/10/new-stackage-features
We have two new updates to Stackage: providing cabal.config files
and including Haddock documentation.Haddock documentation on snapshotsNow all new exclusive snapshots will have haddock links, which you can
access via the following steps:Go to the stackage.org home page.Choose an exclusive snapshot, e.g. GHC 7.8, 2014-10-20.On the snapshot page will be a link in the menu entitled Haddocks.That link will be to an index page
like this
from which you can view documentation of all packages included in the
snapshot. This means you can generally view everything in one place,
on one high availability service.Using Stackage without changing your repoThe recommended way to use Stackage is to simply change your
remote-repo field in your .cabal/config file and run cabal
update. Henceforth your dependencies will be resolved from Stackage,
which is backed by high availability Amazon S3 storage servers, and
you will have successful build plans, compilation and passing
tests. Hurrah!Try Haskell and the
upcoming Haskell.org homepage
were both developed with Stackage. This meant I could just specify the
Stackage snapshot to use in the README and then the next time I want
to upgrade I can just update the snapshot version to get a fresh
working build plan.The issue some people are facing is that they cannot change this
remote-repo field, either because they're using a cabal sandbox,
which doesn't support this yet, or because they just don't want to.The solution to this, in my experience, has been for me to manually go
and run cabal freeze in a project I've already built to get the
cabal.config file and then give these people that file.Now, it's automated via a cabal.config link on snapshot pages:For new developers working on an application who want to use Stackage,
they can do something like this:$ cabal sandbox init
$ curl http://www.stackage.org/ /cabal.config > cabal.config
$ cabal install --only-depWhich will install their dependencies from Hackage. We can't guarantee
this will always work -- as Stackage snapshots sometimes will have a
manual patch in the package to make it properly build with other
packages, but otherwise it's as good as using Stackage as a repo.A cabal freeze output in cabal.config will contain base and similar
packages which are tied to the minor GHC version (e.g. GHC 7.8.2 vs
GHC 7.8.3 have different base numbers), so if you get a cabal.config
and you get a dependencies error about base, you probably need to
open up the cabal.config and remove the line with the base
constraint. Stackage snapshots as used as repos do not have this
constraint (it will use whichever base your GHC major version uses).Another difference is that cabal.config is more like an
“inclusive” Stackage snapshot
-- it includes packages not known to build together, unlike
“exclusive” snapshots which only contain packages known to build and
pass tests together. Ideally every package you need to use (directly
or indirectly) will come from an exclusive snapshot. If not, it's
recommended that you
submit the package name to Stackage,
and otherwise inclusive snapshots or cabal.config are the fallbacks
you have at your disposal.https://www.fpcomplete.com/blog/2014/10/new-stackage-featuresMon, 20 Oct 2014 00:00:00 +0000HLint now spots bad unsafePerformIO
http://neilmitchell.blogspot.com/2014/10/hlint-now-spots-bad-unsafeperformio.html
Neil Mitchelltag:blogger.com,1999:blog-7094652.post-646623140309959667Sun, 19 Oct 2014 21:23:00 +0000Anonymity in public life
http://wellquite.org/blog/anonymity_in_public_life.html
http://wellquite.org/blog/anonymity_in_public_lifeSun, 19 Oct 2014 15:00:00 +0000Quasi-quoting DSLs for free
http://www.well-typed.com/blog/100
Suppose you are writing a compiler for some programming language or DSL. If you are doing source to source transformations in your compiler, perhaps as part of an optimization pass, you will need to construct and deconstruct bits of abstract syntax. It would be very convenient if we could write that abstract syntax using the syntax of your language. In this blog post we show how you can reuse your existing compiler infrastructure to make this possible by writing a quasi-quoter with support for metavariables. As we will see, a key insight is that we can reuse object variables as meta variables.
Toy Language “Imp”
For the sake of this blog post we will be working with a toy language called Imp. The abstract syntax for Imp is defined by
type VarName = String
data Expr =
Var VarName
| Add Expr Expr
| Sub Expr Expr
| Int Integer
| Read
deriving (Data, Typeable, Show, Eq)
data Cmd =
Write Expr
| Assign VarName Expr
| Decl VarName
deriving (Data, Typeable, Show)
data Prog = Prog [Cmd]
deriving (Data, Typeable, Show)
and we will assume that we have some parsec parsers
parseExpr :: Parser Expr
parseProg :: Parser Prog
We will also make use of
topLevel :: Parser a -> Parser a
topLevel p = whiteSpace *> p <* eof
and the following useful combinator for running a parser:
parseIO :: Parser a -> String -> IO a
The details of these parsers are beyond the scope of this post. There are plenty of parsec tutorials online; for instance, you could start with the parsec chapter in Real World Haskell. Moreover, the full code for this blog post, including a simple interpreter for the language, is available on github if you want to play with it. Here is a simple example of an Imp program:
var x ;
x := read ;
write (x + x + 1)
A simple quasi-quoter
We want to be able to write something like
prog1 :: Prog
prog1 = [prog|
var x ;
x := read ;
write (x + x + 1)
|]
where the intention is that the [prog| ... |] quasi-quote will expand to something like
prog1 = Prog [
Decl "x"
, Assign "x" Read
, Write (Add (Add (Var "x") (Var "x")) (Int 1))
]
To achieve this, we have to write a quasi-quoter. A quasi-quoter is an instance of the following data type:
data QuasiQuoter = QuasiQuoter {
quoteExp :: String -> Q Exp
, quotePat :: String -> Q Pat
, quoteType :: String -> Q Type
, quoteDec :: String -> Q [Dec]
}
The different fields are used when using the quasi-quoter in different places in your Haskell program: at a position where we expect a (Haskell) expression, a pattern (we will see an example of that later), a type or a declaration; we will not consider the latter two at all in this blog post.
In order to make the above example (prog1) work, we need to implement quoteExp but we can leave the other fields undefined:
prog :: QuasiQuoter
prog = QuasiQuoter {
quoteExp = \str -> do
l <- location'
c <- runIO $ parseIO (setPosition l *> topLevel parseProg) str
dataToExpQ (const Nothing) c
, quotePat = undefined
, quoteType = undefined
, quoteDec = undefined
}
Let’s see what’s going on here. The quasi-quoter gets as argument the string in the quasi-quote brackets, and must return a Haskell expression in the Template-Haskell Q monad. This monad supports, amongst other things, getting the current location in the Haskell file. It also supports IO.
Location
The first thing that we do is find the current location in the Haskell source file and convert it to parsec format:
location' :: Q SourcePos
location' = aux <$> location
where
aux :: Loc -> SourcePos
aux loc = uncurry (newPos (loc_filename loc)) (loc_start loc)
Running the parser
Once we have the location we then parse the input string to a term in our abstract syntax (something of type Prog). We use parsec’s setPosition to tell parsec where we are in the Haskell source file, so that if we make a mistake such as
prog1 :: Prog
prog1 = [prog|
var x ;
x := read ;
write (x + x + )
|]
we get an error that points to the correct location in our Haskell file:
TestQQAST.hs:6:9:
Exception when trying to run compile-time code:
user error ("TestQQAST.hs" (line 9, column 20):
unexpected ")"
expecting "(", "read", identifier or integer)
Converting to Haskell abstract syntax
The parser returns something of type Prog, but we want something of type Exp; Exp is defined in Template Haskell and reifies the abstract syntax of Haskell. For example, we would have to translate the Imp abstract syntax term
Var "x" :: Prog
to its reflection as a piece of abstract Haskell syntax as
AppE (ConE 'Var) (LitE (StringL "x")) :: TH.Exp
which, when spliced into the Haskell source, yields the original Prog value. Fortunately, we don’t have to write this translation by hand, but we can make use of the following Template Haskell function:
dataToExpQ :: Data a
=> (forall b. Data b => b -> Maybe (Q Exp))
-> a -> Q Exp
This function can translate any term to a reified Haskell expression, as long as the type of the term derives Data (Data instances can be auto-derived by ghc if you enable the DeriveDataTypeable language extension). The first argument allows you to override the behaviour of the function for specific cases; we will see an example use case in the next section. In our quasi-quoter so far we don’t want to override anything, so we pass a function that always returns Nothing.
Once we have defined this quasi-quoter we can write
prog1 :: Prog
prog1 = [prog|
var x ;
x := read ;
write (x + x + 1)
|]
and ghc will run our quasi-quoter and splice in the Haskell expresion corresponding to the abstract syntax tree of this program (provided that we enable the QuasiQuotes language extension).
Meta-variables
Consider this function:
prog2 :: VarName -> Integer -> Prog
prog2 y n = [prog|
var x ;
x := read ;
write (x + y + n)
|]
As mentioned, in the source code for this blog post we also have an interpreter for the language. What happens if we try to run (prog2 "x" 1)?
*Main> intIO $ intProg (prog2 "x" 2)
5
*** Exception: user error (Unbound variable "y")
Indeed, when we look at the syntax tree that got spliced in for prog2 we see
Prog [ Decl "x"
, Assign "x" Read
, Write (Add (Add (Var "x") (Var "y")) (Var "n"))
]
What happened? Didn’t we pass in "x" as the argument y? Actually, on second thought, this makes perfect sense: this is after all what our string parses to. The fact that y and n also happen to Haskell variables, and happen to be in scope at the point of the quasi-quote, is really irrelevant. But we would still like prog2 to do what we expected it to do.
Meta-variables in Template Haskell
To do that, we have to support meta variables: variables from the “meta” language (Haskell) instead of the object language (Imp). Template Haskell supports this out of the box. For example, we can define
ex :: Lift a => a -> Q Exp
ex x = [| id x |]
Given any argument that supports Lift, ex constructs a piece of abstract Haskell syntax which corresponds to the application of the identity function to x. (Don’t confuse this with anti-quotation; see Brief Intro to Quasi-Quotation.) Lift is a type class with a single method
class Lift t where
lift :: t -> Q Exp
For example, here is the instance for Integer:
instance Lift Integer where
lift x = return (LitE (IntegerL x))
Meta-variables in quasi-quotes
Quasi-quotes don’t have automatic support for meta-variables. This makes sense: Template Haskell is for quoting Haskell so it has a specific concrete syntax to work with, where as quasi-quotes are for arbitrary custom syntaxes and so we have to decide what the syntax and behaviour of meta-variables is going to be.
For Imp we want to translate any unbound Imp (object-level) variable in the quasi-quote to a reference to a Haskell (meta-level) variable. To do that, we will introduce a similar type class to Lift:
class ToExpr a where
toExpr :: a -> Expr
and provide instances for variables and integers:
instance ToExpr VarName where
toExpr = Var
instance ToExpr Integer where
toExpr = Int
We will also need to know which variables in an Imp program are bound and unbound; in the source code you will find a function which returns the set of free variables in an Imp program:
fvProg :: Prog -> Set VarName
Overriding the behaviour of dataToExpQ
In the previous section we mentioned that rather than doing the Prog -> Q Exp transformation by hand we use the generic function dataToExpQ to do it for us. However, now we want to override the behaviour of this function for the specific case of unbound Imp variables, which we want to translate to Haskell variables.
Recall that dataToExpQ has type
dataToExpQ :: Data a
=> (forall b. Data b => b -> Maybe (Q Exp))
-> a -> Q Exp
This is a rank-2 type: the first argument to dataToExpQ must itself be polymorphic in b: it must work on any type b that derives Data. So far we have been passing in
const Nothing
which is obviously polymorphic in b since it completely ignores its argument. But how do we do something more interesting? Data and its associated combinators come from a generic programming library called Scrap Your Boilerplate (Data.Generics). A full discussion of of SYB is beyond the scope of this blog post; the SYB papers are a good starting point if you would like to know more (I would recommend reading them in chronological order, the first published paper first). For the sake of what we are trying to do it suffices to know about the existence of the following combinator:
extQ :: (Typeable a, Typeable b) => (a -> q) -> (b -> q) -> a -> q
Given a polymorphic query (forall a)—in our case this is const Nothing—extQ allows to extend the query with a type specific case (for a specific type b). We will use this to give a specific case for Expr: when we see a free variable in an expression we translate it to an application of toExpr to a Haskell variable with the same name:
metaExp :: Set VarName -> Expr -> Maybe ExpQ
metaExp fvs (Var x) | x `Set.member` fvs =
Just [| toExpr $(varE (mkName x)) |]
metaExp _ _ =
Nothing
The improved quasi-quoter
With this in hand we can define our improved quasi-quoter:
prog :: QuasiQuoter
prog = QuasiQuoter {
quoteExp = \str -> do
l <- location'
c <- runIO $ parseIO (setPosition l *> topLevel parseProg) str
dataToExpQ (const Nothing `extQ` metaExp (fvProg c)) c
, quotePat = undefined
, quoteType = undefined
, quoteDec = undefined
}
Note that we are extending the query for Expr, not for Prog; dataToExpQ (or, more accurately, SYB) makes sure that this extension is applied at all the right places. Running (prog2 "x" 2) now has the expected behaviour:
*Main> intIO $ intProg (prog2 "x" 2)
6
14
Indeed, when we have a variable in our code that is unbound both in Imp and in Haskell, we now get a Haskell type error:
prog2 :: VarName -> Integer -> Prog
prog2 y n = [prog|
var x ;
x := read ;
write (x + z + n)
|]
gives
TestQQAST.hs:15:19: Not in scope: ‘z’
Parenthetical remark: it is a design decision whether or not we want to allow local binding sites in a splice to “capture” meta-variables. Put another way, when we pass in "x" to prog2, do we mean the x that is bound locally in prog2, or do we mean a different x? Certainly a case can be made that we should not be able to refer to the locally bound x at all—after all, it’s not bound outside of the snippet! This is an orthogonal concern however and we will not discuss it any further in this blog post.
Quasi-quoting patterns
We can also use quasi-quoting to support patterns. This enables us to write something like
optimize :: Expr -> Expr
optimize [expr| a + n - m |] | n == m = optimize a
optimize other = other
As before, the occurrence of a in this pattern is free, and we intend it to correspond to a Haskell variable, not an Imp variable; the above code should correspond to
optimize (Sub (Add a n) m) | n == m = optimize a
(note that this is comparing Exprs for equality, hence the need for Expr to derive Eq). We did not mean the pattern
optimize (Sub (Add (Var "a") (Var "n")) (Var "m"))
To achieve this, we can define a quasi-quoter for Expr that supports patterns (as well as expressions):
expr :: QuasiQuoter
expr = QuasiQuoter {
quoteExp = \str -> do
l <- location'
e <- runIO $ parseIO (setPosition l *> topLevel parseExpr) str
dataToExpQ (const Nothing `extQ` metaExp (fvExpr e)) e
, quotePat = \str -> do
l <- location'
e <- runIO $ parseIO (setPosition l *> topLevel parseExpr) str
dataToPatQ (const Nothing `extQ` metaPat (fvExpr e)) e
, quoteType = undefined
, quoteDec = undefined
}
The implementation of quotePat is very similar to the definition of quoteExp. The only difference is that we use dataToPatQ instead of dataToExpQ to generate a Haskell pattern rather than a Haskell expression, and we use metaPat to give a type specific case which translates free Imp variables to Haskell pattern variables:
metaPat :: Set VarName -> Expr -> Maybe PatQ
metaPat fvs (Var x) | x `Set.member` fvs = Just (varP (mkName x))
metaPat _ _ = Nothing
Note that there is no need to lift now; the Haskell variable will be bound to whatever matches in the expression.
Limitations
We might be tempted to also add support for Prog patterns. While that is certainly possible, it’s of limited use if we follow the same strategy that we followed for expressions. For instance, we would not be able to write something like
opt [prog| var x ; c |] | x `Set.notMember` fvProg c = opt c
The intention here is that we can remove unused variables. Unfortunately, this will not work because this will cause a parse error: the syntax for Imp does not allow for variables for commands, and hence we also don’t allow for meta-variables at this point. This is important to remember:
By using object-level variables as stand-ins for meta-level variables, we only allow for meta-level variables where the syntax for the object-level language allows variables.
If this is too restrictive, we need to add special support in the ADT and in the corresponding parsers for meta-variables. This is a trade-off in increased expressiveness of the quasi-quotes against additional complexity in their implementation (new parsers, new ADTs).
Conclusions
By reusing object-level variables as stand-ins for meta variables you can reuse existing parsers and ADTs to define quasi-quoters. Using the approach described in this blog we were able to add support for quasi-quoting to a real compiler for a domain specific programming language with a minimum of effort. The implementation is very similar to what we have shown above, except that we also dealt with renaming (so that meta variables cannot be captured by binding sites in the quasi quotes) and type checking (reusing the existing renamer and type checker, of course).edskohttp://www.well-typed.com/blog/100Sun, 19 Oct 2014 14:01:29 +0000Haskell : A neat trick for GHCi
http://www.mega-nerd.com/erikd/Blog/CodeHacking/Haskell/ghci-trick.html
Just found a really nice little hack that makes working in the GHC interactive
REPL
a little easier and more convenient.
First of all, I added the following line to my ~/.ghci file.
:set -DGHC_INTERACTIVE
All that line does is define a GHC_INTERACTIVE pre-processor
symbol.
Then in a file that I want to load into the REPL, I need to add this to the top
of the file:
{-# LANGUAGE CPP #-}
and then in the file I can do things like:
#ifdef GHC_INTERACTIVE
import Data.Aeson.Encode.Pretty
prettyPrint :: Value -> IO ()
prettyPrint = LBS.putStrLn . encodePretty
#endif
In this particular case, I'm working with some relatively large chunks of JSON
and its useful to be able to pretty print them when I'm the REPL, but I have
no need for that function when I compile that module into my project.http://www.mega-nerd.com/erikd/Blog/2014/10/18/ghci-trick.atomFri, 17 Oct 2014 22:16:00 +0000Fixing Haddock docs on Hackage
http://neilmitchell.blogspot.com/2014/10/fixing-haddock-docs-on-hackage.html
Neil Mitchelltag:blogger.com,1999:blog-7094652.post-2841034042035152747Fri, 17 Oct 2014 20:49:00 +0000Notes on Quotients Types
http://jozefg.bitbucket.org/posts/2014-10-17-quotients.html
http://jozefg.bitbucket.org/posts/2014-10-17-quotients.htmlFri, 17 Oct 2014 00:00:00 +0000Generalizing function composition
http://jaspervdj.be/posts/2014-10-17-generalizing-function-composition.html
http://jaspervdj.be/posts/2014-10-17-generalizing-function-composition.htmlFri, 17 Oct 2014 00:00:00 +0000September 2014 1HaskellADay problems and solutions
http://logicaltypes.blogspot.com/2014/10/september-2014-1haskelladay-problems.html
September, 2014September 1st, 2014: They tried to kill the Metal...I don't know where I'm going with that. But rock-n-roll with today's #haskell exercise http://lpaste.net/110331September 2nd, 2014: Good morning! Triangle Sums is our #haskell problem for today: http://lpaste.net/110404 No triangles were harmed in the solution of their sum (nor in the summation of their solution) http://lpaste.net/110432September 3rd, 2014: Pay It Forward. What? You didn't think I'd just say: today's #haskell problem is hard and leave it at that, did you? http://lpaste.net/110444 Paid. Or: a constructivist approach reduces the generated sets from 200M+ down to 8 possible solutions http://lpaste.net/110684 That's doable. ... and here is the 'Mr. Clean' version of the solution: fast, and neat. Groovy! http://lpaste.net/110685September 4th, 2014: Today's #haskell problem: Abacus words http://lpaste.net/110494 because MRFE says "I don't like your math problems; I want more word problems"September 5th, 2014: These 'edgy' relationships these days! Remember when today's #haskell problem didn't involve graph theory? http://lpaste.net/110543 Data.Graph FTW! http://lpaste.net/110571 A solution to today's 4sum #haskell problem, and it didn't require generating 1625702400 solutions!September 8th, 2014: We have puzzles 1 and 5 from the "Montley Stew" problem set for today's #haskell problem http://lpaste.net/110699 The solution-style to Montley Stew isswimming in list-compression stew http://lpaste.net/110750September 9th, 2014: King Tut! http://lpaste.net/110789 Our #haskell problem for today is NOT a Pyramid Scheme. Maybe.September 10th, 2014: 'Sed' is 'but(t)' just another word ... in "'laddin" http://lpaste.net/110833 Today's #haskell problem is mix-n-match words. "But(t) I sed ..." ARG! Enough with the 3rd-grade humor! On with the solution to the mix-n-match words! http://lpaste.net/110859September 11th, 2014: A-plus for you when you solve today's #haskell exercise http://lpaste.net/110862 But an F- (NOT an F# ... geddit?) for /usr/share/dict/words :/ A solution to today's injectInto #haskell problem http://lpaste.net/110891September 12th, 2014: Today's #Haskell problem comes from She. She who commands you solve it before coding it. http://lpaste.net/110925 So, you know: there it is. Okay, 'thurt' is a word in WHICH Universe? A solution to today's #haskell 'ditto' problem http://lpaste.net/110955September 15th, 2014: "The name of the game is Connect Four!" and today's #haskell problem http://lpaste.net/111065 as suggested by a tweet from @DrEugeniaCheng. I played Connect 4 against myself and lost! :/ A semi-solution to today's #haskell problem at http://lpaste.net/111105September 16th, 2014: There's more than one way to slice and dice a matrix for today's #haskell problem http://lpaste.net/111109 (follow-up to yesterday's Connect4) A Hack-n-slash solution to today's diagonal view of matrices. http://lpaste.net/111130 Thebonus solution is provided back at the Connect Four answer to make that game complete: http://lpaste.net/111105September 17th, 2014: Do you Yahoo!? Today's #haskell problem: connecting to Yahoo!'s financial webservice http://lpaste.net/111071 I like my java GREEN! http://lpaste.net/111238 (java means 'coffee') A solution to stock webservice #haskell problem.September 18th, 2014: Star (Tuna?) Fish? http://lpaste.net/111216 A radial word-finding/matching game is today's #haskell puzzle. Wait. Quantum...WHAT? http://lpaste.net/111259 A solution to today's #haskell problem using quantum superpositions to solve it. I'm not joking. STAR POWER! http://lpaste.net/edit/111259 A solution for pretty-printing the star-puzzleSeptember 19th, 2014: Continued fractions and dual inversionals are today's #haskell problem http://lpaste.net/111067 It even comes with (thoughts about) flowers. #Ult Today's problem was inspired by a comment, then the main article, from @aperiodicalhttp://aperiodical.com/2013/11/from-the-mailbag-dual-inversal-numbers/#comment-611141 That was some LOOOOOOOONG Division! http://lpaste.net/111314 A solution to today's #haskell problem.September 22nd, 2014: Oh, noes! The 'M'-word! http://lpaste.net/111419 for today's #haskell exercise. Project Euler, problem 11: 'M' is for 'Monoid' http://lpaste.net/111435 A solution to today's #haskell problem.September 23rd, 2014: "Oh, the snark bites, with his teeth, dear." MACD Knife ... geddit? http://lpaste.net/111468 Today's #haskell problem is a technical indicator.September 24th, 2014: Jones, Smith, and Brown work at the Bank... but not Mr. Banks.A logic puzzle from 1957 for today's #haskell puzzle http://lpaste.net/111461. A pair of PhDs (http://lpaste.net/111580) helped to solve today's #haskell problem. Neatly, too, I might add.September 25th, 2014: Corned-beef hashi? http://lpaste.net/111452 No, that's not right, and now I'm hungry! :( Shoot! Well, anyway: today's #haskell problem.September 26th, 2014: HA! I TOLD you we'd be getting to cipher-text! http://lpaste.net/111459 From the 1700's, still: it IS cipher text for today's #haskell problem. Ooh! The Plot Thickens (like pea soup)! http://lpaste.net/111679 "ALLMENHAVING" and "be mis T r U st ed " is a solution to today's problem.September 29th, 2014: Big (Crypto) Generator! http://lpaste.net/111795 Today's #haskell problem is a follow-on to Friday's. Human Error ... WHAT human error?http://lpaste.net/111829 A solution to today's make-your-own-cypto-table #haskell problemSeptember 30th, 2014: "I wanna be a blue-collar man!" Yes, but who, and which occupation? http://lpaste.net/111755 Today's #haskell problem addresses this. Plumber, ... or painter? IDK! http://lpaste.net/111876 TWO-solutions to today's #haskell problem (one of them MAY be correct... :/ )geophftag:blogger.com,1999:blog-4650294074444534066.post-8541269128157744067Wed, 01 Oct 2014 10:44:00 +0000Switching to sytemd-networkd
http://www.joachim-breitner.de/blog/664-Switching_to_sytemd-networkd
Joachim Breitnerhttp://www.joachim-breitner.de/blog/664-Switching_to_sytemd-networkdTue, 14 Oct 2014 20:26:13 +0000Switching to systemd-networkd
http://www.joachim-breitner.de/blog/664-Switching_to_systemd-networkd
Joachim Breitnerhttp://www.joachim-breitner.de/blog/664-Switching_to_systemd-networkdTue, 14 Oct 2014 20:26:13 +0000Shake's Internal State
http://neilmitchell.blogspot.com/2014/10/shakes-internal-state.html
Neil Mitchelltag:blogger.com,1999:blog-7094652.post-3073759877938928012Mon, 13 Oct 2014 20:53:00 +0000Game idea: “Be Consistent”
http://kpreid.livejournal.com/51492.html
Kevin Reid (kpreid)http://kpreid.livejournal.com/51492.htmlMon, 13 Oct 2014 17:46:51 +0000Mathematics of Program Construction (MPC 2015): first call for papers
http://tomschrijvers.blogspot.com/2014/10/mathematics-of-program-construction-mpc.html
FIRST CALL FOR PAPERS12th International Conference on Mathematics of Program Construction, MPC 2015Königswinter, Germany, 29 June - 1 July 2015http://www.cs.ox.ac.uk/conferences/MPC2015/BACKGROUNDThe MPC conferences aim to promote the development of mathematical principlesand techniques that are demonstrably practical and effective in the processof constructing computer programs, broadly interpreted.The 2015 MPC conference will be held in Königswinter, Germany, from 29th Juneto 1st July 2015. The previous conferences were held in Twente, TheNetherlands (1989), Oxford, UK (1992), Kloster Irsee, Germany (1995),Marstrand, Sweden (1998), Ponte de Lima, Portugal (2000), Dagstuhl, Germany(2002), Stirling, UK (2004, colocated with AMAST), Kuressaare, Estonia (2006,colocated with AMAST), Marseille, France (2008), Québec City, Canada (2010,colocated with AMAST), and Madrid, Spain (2012).TOPICSPapers are solicited on mathematical methods and tools put to use in programconstruction. Topics of interest range from algorithmics to support forprogram construction in programming languages and systems. The notion of"program" is broad, from algorithms to hardware. Some typical areas are typesystems, program analysis and transformation, programming-language semantics,security, and program logics. Theoretical contributions are welcome, providedthat their relevance to program construction is clear. Reports onapplications are welcome, provided that their mathematical basis is evident.We also encourage the submission of "pearls": elegant, instructive, and funessays on the mathematics of program construction.IMPORTANT DATES * Submission of abstracts: 26 January 2015 * Submission of full papers: 2 February 2015 * Notification to authors: 16 March 2015 * Final version: 13 April 2015SUBMISSIONSubmission is in two stages. Abstracts (plain text, 10 to 20 lines) must besubmitted by 26 January 2015. Full papers (pdf) adhering to the LaTeX llncsstyle must be submitted by 2 February 2015. There is no official page limit,but authors should strive for brevity. The web-based system EasyChair will beused for submission (https://easychair.org/conferences/?conf=mpc2015).Papers must report previously unpublished work, and must not be submittedconcurrently to a journal or to another conference with refereed proceedings.Accepted papers must be presented at the conference by one of the authors.Please feel free to write to mpc2015@easychair.org with any questions aboutacademic matters.The proceedings of MPC 2015 will be published in Springer-Verlag's LectureNotes in Computer Science series, as have all the previous editions. Authorsof accepted papers will be expected to transfer copyright to Springer forthis purpose. After the conference, authors of the best papers will beinvited to submit revised versions to a special issue of the Elsevier journalScience of Computer Programming.PROGRAMME COMMITTEERalf Hinze University of Oxford, UK (chair)Eerke Boiten University of Kent, UKJules Desharnais Université Laval, CanadaLindsay Groves Victoria University of Wellington, New ZealandZhenjiang Hu National Institute of Informatics, JapanGraham Hutton University of Nottingham, UKJohan Jeuring Utrecht University and Open University, The NetherlandsJay McCarthy Vassar College, USBernhard Möller Universität Augsburg, GermanyShin-Cheng Mu Academia Sinica, TaiwanDave Naumann Stevens Institute of Technology, USPablo Nogueira Universidad Politécnica de Madrid, SpainUlf Norell University of Gothenburg, SwedenBruno C. d. S. Oliveira The University of Hong Kong, Hong KongJosé Nuno Oliveira Universidade do Minho, PortugalAlberto Pardo Universidad de la República, UruguayChristine Paulin-Mohring INRIA-Université Paris-Sud, FranceTom Schrijvers KU Leuven, BelgiumEmil Sekerinski McMaster University, CanadaTim Sheard Portland State University, USAnya Tafliovich University of Toronto Scarborough, CanadaTarmo Uustalu Institute of Cybernetics, EstoniaJanis Voigtländer Universität Bonn, GermanyVENUEThe conference will take place in Königswinter, Maritim Hotel, whereaccommodation has been reserved. Königswinter is situated on the right bankof the river Rhine, opposite Germany's former capital Bonn, at the foot ofthe Siebengebirge.LOCAL ORGANIZERSRalf Hinze University of Oxford, UK (co-chair)Janis Voigtländer Universität Bonn, Germany (co-chair)José Pedro Magalhães University of Oxford, UKNicolas Wu University of Oxford, UKFor queries about local matters, please write to jv@informatik.uni-bonn.de.Tom Schrijverstag:blogger.com,1999:blog-5844006452378085451.post-7695865876999092168Mon, 13 Oct 2014 08:30:00 +0000Optparse-applicative and custom argument parsers
http://therning.org/magnus/posts/2014-10-13-000-optparse-applicative.html
http://therning.org/magnus/posts/2014-10-13-000-optparse-applicative.htmlMon, 13 Oct 2014 00:00:00 +0000Non-diffusive atmospheric flow #7: PCA for spatio-temporal data
http://www.skybluetrades.net/blog/posts/2014/10/12/data-analysis-ao1-7/index.html
http://www.skybluetrades.net/blog/posts/2014/10/12/data-analysis-ao1-7/index.htmlSun, 12 Oct 2014 18:46:21 +0000Using GHC HEAD
https://leepike.wordpress.com/2014/10/10/using-ghc-head/
I wanted to try out a recent feature in GHC this week, so I was using HEAD. When I say using, I mean it: I wasn’t developing with it, but using it to build Ivory, our safe C EDSL, as well as some libraries written in Ivory. I want to point out a few dragons that lay ahead for others using HEAD (7.9.xxx) today.
The Functor, Applicative, Monad hierarchy (as well as the Alternative and MonadPlus hierarchy) is no longer a warning but an error. You’ll be adding a lot of instances to library code.
You’ll need to update Cabal, which comes as a submodule with the GHC sources. Unfortunately, building Cabal was a pain because of the bootstrapping problem. The bootstrap.sh script in cabal-install is broken (e.g., outdated dependency versions). Getting it to work involved using runhaskell directly, modifying a bunch of Cabal’s dependencies, and getting a little help from Iavor Diatchki.
Some of the datatypes in Template Haskell have changed; notably, the datatypes for creating class constraints have been folded into the datatype for constructing types (constraint kinds!). Many libraries that depend on Template Haskell breaks as a result.
I won’t mention the issues with package dependency upper bounds. Oops, I just did.
Fortunately, once Cabal is updated, Cabal sandboxes work just fine. I wrote a simple shell script to swap out my sandboxes to switch between GHC versions. (It would be a nice feature if Cabal recognized you are using a different version of GHC than the one the cabal sandbox was originally made and created a new sandbox automatically.)
Because I’m on OSX and use Homebrew, I tried using it to manage my GHC versions, including those installed with Brew and those built and installed manually. It works great. When building GHC, configure it to install into your Cellar, or wherever you have Brew install packages. So I ran
> ./configure --prefix=/usr/local/Cellar/ghc/7.9
which makes Brew aware of the new version of GHC, despite being manually installed. After it’s installed,
> brew switch ghc 7.9
takes care of updating all your symbolic links. No more making “my-ghc-7.9″ symbolic links or writing custom shell scripts.Lee Pikehttp://leepike.wordpress.com/?p=717Sat, 11 Oct 2014 04:23:44 +0000Functional Software Engineer at Cake Solutions Ltd (Full-time)
http://functionaljobs.com/jobs/8755-functional-software-engineer-at-cake-solutions-ltd
urn:uuid:e769b50c-6ff9-b861-7ca9-4d946c7ef8b4Fri, 10 Oct 2014 12:02:55 +0000ICFP 2015: Call for Workshop and Co-Located Event Proposals
http://tomschrijvers.blogspot.com/2014/10/icfp-2015-call-for-workshop-and-co.html
CALL FOR WORKSHOP AND CO-LOCATED EVENT PROPOSALS ICFP 2015 20th ACM SIGPLAN International Conference on Functional Programming August 30 – September 5, 2015 Vancouver, Canada http://icfpconference.org/icfp2015/The 120th ACM SIGPLAN International Conference on FunctionalProgramming will be held in Vancouver, British Columbia, Canada onAugust 30-September 5, 2015. ICFP provides a forum for researchersand developers to hear about the latest work on the design,implementations, principles, and uses of functional programming.Proposals are invited for workshops (and other co-located events, suchas tutorials) to be affiliated with ICFP 2015 and sponsored bySIGPLAN. These events should be less formal and more focused than ICFPitself, include sessions that enable interaction among the attendees,and foster the exchange of new ideas. The preference is for one-dayevents, but other schedules can also be considered.The workshops are scheduled to occur on August 30 (the daybefore ICFP) and September 3-5 (the three days after ICFP).----------------------------------------------------------------------Submission details Deadline for submission: November 16, 2014 Notification of acceptance: December 15, 2014Prospective organizers of workshops or other co-located events areinvited to submit a completed workshop proposal form in plain textformat to the ICFP 2015 workshop co-chairs (Tom Schrijvers and NicolasWu), via email to icfp2015-workshops@cs.kuleuven.be by November 16,2014. (For proposals of co-located events other than workshops, pleasefill in the workshop proposal form and just leave blank any sectionsthat do not apply.) Please note that this is a firm deadline.Organizers will be notified if their event proposal is accepted byDecember 15, 2014, and if successful, depending on the event, theywill be asked to produce a final report after the event has takenplace that is suitable for publication in SIGPLAN Notices.The proposal form is available at:http://www.icfpconference.org/icfp2015/icfp15-workshops-form.txtFurther information about SIGPLAN sponsorship is available at:http://acm.org/sigplan/sigplan_workshop_proposal.htm----------------------------------------------------------------------Selection committeeThe proposals will be evaluated by a committee comprising thefollowing members of the ICFP 2015 organising committee, together withthe members of the SIGPLAN executive committee. Workshop Co-Chair: Tom Schrijvers (KU Leuven) Workshop Co-Chair: Nicolas Wu (University of Oxford) General Chair : Kathleen Fisher (Tufts University) Program Chair: John Reppy (University of Chicago)----------------------------------------------------------------------Further informationAny queries should be addressed to the workshop co-chairs (TomSchrijvers and Nicolas Wu), via email toicfp2015-workshops@cs.kuleuven.be.Tom Schrijverstag:blogger.com,1999:blog-5844006452378085451.post-5580734455539596689Fri, 10 Oct 2014 06:58:00 +0000SNAPL
http://wadler.blogspot.com/2014/10/snapl.html
SNAPL will take place 3-6 May 2015 at Asilomar. SNAPL provides a biennial venue to focus on big-picture questions, long-running research programs, and experience reports in programming languages. The ideal SNAPL paper takes one of two forms: A promising idea that would benefit from discussion and feedback.A paper about an ongoing research project that might not be accepted at a traditional conference.Examples include papers that lay out a research roadmapsummarize experiencespresent negative resultsdiscuss design alternativesSNAPL is interested in all aspects of programming languages. The PC is broad and open-minded and receptive to interesting ideas that will provoke thought and discussion. Interesting papers would combine the specific with the general. Submissions are limited to five pages (excluding bibliography), and must be formatted using ACM SIG style. The final papers can be up to 10 pages in length. Accepted papers will be published on an open-access site, probably arXiv CoRR. To encourage authors to submit only their best work, each person can be an author or co-author of a single paper only. SNAPL will prefer experienced presenters and each submission must indicate on the submission site which co-author will present the paper at the conference. SNAPL also accepts one-page abstracts. Abstracts will be reviewed lightly and all submitted abstracts will be published on the SNAPL 2015 web page. Authors of selected abstracts will be invited to give a 5-minute presentation at the gong show at the conference. SNAPL is unaffiliated with any organization. It is a conference for the PL community organized by the PL community. Important DatesSubmission: January 6, 2015 Decisions announced: February 20, 2015 Final versions due: March 20, 2015 Conference: May 3-6, 2015Philip Wadlertag:blogger.com,1999:blog-9757377.post-886958919855274085Thu, 09 Oct 2014 09:39:00 +0000Software Engineer / Developer at Clutch Analytics/ Windhaven Insurance (Full-time)
http://functionaljobs.com/jobs/8753-software-engineer-developer-at-clutch-analytics-windhaven-insurance
urn:uuid:0fab4016-61bd-eddb-710e-b06b29e266b6Wed, 08 Oct 2014 13:26:05 +0000Bake - Continuous Integration System
http://neilmitchell.blogspot.com/2014/10/bake-continuous-integration-system.html
Neil Mitchelltag:blogger.com,1999:blog-7094652.post-6617119528009432249Tue, 07 Oct 2014 21:24:00 +0000Announcing unagi-chan
http://brandon.si/code/announcing-unagi-chan/
Today I released version 0.2 of unagi-chan, a haskell library implementing
fast and scalable FIFO queues with a nice and familiar API. It is
available on hackage
and you can install it with:
$ cabal install unagi-chan
This version provides a bounded queue variant (and closes
issue #1!)
that has performance on par with the other variants in the library. This is
something I’m somewhat proud of, considering that the standard
TBQueue
is not only significantly slower than e.g. TQueue, but also was seen to
livelock at a fairly low level of concurrency (and so is not included in the
benchmark suite).
Here are some example benchmarks. Please do try the new bounded version and see
how it works for you.
What follows are a few random thoughts more or less generally-applicable to the
design of bounded FIFO queues, especially in a high-level garbage-collected
language. These might be obvious, uninteresting, or unintelligible.
What is Bounding For?
I hadn’t really thought much about this before: a bounded queue limits memory
consumption because the queue is restricted from growing beyond some size.
But this isn’t quite right. If for instance we implement a bounded queue by
pre-allocating an array of size bounds then a write operation need not
consume any additional memory; indeed the value to be written has already
been allocated on the heap before the write even begins, and will persist
whether the write blocks or returns immediately.
Instead constraining memory usage is a knock-on effect of what we really care
about: backpressure; when the ratio of “producers” to their writes is high
(the usual scenario), blocking a write may limit memory usage by delaying heap
allocations associated with elements for future writes.
So bounded queues with blocking writes let us:
when threads are “oversubscribed”, transparently indicate to the runtime
which work has priority
limit future resource usage (CPU time and memory) by producer threads
We might also like our bounded queue to support a non-blocking write which
returns immediately with success or failure. This might be thought of
(depending on the capabilities of your language’s runtime) as more general than
a blocking write, but it also supports a distinctly different notion of
bounding, that is bounding message latency: a producer may choose to drop
messages when a consumer falls behind, in exchange for lower latency for future
writes.
Unagi.Bounded Implementation Ideas
Trying to unpack the ideas above helped in a few ways when designing
Unagi.Bounded. Here are a few observations I made.
We need not block before “writing”
When implementing blocking writes, my intuition was to (when the queue is
“full”) have writers block before “making the message available” (whatever that
means for your implementation). For Unagi that means blocking on an MVar, and
then writing a message to an assigned array index.
But this ordering presents a couple of problems: first, we need to be able to
handle async exceptions raised during writer blocking; if its message isn’t
yet “in place” then we need to somehow coordinate with the reader that would
have received this message, telling it to retry.
By unpacking the purpose of bounding it became clear that we’re free to block
at any point during the write (because the write per se does not have the
memory-usage implications we originally naively assumed it had), so in
Unagi.Bounded writes proceed exactly like in our other variants, until the
end of the writeChan, at which point we decide when to block.
This is certainly also better for performance: if a wave of readers comes
along, they need not wait (themselves blocking) for previously blocked writers
to make their messages available.
One hairy detail from this approach: an async exception raised in a blocked
writer does not cause that write to be aborted; i.e. once entered, writeChan
always succeeds. Reasoning in terms of linearizability this only affects
situations in which a writer thread is known-blocked and we would like to abort
that write.
Fine-grained writer unblocking in probably unnecessary and harmful
In Unagi.Bounded I relax the bounds constraint to “somewhere between bounds
and bounds*2”. This allows me to eliminate a lot of coordination between
readers and writers by using a single reader to unblock up to bounds number
of writers. This constraint (along with the constraint that bounds be a power
of two, for fast modulo) seemed like something everyone could live with.
I also guess that this “cohort unblocking” behavior could result in some nicer
stride behavior, with more consecutive non-blocking reads and writes, rather
than having a situation where the queue is almost always either completely full
or empty.
One-shot MVars and Semaphores
This has nothing to do with queues, but just a place to put this observation:
garbage-collected languages permit some interesting non-traditional concurrency
patterns. For instance I use MVars and IORefs that only ever go from empty
to full, or follow a single linear progression of three or four states in their
lifetime. Often it’s easier to design algorithms this way, rather than by using
long-lived mutable variables (for instance I struggled to come up with a
blocking bounded queue design that used a circular buffer which could be made
async-exception-safe).
Similarly the CAS operation (which I get exported from
atomic-primops)
turns out to be surprisingly versatile far beyond the traditional
read/CAS/retry loop, and to have very useful semantics when used on short-lived
variables. For instance throughout unagi-chan I do both of the following:
CAS without inspecting the return value, content that we or any other
competing thread succeeded.
CAS using a known initial state, avoiding an initial readhttp://brandon.si/code/announcing-unagi-chanTue, 07 Oct 2014 17:41:30 +0000New website layout
http://www.joachim-breitner.de/blog/663-New_website_layout
Joachim Breitnerhttp://www.joachim-breitner.de/blog/663-New_website_layoutTue, 07 Oct 2014 15:40:54 +0000ghc-heap-view for GHC 7.8
http://www.joachim-breitner.de/blog/662-ghc-heap-view_for_GHC_7_8
Joachim Breitnerhttp://www.joachim-breitner.de/blog/662-ghc-heap-view_for_GHC_7_8Tue, 07 Oct 2014 13:55:05 +0000Weight-biased leftist heaps verified in Haskell using dependent types
http://lambda.jstolarek.com/2014/10/weight-biased-leftist-heaps-verified-in-haskell-using-dependent-types/
In January I announced my implementation of weight-biased leftist heaps verified with dependent types in Agda. This was part of my work on a paper submitted to CAV’14 conference. The paper got rejected and I decided not to resubmit it anywhere else. At this year’s ICFP listening to Stephanie Weirich’s keynote speech motivated me to finally port that implementation to Haskell, something that I had planned for a couple of months now. You can take a look at the result on github. Here I want to share some of my experiences and insights.
My overall impression is that porting from Agda to Haskell turned out to be fairly straightforward. It was definitely not a complete rewrite. More like syntax adjustments here and there. There were of course some surprises and bumps along the way but nothing too problematic. More precise details are given in the code comments.
Agda beats Haskell
When it comes to programming with dependent types Agda, being a fully-fledged dependently-typed language, beats Haskell in many aspects:
Agda has the same language for terms and types. Haskell separates these languages, which means that if I want to have addition for natural numbers then I need to have two separate definitions for terms and types. Moreover, to tie types and terms together I need singleton types. And once I have singleton types then I need to write third definition of addition that works on singletons. All of this is troublesome to write and use. (This tedious process can be automated by using singletons package.)
interactive agda-mode for Emacs makes writing code much simpler in Agda. Here I was porting code that was already written so having an interactive Emacs mode for Haskell was not at all important. But if I were to write all that dependently-typed code from scratch in Haskell this would be painful. We definitely need better tools for dependently-typed programming in Haskell.
Agda admits Unicode identifiers. This allows me to have type constructors like ≥ or variables like p≥b. In Haskell I have GEq and pgeb, respectively. I find that less readable. (This is very subjective.)
Agda has implicit arguments that can be deduced from types. Haskell does not, which makes some function calls more difficult. Surprisingly that was not as huge problem as I initially thought it will be.
Agda is total, while Haskell is not. Since there are bottoms in Haskell it is not sound as a logic. In other words we can prove false eg. by using undefined.
Haskell beats Agda
The list is noticeably shorter:
Haskell has much better term-level syntax. In many places this resulted in significantly shorter code than in Agda.
Haskell is not total. As stated earlier this has its drawbacks but it also has a good side: we don’t need to struggle with convincing the termination checker that our code does actually terminate. This was painful in Agda since it required using sized types.
Haskell’s gcastWith function is much better than Agda’s subst. Both these functions allow type-safe casts given the proof that the cast is safe. The difference is that Agda’s subst requires more explicit arguments (as I noted earlier the opposite is usually the case) and restricts the cast to the last type parameter (Haskell allows cast for any type parameter).
Summary
While the list of wins is longer for Agda than it is for Haskell I’m actually very happy with Haskell’s performance in this task. The verification in Haskell is as powerful as it is in Agda. No compromises required.
It’s worth remarking that my implementation works with GHC 7.6, so you don’t need the latest fancy type-level features like closed type families. The really essential part are the promoted data types.Jan Stolarekhttp://lambda.jstolarek.com/?p=1565Tue, 07 Oct 2014 13:35:57 +0000Haskell's Prelude is adding Foldable/Traversable
http://www.yesodweb.com/blog/2014/10/classy-base-prelude
Haskell's Prelude is changing to favor using Foldable/Traversable instead of just lists.
Many Haskellers are concerned that upcoming changes to the Prelude couldbreak existing codemake maintaining code more difficultdecrease beginner friendlinessLets discuss these concernsStability and the Prelude design spaceNeil Mitchell writes:Step 3: Incorporate feedback
I expect that will result in a significant number of revisions, and perhaps significant departures from the original design. Note that the classy-prelude package is following the steps above, and has had 38 revisions on Hackage so far.As a contributor to and user of classy-prelude, I wanted to point out something about this statement. Most of these revisions are minor and backwards compatible consisting of bug-fixes or something like adding a non-default implementation of a typeclass method or an additional typeclass instance. A better data point is the number of major revision releases. classy-prelude is at release 0.10 now, so that would be 10.Neil mentions classy-prelude a second time:The classy-prelude work has gone in that direction, and I wish them luck, but the significant changes they've already iterated through suggest the design space is quite large.Of these 10 changes, I would only consider one to be major and represent any kind of change in the design space: the 0.6 release basing classy-prelude on the mono-traversable package.
Some of the version bumps represent a change in code organization between mono-traversable and classy-prelude. One change that required a bump is a change to the type signature of mapM_ that should be made in the Prelude but probably never will because it will break existing code.
The major change in the 0.6 release is very similar to the upcoming changes in the Prelude, except that classy-prelude (via mono-traversable) works on monomorphic structures such as Text in addition to polymorphic structures.
So I would not consider the design space to be large for classy-prelude or for other prelude replacements.
classy-prelude before 0.6 and most other Prelude replacements or type-class conveniences have not worked out very well.
There is only 1 design that has worked well (incorporating Foldable and Traversable), and that is the design being incorporated into the new Prelude.Neil also writes about other Haskell abstractions:We already have that problem with the Control.Arrow module, which (as far as most people use it), is just a pile of tuple combinators. But unlike other tuple combinators, these are ones whose type signature can't be understood. When I want to use &&& or ***I want to point out that classy-prelude solved some of this issue by exporting Data.BiFunctor instead of functions from Data.Arrow, which required a version bump from 0.9.x to 0.10. I also want to point out that these kinds of arguments are straw man arguments. Every proposed abstraction to Haskell has its own advantages and dis-advantages. Because of the need for backwards compatibility, we are going to be able to point to abstractions in the Prelude that are not being used in the right way for a long time. However, Foldable/Traversable is the only serious contender for abstracting over data structures in Haskell. It has stood the test of time so far, but it has not seen a lot of use yet because everyone is initially directed to just use lists for everything, and the next instinct when using other data structures in the current environment is to use qualified names.Iterating the new designOne proposed remedy for dealing with change is trying to release the new Prelude in an iterative way.
This could be a good idea, but in practice it is very difficult to implement: most users are still going to import Prelude rather than trying out something different and giving their feedback.
A better approach than holding it back is to use a design that makes it easier for new releases to make backwards incompatible changes.
One approach to this could be at the package level the way that base-compat operates.
Another approach that could be useful to library authors is incorporate versioning at the module level.Something to keep in mind though is that because the new Prelude needs to try to work with the old Prelude,
there are not that many options in the design space.
classy-prelude has had the luxury of being able to re-think every Haskell wart.
So it was able to remove all partial functions and use Text instead of String in many places.
But that process is very difficult for the actual Prelude, which is severly constrained.Why change? Module qualified names and generic code.The motivation for classy-prelude was to confront one of Haskell's most glaring warts: name-spacing and the need to qualify functions.
We could certainly have our IDE automatically write import statements, but we still end up with needing to use module qualified names.
This isn't really an acceptable way to program.
I have not seen another language where this extra line noise is considered good style.
For Haskell to move forward and be as convenient to use as other programming languages, there are 2 solutions I know of.change the languagemake it convenient to write generic codeChanging the language so that module qualification is not needed is arguably a much better approach.
This is the case in Object-Oriented languages, and possible in languages very similar to Haskell such as Frege that figure out how to disambiguate a function based on the data type being used.
I think this would be a great change to Haskell, but the idea was rejected by Simon Peyton Jones himself during the discussion on fixing Haskell records because it is not compatible with how Haskell's type system operates today. Simon did propose Type directed name resolution which I always though was a great idea, but that proposal was not able to get off the ground in part because changing Haskell's dot operator proved too controversial.So the only practical option I know of is to focus on #2.
Being able to write generic code is an important issue in of itself.
Programmers in most other mainstream languages write code that operates on multiple data structures of a particular shape,
but Haskell programmers are still specializing a lot of their interfaces.Lists are holding Haskell backIt is taken by many to be a truism that programming everything with lists makes things simpler or at least easier for new Haskell programmers.
I have found this statement to be no different than 99% of things given the glorious "simple" label: the "simplicity" is not extensible, does not even live up to its original use case, and ends up creating its own incidental complexity.I used to frequently warp the functions I wrote to fit the mold of Haskell's list.
Now that I use classy-prelude I think about the data structure that is needed. Or often I start with a list, eventually discover that something such as appending is needed, and I am able to quickly change the function to operate on a different data structure.Using an associative list is an extreme example of using the wrong data structure where lookup is O(n) instead of constant or O(log(n)).
But by warping a function I am really talking about writing a function in a way to reduce list appends or doing a double reverse instead of using a more natural DList or a Seq.
This warping process probably involves performing recursion by hand instead of re-using higher-order functions.
As a library developer, I would like to start exposing interfaces that allow my users to use different data structures, but I know that it is also going to cause some inconvenience because of the current state of the Prelude.Neil writes that he had an opposite experience:I have taken over a project which made extensive use of the generalised traverse and sequence functions. Yes, the code was concise, but it was read-only, and even then, required me to "trust" that the compiler and libraries snapped together properly.This kind of report is very worrying and it is something we should take very seriously.
Any you certainly cannot tell someone that their actual experience was wrong.
However, it is human nature to over-generalize our experiences just as it was the nature of the code author in question to over-generalize functions.
In order to have a productive discussion about this, we need to see (at least a sample or example of) the code in question.
Otherwise we are only left guessing at what mistakes the author made.In general I would suggest specializing your application code to lists or other specific structures (this can always be done with type signatures) until there is a need for more abstraction, and that could be a big part of the problem in this case.It would be really great to start having these discussions now based off of actual code examples and to have a community guide that explains the missing common sense for how to use abstractions appropriately.The uncertainty discussed here is the heart of the matter, and talking about what is good for beginners is largely a distraction.Haskell is for programmers first, students in their first class in functional programming secondThis might sound hostile to beginners. In fact, the opposite is the case!
The programming languages that are taught to beginners are the very same ones that are used in industry.
The first programming language taught to me at school was C, and it was not because it was optimized out of the box for beginners.So the way to attract more beginners is simply to become more popular with industry.
Haskell has already reached the growth rate limit of a language that is popular for the sake of learning about programming.That being said, we do need to do a lot of things to make the experience as nice as possible for beginners, and an alternative prelude for beginners could be a great idea.
But making this the default that holds back progress hurts everyone in the long-run.It isn't Beginner vs. Expert anywaysThe most up-voted comment on Reddit states:What other languages have different standard libraries for people learning and people not learning? What could be a greater way to confuse learners, waste their time and make them think this language is a joke than presenting them with n different standard libraries?I will add my own assertion here: Haskell is confusing today because the Prelude is in a backward state that no longer reflects several important best practices (for example, Neil had to create the Safe package!) and it does not hold up once you write more than a trivial amount of code in your module.We also need to keep in mind that using Haskell can be difficult for beginners precisely for some of the same reasons that it is painful for experts.
And the same reason these new changes will be more difficult for beginners (mental overhead of using the Foldable/Traversable abstraction instead of just lists) will also create difficulties for non-beginners.So the changes to the Prelude are going to make some aspects a better for beginners or existing users and others harder.If we really want to improve Haskell for beginners we need to stop creating a false dichotomy between beginner and expert.
We also need to empower committees to make forward progress rather than letting minority objections stall all forward progress.Improving the library processSome have expressed being surprised to learn about what is going on in the Haskell libraries committee at a late stage.
On the other hand, I doubt that hearing more objections earlier would actually be helpful, because the libraries process has not learned from GHC.Take a look at the extensive documentation around proposed changes to improve Haskell's record system.
Creating a solution to Haskell's problem with records was a very difficult process.
There were several designs that looked good in a rough sketch form, but that had issues when explored in thorough detail on the wiki.
More importantly, the wiki helped summarize and explain a discussion that was extremely laborious to read and impossible to understand by looking through a mail list.Before creating a non-minor change to GHC, there is a convention of creating a wiki page (certainly it isn't always done).
At a minimum there is a Trac ticket that can serve a somewhat similar purpose.My suggestion is that the libraries process use the existing GHC or Haskell wiki to create a page for every non-minor change.
The page for Foldable/Traversable would explainwhat is being changedwhich changes create a breakagehow type errors have changedhow library code is affectedhow user code is affectedbest practices for using Foldable/Traversable Right now we are stuck in a loop of repeating the same points that were already made in the original discussion of the proposal.
Given a wiki page, Neil and others could point out the down-sides of the proposal with actual code and have their voice heard in a productive way that builds up our body of knowledge.http://www.yesodweb.com/blog/2014/10/classy-base-preludeMon, 06 Oct 2014 02:50:45 +0000Help me name a game keybinding library.
http://kpreid.livejournal.com/51386.html
Kevin Reid (kpreid)http://kpreid.livejournal.com/51386.htmlSun, 05 Oct 2014 15:22:05 +0000Errata, please
http://wadler.blogspot.com/2014/10/errata-please.html
This is a space where you can leave comments describing errata in any of my published papers. Please include bibliographic details of the paper, and a link to where the paper appears on my web page if you can. Thank you to Dave Della Costa for volunteering the first entry and inspiring the creation of this post, and to all who utilise this space to record and correct my errors for posterity.Philip Wadlertag:blogger.com,1999:blog-9757377.post-5982400608081788450Sun, 05 Oct 2014 14:07:00 +0000Programming in the real world
http://wellquite.org/blog/programming_in_the_real_world.html
http://wellquite.org/blog/programming_in_the_real_worldSun, 05 Oct 2014 09:22:00 +0000How to Rewrite the Prelude
http://neilmitchell.blogspot.com/2014/10/how-to-rewrite-prelude.html
Neil Mitchelltag:blogger.com,1999:blog-7094652.post-8133723697139549869Sun, 05 Oct 2014 07:05:00 +0000GUI - Release of the threepenny-gui library, version 0.5.0.0
http://apfelmus.nfshost.com/blog/2014/10/04-threepenny-gui-0-5.html
http://apfelmus.nfshost.com/blog/2014/10/04-threepenny-gui-0-5.htmlSat, 04 Oct 2014 08:59:59 +0000Script for migrating from WordPress to Hakyll
http://therning.org/magnus/posts/2014-10-04-000-bbwp.html
http://therning.org/magnus/posts/2014-10-04-000-bbwp.htmlSat, 04 Oct 2014 00:00:00 +0000Distributivity in Horner’s Rule
http://patternsinfp.wordpress.com/2011/05/17/distributivity-in-horners-rule/
This is a continuation of my previous post on Horner’s Rule, and in particular, of the discussion there about distributivity in the datatype-generic version of the Maximum Segment Sum problem:
the essential property behind Horner’s Rule is one of distributivity. In the datatype-generic case, we will model this as follows. We are given an -algebra [for a binary shape functor ], and a -algebra [for a collection monad ]; you might think of these as “datatype-generic product” and “collection sum”, respectively. Then there are two different methods of computing a result from an structure: we can either distribute the structure over the collection(s) of s, compute the “product” of each structure, and then compute the “sum” of the resulting products; or we can “sum” each collection, then compute the “product” of the resulting structure. Distributivity of “product” over “sum” is the property that these two different methods agree, as illustrated in the following diagram.
For example, with adding all the integers in an -structure, and finding the maximum of a (non-empty) collection, the diagram commutes.
There’s a bit of hand-waving above to justify the claim that this is really a kind of distributivity. What does it have to do with the common-or-garden equation
stating distributivity of one binary operator over another? That question is the subject of this post.
Distributing over effects
Recall that distributes the shape functor over the monad in its second argument; this is the form of distribution over effects that crops up in the datatype-generic Maximum Segment Sum problem. More generally, this works for any idiom ; this will be important below.
Generalizing in another direction, one might think of distributing over an idiom in both arguments of the bifunctor, via an operator , which is to say, , natural in the . This is the method of the subclass of that Bruno Oliveira and I used in our Essence of the Iterator Pattern paper; informally, it requires just that has a finite ordered sequence of “element positions”. Given , one can define .
That traversability (or equivalently, distributivity over effects) for a bifunctor is definable for any idiom, not just any monad, means that one can also conveniently define an operator for any traversable unary functor . This is because the constant functor (which takes any to ) is an idiom: the method returns the empty list, and idiomatic application appends two lists. Then one can define
where makes a singleton list. For a traversable bifunctor , we define where is the diagonal functor; that is, , natural in the . (No constant functor is a monad, except in trivial categories, so this convenient definition of contents doesn’t work monadically. Of course, one can use a writer monad, but this isn’t quite so convenient, because an additional step is needed to extract the output.)
One important axiom of that I made recent use of in a paper with Richard Bird on Effective Reasoning about Effectful Traversals is that it should be “natural in the contents”: it should leave shape unchanged, and depend on contents only up to the extent of their ordering. Say that a natural transformation between traversable functors and “preserves contents” if . Then, in the case of unary functors, the formalization of “naturality in the contents” requires to respect content-preserving :
In particular, itself preserves contents, and so we expect
to hold.
Folding a structure
Happily, the same generic operation provides a datatype-generic means to “fold” over the elements of an -structure. Given a binary operator and an initial value , we can define an -algebra —that is, a function —by
(This is a slight specialization of the presentation of the datatype-generic MSS problem from last time; there we had . The specialization arises because we are hoping to define such an given a homogeneous binary operator . On the other hand, the introduction of the initial value is no specialization, as we needed such a value for the “product” of an empty “segment” anyway.)
Incidentally, I believe that this “generic folding” construction is exactly what is intended in Ross Paterson’s Data.Foldable library.
Summing a collection
The other ingredient we need is an -algebra . We already decided last time to
stick to reductions—s of the form for associative binary operator ; then we also have distribution over choice: . Note also that we prohibited empty collections in , so we do not need a unit for .
On account of being an algebra for the collection monad , we also get a singleton rule .
Reduction to distributivity for lists
One of the take-home messages in the Effective Reasoning about Effectful Traversals paper is that it helps to reduce a traversal problem for datatypes in general to a more specific one about lists, exploiting the “naturality in contents” property of traversability. We’ll use that tactic for the distributivity property in the datatype-generic version Horner’s Rule.
In this diagram, the perimeter is the commuting diagram given at the start of this post—the diagram we have to justify. Face (1) is the definition of in terms of . Faces (2) and (3) are the expansion of as generic folding of an -structure. Face (4) follows from being an -algebra, and hence being a left-inverse of . Face (5) is an instance of the naturality property of . Face (6) is the property that respects the contents-preserving transformation . Therefore, the whole diagram commutes if Face (7) does—so let’s look at Face (7)!
Distributivity for lists
Here’s Face (7) again:
Demonstrating that this diagram commutes is not too difficult, because both sides turn out to be list folds.
Around the left and bottom edges, we have a fold after a map , which automatically fuses to , where is defined by
or, pointlessly,
Around the top and right edges we have the composition . If we can write as an instance of , we can then use the fusion law for
to prove that this composition equals .
In fact, there are various equivalent ways of writing as an instance of . The definition given by Conor McBride and Ross Paterson in their original paper on idioms looked like the identity function, but with added idiomness:
In the special case that the idiom is a monad, it can be written in terms of (aka ) and :
But we’ll use a third definition:
where
That is,
Now, for the base case we have
as required. For the inductive step, we have:
which completes the fusion proof, modulo the wish about distributivity for :
Distributivity for cartesian product
As for that wish about distributivity for :
which discharges the proof obligation about distributivity for cartesian product, but again modulo two symmetric wishes about distributivity for collections:
Distributivity for collections
Finally, the proof obligations about distributivity for collections are easily discharged, by induction over the size of the (finite!) collection, provided that the binary operator distributes over in the familiar sense. The base case is for a singleton collection, ie in the image of (because we disallowed empty collections); this case follows from the fact that is an -algebra. The inductive step is for a collection of the form with both strictly smaller than the whole (so, if the monad is idempotent, disjoint, or at least not nested); this requires the distribution of the algebra over choice , together with the familiar distribution of over .
Summary
So, the datatype-generic distributivity for -structures of collections that we used for the Maximum Segment Sum problem reduced to distributivity for lists of collections, which reduced to the cartesian product of collections, which reduced to that for pairs. That’s a much deeper hierarchy than I was expecting; can it be streamlined?jeremygibbonshttp://patternsinfp.wordpress.com/?p=205Tue, 17 May 2011 21:53:29 +0000Morality and temptation
http://patternsinfp.wordpress.com/2011/04/11/morality-and-temptation/
Inspired by Bob Harper’s recent postings, I too have a confession to make. I know what is morally right; but sometimes the temptation is too great, and my resolve is weak, and I lapse. Fast and loose reasoning may excuse me, but my conscience would be clearer if I could remain pure in the first place.
Initial algebras, final coalgebras
We know and love initial algebras, because of the ease of reasoning with their universal properties. We can tell a simple story about recursive programs, solely in terms of sets and total functions. As we discussed in the previous post, given a functor , an -algebra is a pair consisting of an object and an arrow . A homomorphism between -algebras and is an arrow such that :
The -algebra is initial iff there is a unique such for each ; for well-behaved functors , such as the polynomial functors on , an initial algebra always exists. We conventionally write “” for the initial algebra, and “” for the unique homomorphism to another -algebra . (In , initial algebras correspond to datatypes of finite recursive data structures.)
The uniqueness of the solution is captured in the universal property:
In words, is this fold iff satisfies the defining equation for the fold.
The universal property is crucial. For one thing, the homomorphism equation is a very convenient style in which to define a function; it’s the datatype-generic abstraction of the familiar pattern for defining functions on lists:
These two equations implicitly characterizing are much more comprehensible and manipulable than a single equation
explicitly giving a value for . But how do we know that this assortment of two facts about is enough to form a definition? Of course! A system of equations in this form has a unique solution.
Moreover, the very expression of the uniqueness of the solution as an equivalence provides many footholds for reasoning:
Read as an implication from left to right, instantiating to to make the left-hand side trivially true, we get an evaluation rule for folds:
Read as an implication from right to left, we get a proof rule for demonstrating that some complicated expression is a fold:
In particular, we can quickly see that the identity function is a fold:
so . (In fact, this one’s an equivalence.)
We get a very simple proof of a fusion rule, for combining a following function with a fold to make another fold:
Using this, we can deduce Lambek’s Lemma, that the constructors form an isomorphism. Supposing that there is a right inverse, and it is a fold, what must it look like?
So if we define , we get . We should also check the left inverse property:
And so on, and so on. Many useful functions can be written as instances of , and the universal property gives us a very powerful reasoning tool—the universal property of is a marvel to behold.
And of course, it all dualizes beautifully. An -coalgebra is a pair with . A homomorphism between -coalgebras and is a function such that :
The -coalgebra is final iff there is a unique homomorphism to it from each ; again, for well-behaved , final coalgebras always exist. We write “” for the final coalgebra, and for the unique homomorphism to it. (In , final coalgebras correspond to datatypes of finite-or-infinite recursive data structures.)
Uniqueness is captured by the universal property
which has just as many marvellous consequences. Many other useful functions are definable as instances of , and again the universal property gives a very powerful tool for reasoning with them.
Hylomorphisms
There are also many interesting functions that are best described as a combination of a fold and an unfold. The hylomorphism pattern, with an unfold followed by a fold, is the best known: the unfold produces a recursive structure, which the fold consumes.
The factorial function is a simple example. The datatype of lists of natural numbers is determined by the shape functor
Then we might hope to write
where and with
More elaborately, we might hope to write as the composition of (to generate a binary search tree) and (to flatten that tree to a list), where is the shape functor for internally-labelled binary trees,
partitions a list of integers into the unit or a pivot and two sublists, and
glues together the unit or a pivot and two sorted lists into one list. In fact, any divide-and-conquer algorithm can be expressed in terms of an unfold computing a tree of subproblems top-down, followed by a fold that solves the subproblems bottom-up.
But sadly, this doesn’t work in , because the types don’t meet in the middle. The source type of the fold is (the carrier of) an initial algebra, but the target type of the unfold is a final coalgebra, and these are different constructions.
This is entirely reasonable, when you think about it. Our definitions in —the category of sets and total functions—necessarily gave us folds and unfolds as total functions; the composition of two total functions is a total function, and so a fold after an unfold ought to be a total function too. But it is easy to define total instances of that generate infinite data structures (such as a function , which generates an infinite ascending list of naturals), on which a following fold is undefined (such as “the product” of an infinite ascending list of naturals). The composition then should not be a total function.
One might try interposing a conversion function of type , coercing the final data structure produced by the unfold into an initial data structure for consumption by the fold. But there is no canonical way of doing this, because final data structures may be “bigger” (perhaps infinitely so) than initial ones. (In contrast, there is a canonical function of type . In fact, there are two obvious definitions of it, and they agree—a nice exercise!)
One might try parametrizing that conversion function with a natural number, bounding the depth to which the final data structure is traversed. Then the coercion is nicely structural (in fact, it’s a fold over the depth), and everything works out type-wise. But having to thread such “resource bounds” through the code does terrible violence to the elegant structure; it’s not very satisfactory.
Continuous algebras
The usual solution to this conundrum is to give up on , and to admit that richer domain structures than sets and total functions are required. Specifically, in order to support recursive definitions in general, and the hylomorphism in particular, one should move to the category of continuous functions between complete partial orders (CPOs). Now is not the place to give all the definitions; see any textbook on denotational semantics. The bottom line, so to speak, is that one has to accept a definedness ordering on values—both on “data” and on functions—and allow some values to be less than fully defined.
Actually, in order to give meaning to all recursive definitions, one has to further restrict the setting to pointed CPOs—in which there is a least-defined “bottom” element for each type , which can be given as the “meaning” (solution) of the degenerate recursive definition at type . Then there is no “empty” CPO; the smallest CPO has just a single element, namely . As with colimits in general, this smallest object is used as the start of a chain of approximations to a limiting solution. But in order for really to be an initial object, one also has to constrain the arrows to be strict, that is, to preserve ; only then is there a unique arrow for each . The category of strict continuous functions between pointed CPOs is called .
It so happens that in , initial algebras and final coalgebras coincide: the objects (pointed CPOs) and are identical. This is very convenient, because it means that the hylomorphism pattern works fine: the structure generated by the unfold is exactly what is expected by the fold.
Of course, it still happen that the composition yields a “partial” (less than fully defined) function; but at least it now type-checks. Categories with this initial algebra/final coalgebra coincidence are called algebraically compact; they were studied by Freyd, but there’s a very good survey by Adámek, Milius and Moss.
However, the story gets murkier than that. For one thing, does not have proper products. (Indeed, an algebraically compact category with products collapses.) But beyond that, —with its restriction to strict arrows—is not a good model of lazy functional programming; , with non-strict arrows too, is better. So one needs a careful balance of the two categories. The consequences for initial algebras and final coalgebras are spelled out in one of my favourite papers, Program Calculation Properties of Continuous Algebras by Fokkinga and Meijer. In a nutshell, one can only say that the defining equation for folds has a unique strict solution in ; without the strictness side-condition, is unconstrained (because for any ). But the situation for coalgebras remains unchanged—the defining equation for unfolds has a unique solution (and moreover, it is strict when is strict).
This works, but it means various strictness side-conditions have to be borne in mind when reasoning about folds. Done rigorously, it’s rather painful.
Recursive coalgebras
So, back to my confession. I want to write divide-and-conquer programs, which produce intermediate data structures and then consume them. Folds and unfolds in do not satisfy me; I want more—hylos. Morally, I realise that I should pay careful attention to those strictness side-conditions. But they’re so fiddly and boring, and my resolve is weak, so I usually just brush them aside. Is there away that I can satisfy my appetite for divide-and-conquer programs while still remaining in the pure world?
Tarmo Uustalu and colleagues have a suggestion. Final coalgebras and algebraic compactness are sufficient but not necessary for the hylo diagram above to have a unique solution; they propose to focus on recursive coalgebras instead. The -coalgebra is “recursive” iff, for each , there is a unique such that :
This is a generalization of initial algebras: if has an initial algebra , then by Lambek’s Lemma has an inverse , and is a recursive coalgebra. And it is a strict generalization: it also covers patterns such as paramorphisms (primitive recursion)—since is a recursive -coalgebra where is the functor taking to —and the “back one or two steps” pattern used in the Fibonacci function.
Crucially for us, almost by definition it covers all of the “reasonable” hylomorphisms too. For example, is a recursive -coalgebra, where is the shape functor for lists of naturals and the -coalgebra introduced above that analyzes a natural into nothing (for zero) or itself and its predecessor (for non-zero inputs). Which is to say, for each , there is a unique such that ; in particular, for the given above that returns 1 or multiplies, the unique is the factorial function. (In fact, this example is also an instance of a paramorphism.) And is a recursive -coalgebra, where is the partition function of quicksort—for any -algebra , there is a unique such that , and in particular when is the glue function for quicksort, that unique solution is quicksort itself.
This works perfectly nicely in ; there is no need to move to more complicated settings such as or , or to consider partiality, or strictness, or definedness orderings. The only snag is the need to prove that a particular coalgebra of interest is indeed recursive. Capretta et al. study a handful of “basic” recursive coalgebras and of constructions on coalgebras that preserve recursivity.
More conveniently, Taylor and Adámek et al. relate recursivity of coalgebras to the more familiar notion of variant function, ie well-founded ordering on arguments of recursive calls. They restrict attention to finitary shape functors; technically, preserving directed colimits, but informally, I think that’s equivalent to requiring that each element of has a finite number of elements—so polynomial functors are ok, as is the finite powerset functor, but not powerset in general. If I understand those sources right, for a finitary functor and an -coalgebra , the following conditions are equivalent: (i) is corecursive; (ii) is well-founded, in the sense that there is a well-founded ordering such that for each “element” of ; (iii) every element of has finite depth; and (iv) there is a coalgebra homomorphism from to .
This means that I can resort to simple and familiar arguments in terms of variant functions to justify hylo-style programs. The factorial function is fine, because ( is a finitary functor, being polynomial, and) the chain of recursive calls to which leads is well-founded; quicksort is fine, because the partitioning step is well-founded; and so on. Which takes a great weight of guilt off my shoulders: I can give in to the temptation to write interesting programs, and still remain morally as pure as the driven snow.jeremygibbonshttp://patternsinfp.wordpress.com/?p=179Mon, 11 Apr 2011 12:58:23 +0000Adjunctions
http://patternsinfp.wordpress.com/2011/03/28/adjunctions/
Universal properties are a generalization of the notion of a Galois connection between two orderings. Or perhaps I should say: universal properties arise from adjunctions, and it is adjunctions that are a generalization of Galois connections. Adjunctions capture in an abstract categorical setting the idea of “optimal solutions to a problem”; and this idea is itself very general, capturing many of the structures underlying common patterns in programming (not to mention the rest of mathematics). Solutions to equations, products, limits of sequences of approximations, and minimality and maximality are just some of the instances of this powerful abstraction that we will make use of. In the preface to Categories for the Working Mathematician, Mac Lane wrote that “adjoint functors arise everywhere”.
Adjoint functors
Two functors and form an adjunction, written , if there is an isomorphism between the sets of arrows in and in . We say that is the left adjoint and the right adjoint. The essence of the isomorphism is captured by two natural transformations in and in , called the unit and counit of the adjunction; is the image in of in , and conversely, is the image in of in . The unit and counit satisfy the laws
From them one can construct the witnesses to the isomorphism for arbitrary arrows: for each arrow in , there is a unique arrow in such that , given by ; and conversely, for each arrow in , there is a unique arrow in such that , given by ; and moreover, these two constructions are each other’s inverses.
Adjunctions from Galois connections
A preorder forms a category: the objects of the category are the elements of the set~, and between any two elements , there is a unique arrow if , and no arrow otherwise. That adjunctions are a generalization of Galois connections follows straightforwardly from the fact that there is at most one arrow between any two objects in a preorder category. Then monotonic functions and between preorders and form a Galois connection precisely if the sets of arrows and are isomorphic—that is, if both and hold, or neither do, or in other words,
Adjoints of the diagonal functor
A very useful example of adjunctions arises in the definition of products—in the category of sets and total functions, for given types , there is an isomorphism between the set of pair-generating functions, of type , and their two projections, pairs of functions of types and . (Indeed, given functions and , one can construct the pair-generating function ; and conversely, given a pair-generating function , one can construct its two projections and ; and moreover, these two constructions are inverses.)
The “isomorphism between sets of arrows” can be elegantly expressed as an adjunction; since it concerns pairs of arrows, one side of the adjunction involves the product category . The right adjoint is the product functor , mapping an object in —that is, a pair of sets—to their cartesian product as an object in , and an arrow in —that is, a parallel pair of functions—to a function in acting pointwise on pairs. In the other direction, the left adjoint is the diagonal functor , mapping an object in to the object in , and a function to the pair of functions as an arrow in . The adjunction amounts to the isomorphism
or equivalently,
The unit and counit of the adjunction are and . In more familiar terms, the unit is a natural transformation in , so a polymorphic function; in fact, it’s the function of type that we might call . However, the counit is a natural transformation in , so not simply a (polymorphic) function; but arrows in are pairs of functions, so we might write this .
Then the “fork” operation is in fact one of the two witnesses to the isomorphism between the sets of arrows: given an arrow in , that is, a pair of functions of types , then is an arrow in , that is, a function of type , given by the construction above:
or, with more points,
The laws that the unit and counit satisfy are
or, in more familiar terms,
The universal property of follows from the isomorphism between sets of arrows:
The universal property of underlies all the useful laws of that operator.
Of course, the situation nicely dualizes too. Coproducts in arise from the isomorphism between the set of arrows and the pairs of arrows in and . Again, “pairs of arrows” suggest the product category; but this time, the diagonal functor is the right adjoint, with the coproduct functor (which takes a pair of sets to their disjoint union) as the left adjoint. That is, the adjunction is , and the isomorphism is
The unit is a natural transformation in , that is, a pair of functions and . The counit is a natural transformation in , which we might call . The “join” of two functions with a common range is a witness to one half of the isomorphism—given an arrow in , then is an arrow in , defined by
The two laws that the unit and counit satisfy are:
or, perhaps more perspicuously,
Another familiar example from functional programming is the notion of currying, which arises when one can construct the function space (the type of functions from to , for each type and ), such that there is an isomorphism between the sets of arrows and . Here, the adjunction is —in this case, both functors are endofunctors on . The unit and counit are natural transformations and . We might call these and , since the first is a curried pair-forming operator, and the second applies a function to an argument:
The laws they satisfy are as follows:
or, in points,
The isomorphism itself is witnessed by the two inverse functions
where and .jeremygibbonshttp://patternsinfp.wordpress.com/?p=135Mon, 28 Mar 2011 10:58:16 +0000Universal properties and Galois connections
http://patternsinfp.wordpress.com/2011/02/15/universal-properties-and-galois-connections/
One recurring theme throughout this series will be that of a universal property—an identity that captures an indirect means of solving a problem, by transforming that problem into a different (and hopefully simpler) domain, while still preserving all its essential properties. In particular, the original problem has a solution if and only if the transformed problem does, and moreover, the solution to the transformed problem can easily be translated back into a solution to the original problem. One can see universal properties as a generalization of the notion of a Galois connection between two orderings, which are a similarly powerful technique of relating problems in two different settings. (In fact, the proper generalization of Galois connections is to adjunctions, but that’s a story for next time.)
Universal properties
The universal property of the operation for products is a representative example. Recall that when and ; and that and . Then is completely defined by its universal property:
This identity repays careful study.
It translates a problem in the more complex domain of products (namely, the problem of showing how some complicated expression can be written in terms of ) into simpler problems (here, equations about the two projections of ).
It’s an equivalence. So not only do you have an implication from left to right (any expressible as a satisfies the two properties on the right), you also have one from right to left (any pair of functions satisfying the two properties on the right induces a ). In other words, is a solution to the equation on the left iff it is a solution on the right; not only does a solution on the right yield a construction on the left, but also the absence of solutions on the right implies the absence on the left. Or again: the equations on the right have a unique solution in —since any two solutions must both be equal to the same expression on the left.
It has many useful simple consequences. You can make the left-hand side trivially true by letting ; then the right-hand side must also be true:
Symmetrically, you can make the right-hand side trivially true by letting and ; then the left-hand side must also be true:
If you further let , you conclude that every pair consists solely of its two projections, nothing more:
In fact, the universal property of tells you everything you need to know about ; you might take that as one justification for the term “universal”.
It also has many useful less obvious consequences. For example, if you’re searching for an that acts independently on the two components of a pair— and —just let and in the universal property, and conclude
(which we’ve written “” elsewhere). For another example, we can deduce a fusion law for : for what does the equation
hold? This matches the left-hand side of the universal property; expanding the right-hand side yields
Such a rich harvest from so small a seed! (In fact, we will see later that an even smaller seed suffices.)
Galois connections
We can see the same structures that occur in universal properties like that of above also in relationships between orderings. As a very simple example, consider the problem of dividing a natural number by two, exactly; the universal property of a solution to this problem is the equivalence
That is, is a solution to the problem “compute ” precisely when ; both the existence and the identification of a solution to a problem expressed in terms of division has been translated to one in terms of multiplication—which is arguably a simpler setting. Note that the universal property amounts to an equivalence
involving the two functions and , which are in some sense inverses. This pattern will crop up over and over again.
The division example involved an equivalence between the two identities and . More generally, another relation than “” might be involved. Extending the previous example to integer division, rounding down, we have for :
Again, this relates the two (in some sense inverse) functions and ; but this time equality is inadequate for stating the problem, and it perhaps more convincing to claim that a more complicated problem has been translated into a simpler one . What is more, translating the problem via this universal property pays dividends when it comes to reasoning about the problem, because the simpler problem space is much more amenable to calculation. For example, properties of repeated division (for ) do not trip off the tongue; but we can reason straightforwardly as follows:
Thus, precisely when , or in other words, .
In this case, the two problem spaces have both involved the same relation on the same domain, namely the natural numbers; that is not essential. For example, the universal property of the floor function from reals to integers is given by:
where, to be completely explicit, we have written for the usual ordering on reals and for the corresponding ordering on integers, and for the injection from the integers into the reals. This time the two problem spaces involve two different orderings on different domains; we say that the pair of functions and form a Galois connection between the orderings and . (We also see that the relationship between the two functions and is becoming less like a pure inverse relationship, and more of an embedding–projection pair.)
As a simple non-arithmetical example of a Galois connection on a single domain, consider some set and a fixed subset ; then
That is, and form a Galois connection between and itself.
A non-arithmetical example between two different domains is afforded by the field of formal concept analysis, which relates “objects” and their “properties”. Given are sets of objects and of properties, and a relation ; we write to denote that object has property . This induces “concept-forming operators” and defined by:
That is, is the set of properties enjoyed by all objects in , and is the set of objects enjoying all the properties in ; a concept is a pair with and . The concept-forming operators form a Galois connection between and :
This construction can be used to translate a problem about the extension of a concept (that is, an enumeration of its instances) into one about the intension (that is, the characteristic properties of its instances). It is related to the observation that “syntax and semantics are adjoint“—under the analogy that “objects” are sets of mathematical structures, “properties” are axioms, and the relation is “satisfaction”, the models of an axiomatic theory are included in a set of structures if and only if the theory logically entails the minimal axiomatization of .jeremygibbonshttp://patternsinfp.wordpress.com/?p=124Tue, 15 Feb 2011 13:45:51 +000011 ways to write your last Haskell program
http://www.joachim-breitner.de/blog/661-11_ways_to_write_your_last_Haskell_program
Joachim Breitnerhttp://www.joachim-breitner.de/blog/661-11_ways_to_write_your_last_Haskell_programThu, 02 Oct 2014 13:47:49 +0000Updating auto-update
http://www.yesodweb.com/blog/2014/10/updating-auto-update
A few weeks back, Kazu and I received an email from Martin Bailey, who was
interested in working with us to further optimize Warp. The subject at the
time was reduced buffer copying and allocations. That subject is very
interesting in itself, and once finalized, will get its own blog post as well. But
that's not the subject of this blog post.After working on some ideas, Kazu benchmarked Warp, and found a massive
performance degradation which had already slipped onto Hackage. The problem
only appears under highly concurrent requests (which is exactly what Kazu's
benchmark was testing). That bug has now been resolved, and users are
recommended to upgrade to the newest versions of auto-update and warp. (We also
included some other performance boosts here, care of Ryan Newton's
atomic-primops package.) This blog post covers the problem, and its solution.It's about timeOne of the required response headers according to the HTTP spec is the Date
header. As you might guess, this consists of the date, as well as the current
time on the server. This has a very specific format specified in the spec. A
naive approach to filling in this header would be, for each request, to run:now <- getCurrentTime
let value = formatTimeHTTP now
headers' = ("Date", value) : headersHowever, when you're writing a server that handles hundreds of thousands of
requests per second, having to get and format the current time on each request
is incredibly expensive. Instead, quite some time ago, Kazu introduced a date
formatting worker thread, which essentially looks like this:let getNowFormatted = formatTimeHTTP <$> getCurrentTime
nowFormatted <- getNowFormatted >>= newIORef
forkIO $ forever $ do
threadDelay 1000000
getNowFormatted >>= writeIORef nowFormatted
return $ readIORef nowFormattedWe fork a single thread that recalculates the formatted time every second,
and updates a mutable reference. This means that, regardless of how many
clients connect, we will always run this computation at most once per second.
And reading the current time requires no system calls, formatting, or
allocation: it's just a memory read.Watt's the matterThe problem with this approach is that, even if there are zero requests, we're
still going to run this computation once a second. This doesn't hurt our
performance too much (it's a relatively cheap operation). However, it does mean
that our process never stops working, which is bad for power consumption. So
we needed a way to let that worker thread turn off when it wasn't needed
anymore, and start up again on demand.If this sounds familiar, it's because we blogged about it just two months
ago. But there's
an implementation detail I want to point out about auto-update. When I started
writing it, I aimed to have the worker thread completely shut down when not
needed, and then for a new worker thread to be spawned on demand. This
resulted in some strange corner cases. In particular, it was possible for two
different callers to spawn two different worker threads at the same time. We
used atomicModifyIORef to ensure that only one of those threads became the
"official" worker, and the other one would shut down right away. There was also
a lot of tricky business around getting async exceptions right.The code wasn't too difficult to follow, and was still pretty short. You can
view it on
Github.The core of the problemUnfortunately, before release, we didn't do enough performance testing of
auto-update in highly concurrent settings. When we threw enough cores at the
problem, we quickly ran into a situation where multiple Haskell threads would
end up making concurrent requests for the auto-update value, and each of those
threads would fork a separate worker thread. Only one of those would survive,
but the forking itself was killing our performance! (I had one benchmark
demonstrating that, for one million requests across one thousand threads on
four cores, over ten thousands worker threads were forked.)There was another problem as well. We made heavy use of atomicModifyIORef to
get this working correctly. Compare this to our original dedicated thread
solution: each data access was a simple, cheap readIORef. By introducing
atomicModifyIORef at each request site, we introduced memory barrier issues
immediately.The solutionAfter iterating a few times, Kazu, Martin and I came up with a fairly elegant
solution to the problem. As noted, the original dedicated thread was in many
ways ideal. A lot of our problems were coming from trying to fork threads on
demand. So we came up with a compromise: why not have a single, dedicated
worker thread, but allow it to go to sleep/block when it's no longer needed?Blocking semantics meant we needed to move beyond IORefs over to either
MVars or STM (we elected for the former, but it would still be interesting to
compare performance with the latter). But we still want to be able to have
incredibly cheap lookup in the common case of a value being precomputed. So we
ended up with three mutable variables:An IORef containing a Maybe a. If a precomputed value is available, it's
present in there as Just a. Otherwise, there's a Nothing value. This
mean that, in the normal case, a requester only needs to (a) do a memory read,
and (b) case analyze the value.An MVar baton to tell the worker thread that someone is waiting for a
value. In the case that the IORef contains Nothing, the requester fills
this MVar. Before it starts working, the worker thread always tries to
takeMVar this baton.An MVar for passing back result values. This may seem redundant with the
IORef, but is necessary for the case of Nothing. A requester putMVars
into the baton, and then blocks in readMVar on this reference until the value
is available. The worker thread will update both the IORef and this value at
the same time, and then go to sleep until it needs to compute again, at which
point the process will loop.Since the requesters never try to fork threads, there's no possibility of
running into the high contention problem of multiple forks. The worst case
scenario is that many requesters see a Nothing value at the same time, and
all end up blocking on the same MVar. While less efficient than just reading
an IORef, this isn't nearly as expensive as what we had previously.There's another big advantage: the normal case no longer uses any
atomicModifyIORef (or any other synchronized memory access), meaning we've
avoided memory barriers during periods of high concurrency.And finally: the code is drastically
simpler.And now that we've fixed our regression, and gotten back high performance
together with better power consumption, we can finally return to Martin's
original idea of better buffer management. More on that soon hopefully :).http://www.yesodweb.com/blog/2014/10/updating-auto-updateThu, 02 Oct 2014 11:24:00 +0000Full Stack Functional Web Engineer at Front Row Education (Full-time)
http://functionaljobs.com/jobs/8745-full-stack-functional-web-engineer-at-front-row-education
urn:uuid:46ebcb3e-6c67-9799-b43b-eae2ac08a63bWed, 01 Oct 2014 19:17:04 +0000Senior Software Engineer at McGraw-Hill Education (Full-time)
http://functionaljobs.com/jobs/8744-senior-software-engineer-at-mcgraw-hill-education
urn:uuid:8f60639b-9a8e-0cf0-1934-b8b8ab73e018Wed, 01 Oct 2014 16:07:57 +0000GHC Weekly News - 2014/09/30
http://ghc.haskell.org/trac/ghc/blog/weekly20140930
thoughtpolicehttp://ghc.haskell.org/trac/ghc/blog/weekly20140930Tue, 30 Sep 2014 20:07:51 +0000List of publications and talks updated
http://jeltsch.wordpress.com/2014/09/30/list-of-publications-and-talks-updated/
The list of publications and talks on my website has been pretty much out of date. Now it is updated, for you to enjoy. :-) Tagged: publication, talkWolfgang Jeltschhttp://jeltsch.wordpress.com/?p=606Tue, 30 Sep 2014 16:22:47 +0000Announcing Yesod 1.4
http://www.yesodweb.com/blog/2014/09/announcing-yesod-1-4
We are happy to announce the release of Yesod 1.4. This includes:Releases of all Yesod packages to support version 1.4.The book content on yesodweb.com is completely updated for Yesod 1.4, with all snippets confirmed to compile and most of the text proofread from scratch for accuracy (in the next week the rest will be finished).A new Stackage snapshot available for GHC 7.8.3.Its worth mentioning that there have been a ton of improvements to Yesod since version 1.2, they just didn't need any breaking changes.Thanks to everyone who provided code, feedback, and testing for this release, it
should be a very solid one!Here's a collection of links that provide various other pieces of information about this release:Announcing Persistent 2Persistent 2.1 Release CandidatePlanning Yesod 1.4Yesod 1.4 release dateChangelogWhat is most exciting to report is that this was a very minor change to Yesod, and
therefore most code should be upgradeable with minor changes. First, the
changelog of breaking changes:New routing system with more overlap checking controlThis requires OverloadedStrings and ViewPatterns.
The generated code is faster and much more readable.Yesod routes are not just type-safe, they also check for overlapping that could cause ambiguity. This is a great feature, but sometimes it gets in your way.
Overlap checking can be turned off for multipieces, entire routes, and parent routes in a hierarchy. For more information, see the commit comment.Dropped backwards compatibility with older versions of dependenciesIn particular, persistent-1 and wai-2. We will talk more about persistent 2.
wai-3 uses a CPS style that will require some middleware to have an additional CPS parameter.
Looking at the wai-extra source code can help with upgrading, but it should just be adding an extra parameter.yesod-auth works with your database and your JSONThere is better support for non-persistent backends in yesod-auth. See pull request 821 for details. For most users, you can fix this by adding instance YesodAuthPersist App to your Foundation.hs.yesod-auth already released a breaking change to be able to accept JSON everywhere.
That bumped the version to 1.3
We like to keep the yesod-* packages in sync, so now everything is getting bumped to 1.4 together.In the 1.4 release, we also fixed requireAuth and and requireAuthId to return a 401 response when a JSON response is requested. See pull request 783.yesod-test sends HTTP/1.1 as the versionThis may require updating tests to expect 303 instead of 302 redirects.Type-based caching with keys.The Type-based caching code was moved into a separate module without Yesod dependencies and documented. If there is interest in seeing this as a separate package let us know, but it is also pretty easy to just copy the module.To me, TypeCache is a beautiful demonstration of Haskell's advanced type system that shows how you can get the best of both worlds in a strongly typed language.type TypeMap = HashMap TypeRep DynamicAbove we have the wonderful juxtaposition of Haskell's strong typing in the Key, and dynamic typing in the value. This HashMap is used to cache the result of a monadic action.cached :: (Monad m, Typeable a)
=> TypeMap
-> m a -- ^ cache the result of this action
-> m (Either (TypeMap, a) a) -- ^ Left is a cache miss, Right is a hitDynamic is used to have a HashMap of arbitrary value types.
TypeRep is used to create a unique key for the cache.
Yesod uses this to cache the authentication lookup of the database for the duration of the request.newtype CachedMaybeAuth val = CachedMaybeAuth { unCachedMaybeAuth :: Maybe val }
deriving Typeable
cachedAuth
= fmap unCachedMaybeAuth
. cached
. fmap CachedMaybeAuth
. getAuthEntityCachedMaybeAuth is a newtype that isn't exported. TypeRep is specific to a module, so this pattern guarantees that your cache key will not conflict outside of your module.This functionality was in yesod-1.2 even though the code was not separated into a new module.
The 1.4 release adds the ability to cache multiple values per typetype KeyedTypeMap = HashMap (TypeRep, ByteString) Dynamic
cachedBy :: (Monad m, Typeable a)
=> KeyedTypeMap
-> ByteString -- ^ a cache key
-> m a -- ^ cache the result of this action
-> m (Either (KeyedTypeMap, a) a) -- ^ Left is a cache miss, Right is a hitThis is useful if your monadic action has inputs: if you serialize them to a ByteString you can use thm as a key.Upgrade guideThe most significant set of changes in the Yesod ecosystem actually landed in
Persistent 2. However, these were mostly internal changes with new features that maintain backwards compatibility, so many users will be unaffected.To kickoff the upgrade process, you need to change update your cabal file to allow yesod version 1.4.
If you had constraints on persistent, update them to > 2.1
If you are using cabal freeze to peg your versions in the cabal.config file, cabal will provide you no assistance in making a smooth upgrae.
You are probably going to want to delete a whole lot of things in cabal.config (or possibley the entire file), and upgrade a lot of dependencies at once.
When you are done and things compile again, you will want to do a cabal freezeAs has become the custom for each major release, the upgrade
process is documented by the diff of the Haskellers code base upgrading to Yesod 1.4.
For Haskellers it was pretty simple.In sum:Replace type YesodPersistBackend App = SqlPersist with type YesodPersistBackend App = SqlBackend.Add instance YesodAuthPersist App to Foundation.hs.Add the ViewPatterns language extension.If you have more complex persistent code you may have more to do.
Look at the previous post on persistent-2.1http://www.yesodweb.com/blog/2014/09/announcing-yesod-1-4Tue, 30 Sep 2014 11:00:00 +0000How we might abolish Cabal Hell, part 1
http://www.well-typed.com/blog/99
At ICFP a few weeks ago a hot topic in the corridors and in a couple talks was the issues surrounding packaging and “Cabal Hell”.
Fortunately we were not just discussing problems but solutions. Indeed I think we have a pretty good understanding now of where we want to be, and several solutions are in development or have reasonably clear designs in peoples’ heads.
I want to explain what’s going on for those not already deeply involved in the conversation. So this is the first of a series of blog posts on the problems and solutions around Cabal hell.
There are multiple problems and multiple solutions. The solutions overlap in slightly complicated ways. Since it is a bit complicated, I’m going to start with the big picture of the problems and solutions and how they relate to each other. In subsequent posts I’ll go into more detail on particular problems and solutions.
“Cabal hell”: the problems
So what is “Cabal hell”? Let’s consult the dictionary…
Cabal Hell
The feeling of powerlessness one has when Cabal does not do what one wanted and one does not know how to fix it.
I’m joking obviously, but my point is that Cabal hell is not a precise technical term. There are a few different technical problems (and misunderstandings and UI problems) that can cause Cabal hell.
A useful concept when talking about this topic is that of the packaging “wild wild west”. What we mean is whether we are in a context where we reasonably expect packages to work together (because there has been some deliberate effort to make them work together), or if we are in the “wild wild west”. In the “wild wild west” we have to do things like deal with packages that were uploaded yesterday by multiple different authors. The point is that nobody has yet had time to try and make things consistent. It is a useful concept because we have developers who need to deal with the “wild wild west” and those who would really rather not, and the solutions tend to look a bit different.
Another term we often use when talking about packages is “consistency”. What we mean is that in a collection of packages there is at most one version of each package. For example when you ask cabal-install to install package A and B, we say that it will try to find a “consistent” set of dependencies – meaning a set including A, B and their dependencies that has only one version of any package.
“Cabal hell”: the symptoms
So lets consider a breakdown of the technical problems. To start with lets look at a breakdown based on the symptoms that a developer in Cabal Hell experiences
We can first break things down by whether there is a solution or not. That is, whether a perfect dependency resolver could find a plan to install the package(s) and their dependencies consistently. We want such a solution because it’s a prerequisite for installing working packages. (We’re ignoring the possibility that there is a solution but the solver fails to find one. That is possible but it’s a relatively rare problem.)
Given the situation where the solver tells us that there is no solution, there are a few different cases to distinguish:
No solution expected
The failure was actually expected. For example a developer updating their package to work with the latest version of GHC is not going to be surprised if their initial install attempt fails. Then based on what the solver reports they can work out what changes they need to make to get things working.
Solution had been expected
The more common case is that the developer was not expecting to be working in the wild west. The developer had an expectation that the package or packages they were asking for could just be installed. In this case the answer “no that’s impossible” from the solver is very unhelpful, even though it’s perfectly correct.
Unnecessary solver failure
The symptoms here are exactly the same, namely the solver cannot find a solution, but the reason is different. More on reasons in a moment.
Even when there is a solution we can hit a few problems:
Compile error
Compilation can fail because some interface does not match. Typically this will manifest as a naming error or type error.
Breaking re-installations
Cabal’s chosen solution would involve reinstalling an existing version of a package but built with different dependencies. This re-installation would break any packages that depend on the pre-existing instance of the installed package. By default cabal-install will not go ahead with such re-installation, but you can ask it to do so.
Type errors when using packages together
It is possible to install two package and then load them both in GHCi and find that you cannot use them together because you get type errors when composing things defined in the two different packages.
“Cabal hell”: the reasons
So those are the major problems. Lets look at some reasons for those problems.
Inconsistent versions of dependencies required
There are two sub-cases worth distinguishing here. One is where the developer is asking for two or more packages that could be installed individually, but cannot be installed and used together simultaneously because they have clashing requirements on their common dependencies. The other is that a package straightforwardly has no solution (at least with the given compiler & core library versions), because of conflicting constraints of its dependencies.
Constraints wrong
With under-constrained dependencies we get build failures, and with over-constrained dependencies we get unnecessary solver failures. That is, a build failure is (almost always) due to dependency constraints saying some package version combination should work, when actually it does not. And the dual problem: an unnecessary solver failure is the case where there would have been a solution that would actually compile, if only the constraints had been more relaxed.
Single instance restriction
Existing versions of GHC and Cabal let you install multiple versions of a package, but not multiple instances of the same version of a package. This is the reason why Cabal has to reinstall packages, rather than just add packages.
Inconsistent environment
These errors occur because cabal-install does not enforce consistency in the developer’s environment, just within any set of packages it installs simultaneously.
We’ll go into more detail on all of these issues in subsequent posts, so don’t worry if these things don’t fully make sense yet.
“Cabal hell”: the solutions
There are several problems and there isn’t one solution that covers them all. Rather there are several solutions. Some of those solutions overlap with each other, meaning that for some cases either solution will work. The way the solutions overlap with the problems and each other is unfortunately a bit complicated.
Here’s the overview:
So what does it all mean?
We’ll look at the details of the solutions in subsequent posts. At this stage the thing to understand is which solutions cover which problems, and where those solutions overlap.
We’ll start with the two most important solutions. They’re the most important in the sense that they cover the most cases.
Nix-style persistent store with multiple consistent environments
This solves all the cases of breaking re-installations, and all cases of inconsistent environments. It doesn’t help with wrong constraints.
You’ll note that it covers some cases where there is no solution and you might wonder what this can mean. Some cases where there is no solution are due to two (or more) sets of packages that could be installed independently but cannot be installed together consistently. In a nix-style setting it would be possible to offer developers the option to install the packages into separate environments when the solver determines that this is possible.
Curated consistent package collections
These are things like the Debian Haskell packages or Stackage. This solves some cases of each of the different problems: breaking re-installations, inconsistent environments, wrong constraints and lack of consistent solutions. It solves those cases to the extent that the package collection covers all the packages that the developer is interested in. For many developers this will be enough. Almost by definition however it cannot help with the “wild west” of packages because the curation takes time and effort. Unless used in combination with a isolated environment solution (e.g. nix-style, but also less sophisticated systems like hsevn or cabal sandboxes) it does not allow using multiple versions of the collection (e.g. different projects using different Stackage versions).
It is worth noting that these two solutions should work well together. Neither one subsumes the other. We don’t need to pick between the two. We should pick both. The combination would get us a long way to abolishing Cabal hell.
There are also a number of smaller solutions:
Automatic build reporting
This helps with detecting compile errors arising from constraints that are too lax. It doesn’t help with constraints that are too tight. This solution requires a combination of automation and manual oversight to fix package constraints and to push those fixes upstream.
Upper-bound build bots
This is similar to gathering build reports from users, but instead of looking at cases of compile failure (constraints too lax), it explicitly tries relaxing upper bounds and checks if things still compile and testsuites work. Again, this requires automation to act on the information gleaned to minimise manual effort.
Package interface compatibility tools
This is to help package authors get their dependency constraints right in the first place. It can help them follow a version policy correctly, and tell them what minimum and maximum version bounds of their dependencies to use. It does not completely eliminate the need to test, because type compatibility does not guarantee semantic compatibility. Solutions in this area could eliminate a large number of cases of wrong constraints, both too lax and too tight.
Private dependencies
This allows solutions to exist where they do not currently exist, by relaxing the consistency requirement in a safe way. It means global consistency of dependencies is not always required, which allows many more solutions. This solution would cover a lot of cases in the “wild wild west” of packaging, and generally in the large set of packages that are not so popular or well maintained as to be included in a curated collection.
Next time…
So that’s the big picture of the problems and solutions and how they relate to each other. In subsequent posts we’ll look in more detail at the problems and solutions, particularly the solutions people are thinking about or actively working on.duncanhttp://www.well-typed.com/blog/99Tue, 30 Sep 2014 10:19:33 +0000Adding tags
http://therning.org/magnus/posts/2014-09-30-000-adding-tags.html
http://therning.org/magnus/posts/2014-09-30-000-adding-tags.htmlTue, 30 Sep 2014 00:00:00 +0000Persistent 2.1 released
http://www.yesodweb.com/blog/2014/09/persistent-2
Persistent 2.1, a stable release of the next generation of persistent is released to Hackage.Persistent is an ORM for Haskell that keeps everything type-safe.Persistent 2.1 featuresa flexible, yet more type-safe Key typea simplified monad stackI already announced persistent 2
and the 2.1 release candidate.Everyone should set their persistent dependencies to > 2.1 && < 3. 2.0.x was the unstable release and is now deprecated.I want to thank all the early persistent 2 adopters for putting up with a fast-moving, buggy code base. This was an experiment in shipping an unstable version, and what I learned from it is that it was a great process, but we need to make sure Travis CI is running properly, which it is now!Persistent 2.1 library supportThe persistent and persistent-template libraries should support any kind of primary key type that you need. The backends are still catching up to the new featurespersistent-sqlite backend has fully implemented these features.persistent-postgres and persitent-mysql don't yet support changing the type of the id fieldpersistent-mongoDB does not yet support composite primary keysAll of the above packages except persistent-mysql are being well maintained, but just developing new features at their own pace. persistent-mysql is in the need of a dedicated maintainer. There are some major defects in the migration code that have gone unresolved for a long time now.persistent-redis is in the process of being upgraded to 2.1persistent-zookeeper was just released, but it is on persistent 1.3.*There are other persistent packages out there that I have not had the chance to check on yet, most noteably persistent-odbc. Feel free to ask for help with upgrading.Persistent 2.1 upgrade guideSimple persistent usage may not need any changes to upgrade.The fact that the Key type is now flexible means it may need to be constrained.
So if you have functions that have Key in the type signature that are not specific to one PersistEntity, you may need to constrain them to the BackendKey type.
An easy way to do this is using ConstraintKinds.type DBEntity record =
( PersistEntityBackend record ~ MongoContext
, PersistEntity record
, ToBackendKey MongoContext record
)A SQL user would use SqlBackend instead of MongoContext. So you can now change the type signature of your functions:- PersistEntity record => Key record
+ DBEntity record => Key recordDepending on how you setup your monad stacks, you may need some changes.
Here is one possible approach to creating small but flexible Monad stack type signatures.
It requires Rank2Types, and the code show is specialized to MongoDB. type ControlIO m = ( MonadIO m , MonadBaseControl IO m)
type LogIO m = ( MonadLogger m , ControlIO m)
-- these are actually types, not constraints
-- with persistent-2 things work out a lot easier this way
type DB a = LogIO m => ReaderT MongoContext m a
type DBM m a = LogIO m => ReaderT MongoContext m aThe basic type signature is just DB () (no constraints required).
For working with different monad stacks, you can use DBM.
If you are using conduits, you will have MonadResource m => DBM m ().
Here is another example:class Monad m => HasApp m where
getApp :: m App
instance HasApp Handler where
getApp = getYesod
instance HasApp hasApp => HasApp (ReaderT MongoContext hasApp) where
getApp = lift $ getApp
instance MonadIO m => HasApp (ReaderT App m) where
getApp = ask
-- | synonym for DB plus HasApp operations
type DBApp a = HasApp m => DBM m a
type DBAppM m a = HasApp m => DBM m a With this pattern our return type signature is always ReaderT MongoContext m, and we are changing m as needed. A different approach is to have a return type signature of m and to place a MonadReader constraint on it.type Mongo m = (LogIO m, MonadReader MongoContext m)Right now this approach requires using a call to
Database.MongoDB.liftDB around each database call, but I am sure there are approaches to dealing with that. One approach would be to wrap every persistent "primitive" with liftDB.http://www.yesodweb.com/blog/2014/09/persistent-2Mon, 29 Sep 2014 23:51:38 +0000Structure and Efficiency of Computer Programs
http://existentialtype.wordpress.com/2014/09/28/structure-and-efficiency-of-computer-programs/
For decades my colleague, Guy Blelloch, and I have been promoting a grand synthesis of the two “theories” of computer science, combinatorial theory and logical theory. It is only a small exaggeration to say that these two schools of thought operate in isolation. The combinatorial theorists concern themselves with efficiency, based on hypothetical translations of high-level algorithms to low-level machines, and have no useful theory of composition, the most important tool for developing large software systems. Logical theorists concern themselves with composition, emphasizing the analysis of the properties of components of systems and how those components may be combined; the entire subject of logic is a theory of composition (entailment). But relatively scant attention is paid to efficiency, and, to a distressingly large extent, the situation is worsening, rather than improving.
Guy and I have been arguing, through our separate and joint work, for the applicability of PL ideas to algorithms design, leading, for example, to the concept of adaptive programming that has been pursued aggressively by Umut Acar over the last dozen years. And we have argued for the importance of cost analysis, for various measures of cost, at the level of the code that one actually writes, rather than in terms of how it is supposedly compiled. Last spring, after initial discussions with Anindya Banerjee at NSF last winter, I decided to write a position paper on the topic, outlining the scientific opportunities and challenges that would arise from an attempt to unify the two, disparate theories of computing. The first draft was circulated privately in May, and was revised, very lightly, in July in preparation for a conference call sponsored by NSF among a group of leading researchers in both PL’s and Algorithms with the goal to find common ground and isolate key technical challenges.
I am delighted (and relieved) to see that Swarat Chaudhuri, in a post on his PL Enthusiast blog, has heartily endorsed our proposal for a grand synthesis of the “two theories” of Computer Science. During his visit, Swarat had lengthy discussions with Umut, Guy, and me on our work in both research and education, but were surprised and disheartened by his opposition to our approach. His concern was based on the common misapprehension that it is impossible to give a useful cost model for the lambda calculus, which would thereby undermine the entire body of work on which Guy and I, among others, had been pursuing for decades. Coming from such a distinguished researcher as Chaudhuri, his opposition created for us a period of anxiety, could we be wrong? But no, it is simply not true. Guy and John Greiner provided an adequate cost model for the lambda calculus (under both a sequential and a parallel interpretation) in 1993, and that paper has withstood decades of scrutiny. But it did take quite some time to sort this out to be absolutely sure. For some mysterious reason, when it comes to the lambda calculus nonsense gets twice around the world before the truth can get its boots on, to borrow a turn of phrase from Mark Twain. After some back-and-forth, the matter is settled, and I am delighted that we can now count Swarat among our supporters. It would have been a heavy burden for us to have to bear the opposition of a distinguished researcher such as himself to the very foundations of our proposed program.
Which is not to say that there are not serious obstacles to be overcome if such a grand synthesis is to be accomplished. The first step is to get the right people together to discuss the issues and to formulate a unified vision of what are the core problems, and what are promising directions for the short- and long-term. To this end there is likely to be a workshop held during the next academic year to start addressing these problems at a scientific level. Contrary to what is implied in the PL Enthusiast post, my position paper is not a proposal for funding, but is rather a proposal for a scientific meeting designed to bring together two largely (but not entirely) disparate communities. This summer NSF hosted a three-hour long conference call among a number of researchers in both areas with a view towards formulating a workshop proposal in the near future. Please keep an eye out for future announcements. I think there are many good problems to be considered, and many opportunities for new results.
I would like to mention that I am particularly grateful to Anindya Banerjee at NSF for initiating the discussion last winter that led to my position paper, and for helping to move forward the process of formulating a workshop proposal. And I am very happy to learn of Swarat’s endorsement; it will go a long way towards helping attract interest from both sides of the great divide.Filed under: Research Tagged: algorithms, programming languages, researchRobert Harperhttp://existentialtype.wordpress.com/?p=1011Mon, 29 Sep 2014 00:11:55 +0000Adding support for comments
http://therning.org/magnus/posts/2014-09-29-000-support-for-comments.html
http://therning.org/magnus/posts/2014-09-29-000-support-for-comments.htmlMon, 29 Sep 2014 00:00:00 +0000Notes on Abstract and Existential Types
http://jozefg.bitbucket.org/posts/2014-09-29-abstraction-existentials.html
http://jozefg.bitbucket.org/posts/2014-09-29-abstraction-existentials.htmlMon, 29 Sep 2014 00:00:00 +0000sml-family.org up and running!
http://existentialtype.wordpress.com/2014/09/26/sml-family-org-up-and-running/
After far too long, and far too many obstacles to be overcome, Dave MacQueen, Lars Bergstrom, and I have finally prepared an open-source site for the entire family of languages derived from Standard ML. The defining characteristic of Standard ML has always been that it has a mathematically precise definition, so that it is always clear what is a valid program and how it should behave. And indeed we have seven different working compilers, all of which are compatible with each other, with the exception of some corner cases arising from known mistakes in the definition. Moreover, there are several active projects developing new variations on the language, and it would be good to maintain the principle that such extensions be precisely defined.
To this end the sources of the 1990 and 1997 versions of the definition are on the web site, with the permission of MIT Press, as is the type-theoretic definition formulated by Chris Stone and me, which was subsequently used as the basis for a complete machine-checked proof of type safety for the entire language done by Karl Crary, Daniel K. Lee. It is be hoped that the errors in the definition (many are known, we provide links to the extensive lists provided by Kahrs and Rossberg in separate investigations) may now be corrected by a community process. Anyone is free to propose an alteration to be merged into the main branch, which is called “SML, The Living Language” and also known as “Successor ML”. One may think of this as the third edition of the definition, but one that is in continual revision by the community. Computer languages, like natural languages and like mathematics, belong to us all collectively, and we all contribute to their evolution.
Everyone is encouraged to create forks for experimental designs or new languages that enrich, extend, or significantly alter the semantics of the language. The main branch will be for generally accepted corrections, modifications, and extensions, but it is to be expected that completely separate lines of development will also emerge.
The web site, sml-family.org is up and running, and will be announced in various likely places very soon.
Update: We have heard that some people get a “parked page” error from GoDaddy when accessing sml-family.org. It appears to be a DNS propagation problem.
Update: The DNS problems have been resolved, and I believe that the web site is stably available now as linked above.Filed under: Research Tagged: functional programming, smlRobert Harperhttp://existentialtype.wordpress.com/?p=1004Fri, 26 Sep 2014 19:06:44 +0000Reading highlights this week
http://wellquite.org/blog/reading_highlights_this_week.html
http://wellquite.org/blog/reading_highlights_this_weekSat, 27 Sep 2014 14:08:00 +0000Announcing: Heist v0.14
http://snapframework.com/blog/2014/09/24/heist-0.14-released
The Snap team is happy to announce the release of version 0.14 of Heist.Major ChangesNamespace SupportHeist now has support for namespaces. This allows you to configure Heist so that all of your splices require a namespace. Requiring a namespace allows Heist to be more aggressive with errors for unbound splices. For instance, imagine you set the hcNamespace field in your HeistConfig to “h”, and you bind two splices.mySplices = do
"foo" #! fooSplice
"bar" #! barSpliceWith this setup, you would put the “h” namespace on all of the splice tags in your templates. Instead of calling those splices with “ ” and “ ”, you would use “ ” and “ ”. So why go to all this trouble so you have to type more? Because it allows Heist to do more error checking. Without namespaces there is no way for Heist to know whether a tag is supposed to be a splice or not. We could use the list of valid HTML tags to infer it, but that significantly constrains the scope of what we intended for Heist. This approach allows the user to be explicit about which tags should be splices. If you do not want to use namespaces, set the namespace to the empty string.Along with the namespace field, we introduced the hcErrorNotBound for controlling the error checking. When hcErrorNotBound is True, Heist will generate an error message if it encounters any namespaced tags that do not have splices bound for them. This eliminates a large class of bugs where users were using a splice in their templates, but forgot to bind it in their code. The intent is that users will usually want to have this error checking turned on. But we felt it was also important to be able to use namespacing without the strict enforcement, so we included this flag to give users full control.Generalized Error ReportingSince this release is doing more error checking, we decided to expose error facilities to the user. This release exposes a new function tellSpliceError that you can use when error conditions are detected in your splices. If you are using compiled Heist, then all your templates will be processed up front at load time. If any of your load time or compiled splices detect an error condition that the user needs to fix, you can call tellSpliceError with an error message. If there are any errors, Heist initialization will fail and all the errors will be returned.Restructured HeistConfigThe addition of hcNamespace and hcErrorNotBound to HeistConfig required some restructuring. Previously HeistConfig had a Monoid instance, but we removed that since the new fields make it unclear which instance should be used. But we also did not want to completely get rid of the monoid functionality either. So in order to get the best of both worlds, we refactored all of HeistConfig’s previous fields into another data structure called SpliceConfig. This way we can keep the Monoid instance for SpliceConfig and still avoid imposing a weird set of semantics on the user.Unfortunately, given the use of field accessors it was impossible to make this change without breaking backwards compatibility. What seems like it should have been a simple addition of a couple parameters ended up being a more significant refactoring. To make these kinds of changes easier in the future Heist now exports lenses to all of the HeistConfig fields as well as an emptyHeistConfig value to use as a starting point. These lenses work with both the lens and lens-family-core packages and we export them without incurring a dependency on either lens package.The HeistConfig constructor and field accessors have been moved to the Heist.Internal.Types module, so if you really need them, they are still available. However, be aware that Internal modules are subject to change without the deprecation cycle that we use for other modules.Minor improvementsFactored out SpliceAPI module into separate map-syntax package and deprecated the old module which will be removed in the next major release.Snap has been updated to support this Heist 0.14.Doug Beardsleyhttp://snapframework.com/blog/2014/09/24/heist-0.14-releasedWed, 24 Sep 2014 10:10:00 +0000Haskell courses and Haskell eXchange
http://www.well-typed.com/blog/98
In the beginning of October, my colleage Adam Gundry and I will spend a full week in London again for Haskell-related activities: on Monday and Tuesday (October 6–7), we will teach Fast Track to Haskell, a two-day introduction course to Haskell, targeted at people who want to get started with Haskell or learn more about functional programming in general. On Wednesday (October 8), there’s the Haskell eXchange, a one-day conference full of interesting talks on Haskell-related topics. On Thursday and Friday (October 9–10), we will look at more advanced Haskell concepts and programming patterns in Advanced Haskell.
All three events are still open for registration.
Haskell eXchange
The Haskell eXchange will take place in London for the third time now, and I’m happy to report that there’s going to be a really fantastic program again:
As is almost traditional by now, Simon Peyton Jones (Microsoft Research) himself will open the conference, this time with a talk on “Safe, zero-cost coercions in Haskell”.
This is followed by Jeremy Gibbons (University of Oxford) with “Categories for the Working Haskeller”, explaining to Haskell developers and people who are interested in Haskell what role category theory plays in Haskell and if/how categories can be helpful.
I’m very pleased that Bryan O’Sullivan (Facebook) has agreed to give a presentation at the Haskell eXchange this year. As the author of countless Haskell libraries (many of which are among the most used in the entire Haskell ecosystem), and being a co-author of the widely known O’Reilly book “Real World Haskell”, he’s certainly learned how to squeeze a bit of extra performance out of Haskell code when needed. He’s going to share his experiences and provide valuable advice in his talk.
After lunch, we’ll continue with a pair of talks looking at using Haskell for the development of RESTful web services from slightly different angles. Erik Hesselink (Silk) is going to present the rest framework, which makes it easy to develop and maintain REST APIs, independent of the underlying web framework you use. After that, Chris Dornan (Iris Connect) and Adam Gundry (Well-Typed) will talk about api-tools and in particular address the question of how you can solve the problem of schema migrations nicely.
Tim Williams and Peter Marks (both Barclays) will give a joint talk on Lucid, their in-house non-embedded DSL that is written in Haskell and has a mostly structural type system with interesting features such as row polymorphism and extensible records as well as extensible sum-types.
The talks will be concluded by Oliver Charles (Fynder), well-known for his tireless efforts in the “24 days of Hackage” series, who is going to show us how the use of GHC’s most advanced type system extensions helps him write better real-world code at his company.
After the talks, there’s going to be pizza and beer and an informal “Park Bench Discussion” where we can all discuss the questions that have been raised throughout the day in more detail.
I hope you’re as excited about this program as I am: I think there’s a fantastic range of topics covered, from language features and theoretical aspects, practical advice for programmers to interesting case studies of real-world code. Also, it’s an excellent opportunity to meet fellow developers interested in Haskell. If you’re working for a company using Haskell and are looking for new developers, this may be an excellent opportunity to recruit. On the other hand, if you’d like nothing more than a Haskell job, this is an opportunity to meet people who are actually using it in practice, and may have a job for you or at least be able to give you advice on how to find one.
If you haven’t registered yet, please consider doing so! We’re looking forward to meeting you there.
Fast Track to Haskell and Advanced Haskell
These two successful courses have been offered on a regular basis since October 2012. They’re continuously updated to reflect the latest changes in the Haskell world, such as updates to the infrastructure, new features of the main Haskell compiler GHC, or exciting new libraries.
Both courses are hands-on, comprising a combination of lectures, interactive coding and exercises that the participants are supposed to work on alone or in teams, with the help of the teacher(s).
The Fast Track course is for people who know how to program, but have little or no experience in Functional Programming or Haskell. It teaches Haskell in from scratch in just two days, covering important concepts such as datatypes, polymorphism, higher-order functions, type classes, how IO works in Haskell, and ending with an introduction to monads. It’s also interesting for people who are interested in learning about functional programming in general, because Haskell is a prime example of a functional programming language, and the course focuses on the important programming concepts more than on language peculiarities.
The Advanced Haskell course is for people who have some experience with Haskell, but want to learn more. We’re going to discuss (functional) data structures and their complexity, have a detailed look at how lazy evaluation works and how it is implemented, how to reason about performance and how to use various debugging tools. Somewhat depending on demand, there’s also the option to learn more about advanced programming patterns, such as monads, applicative functors and monad transformers, about concurrency and parallelism, or about the more advanced features of the Haskell type system such as GADTs and type families.
Being in the same week as the Haskell eXchange makes it possible to combine one of the courses (or even both) with the eXchange, where you can hear several other viewpoints and get to know more Haskellers!
Other courses
We’re offering additional training courses on-demand and on-site for companies in Europe, the US, or anywhere in the world on request. See our training page for more information.
HacBerlin
By the way, I’m also going to be at the Haskell Hackathon in Berlin this upcoming weekend. On Sunday, I’m going to give a talk on parser combinators. You can still register for the Hackathon, too. It’s free.andreshttp://www.well-typed.com/blog/98Tue, 23 Sep 2014 10:10:42 +0000