# News aggregator

### Mike Izbicki: The type lens laws

*(or how to promote quickcheck and rewrite rules to the type level)*

We’ve seen how to use the typeparams library to soup up our Functor and Applicative type classes. But we’ve been naughty little haskellers—we’ve been using type lenses without discussing their laws! Today we fix this oversight. **Don’t worry if you didn’t read/understand the previous posts.** This post is much simpler and does not require any background.

First, we’ll translate the standard lens laws to the type level. Then we’ll see how these laws can greatly simplify the type signatures of our functions. Finally, I’ll propose a very simple (yes, I promise!) GHC extension that promotes rewrite rules to the type level. These type level rewrite rules would automatically simplify our type signatures for us. It’s pretty freakin awesome.

What exactly is a type lens?Today, we won’t actually import anything from the typeparams library. Instead, we’ll be building up everything from scratch.

> {-# LANGUAGE TypeFamilies #-} > {-# LANGUAGE MultiParamTypeClasses #-} > {-# LANGUAGE PolyKinds #-} > {-# LANGUAGE RankNTypes #-} > {-# LANGUAGE ConstraintKinds #-} > {-# LANGUAGE FlexibleContexts #-} > import Control.Category > import Prelude hiding ( (.), id ) > import GHC.ExtsGiven a data type:

> data Example a b c = Example a b cWe construct the following empty classes:

> class Param_a (p :: * -> Constraint) t -- has kind :: * -> Constraint > class Param_b (p :: * -> Constraint) t > class Param_c (p :: * -> Constraint) tThese classes are the type level lenses. Each one uniquely identifies a parameter of the Example data type. To use these lenses, we will need to be able to represent them at the value level. So we create the singleton type:

> data TypeLens p q = TypeLensNow, we can create three values that uinquely identify the three type parameters:

> _a = TypeLens :: TypeLens p (Param_a p) > _b = TypeLens :: TypeLens p (Param_b p) > _c = TypeLens :: TypeLens p (Param_c p)We’re calling these things lenses, so they must be composable. In fact, they compose really easy. Check out their Category instance:

> instance Category TypeLens where > id = TypeLens > t1.t2 = TypeLensWhen we chain values together using the (.) composition operator, we create a chain of classes at the type level. For example:

ghci> :t _a._b _a._b :: TypeLens p (Param_a (Param_b p)) ghci> :t _a._b._c _a._b._c :: TypeLens p (Param_a (Param_b (Param_c p))) ghci> > :t _a._a._b._c._a._b _a._a._b._c._a._b :: TypeLens p (Param_a (Param_a (Param_b (Param_c (Param_a (Param_b p))))))These chains of classes correspond to a nesting of data types. For the Example type we created above, _a._b would refer to the type param b1 in the type:

Example (Example a1 b1 c1) b2 c2_a._b._c would refer to b2 in the type:

Example (Example a1 b1 (Example a2 b2 c2)) b0 c0and _a._a._b._c._a._b would refer to the parameter b6 in the monster type:

Example ( Example ( Example a2 ( Example a3 b3 ( Example ( Example a5 ( Example a6 b6 c6 ) c5 ) b4 c4 ) ) c2 ) b1 c1 ) b0 c0 getters and settersThe whole point of lenses is they give us an easy way to get and set parameters. At the type level, we do that with these type families:

> type family GetParam (p :: * -> Constraint) (t :: *) :: * > type family SetParam (p :: * -> Constraint) (a :: *) (t :: *) :: *For our Example data type, the implementations look like:

> type instance GetParam (Param_a p) (Example a b c) = GetParam p a > type instance GetParam (Param_b p) (Example a b c) = GetParam p b > type instance GetParam (Param_c p) (Example a b c) = GetParam p c > type instance SetParam (Param_a p) a' (Example a b c) = Example (SetParam p a' a) b c > type instance SetParam (Param_b p) b' (Example a b c) = Example a (SetParam p b' b) c > type instance SetParam (Param_c p) c' (Example a b c) = Example a b (SetParam p c' c)These definitions are recursive, so we need a base case to halt the recursion:

> class Base t > type instance GetParam Base t = t > type instance SetParam Base t' t = t'Here are some example usages of the GetParam family:

ghci> :t undefined :: GetParam (Param_a Base) (Example Int b c) :: Int ghci> :t undefined :: GetParam (Param_b Base) (Example Int Float c) :: Float ghci> :t undefined :: GetParam (Param_a (Param_b Base)) (Example (Example a1 Int c1) b2 Float) :: Int ghci> :t undefined :: GetParam (Param_c Base) (Example (Example a1 Int c1) b2 Float) :: FloatAnd similar uses of the SetParam family:

ghci> :t undefined :: SetParam (Param_a Base) Char (Example Int b Float) :: Example Char b Float ghci> :t undefined :: SetParam (Param_c Base) Char (Example Int b Float) :: Example Int b Char ghci> :t undefined :: SetParam (Param_a (Param_b Base)) Char (Example (Example a1 Int c1) b2 Float) :: Example (Example a1 Char c1) b2 Float ghci> :t undefined :: SetParam (Param_c Base) Char (Example (Example a1 Int c1) b2 Float) :: Example (Example a1 Int c1) b2 Char the lens lawsThe first lens law is that if we set a type parameter to its current value, then the overall type does not change. In code, this looks like:

> type LensLaw1 lens t = t ~ SetParam lens (GetParam lens t) tThe second lens law states that if we set a type parameter to a certain value, then get the value at the location of the lens, then we should get back our original type. In code:

> type LensLaw2 lens a t = a ~ GetParam lens (SetParam lens a t)And lastly, if we set the same parameter twice, then the last setter wins. In code:

> type LensLaw3 lens a b t = a ~ GetParam lens (SetParam lens a (SetParam lens b t))There are many other laws that can be derived from these three simple laws. For example, we can derive this fourth lens law from laws 1 and 3:

> type LensLaw4 lens a b t = SetParam lens a (SetParam lens b t) ~ SetParam lens a tWe’re glossing over some technicalities involving injective type families, here, but we’ll return to this later in the post.

promoting quick check to the type levelAny time we have laws in Haskell, we’ve got to prove that they hold. Sometimes, parametricity does this for us automatically (as in the case of the Functor laws). But usually, we rely on test frameworks like QuickCheck. Therefore, we need these frameworks at the type level.

This turns out to be straightforward. We can use these functions to verify our laws:

> property_lensLaw1 :: LensLaw1 lens t => TypeLens Base lens -> t -> () > property_lensLaw1 _ _ = () > property_lensLaw2 :: LensLaw2 lens a t => TypeLens Base lens -> a -> t -> () > property_lensLaw2 _ _ _ = () > property_lensLaw3 :: LensLaw3 lens a b t => TypeLens Base lens -> a -> b -> t -> () > property_lensLaw3 _ _ _ _ = ()We test the laws as follows. First, specialize all the type variables in the function. Then, ask GHC if the function type checks. If it does, then the law holds for the type variables we chose.

Here is an example:

ghci> property_lensLaw1 _a (undefined :: Example Int Float String) () ghci> property_lensLaw2 _a (undefined :: String) (undefined :: Example Int Float String) () ghci> property_lensLaw3 _a (undefined :: String) (undefined :: [a]) (undefined :: Example Int Float String) ()Now, let’s write some GetParam/SetParam instances that do not obey the laws and see what happens. In the NationalSecurityAgency type below, GetParams works just fine, but SetParams is broken.

> data NationalSecurityAgency x = NationalSecurityAgency > class Param_x (p :: * -> Constraint) t > _x = TypeLens :: TypeLens p (Param_x p) > type instance GetParam (Param_x p) (NationalSecurityAgency x) = x > type instance SetParam (Param_x p) x' (NationalSecurityAgency x) = NationalSecurityAgency StringWhen we test the first lens law using a String, everything works fine:

ghci> lensLaw1 _x (undefined :: NationalSecurityAgency String) ()But when we test it using an Int, the type checker explodes:

ghci> lensLaw1 _x (undefined :: NationalSecurityAgency Int) :73:1: Couldn't match type ‘[Char]’ with ‘Int’ Expected type: SetParam (Param_x Base) (GetParam (Param_x Base) (NationalSecurityAgency Int)) (NationalSecurityAgency Int) Actual type: NationalSecurityAgency Int In the expression: lensLaw1 _x (undefined :: NationalSecurityAgency Int) In an equation for ‘it’: it = lensLaw1 _x (undefined :: NationalSecurityAgency Int)You can imagine a template haskell quickcheck that calls these property functions many times on random types to give a probabalistic test our type laws hold.

using the lawsThese laws will greatly simplify inferred types in our programs. We’ll see why using an example.

Consider the beloved Applicative sequencing operator (*>) . In the standard libraries, it has the type:

(*>) :: Applicative f => f a -> f b -> f bSweet and simple.

In the applicative class we generated yesterday, however, the sequencing operator is pretty nasty looking. GHCi reports it has the type of:

> (*>) :: > ( Applicative lens > ( SetParam > lens > (a1 -> GetParam lens (SetParam lens (a -> GetParam lens tb1) tb1)) > (SetParam lens (a -> GetParam lens tb1) tb1) > ) > , Applicative lens (SetParam lens (a -> GetParam lens tb1) tb1) > , Applicative lens tb1 > , (b1 -> a2 -> a2) ~ GetParam > lens > (SetParam > lens > (a1 -> GetParam lens (SetParam lens (a -> GetParam lens tb1) tb1)) > (SetParam lens (a -> GetParam lens tb1) tb1)) > , a1 ~ GetParam lens (SetParam lens a1 (SetParam lens (a -> GetParam lens tb1) tb1)) > , tb0 ~ SetParam lens a tb1 > , ta ~ SetParam lens a1 (SetParam lens (a -> GetParam lens tb1) tb1) > , a ~ GetParam lens (SetParam lens a tb1) > ) => ta > -> tb0 > -> TypeLens Base lens > -> tb1 > (*>) = undefined > class Applicative lens tYikes! What the hell does that beast do?!

Somehow, we need to simplify this type signature, and the type lens laws are what lets us do this. For example, one of the constraints above is:

a1 ~ GetParam lens (SetParam lens a1 (SetParam lens (a -> GetParam lens tb1) tb1))We can use the third lens law to simplify this to:

a1 ~ GetParam lens (SetParam lens a1 tb1)If we repeat this process many times, we get a type signature that looks like:

> newop :: > ( Applicative lens ( SetParam lens ( a -> b -> b ) tb ) > , Applicative lens ( SetParam lens ( b -> b ) tb ) > , Applicative lens tb > , tb ~ SetParam lens b tb > , LensLaw2 lens (b->b) tb > , LensLaw2 lens b tb > , LensLaw3 lens (a -> b -> b) (b -> b) tb > , LensLaw3 lens a (b->b) tb > , LensLaw4 lens (a->b->b) (b->b) tb > , LensLaw4 lens a (b->b) tb > ) => SetParam lens a tb > -> tb > -> TypeLens Base lens > -> tb > newop = (*>)This looks quite a bit better, but is still less than ideal. Actually, this is as far as you can get with the lens laws in GHC 7.8. You need injective type families to go further. (See this mailing list thread and this ghc trac issue for more details about what injective type families are.) Currently, injectve type families are slated to enter GHC 7.10, so the rest of this post will be a bit more speculative about what this future GHC can do.

injecting power into the lens lawsLet’s take another look at the type synonyms for the lens laws:

type LensLaw1 lens t = t ~ SetParam lens (GetParam lens t) t type LensLaw2 lens a t = a ~ GetParam lens (SetParam lens a t) type LensLaw3 lens a b t = a ~ GetParam lens (SetParam lens a (SetParam lens b t))This code only enforces that the laws hold for certain parameters. But that’s not what we want! All types are equal in the eyes of the law, so what we really want is type synonyms that look like:

type LensLaw1' = forall lens t. t ~ SetParam lens (GetParam lens t) t type LensLaw2' = forall lens a t. a ~ GetParam lens (SetParam lens a t) type LensLaw3' = forall lens a b t. a ~ GetParam lens (SetParam lens a (SetParam lens b t))Unfortunately, sticking this into GHC yields the dreaded “type families may not be injective” error message. With injective type families, we would be able to write these laws. (This is a somewhat bold claim that I won’t justify here.) Then our code would simplify further to:

newop' :: ( Applicative lens ( SetParam lens ( a -> b -> b ) tb ) , Applicative lens ( SetParam lens ( b -> b ) tb ) , Applicative lens tb , tb ~ SetParam lens b tb , LensLaw1' , LensLaw2' , LensLaw3' ) => SetParam lens a tb -> tb -> TypeLens Base lens -> tb newop' = (*>) a proposal for new syntaxWe can still do better. The lens laws are not something that applies only to specific functions. They are global properties of the type families, and they apply everywhere. Therefore, they should be implicitly added as constraints into every type signature.

We could make this happen by adding a new syntax called “type rules”. In the same way that value level rewrite rules simplify our values, these type rules would simplify our types. The syntax could look something like:

type rule LensLaw1' = forall lens t. t ~ SetParam lens (GetParam lens t) t type rule LensLaw2' = forall lens a t. a ~ GetParam lens (SetParam lens a t) type rule LensLaw3' = forall lens a b t. a ~ GetParam lens (SetParam lens a (SetParam lens b t))There are two differences between a type rule and a regular type synonym: First, they can take no type parameters. Second, they are implicitly added to every type signature in your program.

The three rules above would allow us to rewrite our function as:

newop'' :: ( Applicative lens ( SetParam lens ( a -> b -> b ) tb ) , Applicative lens ( SetParam lens ( b -> b ) tb ) , Applicative lens tb , tb ~ SetParam lens b tb ) => SetParam lens a tb -> tb -> TypeLens Base lens -> tb newop'' = (*>)That is soooo much nicer!

Stay tunedWe still have some work to go to get our newop function’s type signature as simple as (*>) from the standard library. But I think we’ve got a realistic shot at it. In a coming post I’ll be proposing a way to combine the multiple Applicative constraints into a single constraint, and a nice looking sugar over the SetParam/GetParam type families.

If you didn’t quite follow the previous posts about Functors and Applicatives, they might make a bit more sense now.

### Announcement: Bang, a drum machine DSL for Haskell

Posted this to haskell-cafe this morning, but wanted to shoot you guys the message as well because I'd love more feedback. :)

I've been working on "Bang" on and off for about a month or two now, and finally thought it was "good enough" to open-source and show to the public! I've been having fun with it, and hopefully some of you will, too. It currently supports basically all of the primitive transformations that I could think of doing on a drum sequence, such as reversing, mirroring, changing duration and tempo. There are a bunch of operators built in that make it easy to write things like polyrhythms, and infinite sequences of notes are possible as well.

The source code and basic tutorial are up on Github

And the package + more detailed documentation is up on Hackage

Thanks guys, and enjoy!

submitted by 5outh[link] [16 comments]

### XMonad and xinput.d.

### berp: An implementation of Python 3

### Links to accepted papers for ICFP 2014

### 2014 APL Programming Competition is Open

The sixth annual International APL Problem Solving Competition is now live!

Dyalog Ltd invites students worldwide to put their programming and problem-solving skills to the test by using any APL system to develop solutions to ten questions and solve a series of problems. This is a contest for people who love a challenge and learning new things for fun, with the added bonus that you can win one of 43 cash prizes totalling $8,500, including a grand prize of $2,500 and a trip to Eastbourne in the U.K. to attend the annual Dyalog Ltd user meeting in September 2014.

For the rules and eligibility criteria and to enter the competition, go to http://www.dyalogaplcompetition.com/.

If you have friends who love a challenge and learning new things for fun, or you know students who might be interested in participating, then please recommend this contest to them.

The deadline for submitting solutions is 6 August 2014. Winners will be announced on 18 August 2014.

Good luck and have fun!

### What's the deal with Yesod?

I used to feel that Yesod had a lot of promise. But it has really failed to deliver. Major failings:

- still no blog system, after years of discussion about it. Never mind things like CRUD screens. Shouldn't these be derivable from the Persistent model?
- highly, highly opinionated at the core level. This wouldn't be so bad, but it's also wrong very often. I know this is just my opinion. But I also know that when I make opinionated choices in my libraries, I do them in type classes and provide a way to override my choice. Yesod abandoned that principle a long time ago.
- Highly inconsistent and type un-safe interfaces. This is especially scary in the Auth system. A "Creds master" is a text token and list of text key-values. The semantics of the key-value pairs depends on the Auth plugin that sets the Creds master. Really? String typing? In 2014? In a strongly typed language? There are a
**lot**of examples like this, especially in the Auth system. The bizarre thing is, Yesod already uses TypeFamilies all over the place, so there is literally no reason to pass around a blob of texts. - type safe URLs are over-hyped. Especially for a "RESTful" framework. Type safe URLs just aren't useful when your hrefs are dynamically generated by JavaScript.
- Having a "Foundation" module splits your project in two -- the stuff that imports Foundation, and the stuff Foundation imports. This division is really painful. Moving code from one side of the Foundation to the other very often breaks code, just because the Import.hs module doesn't work.
- Actually, the whole Import idea is misguided. I end up having to import parts of Prelude constantly, especially on the framework side of the Foundation boundary.
- There are like 5 different ways to load a widget. The pro's and con's are not explained anywhere, including the source code.
The documentation is actually really really bad. Consider:

-- | Determine the ID associated with the set of credentials.

getAuthId :: Creds master -> HandlerT master IO (Maybe (AuthId master))

-- | Retrieves user credentials, if user is authenticated.

By default, this calls defaultMaybeAuthId to get the user ID from the session. This can be overridden to allow authentication via other means, such as checking for a special token in a request header. This is especially useful for creating an API to be accessed via some means other than a browser.

maybeAuthId :: HandlerT master IO (Maybe (AuthId master))

Notice that maybeAuthId does not return a Creds master. Notice that 'getAuthId' determines the ID associated with a set of credentials. Notice that this means having to read the spaghetti code to figure out what is actually going on. This is even worse, since the semantics for credentials aren't even defined in Yesod.Auth. They're defined by plugins.

- The documentation is even worse than that. If you Google for Yesod function names, Google ends up pointing you toward old versions. Especially since a lot of the functions have become private in newer versions (so they don't get documented on Hackage). Fair enough, but Yesod was always a bit on the spaghetti side, and this just pours on thick, inky squid sauce. In other words,
*obscure*. - Multitudes of special cases. Why is whamlet a widget quasiquoter, but not julius?
- The community is not very good. It's the weakest community I've seen from a "major" Haskell project.

Strengths:

- Hamlet is sweet. I actually do like type safe URLs. And the templating language is nice.
- Persistent: I can take it or leave it, honestly. But it's decent enough to count as a strength.
- esqueleto: an "associated" project.

I'm 100% sure there are other strengths. And that I am feeling uncharitable this evening.

Is Yesod a viable platform? Will it ever be one? Or is it just a vehicle for Michael Snoyman to write a book?

submitted by 2piix[link] [46 comments]

### Exceptions and monad transformers

### Yesod Web Framework: Exceptions and monad transformers

Duncan Coutts kicked off a discussion on the core libraries mailing list in April about exception handling in monad transformers. We made a lot of headway in that discussion, and agreed to bring up the topic again on the libraries mailing list, but unfortunately none of us ever got around to that. So I'm posting a summary of that initial discussion (plus some of my own added thoughts) to hopefully get a broader discussion going.

The initial thread kicked off with a link to ghc's ExceptionMonad typeclass, which encapsulates the ability to catch exceptions, mask async exceptions, and guarantee cleanup actions (a.k.a. bracket/finally). The question is: is there a canonical way to do the same thing, without depending on the ghc library?

As is usually the case in the Haskell ecosystem, the answer is that there are about five different packages providing this functionality. I'd break them down into two categories:

- Packages which define a typeclass (or set of typeclasses) specifically for exception handling. Such examples include MonadCatchIO-mtl, MonadCatchIO-transformers, and exceptions.
- Packages which define a generic way to embed a monad transformer inside the value, and thereby perform
*any*control operation in the base monad. Examples are monad-peel and monad-control (or if you want to go really far in time, neither).

Fortunately, most of those options have been deprecated in favor of alternatives. Today, there are really two choices: exceptions and monad-control. I'd like to describe these in a bit more detail, and contrast some of the pluses and minuses of both approaches. My overall goals are twofold:

- Get more knowledge out there about the advantages of the two libraries.
- Work towards a community consensus on when each library should be used.

I'm interested in the latter point, since having a consistent usage of the MonadBaseControl vs MonadMask typeclasses in various packages makes it easier to reuse code.

Note: I don't mean to take credit for the ideas that are expressed in this blog post. As I said, it's a combination of summary of a previous discussion (mostly amongst Duncan, Edward, and myself) and a few new thoughts from me.

exceptionsThe exceptions package exposes three typeclasses, all specifically geared at exception handling, and each one incrementally more powerful than the previous one. MonadThrow is for any monad which can throw exceptions. Some examples of instances are:

- IO, where the exception becomes a runtime exception.
- Either, where the exception becomes the Left value.
- Maybe, where an exception results in Nothing.
- Any monad transformer built on top of one of those. (Note also that there's a special CatchT transformer, which keeps the exception in the transformer itself.)

In addition to just throwing exceptions, you often want to be able to catch exceptions as well. For that, the MonadCatch typeclass is available. However, some monads (in particular, Maybe) cannot be MonadCatch instances, since there's no way to recover the thrown exception from a Nothing.

The final typeclass is MonadMask, which allows you to guarantee that certain actions are run, even in the presence of exceptions (both synchronous and asynchronous). In order to provide that guarantee, the monad stack must be able to control its flow of execution. In particular, this excludes instances for two categories of monads:

- Continuation based monads, since the flow of execution may ignore a callback entirely, or call it multiple times. (For more information, see my previous blog post.)
- Monads with multiple exit points, such as ErrorT over IO.

And this is the big advantage of the exceptions package vs MonadCatchIO: by making this distinction between catching and masking, we end up with instances that are well behaved, and finally functions that guarantee cleanup happens once, and only once.

One design tradeoff is that all exceptions are implicitly converted to SomeException. An alternate approach is possible, but ends up causing many more problems.

monad-controlmonad-control takes a completely different approach. Let's consider the StateT Int IO monad stack, and consider a function

foo :: StateT String IO IntNow suppose that I'd like to catch any exceptions thrown by foo, using the standard try function (specialized to IOException for simplicity):

tryIO :: IO a -> IO (Either IOException a)Obviously these two functions don't mix together directly. But can we coerce them into working together somehow? The answer lies in exposing the fact that, under the surface, StateT just becomes a function in IO returning a tuple. Working that way, we can write a tryState function:

tryState :: StateT String IO a -> StateT String IO (Either IOException a) tryState (StateT f) = StateT $ \s0 -> do eres <- tryIO $ f s0 return $ case eres of Left e -> (Left e, s0) Right (x, s1) -> (Right x, s1)(Full example on School of Haskell.) The technique here is to:

- Capture the initial state.
- Use tryIO on the raw IO function.
- Case analyze the result, either getting an exception or a successful result and new state. Either way, we need to reconstitute the internal state of the transformer, in the former by using the initial state, in the latter, using the newly generated state.

It turns out that this embedding technique can be generalized in two different ways:

- It applies to just about any IO function, not just exception functions.
- It applies to many different transformers, and to arbitrarily deep layerings of these transformers.

For examples of the power this provides, check out the lifted-base package, which includes such things as thread forking, timeouts, FFI marshaling.

This embedding technique does *not* work for all transformers. As you've
probably guessed, it does not work for continuation-based monads.

Even though these libraries are both being proposed for solving the same problem (exception handling in transformer stacks), that's actually just a narrow overlap between the two. Let's look at some of the things each library handles that the other does not:

- exceptions allows throwing exceptions in many more monads than monad-control works with. In particular, monad-control can
*only*handle throwing exceptions in IO-based stacks. (Note that this actually has nothing to do with monad-control.) - exceptions allows
*catching*exceptions in many more monads as well, in particular continuation based monads. - monad-control allows us to do far more than exception handling.

So the overlap squarely falls into: throwing, catching, and cleaning up from exceptions in a monad transformer stack which can be an instance of MonadMask/MonadBaseControl, which is virtually any stack without short-circuiting or continuations, and is based on IO.

Given that the overlap is relatively narrow, the next question is- if you have a situation that could use either approach- which one should you use? I think this is something that as a community, we should really try to standardize on. It would be beneficial from a library user standpoint if it was well accepted that "oh, I'm going to need a bracket here, so I should use MonadXXX as the constraint," since it will make library building more easily composable.

To help kick off that discussion, let me throw in my more subjective opinions on the topic:

- exceptions is an easier library for people to understand. I've been using monad-control for a while, and frankly I still find it intimidating.
- If you're writing a function that might fail, using MonadThrow as the constraint can lead to much better code composability and more informative error messages. (I'm referring back to 8 ways to report errors in Haskell.)
- exceptions allows for more fine-grained constraints via MonadThrow/MonadCatch/MonadMask.
- monad-control makes it virtually impossible to write an incorrect instance. It's fairly easy to end up writing an invalid MonadMask instance, however, which could easily lead to broken code. This will hopefully be addressed this documentation and education, but it's still a concern of mine.
- monad-control requires more language extensions.
- While there are things that exceptions does that monad-control does not, those are relatively less common.

Overall, I'm leaning in the direction that we should recommend exceptions as the standard, and reserve monad-control as a library to be used for the cases that exceptions doesn't handle at all (like arbitrary control functions). This is despite the fact that, until now, all of my libraries have used monad-control. If the community ends up deciding on exceptions, I agree to (over time) move my libraries in that direction.

### Call for participation: HLPP 2014 - 7th Symposium on High-Level Parallel Programming and Applications

### Announcement: Bang, a drum DSL for Haskell

### Problems using ghc 7.8.2 with options -staticlib and-threaded on osx

### Oliver Charles: A Category for Correct-By-Construction Serializers and Deserializers

Frequently in computer programming we need to work with data in different representations, and we need to work with the data on both sides of said representation. For example, we might have some Haskell data types in memory, which we later serialize to disk. When the user restarts our application, we need to reload this data back into Haskell data types, to allow them to resume work.

Haskell provides us with machinery for doing this serialization via the binary library, which gives us the Binary type class with two methods:

class Binary t where put :: t -> Put get :: Get tget deserializes a sequence of bytes into Haskell values, while put operates in the reverse direction - transforming Haskell values to a sequence of bytes.

Usually, we want the implementations of these methods to be mutual inverses - the computation in get should restore data serialized with put, and vice versa. Unfortunately, nothing in the type system nor the structure of these methods gives us this guarantee - it’s all down to the programmer. I don’t trust myself, so I set out to investigate a more reliable approach.

Ideally, we would like to build up serializers and deserializers from smaller pieces, such that each piece carries its own inverse. For example, we could pair up serialization for a String with its own inverse:

type Serializer a = (Get a, a -> Put) string :: Serializer String string = (get, put)As long as String has a Binary instance where get and put correctly specified, we know that string is going to function as we expect in both directions.

We’re on to something here, but currently this only works for single Strings. What if I have a pair of Strings that I want to serialize? From what we’ve seen so far, there’s no way to combine our bidirectional serializers. Earlier I mentioned that we would like to work with small pieces and compose them - lets see if we can solve this problem for just serialization first.

Serialization *consumes* data. If we have data to serialize, the application of one serializer should consume some of this data, leaving us with slightly less data that we have to continue serializing. By repeated application of serializers, we will eventually have considered the entire structure and will have nothing left to do. This consumption of a structure bit-by-bit suggests that serialization will be a type changing operation, as a record with a field removed is certainly not the same type as its larger record. So let’s try and incorporate that:

Composition of Serializing should now be clear - we just need to compose them one after another:

(.) :: Serializing b c -> Serializing a b -> Serializing a c (Serializing g) . (Serializing f) = Serializing (f >=> g) putTwoStrings :: Serializing (String, String) () putTwoStrings = pString1 . pString2We’ve built a serializer that can serialize a tuple of two strings, and we did so piece-by-piece. While what we have so far is not entirely satisfactory, it seems like we’re heading in the right direction. We’ll come back to this later, but first let’s see if the same ideas translate to deserializers.

Our serializer consumed data, so deserialization is naturally the opposite of consuming data - that is, deserialization *produces* data. When we deserialize we’ll start with nothing, and we’ll deserialize a few bytes into part of our structure one step at a time. Each step of deserialization should take the smaller structure and expand it into a larger structure - eventually leading us to the desired structure. Again, this will be a type changing operation, and we can encode all of this just as we did with Serializing:

As you can see, it’s pretty much exactly the same idea. The only difference is that now each of our deserializers return a slightly *bigger* structure, whereas our serializers would move our structure to something *smaller*.

Just to prove that what we have so far works, we can try this in GHCI:

> let bytes = case putTwoStrings of Serializing p -> runPut (p ("Hello", "World!")) > case getTwoStrings of Deserializing g -> runGet (g ()) (LBS.pack bytes) ("Hello","World!")To carry on working towards our goal, we need to pair the Serializer up with its Deserializer. Unfortunately, what we have so far won’t work:

data Serializer a b = Serializer (a -> Get b) (a -> Put b)Notice here how the types *both* move from a to b - that’s certainly not going to work, as the shape of the data is changing in opposite directions! In Get, a is “smaller” than b, whereas for Put a is “larger” then b. In order to work around this, we just need to swap the order of types in one of these functions - I’ve swapped the order for Put:

This makes sense - if put will shrink our structure, then get can move from this smaller structure back to the original structure. We can express our string1 and string2 serializers now:

string2 :: Serializer (String, String) String string2 = Serializer (\(a, b) -> do put a; return b) (\s -> do { s' <- get; return (s', s) }) string1 :: Serializer String () string1 = Serializer put (\() -> get)We were able to compose things before, and we can certainly compose things here…

(.) :: Serializer b c -> Serializer a b -> Serializer a c (Serializer g g') . (Serializer f f') = Serializer (f >=> g) (g' >=> f') twoStrings :: Serializer (String, String) () twoStrings = string1 . string2However, this has a rather significant problem - can you spot it? Take time to think about this and see if you can work out what’s going wrong.

Did you find it? If we fire up GHCI and have a play with our twoStrings serializer, lets see what we get…

> let bytes = case twoStrings of Serializer _ p -> runPut (p ("A", "B")) > case twoStrings of Serializer g _ -> runGet (g ()) bytes ("B","A")Oh no - that’s not what we wanted at all! The problem is that the order of effects are being reversed. When we put data, we put the first tuple element first, and then the second. However, we’re reading data in the opposite order - expecting the *second* element to be first in the stream, which is clearly not correct. For (String, String) the deserializer works but the tuple is in the wrong order - for other data types this would lead to a runtime exception.

With the current definition of Serializer, there’s simply no way around this - the types won’t let us run effects in different orders. The reason for this is that we can only access the underlying Get computation by having the smaller structure around first. However, we can be sneaky and changes things around just enough to let us run Get in a different order. Now the Get computation is no longer a function, but is a computation that *returns* a function:

With this change we *do* have access to any Get computation we like, and we are free to run them in a different order:

Now it’s clear that both our Put and our Get computations are sequenced in the same order - nice! It turns out that our composition comes with a sane definition of identity too, which means our Serializer can be used with Category:

instance Category Serializer where (Serializer g g') . (Serializer f f') = Serializer (do buildF <- g buildG <- f return (buildF . buildG)) (g' >=> f') id = Serializer (return id) return Serializing Through Heterogeneous ListsWe have finally reached a nice core to our solution, but the surface API isn’t really working out. We had to write different Serializers for both (String, String) and String, which is certainly not desirable. Ultimately, we would like to be able to work with just one Serializer for String, and compose them however we please.

Unfortunately, working with tuples is causing us the real pain here. The reason for this is that tuples don’t really have any structure that would allow us to work with them in any sort of principled manner. Instead, what we can do is use a heterogeneous list, which we can recurse on just like an ordinary linked list. So, we introduce a type for heterogeneous lists:

data List :: [*] -> * where Nil :: List '[] Cons :: a -> List as -> List (a ': as)And now we can use the new poly-kinded Category to upgrade Serializer to work with these lists:

data Serializer :: [*] -> [*] -> * where Serializer :: (Get (List a -> List b)) -> (List b -> PutM (List a)) -> Serializer a b instance Category Serializer where (Serializer g g') . (Serializer f f') = Serializer (do mkB <- g mkA <- f return (mkB . mkA)) (g' >=> f') id = Serializer (return id) returnThis was quite a detour, and has this really helped us? Indeed it has, as we can now we can write a much more general Serializer String:

string :: Serializer as (String ': as) string = Serializer (do a <- get; return (Cons a)) (\(Cons a as) -> do put a; return as)The type of string now indicates that this Serializer can serialize anything that starts with a String, and likewise when deserializing it expects a String to be the first element. This composes exactly as we’d expect:

twoStrings :: Serializer as (String ': String ': as) twoStrings = string . stringAll we need to do is unwrap the List resulting from a Get or wrap up data in a List for Put and we’re good to go:

> let bytes = case twoStrings of Serializer _ p -> runPut (void $ p ("A" `Cons` ("B" `Cons` Nil))) > case twoStrings of Serializer g _ -> runGet (($ Nil) <$> g) bytes Cons "A" (Cons "B" Nil) Destructuring Data Via PrismsThe API we’ve built works really well if we already have data decomposed into a List, but we don’t normally have this luxury. This means we need a way to convert from a data type to it’s constituent parts, and this is exactly the functionality that Prisms in the lens library provide us with. While Prisms can be a little hard to get your head around, it can be illuminating to experiment with them in GHCI:

> review _Cons (10, []) [10] > review _Cons (10, [20]) [10,20] > review _Cons (1, [2..5]) [1,2,3,4,5] > preview _Cons [10, 20, 30] Just (10,[20,30]) > preview _Cons [10] Just (10,[]) > preview _Cons [] NothingPrisms have two main operations: review and preview. review lets us construct some data out of its parts - above we use _Cons with (10, [20]), which is the same as (10 : [20]) - resulting in the list [10, 20]. preview lets us go the other way, which is the same idea as pattern matching on a constructor. If we preview _Cons on non-empty lists, then the pattern matching succeeds and the list is separated into its head and tail. However, we can’t pattern match with _Cons on an empty list, so preview returns Nothing - which corresponds to a pattern match failure.

Armed with Prism, we’re almost entirely ready to go! The only problem is that Prism normally works with tuples, which we’ve already seen aren’t a great data for our needs. It’s entirely mechanical to convert between tuples and List, so we simply move between them with a type class. Combining this all together, we have the following:

class ListIso a b | a -> b, b -> a where _HList :: Iso' b (List a) usePrism :: ListIso a b => Prism' d b -> Serializer a '[d] usePrism p = Serializer get put where put (Cons d Nil) = do Just tuple <- return (preview p d) return (tuple ^. _HList) get = return $ \hlist -> Cons (review p (hlist ^. from _HList)) NilNow we are free to use this on our data types, just as we’d expect:

instance ListIso '[a, b] (a, b) where _HList = iso (\(a, b) -> Cons a (Cons b Nil)) (\(Cons a (Cons b Nil)) -> (a, b)) data PairOfStrings = PairOfStrings String String makePrisms ''PairOfStrings pairOfStrings :: Serializer '[] '[PairOfStrings] pairOfStrings = usePrism _PairOfStrings . string . string ChoicesIf you look closely at our definition of usePrism you might have seen something suspicious. Here’s the relevant code:

usePrism = ... where put (Cons d Nil) = do Just tuple <- return (Lens.preview p d) return (tuple ^. _HList)In our put definition, we are assuming that Lens.preview is always returning a Just value. However, we saw earlier that this isn’t necessarily the case - the Prism corresponds to one of potentially many constructors. If we try and use usePrism with a prism that doesn’t match our expectations, then things go horribly wrong:

data Strings = PairOfStrings String String | ThreeStrings String String String makePrims ''Strings > case pairOfStrings of Serializer _ p -> runPut (void $ p (ThreeStrings "Uh" "Oh" "!" `Cons` Nil)) "*** Exception: Pattern match failure in do expression at ...What we need to do is to allow for choice - if we have multiple possible prisms, then we need to consider each one. This corresponds to exhaustive pattern matching in case analysis.

It turns out choice is relatively straight forward to add in. Get is already an instance of MonadPlus, so we get choice there for free. Put however is a little more involved, as it doesn’t have an instance of MonadPlus. The best solution I’ve found thus far is to wrap up our Put computation inside Maybe, but this isn’t entirely satisfactory. Unfortunately binary doesn’t quite export enough to have a less expensive solution (PairS doesn’t have its oconstructor exported).

Monoid is a sensible type class to use for alternatives - choice is associative, and there is a sane identity (an always-failing Serializer). Thus the final definition of Serializer and its associated type classes are:

data Serializer :: [*] -> [*] -> * where Serializer :: (Get (List a -> List b)) -> (List b -> Maybe (PutM (List a))) -> Serializer a b instance Category Serializer where (Serializer g g') . (Serializer f f') = Serializer (g >>= \b -> f >>= \a -> return (b . a)) (\a -> do putF <- g' a let (b, lbs) = runPutM putF putG <- f' b return (putLazyByteString lbs >> putG)) id = Serializer (return id) (return . return) instance Monoid (Serializer a b) where mempty = Serializer mzero (const mzero) (Serializer g p) `mappend` (Serializer g' p') = Serializer (g `mplus` g') (\i -> p i `mplus` p' i)Armed with this final definition of Serializer, we’re almost ready to provide a complete definition of serializing our Strings type. We need to provide a little extra information however, which allows us to disambiguate constructors. This is because if we are deserializing, if I read two strings I don’t necessarily know constructor to choose (yes, if we considered EOF this could be done, I’m going for brevity). You can find the definition of disambiguate in the full code listing.

Thus the final user-facing code is just:

strings :: Serializer '[] '[Strings] strings = mconcat [ usePrism _PairOfStrings . disambiguate 1 . string . string , usePrism _ThreeStrings . disambiguate 2 . string . string . string ]And just to prove it all works…

> let Just putter = case strings of Serializer _ p -> p (ThreeStrings "A" "B" "C" `Cons` Nil) bytes = runPut (void putter) > case strings of Serializer g _ -> runGet (($ Nil) <$> g) bytes Cons (ThreeStrings "A" "B" "C") Nil > let Just putter = case strings of Serializer _ p -> p (PairOfStrings "Hello" "World!" `Cons` Nil) bytes = runPut (void putter) > case strings of Serializer g _ -> runGet (($ Nil) <$> g) bytes Cons (PairOfStrings "Hello" "World!") Nil Final ThoughtsWe’ve seen that it’s possible to build correct-by-construction serializers and deserializers, and we got there by breaking down our problem into small parts and finding a good way to combine the parts together. Hopefully, I’ve illustrated some of the problems that arise from a naive solution, and how these problems guided us towards an implementation that is both more correct and more flexible.

Serializer is still not perfect however. With the idea of choice above, there’s no way to indicate exhaustive pattern matching. For example, in strings we are considering both constructors, yet put strings returns Maybe Put. This isn’t particularly satisfactory, because it should now always be possible to serialize this data type! On a similar note, it becomes harder to get compile time checks about exhaustive pattern matching, because we’re no longer doing case analysis explicitly. This is an interesting problem to me, and one that I would still like to solve.

There is also a bit more work that we might want to consider doing with Get and Put, which is to use a different concept of choice. There are other options than using Maybe - for example we could use lists which would inform us of *all* possible serializations for a data type, which might provide better debugging information than simply using the first one that matches.

I’d like to conclude by mentioning that the ideas here aren’t particularly new. In 2010 Rendel and Ostermann presented a solution using a category of partial isomorphisms and product functors from this category to Hask, which lead to various libraries on Hackage such as invertible-syntax, and boomerang. At ZuriHack, Martijn van Steenbergen presented the latest version of JsonGrammar, which uses a free category to describe operations on a JSON AST, and also illustrated how one can use prisms to provide a modern vocabulary for partial isomorphisms. json-grammar uses a stack-prism data type, which achieves the same goal as using heterogeneous lists, but does require another Template Haskell call (makeStackPrisms).

While I’m happy with the solution so far, I haven’t finished playing around with this. It’s unclear to me how this plays with recursive data types (for example, does this work for lists? What about trees?), and I need to learn more about stack-prism to see if using heterogenous lists impedes composition (as Sjoerd Visscher has warned me!). Hopefully I’ll be able to start using what I have so far in production, iron out the last problems, and release this to Hackage in the near future.

Thanks for reading, a full code listing can be found on Github

### New Functional Programming Job Opportunities

### Is there a functional concept similar to Union-Find?

Obviously, one could do a naive translation, such as simply using a monad for effects or doing incremental updates, but it seems to me that in functional programming, it would make sense to make it a monoid and stuff like that.

submitted by tailcalled[link] [7 comments]