Planet Haskell

July 06, 2015

Roman Cheplyaka

How Haskell handles signals

How is it possible to write signal handlers in GHC Haskell? After all, the set of system calls allowed inside signal handlers is rather limited. In particular, it is very hard to do memory allocation safely inside a signal handler; one would have to modify global data (and thus not be reentrant), call one of the banned syscalls (brk, sbrk, or mmap), or both.

On the other hand, we know that almost any Haskell code requires memory allocation. So what’s the trick?

The trick is that a Haskell handler is not installed as a true signal handler. Instead, a signal is handled by a carefully crafted RTS function generic_handler (rts/posix/Signals.c). All that function does (assuming the threaded RTS) is write the signal number and the siginfo_t structure describing the signal to a special pipe (called the control pipe, see GHC.Event.Control).

The other end of this pipe is being watched by the timer manager thread (GHC.Event.TimerManager). When awaken by a signal message from the control pipe, it looks up the handler corresponding to the signal number and, in case it’s an action, runs it in a new Haskell thread.

The signal handlers are stored in a global array, signal_handlers (GHC.Conc.Signal). When you install a signal action in Haskell, you put a stable pointer to the action’s code into the array cell corresponding to the signal number, so that the timer thread could look it up later when an actual signal is delivered.

See also https://ghc.haskell.org/trac/ghc/wiki/Commentary/Rts/Signals.

July 06, 2015 08:00 PM

Daniel Mlot (duplode)

Applicative Archery

It is widely agreed that the laws of the Applicative class are not pretty to look at.

pure id <*> v = v                            -- identity
pure f <*> pure x = pure (f x)               -- homomorphism
u <*> pure y = pure ($ y) <*> u              -- interchange
pure (.) <*> u <*> v <*> w = u <*> (v <*> w) -- composition

Monad laws, in comparison, not only look less odd to begin with but can also be stated in a much more elegant way in terms of Kleisli composition (<=<). Shouldn’t there be an analogous nice presentation for Applicative as well? That became a static question in my mind while I was studying applicative functors many moons ago. After finding surprisingly little commentary on this issue, I decided to try figuring it out by myself. 1

Let’s cast our eye over Applicative:

class Functor t => Applicative t where
    pure  :: a -> t a
    (<*>) :: t (a -> b) -> t a -> t b

If our inspiration for reformulating Applicative is Kleisli composition, the only sensible plan is to look for a category in which the t (a -> b) functions-in-a-context from the type of (<*>) are the arrows, just like a -> t b functions are arrows in a Kleisli category. Here is one way to state that plan in Haskell terms:

> class Applicative t => Starry t where
>     idA  :: t (a -> a)
>     (.*) :: t (b -> c) -> t (a -> b) -> t (a -> c)
> 
>     infixl 4 .*
> -- The Applicative constraint is wishful thinking:
> -- When you wish upon a star...

The laws of Starry are the category laws for the t (a -> b) arrows:

idA .* v = v                -- left identity
u .* idA = u                -- right identity
u .* v .* w = u .* (v .* w) -- associativity

The question, then, is whether it is possible to reconstruct Applicative and its laws from Starry. The answer is a resounding yes! The proof is in this manuscript, which I have not transcribed here as it is a little too long for a leisurely post like this one 2. The argument is set in motion by establishing that pure is an arrow mapping from Hask to a Starry category, and that both (<*>) and (.*) are arrow mappings in the opposite direction. That leads to several naturality properties of those functors, from which the Applicative laws can be obtained. Along the way, we also get definitions for the Starry methods in terms of the Applicative ones…

>     idA = pure id
>     u .* v = fmap (.) u <*> v

… and vice-versa:

pure x = fmap (const x) idA
u <*> v = fmap ($ ()) (u .* fmap const v)

Also interesting is how the property relating fmap and (<*>)

fmap f u = pure f <*> u

… now tells us that a Functor is the result of composing the pure functor with the (<*>) functor. That becomes more transparent if we write it point-free:

fmap = (<*>) . pure

In order to ensure Starry is equivalent to Applicative we still need to prove the converse, that is, obtain the Starry laws from the Applicative ones and the definitions of idA and (.*) just above. That is not difficult; all it takes is substituting the definitions in the Starry laws and:

  • For left identity, noticing that (id .) = id.

  • For right identity, applying the interchange law and noticing that ($ id) . (.) is id in a better disguise.

  • For associativity, using the laws to move all (.) to the left of the (<*>) and then verifying that the resulting messes of dots in both sides are equivalent.

As a tiny example, here is the Starry instance of Maybe

instance Starry Maybe where
    idA              = Just id
    Just g .* Just f = Just (g . f)
    _      .* _      = Nothing

… and the verification of the laws for it:

-- Left identity:
idA .* u = u
Just id .* u = u
-- u = Nothing
Just id .* Nothing = Nothing
Nothing = Nothing
-- u = Just f
Just id .* Just f = Just f
Just (id . f) = Just f
Just f = Just f

-- Right identity:
u .* idA = u
u .* Just id = u
-- u = Nothing
Nothing .* Just id = Nothing
Nothing = Nothing
-- u = Just g
Just g .* Just id = Just g
Just (g .* id) = Just g
Just g = Just g

-- Associativity:
u .* v .* w = u .* (v .* w)
-- If any of u, v and w are Nothing, both sides will be Nothing.
Just h .* Just g .* Just f = Just h .* (Just g .* Just f)
Just (h . g) .* Just f = Just h .* (Just (g . f))
Just (h . g . f) = Just (h . (g . f))
Just (h . g . f) = Just (h . g . f)

It works just as intended:

GHCi> Just (2*) .* Just (subtract 3) .* Just (*4) <*> Just 5
Just 34
GHCi> Just (2*) .* Nothing .* Just (*4) <*> Just 5
Nothing

I do not think there will be many opportunities to use the Starry methods in practice. We are comfortable enough with applicative style, through which we see most t (a -> b) arrows as intermediates generated on demand, rather than truly meaningful values. Furthermore, the Starry laws are not truly easier to prove (though they are certainly easier to remember!). Still, it was an interesting exercise to do, and it eases my mind to know that there is a neat presentation of the Applicative laws that I can relate to.

This post is Literate Haskell, in case you wish to play with Starry in GHCi (here is the raw .lhs file ).

> instance Starry Maybe where
> instance Starry [] where
> instance Starry ((->) a) where
> instance Starry IO where

As for proper implementations in libraries, the closest I found was Data.Semigroupoid.Static, which lives in Edward Kmett’s semigroupoids package. “Static arrows” is the actual technical term for the t (a -> b) arrows. The module provides…

newtype Static f a b = Static { runStatic :: f (a -> b) }

… which uses the definitions shown here for idA and (.*) as id and (.) of its Category instance.

<section class="footnotes">
  1. There is a reasonably well-known alternative formulation of Applicative: the Monoidal class as featured in this post by Edward Z. Yang. While the laws in this formulation are much easier to grasp, Monoidal feels a little alien from the perspective of a Haskeller, as it shifts the focus from function shuffling to tuple shuffling.

  2. Please excuse some oddities in the manuscript, such as off-kilter terminology and weird conventions (e.g. consistently naming arguments in applicative style as w <*> v <*> u rather than u <*> v <*> w in applicative style). The most baffling choice was using id rather than () as the throwaway argument to const. I guess I did that because ($ ()) looks bad in handwriting.

</section>
Comment on GitHub (see the full post for a reddit link)

by Daniel Mlot at July 06, 2015 08:00 PM

The GHC Team

GHC Weekly News - 2015/07/06

Hi *,

Welcome for the latest entry in the GHC Weekly News. The past week, GHC HQ met up to discuss the status of the approaching 7.10.2 release.

7.10.2 status

After quite some delay due to a number of tricky regressions in 7.10.1, 7.10.2 is nearing the finish line. Austin cut release candidate 2 on Friday and so far the only reports of trouble appear to be some validation issues, most of which have already been fixed thanks to Richard Eisenberg.

7.10.2 will include a number of significant bug-fixes. These include,

  • #10521, where overlap of floating point STG registers weren't properly accounted for, resulting in incorrect results in some floating point computations. This was fixed by the amazing Reid Barton.
  • #10534, a type-safety hole enabling a user to write unsafeCoerce with data families and coerce. Fix due to the remarkable Richard Eisenberg.
  • #10538, where some programs would cause the simplifier to emit an empty case, resulting in runtime crashes. Fix due to the industrious Simon Peyton Jones.
  • #10527, where the simplifier would expend a great deal of effort simplifying arguments which were never demanded by the callee.
  • #10414, where a subtle point of the runtime system's black-holing mechanism resulting in hangs on a carefully constructed testcase.
  • #10236, where incorrect DWARF annotations would be generated, resulting in incorrect backtraces. Fixed by Peter Wortmann
  • #7450, where cached free variable information was being unnecessarily dropped by the specialiser, resulting in non-linear compile times for some programs.

See the status page for a complete listing of issues fixed in this release.

In the coming days we will being working with FP Complete to test the pre-release against Stackage. While Hackage tends to be too large to build in bulk, the selection of packages represented in Stackage is feasible to build and is likely to catch potential regressions. Hopefully this sort of large-scale validation will become common-place for future releases.

If all goes well, 7.10.2 will mark the end of the 7.10 series. However, there is always the small possibility that a major regression will be found. In this case we will cut a 7.10.3 release which will include a few patches which didn't make it into 7.10.2.

Other matters

It has been suggested in #10601 that GHC builds should ship with DWARF symbols for the base libraries and runtime system. While we all want to see this new capability in users' hands, 7.10.2 will, like 7.10.1, not be shipping with debug symbols. GHC HQ will be discussing the feasibility of including debug symbols with 7.12 in the future. In the meantime, we will be adding options to build.mk to make it easier for users to build their own compilers with debug-enabled libraries.

In this week's GHC meeting the effort to port GHC's build system to the Shake? build system briefly came up. Despite the volume of updates on the Wiki Simon reports that the project is still moving along. The current state of the Shake-based build system can be found on Github.

While debugging #7540 it became clear that there may be trouble lurking in the profiler. Namely when profiling GHC itself lintAnnots is showing up strongly where it logically should not. This was previously addressed in #10007, which was closed after a patch by Simon Marlow was merged. As it appears that this did not fully resolve the issue I'll be looking further into this.

~ Ben

by bgamari at July 06, 2015 04:25 PM

Well-Typed.Com

Dependencies for Cabal Setup.hs files and other goodies

No untracked dependencies!

Years ago, back when Isaac Potoczny-Jones and others were defining the Cabal specification, the big idea was to make Haskell software portable to different environments. One of the mantras was “no untracked dependencies!”.

The problem at the time was that Haskell code had all kinds of implicit dependencies which meant that while it worked for you, it wouldn’t build for me. For example, I might not have some other module that it needed, or the right version of the module.

So of course that’s what the build-depends in .cabal files is all about, requiring that the author of the code declare just what the code requires of its environment. The other important part is that the build system only lets your code see the dependencies you’ve declared, so that you don’t accidentally end up with these untracked dependencies.

This mantra of no untracked dependencies is still sound. If we look at a system like nix, part of what enables it to work so well is that it is absolutely fanatical about having no untracked dependencies.

Untracked dependencies?!

One weakness in the original Cabal specification is with Setup.hs scripts. These scripts are defined in the spec to be the entry point for the system. According to the Cabal spec, to build a package you’re required to compile the Setup.hs script and then use its command line interface to get things done. Because in the original spec the Setup.hs is the first entry point, it’s vital that it be possible to compile Setup.hs without any extra fuss (the runhaskell tool was invented just to make this possible, and to make it portable across compilers).

But by having the Setup.hs as the primary entry point, it meant that it’s impossible to reliably use external code in a Setup.hs script, because you cannot guarantee that that code is pre-installed. Going back to the “no untracked dependencies” mantra, we can see of course that all dependencies of Setup.hs scripts are in fact untracked!

This isn’t just a theoretical problem. Haskell users that do have complex Setup.hs scripts often run into versioning problems, or need external tools to help them get the pre-requisite packages installed. Or as another example: Michael Snoyman noted earlier this year in a diagnosis of an annoying packaging bug that:

As an aside, this points to another problematic aspect of our toolchain: there is no way to specify constraints on dependencies used in custom Setup.hs files. That’s actually caused more difficulty than it may sound like, but I’ll skip diving into it for now.

The solution: track dependencies!

As I said, the mantra of no untracked dependencies is still sound, we just need to apply it more widely.

These days the Setup.hs is effectively no longer a human interface, it is now a machine interface used by other tools like cabal or by distro’s install scripts. So we no longer have to worry so much about Setup.hs scripts always compiling out of the box. It would be acceptable now to say that the first entry point for a tool interacting with a package is the .cabal file, which might list the dependencies of the Setup.hs. The tool would then have to ensure that those dependencies are available when compiling the Setup.hs.

So this is exactly what we have now done. Members of the Industrial Haskell Group have funded us to fix this long standing problem and we have recently merged the solution into the development version of Cabal and cabal-install.

From a package author’s point of view, the solution looks like this: in your .cabal file you can now say:

build-type: Custom

custom-setup
  setup-depends: base >= 4.6,
                 directory >= 1.0,
                 Cabal >= 1.18 && < 1.22,
                 acme-setup-tools == 0.2.*

So it’s a new stanza, like libraries or executables, and like these you can specify the library dependencies of the Setup.hs script.

Now tools like cabal will compile the Setup.hs script with these and only these dependencies, just like it does normally for executables. So no more untracked dependencies in Setup.hs scripts. Newer cabal versions will warn about not using this new section. Older cabal versions will ignore the new section (albeit with a warning). So over time we hope to encourage all packages with custom setup scripts to switch over to this.

In addition, the Setup.hs script gets built with CPP version macros (MIN_VERSION_{pkgname}) available so that the code can be made to work with a wider range of versions of its dependencies.

In the solver…

So on the surface this is all very simple and straightforward, a rather minor feature even. In fact it’s been remarkably hard to implement fully for reasons I’ll explain, but the good news is that it works and the hard work has also gotten us solutions to a couple other irksome problems.

Firstly, why isn’t it trivial? It’s inevitable that sooner or later you will find that your application depends on one package that has setup deps like Cabal == 1.18.* and another with setup deps like Cabal == 1.20.*. At that point we have a problem. Classically we aim to produce a build plan that uses at most one version of each package. We do that because otherwise there’s a danger of type errors from using multiple versions of the same package. Here with setup dependencies there is no such danger: it’s perfectly possible for me to build one setup script with one version of the Cabal library and another script with a different Cabal version. Because these are executables and not libraries, the use of these dependencies does not “leak”, and so we would be safe to use different versions in different places.

So we have extended the cabal solver to allow for limited controlled use of multiple versions of the same package. The constraint is that all the “normal” libraries and exes all use the same single version, just as before, but setup scripts are allowed to introduce their own little world where independent choices about package versions are allowed. To keep things sane, the solver tries as far as possible not to use multiple versions unless it really has to.

If you’re interested in the details in the solver, see Edsko’s recent blog post.

Extra goodies

This work in the solver has some extra benefits.

Improve Cabal lib API without breaking everything

In places the Cabal library is a little crufty, and the API it exposes was never really designed as an API. It has been very hard to fix this because changes in the Cabal library interface break Setup.hs scripts, and there was no way for packages to insulate themselves from this.

So now that we can have packages have proper dependencies for their custom Setup.hs, the flip side is that we have an opportunity to make breaking changes to the Cabal library API. We have an opportunity to throw out the accumulated cruft, clean up the code base and make a library API that’s not so painful to use in Setup.hs scripts.

Shim (or compat) packages for base

Another benefit is that the new solver is finally able to cope with having “base shim” packages, as we used in the base 3.x to 4.x transition. For two GHC releases, GHC came with both base-3.x and base-4.x. The base-4 was the “true” base, while the base-3 was a thin wrapper that re-exported most of base-4 (and syb), but with some changes to implement the old base-3 API. At the time we adapted cabal to cope with this situation of having two versions of a package in a single solution.

When the new solver was implemented however support for this situation was not added (and the old solver implementation was retained to work with GHC 6.12 and older).

This work for setup deps has made it relatively straightforward to add support for these base shims. So next time GHC needs to make a major bump to the version of base then we can use the same trick of using a shim package. Indeed this might also be a good solution in other cases, perhaps cleaner than all these *-compat packages we’ve been accumulating.

It has also finally allowed us to retire the old solver implementation.

Package cycles involving test suites and benchmarks

Another feature that is now easy to implement (though not actually implemented yet) is dealing with the dependency cycles in packages’ test suites and benchmarks.

Think of a core package like bytestring, or even less core like Johan’s cassava csv library. These packages have benchmarks that use the excellent criterion library. But of course criterion is a complex beast and itself depends on bytestring, cassava and a couple dozen other packages.

This introduces an apparent cycle and cabal will fail to find an install plan. I say apparent cycle because there isn’t really a cycle: it’s only the benchmark component that uses criterion, and nothing really depends on that.

Here’s another observation: when benchmarking a new bytestring or cassava, it does not matter one bit that criterion might be built against an older stable version of bytestring or cassava. Indeed it’s probably sensible that we use a stable version. It certainly involves less rebuilding: I don’t really want to rebuild criterion against each minor change in bytestring while I’m doing optimisation work.

So here’s the trick: we break the cycle by building criterion (or say QuickCheck or tasty) against another version of bytestring, typically some existing pre-installed one. So again this means that our install plan has two versions of bytestring in it: the one we mean to build, and the one we use as a dependency for criterion. And again this is ok, just as with setup dependencies, because dependencies of test suites and benchmarks do not “leak out” and cause diamond dependency style type errors.

One technical restriction is that the test suite or benchmark must not depend on the library within the same package, but must instead use the source files directly. Otherwise there would genuinely be a cycle.

Now in general when we have multiple components in a .cabal file we want them to all use the same versions of their dependencies. It would be deeply confusing if a library and an executable within the same package ended up using different versions of some dependency that might have different behaviour. Cabal has always enforced this, and we’re not relaxing it now. The rule is that if there are dependencies of a test suite or benchmark that are not shared with the library or executable components in the package, then we are free to pick different versions for those than we might pick elsewhere within the same solution.

As another example – that’s nothing to do with cycles – we might pick different versions of QuickCheck for different test suites in different packages (though only where necessary). This helps with the problem that one old package might require QuickCheck == 2.5.* while another requires QuickCheck == 2.8.*. But it’d also be a boon if we ever went through another major QC-2 vs QC-3 style of transition. We would be able to have both QC-2 and QC-3 installed and build each package’s test suite against the version it requires, rather than freaking out that they’re not the same version.

Private dependencies in general

Technically, this work opens the door to allowing private dependencies more generally. We’re not pursuing that at this stage, in part because it is not clear that it’s actually a good idea in general.

Mark Lentczner has pointed out the not-unreasonable fear that once you allow multiple versions of packages within the same solution it will in practice become impossible to re-establish the situation where there is just one version of each package, which is what distros want and what most people want in production systems.

So that’s something we should consider carefully as a community before opening those flood gates.

by duncan at July 06, 2015 03:10 PM

Ken T Takusagawa

[dcqhszdf] ChaCha cipher example

The ChaCha cipher seems not to get as much love as Salsa20. Here is a step-by-step example of the ChaCha round function operating on a matrix. The format of the example is loosely based on the analogous example in section 4.1 of this Salsa20 paper: D. J. Bernstein. The Salsa20 family of stream ciphers. Document ID: 31364286077dcdff8e4509f9ff3139ad. URL: http://cr.yp.to/papers.html#salsafamily. Date: 2007.12.25.

original column [a;b;c;d]
61707865
04030201
14131211
00000007

after first line of round function
65737a66
04030201
14131211
7a616573

after second line of round function
65737a66
775858a7
8e747784
7a616573

after third line of round function
dccbd30d
775858a7
8e747784
aab67ea6

after all 4 lines of round function, i.e., quarter round
dccbd30d
395746a7
392af62a
aab67ea6

original matrix, with the same original column above
61707865 3320646e 79622d32 6b206574
04030201 08070605 0c0b0a09 100f0e0d
14131211 18171615 1c1b1a19 201f1e1d
00000007 00000000 01040103 06020905

one round (4 quarter rounds on columns)
dccbd30d 109b031b 0eb5ed20 4483ec2b
395746a7 d88a8f5f 7a292fab b06c9135
392af62a 6ac28db6 dfbce7ba a234a188
aab67ea6 e8383c7a 8d694938 0791063e

after shift rows
dccbd30d 109b031b 0eb5ed20 4483ec2b
d88a8f5f 7a292fab b06c9135 395746a7
dfbce7ba a234a188 392af62a 6ac28db6
0791063e aab67ea6 e8383c7a 8d694938

after another 4 quarter rounds on columns
06b44c34 69a94c11 2ce99b08 216830d1
29b215bd 721e2a33 f0a18097 708e1ee5
2b0e8de3 b801251f 42265fb2 696de1c2
e6fef362 c96c6325 c6cc126e 82c0635a

unshifting rows (concludes 1 double round)
06b44c34 69a94c11 2ce99b08 216830d1
708e1ee5 29b215bd 721e2a33 f0a18097
42265fb2 696de1c2 2b0e8de3 b801251f
c96c6325 c6cc126e 82c0635a e6fef362

after 8 rounds (4 double rounds)
f6093fbb efaf11c6 8bd2c9a4 bf1ff3da
bf543ce8 c46c6b5e c717fe59 863195b1
2775d1a0 babe2495 1b5c653e df7dc23c
5f3e08d7 041df75f f6e58623 abc0ab7e

Adding the original input to the output of 8 rounds
5779b820 22cf7634 0534f6d6 2a40594e
c3573ee9 cc737163 d3230862 9640a3be
3b88e3b1 d2d53aaa 37777f57 ff9ce059
5f3e08de 041df75f f7e98726 b1c2b483

reading the above as bytes, little endian
20 b8 79 57 34 76 cf 22 d6 f6 34 05 4e 59 40 2a
e9 3e 57 c3 63 71 73 cc 62 08 23 d3 be a3 40 96
b1 e3 88 3b aa 3a d5 d2 57 7f 77 37 59 e0 9c ff
de 08 3e 5f 5f f7 1d 04 26 87 e9 f7 83 b4 c2 b1

same as above but with 20000 rounds (10000 double rounds)
11 a3 0a d7 30 d2 a3 dc d8 ad c8 d4 b6 e6 63 32
72 c0 44 51 e2 4c ed 68 9d 8d ff 27 99 93 70 d4
30 2e 83 09 d8 41 70 49 2c 32 fd d9 38 cc c9 ae
27 97 53 88 ec 09 65 e4 88 ff 66 7e be 7e 5d 65

The example was calculated using an implementation of ChaCha in Haskell, whose end results agree with Bernstein's C reference implementation. The Haskell implementation is polymorphic, allowing as matrix elements any data type (of any word width) implementing Bits, and parametrizable to matrices of any size 4xN. (Security is probably bad for N not equal to 4. For word width different from 32, you probably want different rotation amounts.) The flexibility comes at a cost: the implemention is 3000 times slower than Bernstein's reference C implementation (which is in turn is slower than SIMD optimized assembly-language implementations).

Also included in the same project is a similar Haskell implementation of Salsa20, parametrized to matrices of any size MxN because of the more regular structure of the Salsa20 quarter round function compared to ChaCha. We demonstrate taking advantage of polymorphism to use the same code both to evaluate Salsa20 on Word32 and to generate C code for the round function.

by Ken ([email protected]) at July 06, 2015 04:15 AM

Yesod Web Framework

yesod-table

Announcing yesod-table

Over the last two years, I've seen the need for safe dynamic table-building in half a dozen yesod projects I've worked on. After several design iterations, the result of this experience is yesod-table, which saw its first stable release last week. This blog post will contain code excerpts, but you can also look at the documentation the full example app on github, which can be compiled and run.

Naive Solution

Before getting into specifics about yesod-table, I want to take a look at the naive table-building strategy and identify the common pitfalls. Let's say that you have a data types Color and Person:

data Color = Red | Green | Blue | Purple
  deriving (Show)
data Person = Person
  { firstName     :: Text
  , lastName      :: Text
  , age           :: Int
  , favoriteColor :: Color
  }

We have a list of Person (let's call it people), and we want to show them all in a table. You could write out a hamlet file like this:

<table>
  <thead>
    <tr>
      <th>First Name</th>
      <th>Last Name</th>
      <th>Age</th>
  <tbody>
    $forall p <- people
      <tr>
        <td>#{firstName p}
        <td>#{lastName p}
        <td>#{show (age p)}

And there it is. This is the simplest solution to building a table. In fact, if you've worked on web applications for any length of time, you've probably written code like this before. I've implemented this pattern in PHP+html, in rails+haml, and in yesod+hamlet projects. And every time, it is unsatisfactory.

Problems With Naive Solution

Let's take a look at three reasons why this solution leaves us wanting something more:

  • Duplication. After building a few tables this way, you realize that you are copying the HTML elements and the list iteration ($forall) every time.
  • Non-composability. If I want to build a similar table, one that shows the same fields but additionally has a column for favoriteColor, I have to copy the whole thing. I can't glue another piece onto the end.
  • Breakable Invariant. If we do decide to add a favoriteColor column, we might try simply adding <td>#{show (favoriteColor p)} to the end. This would cause incorrect behavior at runtime, because we would have forgotten to add <th>Favorite Color to the table header. The problem is that we have an invariant not captured by the type system: thead and the tbody loop must have the same number of <th>/<td> elements, and the order must match.

In particular, the last issue (breakable invariant) has been a source of great pains to me before. On a three-column table, you are less likely to forget the <th> or put it in the wrong place. As the table gets larger though (six or more columns), these mistakes become easier to make, and it's harder to be sure that you did the right thing until you see it at runtime.

Example with yesod-table

So let's take a look at how yesod-table addresses these issues. The module it provides should be imported as follows:

import Yesod.Table (Table)
import qualified Yesod.Table as Table

Let's build the same table we saw earlier:

peopleBasicInfoTable :: Table site Person
peopleBasicInfoTable = mempty
  <> Table.text   "First Name" firstName
  <> Table.text   "Last Name"  lastName
  <> Table.string "Age"        (show . age)

And then we can feed it data and render it with buildBootstrap:

-- Although it's called buildBootstrap, it builds a table just fine
-- if you aren't using bootstrap. It just adds bootstrap's table classes.
getExamplePeopleR = defaultLayout $ Table.buildBootstrap peopleTable people

Explanation of Internals

The key to this approach is looking at a table pattern (called a Table in this library) as a collection of columns, not a collection of rows. From the yesod-table source, we have:

newtype Table site a = Table (Seq (Column site a))
  deriving (Monoid)

data Column site a = Column
  { header :: !(WidgetT site IO ())
  , cell :: !(a -> WidgetT site IO ()) 
  }

Each column is just the content that will go in the <th> (the value of header) and a function that, given the data for a table row, will produce the content that belongs in the <td>. A table is trivially a collection of columns and gets a Monoid instance from Seq for free (for those unfamiliar, Seq a is like [a] but with different performance characteristics). Consequently, any two Tables that are parameterized over the same types can be concatenated. As a final note of explanation, the Table.text function that we saw above just a helper for building singleton tables. So, the three Tables below are equivalant:

import qualified Data.Sequence as Seq
import qualified Data.Text as Text
-- These three generate a single-column table that displays the age.
reallyEasyToReadTable, easyToReadTable, hardToReadTable :: Table site Person
reallyEasyToReadTable = Table.int "Age" age
easyToReadTable = Table.text "Age" (Text.pack . show . age)
hardToReadTable = Table.Table $ Seq.singleton $ Table.Column 
  (toWidget $ toHtml "Age")
  (toWidget . toHtml . show . age)

As should be clear, the convenience functions for singleton Tables should always be preferred.

How Is This Better?

Now to address the most important question: Why is this better than what we had earlier? Firstly, consider the issue of the breakable invariant. This is now a non-issue. Imagine that we modified the earlier table to show a person's favorite color as well:

peopleFullInfoTable1 :: Table site Person
peopleFullInfoTable1 = mempty
  <> Table.text   "First Name"     firstName
  <> Table.text   "Last Name"      lastName
  <> Table.text   "Age"            (show . age)
  <> Table.string "Favorite Color" (show . favoriteColor)

The table is correct by construction. You cannot forget the column header because it's part of the Column data type. You're less likely to make this mistake, because now that information is directly beside the content-extracting function, but even if you somehow typed this instead, you would get a compile-time error:

  <> Table.string (show . favoriteColor)

Secondly, we can look at duplication. All the table-rendering logic is moved into buildBootstrap (and you can write your own table renderer if that one is not satisfactory). The Table that we are using now has neither the HTML elements nor the list iteration that we dealt with earlier.

Finally, we can look at composability. As an alternative way of adding the column for a person's favorite color, we could write:

peopleFullInfoTable2 :: Table site Person
peopleFullInfoTable2 = mempty
  <> peopleBasicInfoTable
  <> Table.string "Favorite Color" (show . favoriteColor)

Additionally, if we need to promote this Table to work on something like Entity Person (if it was backed by persistent), we could do this:

-- You need to use ekmett's contravariant package
peopleEntityFullInfoTable :: Table site (Entity Person)
peopleEntityFullInfoTable = contramap entityVal peopleFullInfoTable2

I won't go into contravariant functors here, but it's a very useful pattern for working with Tables. The astute reader will notice that the monoidal composition pattern shown earlier means that we can only append or prepend columns. We cannot inject them into the middle. I'll give yesod-table a B minus on to composability objective.

Closing Notes and Acknowledgements

One final closing note. You may have noticed that all of the Tables in this post were parameterized over site. This is because they don't depend on a particular foundation type. Usually, the way that this can happen is that you use a route in one of the columns:

-- Assume that our foundation type was named App
peopleTableWithLink :: Table App (Entity Person)
peopleTableWithLink = mempty
  <> peopleEntityFullInfoTable
  <> Table.linked "Profile Page" (const "View") (PersonProfileR . entityKey)

The above example must be parameterized over App (or whatever your foundation type is named), not over site.

This monoidal approach to building tables was inspired by Gabriel Gonzalez's Equational Reasoning at Scale and by the classic diagrams paper. I hope that others find the library useful. I am very open to pull requests and suggestions, so if you have an idea for a convenience function, feel free to open up an issue on the github page.

July 06, 2015 12:00 AM

Danny Gratzer

A Basic Tutorial on JonPRL

Posted on July 6, 2015
Tags: jonprl, types

I was just over at OPLSS for the last two weeks. While there I finally met Jon Sterling in person. What was particularly fun is that for that last few months he’s been creating a proof assistant called JonPRL in the spirit of Nuprl. As it turns out, it’s quite a fun project to work on so I’ve implemented a few features in it over the last couple of days and learned more or less how it works.

Since there’s basically no documentation on it besides the readme and of course the compiler so I thought I’d write down some of the stuff I’ve learned. There’s also a completely separate post on the underlying type theory for Nuprl and JonPRL that’s very interesting in its own right but this isn’t it. Hopefully I’ll get around to scribbling something about that because it’s really quite clever.

Here’s the layout of this tutorial

  • First we start with a whirlwind tutorial. I’ll introduce the basic syntax and we’ll go through some simple proofs together
  • I’ll then dive into some of the rational behind JonPRL’s theory. This should help you understand why some things work how they do
  • I’ll show off a few of JonPRL’s more unique features and (hopefully) interest you enough to start fiddling on your own

Getting JonPRL

JonPRL is pretty easy to build and install and having it will make this post more enjoyable. You’ll need smlnj since JonPRL is currently written in SML. This is available in most package managers (including homebrew) otherwise just grab the binary from the website. After this the following commands should get you a working executable

  • git clone ssh://[email protected]/jonsterling/jonprl
  • cd jonprl
  • git submodule init
  • git submodule update
  • make (This is excitingly fast to run)
  • make test (If you’re doubtful)

You should now have an executable called jonprl in the bin folder. There’s no prelude for jonprl so that’s it. You can now just feed it files like any reasonable compiler and watch it spew (currently difficult-to-decipher) output at you.

If you’re interested in actually writing JonPRL code, you should probably install David Christiansen’s Emacs mode. Now that we’re up and running, let’s actually figure out how the language works

The Different Languages in JonPRL

JonPRL is composed of really 3 different sorts of mini-languages

  • The term language
  • The tactic language
  • The language of commands to the proof assistant

In Coq, these roughly correspond to Gallina, Ltac, and Vernacular respectively.

The Term Language

The term language is an untyped language that contains a number of constructs that should be familiar to people who have been exposed to dependent types before. The actual concrete syntax is composed of 3 basic forms:

  • We can apply an “operator” (I’ll clarify this in a moment) with op(arg1; arg2; arg3).
  • We have variables with x.
  • And we have abstraction with x.e. JonPRL has one construct for binding x.e built into its syntax, that things like λ or Π are built off of.

An operator in this context is really anything you can imagine having a node in an AST for a language. So something like λ is an operator, as is if or pair (corresponding to (,) in Haskell). Each operator has a piece of information associated with it, called its arity. This arity tells you how many arguments an operator takes and how many variables x.y.z. ... each is allowed to bind. For example, with λ has an arity is written (1) since it takes 1 argument which binds 1 variable. Application (ap) has the arity (0; 0). It takes 2 arguments neither of which bind a variable.

So as mentioned we have functions and application. This means we could write (λx.x) y in JonPRL as ap(λ(x.x); y). The type of functions is written with Π. Remember that JonPRL’s language has a notion of dependence so the arity is (0; 1). The construct Π(A; x.B) corresponds to (x : A) → B in Agda or forall (x : A), B in Coq.

We also have dependent sums as well (Σs). In Agda you would write (M , N) to introduce a pair and Σ A λ x → B to type it. In JonPRL you have pair(M; N) and Σ(A; x.B). To inspect a Σ we have spread which let’s us eliminate a pair pair. Eg spread(0; 2) and you give it a Σ in the first spot and x.y.e in the second. It’ll then replace x with the first component and y with the second. Can you think of how to write fst and snd with this?

There’s sums, so inl(M), inr(N) and +(A; B) corresponds to Left, Right, and Either in Haskell. For case analysis there’s decide which has the arity (0; 1; 1). You should read decide(M; x.N; y.P) as something like

    case E of
      Left x -> L
      Right y -> R

In addition we have unit and <> (pronounced axe for axiom usually). Neither of these takes any arguments so we write them just as I have above. They correspond to Haskell’s type- and value-level () respectively. Finally there’s void which is sometimes called false or empty in theorem prover land.

You’ll notice that I presented a bunch of types as if they were normal terms in this section. That’s because in this untyped computation system, types are literally just terms. There’s no typing relation to distinguish them yet so they just float around exactly as if they were λ or something! I call them types because I’m thinking of later when we have a typing relation built on top of this system but for now there are really just terms. It was still a little confusing for me to see Π(unit; _.unit) in a language without types, so I wanted to make this explicit.

Now we can introduce some more exotic terms. Later, we’re going to construct some rules around them that are going to make it behave that way we might expect but for now, they are just suggestively named constants.

  • U{i}, the ith level universe used to classify all types that can be built using types other than U{i} or higher. It’s closed under terms like Π and it contains all the types of smaller universes
  • =(0; 0; 0) this is equality between two terms at a type. It’s a proposition that’s going to precisely mirror what’s going on later in the type theory with the equality judgment
  • ∈(0; 0) this is just like = but internalizes membership in a type into the system. Remember that normally “This has that type” is a judgment but with this term we’re going to have a propositional counterpart to use in theorems.

In particular it’s important to distinguish the difference between the judgment and ∈ the term. There’s nothing inherent in above that makes it behave like a typing relation as you might expect. It’s on equal footing with flibbertyjibberty(0; 0; 0).

This term language contains the full untyped lambda calculus so we can write all sorts of fun programs like

    λ(f.ap(λ(x.ap(f;(ap(x;x)))); λ(x.ap(f;(ap(x;x)))))

which is just the Y combinator. In particular this means that there’s no reason that every term in this language should normalize to a value. There are plenty of terms in here that diverge and in principle, there’s nothing that rules out them doing even stranger things than that. We really only depend on them being deterministic, that e ⇒ v and e ⇒ v' implies that v = v'.

Tactics

The other big language in JonPRL is the language of tactics. Luckily, this is very familiarly territory if you’re a Coq user. Unluckily, if you’ve never heard of Coq’s tactic mechanism this will seem completely alien. As a quick high level idea for what tactics are:

When we’re proving something in a proof assistant we have to deal with a lot of boring mechanical details. For example, when proving A → B → A I have to describe that I want to introduce the A and the B into my context, then I have to suggest using that A the context as a solution to the goal. Bleh. All of that is pretty obvious so let’s just get the computer to do it! In fact, we can build up a DSL of composable “proof procedures” or /tactics/ to modify a particular goal we’re trying to prove so that we don’t have to think so much about the low level details of the proof being generated. In the end this DSL will generate a proof term (or derivation in JonPRL) and we’ll check that so we never have to trust the actual tactics to be sound.

In Coq this is used to great effect. In particular see Adam Chlipala’s book to see incredibly complex theorems with one-line proofs thanks to tactics.

In JonPRL the tactic system works by modifying a sequent of the form H ⊢ A (a goal). Each time we run a tactic we get back a list of new goals to prove until eventually we get to trivial goals which produce no new subgoals. This means that when trying to prove a theorem in the tactic language we never actually see the resulting evidence generated by our proof. We just see this list of H ⊢ As to prove and we do so with tactics.

The tactic system is quite simple, to start we have a number of basic tactics which are useful no matter what goal you’re attempting to prove

  • id a tactic which does nothing
  • t1; t2 this runs the t1 tactic and runs t2 on any resulting subgoals
  • *{t} this runs t as long as t does something to the goal. If t ever fails for whatever reason it merely stops running, it doesn’t fail itself
  • ?{t} tries to run t once. If t fails nothing happens
  • !{t} runs t and if t does anything besides complete the proof it fails. This means that !{id} for example will always fail.
  • t1 | t2 runs t1 and if it fails it runs t2. Only one of the effects for t1 and t2 will be shown.
  • t; [t1, ..., tn] first runs t and then runs tactic ti on subgoal ith subgoal generated by t
  • trace "some words" will print some words to standard out. This is useful when trying to figure out why things haven’t gone your way.
  • fail is the opposite of id, it just fails. This is actually quite useful for forcing backtracking and one could probably implement a makeshift !{} as t; fail.

It’s helpful to see this as a sort of tree, a tactic takes one goal to a list of a subgoals to prove so we can imagine t as this part of a tree

      H
      |
———–————————— (t)
H'  H''  H'''

If we have some tactic t2 then t; t2 will run t and then run t2 on H, H', and H''. Instead we could have t; [t1, t2, t3] then we’ll run t and (assuming it succeeds) we’ll run t1 on H', t2 on H'', and t3 on H'''. This is actually how things work under the hood, composable fragments of trees :)

Now those give us a sort of bedrock for building up scripts of tactics. We also have a bunch of tactics that actually let us manipulate things we’re trying to prove. The 4 big ones to be aware of are

  • intro
  • elim #NUM
  • eq-cd
  • mem-cd

The basic idea is that intro modifies the A part of the goal. If we’re looking at a function, so something like H ⊢ Π(A; x.B), this will move that A into the context, leaving us with H, x : A ⊢ B.

If you’re familiar with sequent calculus intro runs the appropriate right rule for the goal. If you’re not familiar with sequent calculus intro looks at the outermost operator of the A and runs a rule that applies when that operator is to the right of a the .

Now one tricky case is what should intro do if you’re looking at a Σ? Well now things get a bit dicey. We’d might expect to get two subgoals if we run intro on H ⊢ Σ(A; x.B), one which proves H ⊢ A and one which proves H ⊢ B or something, but what about the fact that x.B depends on whatever the underlying realizer (that’s the program extracted from) the proof of H ⊢ A! Further, Nuprl and JonPRL are based around extract-style proof systems. These mean that a goal shouldn’t depend on the particular piece of evidence proving of another goal. So instead we have to tell intro up front what we want the evidence for H ⊢ A to be is so that the H ⊢ B section may use it.

To do this we just give intro an argument. For example say we’re proving that · ⊢ Σ(unit; x.unit), we run intro [<>] which gives us two subgoals · ⊢ ∈(<>; unit) and · ⊢ unit. Here the [] let us denote the realizer we’re passing to intro. In general any term arguments to a tactic will be wrapped in []s. So the first goal says “OK, you said that this was your realizer for unit, but is it actually a realizer for unit?” and the second goal substitutes the given realizer into the second argument of Σ, x.unit, and asks us to prove that. Notice how here we have to prove ∈(<>; unit)? This is where that weird type comes in handy. It let’s us sort of play type checker and guide JonPRL through the process of type checking. This is actually very crucial since type checking in Nuprl and JonPRL is undecidable.

Now how do we actually go about proving ∈(<>; unit)? Well here mem-cd has got our back. This tactic transforms ∈(A; B) into the equivalent form =(A; A; B). In JonPRL and Nuprl, types are given meaning by how we interpret the equality of their members. In other words, if you give me a type you have to say

  1. What canonical terms are in that terms
  2. What it means for two canonical members to be equal

Long ago, Stuart Allen realized we could combine the two by specifying a partial equivalence relation for a type. In this case rather than having a separate notion of membership we check to see if something is equal to itself under the PER because when it is that PER behaves like a normal equivalence relation! So in JonPRL ∈ is actually just a very thin layer of sugar around = which is really the core defining notion of typehood. To handle = we have eq-cd which does clever things to handle most of the obvious cases of equality.

Finally, we have elim. Just like intro let us simplify things on the right of the ⊢, elim let’s us eliminate something on the left. So we tell elim to “eliminate” the nth item in the context (they’re numbered when JonPRL prints them) with elim #n.

Just like with anything, it’s hard to learn all the tactics without experimenting (though a complete list can be found with jonprl --list-tactics). Let’s go look at the command language so we can actually prove some theorems.

Commands

So in JonPRL there are only 4 commands you can write at the top level

  • Operator
  • [oper] =def= [term] (A definition)
  • Tactic
  • Theorem

The first three of these let us customize and extend the basic suite of operators and tactics JonPRL comes with. The last actually lets us state and prove theorems.

The best way to see these things is by example so we’re going to build up a small development in JonPRL. We’re going to show that products are monoid with unit up to some logical equivalence. There are a lot of proofs involved here

  1. prod(unit; A) entails A
  2. prod(A; unit) entails A
  3. A entails prod(unit; A)
  4. A entails prod(A; unit)
  5. prod(A; prod(B; C)) entails prod(prod(A; B); C)
  6. prod(prod(A; B); C) entails prod(A; prod(B; C))

I intend to prove 1, 2, and 5. The remaining proofs are either very similar or fun puzzles to work on. We could also prove that all the appropriate entailments are inverses and then we could say that everything is up to isomorphism.

First we want a new snazzy operator to signify nondependent products since writing Σ(A; x.B) is kind of annoying. We do this using operator

    Operator prod : (0; 0).

This line declares prod as a new operator which takes two arguments binding zero variables each. Now we really want JonPRL to know that prod is sugar for Σ. To do this we use =def= which gives us a way to desugar a new operator into a mess of existing ones.

    [prod(A; B)] =def= [Σ(A; _.B)].

Now we can change any occurrence of prod(A; B) for Σ(A; _.B) as we’d like. Okay, so we want to prove that we have a monoid here. What’s the first step? Let’s verify that unit is a left identity for prod. This entails proving that for all types A, prod(unit; A) ⊃ A and A ⊃ prod(unit; A). Let’s prove these as separate theorems. Translating our first statement into JonPRL we want to prove

    Π(U{i}; A.
    Π(prod(unit; A); _.
    A))

In Agda notation this would be written

    (A : Set) → (_ : prod(unit; A)) → A

Let’s prove our first theorem, we start by writing

    Theorem left-id1 :
      [Π(U{i}; A.
       Π(prod(unit; A); _.
       A))] {
      id
    }.

This is the basic form of a theorem in JonPRL, a name, a term to prove, and a tactic script. Here we have id as a tactic script, which clearly doesn’t prove our goal. When we run JonPRL on this file (C-c C-l if you’re in Emacs) you get back

[XXX.jonprl:8.3-9.1]: tactic 'COMPLETE' failed with goal:
⊢ ΠA ∈ U{i}. (prod(unit; A)) => A

Remaining subgoals:
⊢ ΠA ∈ U{i}. (prod(unit; A)) => A

So focus on that Remaining subgoals bit, that’s what we have left to prove, it’s our current goal. Now you may notice that this outputted goal is a lot prettier than our syntax! That’s because currently in JonPRL the input and outputted terms may not match, the latter is subject to pretty printing. In general this is great because you can read your remaining goals, but it does mean copying and pasting is a bother. There’s nothing to the left of that ⊢ yet so let’s run the only applicable tactic we know. Delete that id and replace it with

    {
      intro
    }.

The goal now becomes

Remaining subgoals:

1. A : U{i}
⊢ (prod(unit; A)) => A

⊢ U{i} ∈ U{i'}

Two ⊢s means two subgoals now. One looks pretty obvious, U{i'} is just the universe above U{i} (so that’s like Set₁ in Agda) so it should be the case that U{i} ∈ U{i'} by definition! So the next tactic should be something like [???, mem-cd; eq-cd]. Now what should that ??? be? Well we can’t use elim because there’s one thing in the context now (A : U{i}), but it doesn’t help us really. Instead let’s run unfold <prod>. This is a new tactic that’s going to replace that prod with the definition that we wrote earlier.

    {
      intro; [unfold <prod>, mem-cd; eq-cd]
    }

Notice here that , behinds less tightly than ; which is useful for saying stuff like this. This gives us

Remaining subgoals:

1. A : U{i}
⊢ (unit × A) => A

We run intro again

    {
      intro; [unfold <prod>, mem-cd; eq-cd]; intro
    }

Now we are in a similar position to before with two subgoals.

    Remaining subgoals:

    1. A : U{i}
    2. _ : unit × A
    ⊢ A


    1. A : U{i}
    ⊢ unit × A ∈ U{i}

The first subgoal is really what we want to be proving so let’s put a pin in that momentarily. Let’s get rid of that second subgoal with a new helpful tactic called auto. It runs eq-cd, mem-cd and intro repeatedly and is built to take care of boring goals just like this!

    {
      intro; [unfold <prod>, mem-cd; eq-cd]; intro; [id, auto]
    }

Notice that we used what is a pretty common pattern in JonPRL, to work on one subgoal at a time we use []’s and ids everywhere except where we want to do work, in this case the second subgoal.

Now we have

Remaining subgoals:

1. A : U{i}
2. _ : unit × A
⊢ A

Cool! Having a pair of unit × A really ought to mean that we have an A so we can use elim to get access to it.

    {
      intro; [unfold <prod>, mem-cd; eq-cd]; intro; [id, auto];
      elim #2
    }

This gives us

Remaining subgoals:

1. A : U{i}
2. _ : unit × A
3. s : unit
4. t : A
⊢ A

We’ve really got the answer now, #4 is precisely our goal. For this situations there’s assumption which is just a tactic which succeeds if what we’re trying to prove is in our context already. This will complete our proof

    Theorem left-id1 :
      [Π(U{i}; A.
       Π(prod(unit; A); _.
       A))] {
      intro; [unfold <prod>, mem-cd; eq-cd]; intro; [id, auto];
      elim #2; assumption
    }.

Now we know that auto will run all of the tactics on the first line except unfold <prod>, so what we just unfold <prod> first and run auto? It ought to do all the same stuff.. Indeed we can shorten our whole proof to unfold <prod>; auto; elim #2; assumption. With this more heavily automated proof, proving our next theorem follows easily.

    Theorem right-id1 :
      [Π(U{i}; A.
       Π(prod(A; unit); _.
       A))] {
      unfold <prod>; auto; elim #2; assumption
    }.

Next, we have to prove associativity to complete the development that prod is a monoid. The statement here is a bit more complex.

    Theorem assoc :
      [Π(U{i}; A.
       Π(U{i}; B.
       Π(U{i}; C.
       Π(prod(A; prod(B;C)); _.
       prod(prod(A;B); C)))))] {
      id
    }.

In Agda notation what I’ve written above is

    assoc : (A B C : Set) → A × (B × C) → (A × B) × C
    assoc = ?

Let’s kick things off with unfold <prod>; auto to deal with all the boring stuff we had last time. In fact, since x appears in several nested places we’d have to run unfold quite a few times. Let’s just shorten all of those invocations into *{unfold <prod>}

    {
      *{unfold <prod>}; auto
    }

This leaves us with the state

Remaining subgoals:

1. A : U{i}
2. B : U{i}
3. C : U{i}
4. _ : A × B × C
⊢ A


1. A : U{i}
2. B : U{i}
3. C : U{i}
4. _ : A × B × C
⊢ B


1. A : U{i}
2. B : U{i}
3. C : U{i}
4. _ : A × B × C
⊢ C

In each of those goals we need to take apart the 4th hypothesis so let’s do that

    {
      *{unfold <prod>}; auto; elim #4
    }

This leaves us with 3 subgoals still

1. A : U{i}
2. B : U{i}
3. C : U{i}
4. _ : A × B × C
5. s : A
6. t : B × C
⊢ A


1. A : U{i}
2. B : U{i}
3. C : U{i}
4. _ : A × B × C
5. s : A
6. t : B × C
⊢ B


1. A : U{i}
2. B : U{i}
3. C : U{i}
4. _ : A × B × C
5. s : A
6. t : B × C
⊢ C

The first subgoal is pretty easy, assumption should handle that. In the other two we want to eliminate 6 and then we should be able to apply assumption. In order to deal with this we use | to encode that disjunction. In particular we want to run assumption OR elim #6; assumption leaving us with

    {
      *{unfold <prod>}; auto; elim #4; (assumption | elim #6; assumption)
    }

This completes the proof!

    Theorem assoc :
      [Π(U{i}; A.
       Π(U{i}; B.
       Π(U{i}; C.
       Π(prod(A; prod(B;C)); _.
       prod(prod(A;B); C)))))] {
      *{unfold <prod>}; auto; elim #4; (assumption | elim #6; assumption)
    }.

As a fun puzzle, what needs to change in this proof to prove we can associate the other way?

What on earth did we just do!?

So we just proved a theorem.. but what really just happened? I mean how did we go from “Here we have an untyped computation system which types just behaving as normal terms” to “Now apply auto and we’re done!”. In this section I’d like to briefly sketch the path from untyped computation to theorems.

The path looks like this

  • We start with our untyped language and its notion of computation

    We already discussed this in great depth before.

  • We define a judgment a = b ∈ A.

    This is a judgment, not a term in that language. It exists in whatever metalanguage we’re using. This judgment is defined across 3 terms in our untyped language (I’m only capitalizing A out of convention). This is supposed to represent that a and b are equal elements of type A. This also gives meaning to typehood: something is a type in CTT precisely when we know what the partial equivalence relation defined by - = - ∈ A on canonical values is.

    Notice here that I said partial. It isn’t the case that a = b ∈ A presupposes that we know that a : A and b : A because we don’t have a notion of : yet!

    In some sense this is where we depart from a type theory like Coq or Agda’s. We have programs already and on top of them we define this 3 part judgment which interacts which computation in a few ways I’m not specifying. In Coq, we would specify one notion of equality, generic over all types, and separately specify a typing relation.

  • From here we can define the normal judgments of Martin Lof’s type theory. For example, a : A is a = a ∈ A. We recover the judgment A type with A = A ∈ U (where U here is a universe).

This means that inhabiting a universe A = A ∈ U, isn’t necessarily inductively defined but rather negatively generated. We specify some condition a term must satisfy to occupy a universe.

Hypothetical judgments are introduced in the same way they would be in Martin-Lof’s presentations of type theory. The idea being that H ⊢ J if J is evident under the assumption that each term in H has the appropriate type and furthermore that J is functional (respects equality) with respect to what H contains. This isn’t really a higher order judgment, but it will be defined in terms of a higher order hypothetical judgment in the metatheory.

With this we have something that walks and quacks like normal type theory. Using the normal tools of our metatheory we can formulate proofs of a : A and do normal type theory things. This whole development is building up what is called “Computational Type Theory”. The way this diverges from Martin-Lof’s extensional type theory is subtle but it does directly descend from Martin-Lof’s famous 1979 paper “Constructive Mathematics and Computer Programming” (which you should read. Instead of my blog post).

Now there’s one final layer we have to consider, the PRL bit of JonPRL. We define a new judgment, H ⊢ A [ext a]. This is judgment is cleverly set up so two properties hold

  • H ⊢ A [ext a] should entail that H ⊢ a : A or H ⊢ a = a ∈ A
  • In H ⊢ A [ext a], a is an output and H and A are inputs. In particular, this implies that in any inference for this judgment, the subgoals may not use a in their H and A.

This means that a is completely determined by H and A which justifies my use of the term output. I mean this in the sense of Twelf and logic programming if that’s a more familiar phrasing. It’s this judgment that we see in JonPRL! Since that a is output we simply hide it, leaving us with H ⊢ A as we saw before. When we prove something with tactics in JonPRL we’re generating a derivation, a tree of inference rules which make H ⊢ A evident for our particular H and A! These rules aren’t really programs though, they don’t correspond one to one with proof terms we may run like they would in Coq. The computational interpretation of our program is bundled up in that a.

To see what I mean here we need a little bit more machinery. Specifically, let’s look at the rules for the equality around the proposition =(a; b; A). Remember that we have a term <> lying around,

     a = b ∈ A
————————————————————
<> = <> ∈ =(a; b; A)

So the only member of =(a; b; A) is <> if a = b ∈ A actually holds. First off, notice that <> : A and <> : B doesn’t imply that A = B! In another example, λ(x. x) ∈ Π(A; _.A) for all A! This is a natural consequence of separating our typing judgment from our programming language. Secondly, there’s not really any computation in the e of H ⊢ =(a; b; A) (e). After all, in the end the only thing e could be so that e : =(a; b; A) is <>! However, there is potentially quite a large derivation involved in showing =(a; b; A)! For example, we might have something like this

x : =(A; B; U{i}); y : =(b; a; A) ⊢ =(a; b; B)
———————————————————————————————————————————————— Substitution
x : =(A; B; U{i}); y : =(b; a; A) ⊢ =(a; b; A)
———————————————————————————————————————————————— Symmetry
x : =(A; B; U{i}); y : =(b; a; A) ⊢ =(b; a; A)
———————————————————————————————————————————————— Assumption

Now we write derivations of this sequent up side down, so the thing we want to show starts on top and we write each rule application and subgoal below it (AI people apparently like this?). Now this was quite a derivation, but if we fill in the missing [ext e] for this derivation from the bottom up we get this

x : =(A; B; U{i}); y : =(b; a; A) ⊢ =(a; b; B)
———————————————————————————————————————————————— Substitution [ext <>]
x : =(A; B; U{i}); y : =(b; a; A) ⊢ =(a; b; A)
———————————————————————————————————————————————— Symmetry     [ext <>]
x : =(A; B; U{i}); y : =(b; a; A) ⊢ =(b; a; A)
———————————————————————————————————————————————— Assumption   [ext x]

Notice how at the bottom there was some computational content (That x signifies that we’re accessing a variable in our context) but than we throw it away right on the next line! That’s because we find that no matter what the extract was that let’s us derive =(b; a; A), the only realizer it could possible generate is <>. Remember our conditions, if we can make evident the fact that b = a ∈ A then <> ∈ =(b; a; A). Because we somehow managed to prove that b = a ∈ A holds, we’re entitled to just use <> to realize our proof. This means that despite our somewhat tedious derivation and the bookkeeping that we had to do to generate that program, that program reflects none of it.

This is why type checking in JonPRL is woefully undecidable: in part, the realizers that we want to type check contain none of the helpful hints that proof terms in Coq would. This also means that extraction from JonPRL proofs is built right into the system and we can actually generate cool and useful things! In Nuprl-land, folks at Cornell actually write proofs and use this realizers to run real software. From what Bob Constable said at OPLSS they can actually get these programs to run fast (within 5x of naive C code).

So to recap, in JonPRL we

  • See H ⊢ A
  • Use tactics to generate a derivation of this judgment
  • Once this derivation is generated, we can extract the computational content as a program in our untyped system

In fact, we can see all of this happen if you call JonPRL from the command line or hit C-c C-c in emacs! On our earlier proof we see

Operator prod : (0; 0).
⸤prod(A; B)⸥ ≝ ⸤A × B⸥.

Theorem left-id1 : ⸤⊢ ΠA ∈ U{i}. (prod(unit; A)) => A⸥ {
  fun-intro(A.fun-intro(_.prod-elim(_; _.t.t); prod⁼(unit⁼; _.hyp⁼(A))); U⁼{i})
} ext {
  λ_. λ_. spread(_; _.t.t)
}.

Theorem right-id1 : ⸤⊢ ΠA ∈ U{i}. (prod(A; unit)) => A⸥ {
  fun-intro(A.fun-intro(_.prod-elim(_; s._.s); prod⁼(hyp⁼(A); _.unit⁼)); U⁼{i})
} ext {
  λ_. λ_. spread(_; s._.s)
}.

Theorem assoc : ⸤⊢ ΠA ∈ U{i}. ΠB ∈ U{i}. ΠC ∈ U{i}. (prod(A; prod(B; C))) => prod(prod(A; B); C)⸥ {
  fun-intro(A.fun-intro(B.fun-intro(C.fun-intro(_.independent-prod-intro(independent-prod-intro(prod-elim(_;
  s.t.prod-elim(t; _._.s)); prod-elim(_; _.t.prod-elim(t;
  s'._.s'))); prod-elim(_; _.t.prod-elim(t; _.t'.t')));
  prod⁼(hyp⁼(A); _.prod⁼(hyp⁼(B); _.hyp⁼(C)))); U⁼{i}); U⁼{i});
  U⁼{i})
} ext {
  λ_. λ_. λ_. λ_. ⟨⟨spread(_; s.t.spread(t; _._.s)), spread(_; _.t.spread(t; s'._.s'))⟩, spread(_; _.t.spread(t; _.t'.t'))⟩
}.

Now we can see that those Operator and bits are really what we typed with =def= and Operator in JonPRL, what’s interesting here are the theorems. There’s two bits, the derivation and the extract or realizer.

{
  derivation of the sequent · ⊢ A
} ext {
  the program in the untyped system extracted from our derivation
}

We can move that derivation into a different proof assistant and check it. This gives us all the information we need to check that JonPRL’s reasoning and helps us not trust all of JonPRL (I wrote some of it so I’d be a little scared to trust it :). We can also see the computational bit of our proof in the extract. For example, the computation involved in taking A × unit → A is just λ_. λ_. spread(_; s._.s)! This is probably closer to what you’ve seen in Coq or Idris, even though I’d say the derivation is probably more similar in spirit (just ugly and beta normal). That’s because the extract need not have any notion of typing or proof, it’s just the computation needed to produce a witness of the appropriate type. This means for a really tricky proof of equality, your extract might just be <>! Your derivation however will always exactly reflect the complexity of your proof.

Killer features

OK, so I’ve just dumped about 50 years worth of hard research in type theory into your lap which is best left to ruminate for a bit. However, before I finish up this post I wanted to do a little bit of marketing so that you can see why one might be interested in JonPRL (or Nuprl). Since we’ve embraced this idea of programs first and types as PERs, we can define some really strange types completely seamlessly. For example, in JonPRL there’s a type ⋂(A; x.B), it behaves a lot like Π but with one big difference, the definition of - = - ∈ ⋂(A; x.B) looks like this

a : A ⊢ e = e' ∈ [a/x]B
————————————————————————
   e = e' ∈ ⋂(A; x.B)

Notice here that e and e' may not use a anywhere in their bodies. That is, they have to be in [a/x]B without knowing anything about a and without even having access to it.

This is a pretty alien concept that turned out to be new in logic as well (it’s called “uniform quantification” I believe). It turns out to be very useful in PRL’s because it lets us declare things in our theorems without having them propogate into our witness. For example, we could have said

    Theorem right-id1 :
          [⋂(U{i}; A.
           Π(prod(A; unit); _.
           A))] {
          unfold <prod>; auto; elim #2; assumption
        }.

With the observation that our realizer doesn’t need to depend on A at all (remember, no types!). Then the extract of this theorem is

λx. spread(x; s._.s)

There’s no spurious λ _. ... at the beginning! Even more wackily, we can define subsets of an existing type since realizers need not have unique types

e = e' ∈ A  [e/x]P  [e'/x]P
————————————————————————————
  e = e' ∈ subset(A; x.P)

And in JonPRL we can now say things like “all odd numbers” by just saying subset(nat; n. ap(odd; n)). In intensional type theories, these types are hard to deal with and still the subject of open research. In CTT they just kinda fall out because of how we thought about types in the first place. Quotients are a similarly natural conception (just define a new type with a stricter PER) but JonPRL currently lacks them (though they shouldn’t be hard to add..).

Finally, if you’re looking for one last reason to dig into **PRL, the fact that we’ve defined all our equalities extensionally means that several very useful facts just fall right out of our theory

    Theorem fun-ext :
      [⋂(U{i}; A.
       ⋂(Π(A; _.U{i}); B.
       ⋂(Π(A; a.ap(B;a)); f.
       ⋂(Π(A; a.ap(B;a)); g.

       ⋂(Π(A; a.=(ap(f; a); ap(g; a); ap(B; a))); _.
       =(f; g; Π(A; a.ap(B;a))))))))] {
      auto; ext; ?{elim #5 [a]}; auto
    }.

This means that two functions are equal in JonPRL if and only if they map equal arguments to equal output. This is quite pleasant for formalizing mathematics for example.

Wrap Up

Whew, we went through a lot! I didn’t intend for this to be a full tour of JonPRL, just a taste of how things sort of hang together and maybe enough to get you looking through the examples. Speaking of which, JonPRL comes with quite a few examples which are going to make a lot more sense now.

Additionally, you may be interested in the documentation in the README which covers most of the primitive operators in JonPRL. As for an exhaustive list of tactics, well….

Hopefully I’ll be writing about JonPRL again soon. Until then, I hope you’ve learned something cool :)

A huge thanks to David Christiansen and Jon Sterling for tons of helpful feedback on this

<script type="text/javascript"> var disqus_shortname = 'codeco'; (function() { var dsq = document.createElement('script'); dsq.type = 'text/javascript'; dsq.async = true; dsq.src = '//' + disqus_shortname + '.disqus.com/embed.js'; (document.getElementsByTagName('head')[0] || document.getElementsByTagName('body')[0]).appendChild(dsq); })(); </script> <noscript>Please enable JavaScript to view the comments powered by Disqus.</noscript> comments powered by Disqus

July 06, 2015 12:00 AM

July 04, 2015

Edwin Brady

Cross-platform Compilers for Functional Languages

I’ve just submitted a new draft, Cross-platform Compilers for Functional Languages. Abstract:

Modern software is often designed to run on a virtual machine, such as the JVM or .NET’s CLR. Increasingly, even the web browser is considered a target platform with the Javascript engine as its virtual machine. The choice of programming language for a project is therefore restricted to the languages which target the desired platform. As a result, an important consideration for a programming language designer is the platform to be targetted. For a language to be truly cross-platform, it must not only support different operating systems (e.g. Windows, OSX and Linux) but it must also target different virtual machine environments such as JVM, .NET, Javascript and others. In this paper, I describe how this problem is addressed in the Idris programming language. The overall compilation process involves a number of intermediate representations and Idris exposes an interface to each of these representations, allowing back ends for different target platforms to decide which is most appropriate. I show how to use these representations to retarget Idris for multiple platforms, and further show how to build a generic foreign function interface supporting multiple platforms.

Constructive comments and suggestions are welcome, particularly if you’ve tried implementing a code generator for Idris.


by edwinb at July 04, 2015 11:06 AM

July 03, 2015

Brandon Simmons

Translating some stateful bit-twiddling to haskell

I just started implementing SipHash in hashabler and wanted to share a nice way I found to translate stateful bit-twiddling code in C (which makes heavy use of bitwise assignment operators) to haskell.

I was working from the reference implementation. As you can see statefulness and mutability are an implicit part of how the algorithm is defined, as it modifies the states of the v variables.

#define SIPROUND                                        \
  do {                                                  \
    v0 += v1; v1=ROTL(v1,13); v1 ^= v0; v0=ROTL(v0,32); \
    v2 += v3; v3=ROTL(v3,16); v3 ^= v2;                 \
    v0 += v3; v3=ROTL(v3,21); v3 ^= v0;                 \
    v2 += v1; v1=ROTL(v1,17); v1 ^= v2; v2=ROTL(v2,32); \
  } while(0)

int  siphash( uint8_t *out, const uint8_t *in, uint64_t inlen, const uint8_t *k )
{

  /* ... */

  for ( ; in != end; in += 8 )
  {
    m = U8TO64_LE( in );
    v3 ^= m;

    TRACE;
    for( i=0; i<cROUNDS; ++i ) SIPROUND;

    v0 ^= m;
  }

I wanted to translate this sort of code as directly as possible (I’d already decided if it didn’t work on the first try I would burn my laptop and live in the woods, rather than debug this crap).

First we’ll use name shadowing to “fake” our mutable variables, making it easy to ensure we’re always dealing with the freshest values.

{-# OPTIONS_GHC -fno-warn-name-shadowing #-}

We’ll also use RecordWildCards to make it easy to capture the “current state” of these values, through folds and helper functions.

{-# LANGUAGE RecordWildCards #-}

And finally we use the trivial Identity monad (this trick I learned from Oleg) which gets us the proper scoping we want for our v values:

import Data.Functor.Identity

Here’s a bit of the haskell:

siphash :: Hashable a => SipKey -> a -> Word64
siphash (k0,k1) = \a-> runIdentity $ do
    let v0 = 0x736f6d6570736575
        v1 = 0x646f72616e646f6d
        v2 = 0x6c7967656e657261
        v3 = 0x7465646279746573

    ...

    v3 <- return $ v3 `xor` k1;
    v2 <- return $ v2 `xor` k0;
    v1 <- return $ v1 `xor` k1;
    v0 <- return $ v0 `xor` k0;

    ...

    -- Initialize rest of SipState:
    let mPart          = 0
        bytesRemaining = 8
        inlen          = 0
    SipState{ .. } <- return $ hash (SipState { .. }) a

    let !b = inlen `unsafeShiftL` 56

    v3 <- return $ v3 `xor` b
    -- for( i=0; i<cROUNDS; ++i ) SIPROUND;
    (v0,v1,v2,v3) <- return $ sipRound v0 v1 v2 v3
    (v0,v1,v2,v3) <- return $ sipRound v0 v1 v2 v3
    v0 <- return $ v0 `xor` b

    ...

    (v0,v1,v2,v3) <- return $ sipRound v0 v1 v2 v3

    return $! v0 `xor` v1 `xor` v2 `xor` v3

If you were really doing a lot of this sort of thing, you could even make a simple quasiquoter that could translate bitwise assignment into code like the above.

July 03, 2015 05:58 PM

Philip Wadler

Don Syme awarded Silver Medal by Royal Academy of Engineering

 Congratulations, Don!
For over two decades, the Academy’s Silver Medals have recognised exceptional personal contributions from early- to mid-career engineers who have advanced the cause of engineering in the UK.
Three of the UK’s most talented engineers are to receive the Royal Academy of Engineering’s coveted Silver Medal for remarkable technical  achievements in their fields, coupled with commercial success.
They are the inventor of 3D printed surgical instruments, an
indoor location-tracking technology pioneer, and the creator of the F#
computer programming language.
 Full RAE Announcement. Spotted by Kevin Hammond.

by Philip Wadler ([email protected]) at July 03, 2015 04:28 PM

Mark Jason Dominus

The annoying boxes puzzle: solution

I presented this logic puzzle on Wednesday:

There are two boxes on a table, one red and one green. One contains a treasure. The red box is labelled "exactly one of the labels is true". The green box is labelled "the treasure is in this box."

Can you figure out which box contains the treasure?

It's not too late to try to solve this before reading on. If you want, you can submit your answer here:

The treasure is in the red box
The treasure is in the green box
There is not enough information to determine the answer
Something else:

Results

There were 506 total responses up to Fri Jul 3 11:09:52 2015 UTC; I kept only the first response from each IP address, leaving 451. I read all the "something else" submissions and where it seemed clear I recoded them as votes for "red", for "not enough information", or as spam. (Several people had the right answer but submitted "other" so they could explain themselves.) There was also one post attempted to attack my (nonexistent) SQL database. Sorry, Charlie; I'm not as stupid as I look.

	 66.52%  300 red
	 25.72   116 not-enough-info
	  3.55    16 green
	  2.00     9 other
	  1.55     7 spam
	  0.44     2 red-with-qualification
	  0.22     1 attack

	100.00   451 TOTAL
One-quarter of respondents got the right answer, that there is not enough information given to solve the problem, Two-thirds of respondents said the treasure was in the red box. This is wrong. The treasure is in the green box.

What?

Let me show you. I stated:

There are two boxes on a table, one red and one green. One contains a treasure. The red box is labelled "exactly one of the labels is true". The green box is labelled "the treasure is in this box."

The labels are as I said. Everything I told you was literally true.

The treasure is definitely not in the red box.

No, it is actually in the green box.

(It's hard to see, but one of the items in the green box is the gold and diamond ring made in Vienna by my great-grandfather, which is unquestionably a real treasure.)

So if you said the treasure must be in the red box, you were simply mistaken. If you had a logical argument why the treasure had to be in the red box, your argument was fallacious, and you should pause and try to figure out what was wrong with it.

I will discuss it in detail below.

Solution

The treasure is undeniably in the green box. However, correct answer to the puzzle is "no, you cannot figure out which box contains the treasure". There is not enough information given. (Notice that the question was not “Where is the treasure?” but “Can you figure out…?”)

(Fallacious) Argument A

Many people erroneously conclude that the treasure is in the red box, using reasoning something like the following:

  1. Suppose the red label is true. Then exactly one label is true, and since the red label is true, the green label is false. Since it says that the treasure is in the green box, the treasure must really be in the red box.
  2. Now suppose that the red label is false. Then the green label must also be false. So again, the treasure is in the red box.
  3. Since both cases lead to the conclusion that the treasure is in the red box, that must be where it is.

What's wrong with argument A?

Here are some responses people commonly have when I tell them that argument A is fallacious:

"If the treasure is in the green box, the red label is lying."

Not quite, but argument A explicitly considers the possibility that the red label was false, so what's the problem?

"If the treasure is in the green box, the red label is inconsistent."

It could be. Nothing in the puzzle statement ruled this out. But actually it's not inconsistent, it's just irrelevant.

"If the treasure is in the green box, the red label is meaningless."

Nonsense. The meaning is plain: it says “exactly one of these labels is true”, and the meaning is that exactly one of the labels is true. Anyone presenting argument A must have understood the label to mean that, and it is incoherent to understand it that way and then to turn around and say that it is meaningless! (I discussed this point in more detail in 2007.)

"But the treasure could have been in the red box."

True! But it is not, as you can see in the pictures. The puzzle does not give enough information to solve the problem. If you said that there was not enough information, then congratulations, you have the right answer. The answer produced by argument A is incontestably wrong, since it asserts that the treasure is in the red box, when it is not.

"The conditions supplied by the puzzle statement are inconsistent."

They certainly are not. Inconsistent systems do not have models, and in particular cannot exist in the real world. The photographs above demonstrate a real-world model that satisfies every condition posed by the puzzle, and so proves that it is consistent.

"But that's not fair! You could have made up any random garbage at all, and then told me afterwards that you had been lying."

Had I done that, it would have been an unfair puzzle. For example, suppose I opened the boxes at the end to reveal that there was no treasure at all. That would have directly contradicted my assertion that "One [box] contains a treasure". That would have been cheating, and I would deserve a kick in the ass.

But I did not do that. As the photograph shows, the boxes, their colors, their labels, and the disposition of the treasure are all exactly as I said. I did not make up a lie to trick you; I described a real situation, and asked whether people they could diagnose the location of the treasure.

(Two respondents accused me of making up lies. One said:

There is no treasure. Both labels are lying. Look at those boxes. Do you really think someone put a treasure in one of them just for this logic puzzle?
What can I say? I _did_ do this. Some of us just have higher standards.)

"But what about the labels?"

Indeed! What about the labels?

The labels are worthless

The labels are red herrings; the provide no information. Consider the following version of the puzzle:

There are two boxes on a table, one red and one green. One contains a treasure.

Which box contains the treasure?

Obviously, the problem cannot be solved from the information given.

Now consider this version:

There are two boxes on a table, one red and one green. One contains a treasure. The red box is labelled "gcoadd atniy fnck z fbi c rirpx hrfyrom". The green box is labelled "ofurb rz bzbsgtuuocxl ckddwdfiwzjwe ydtd."

Which box contains the treasure?

One is similarly at a loss here.

(By the way, people who said one label was meaningless: this is what a meaningless label looks like.)

There are two boxes on a table, one red and one green. One contains a treasure. The red box is labelled "exactly one of the labels is true". The green box is labelled "the treasure is in this box."

But then the janitor happens by. "Don't be confused by those labels," he says. "They were stuck on there by the previous owner of the boxes, who was an illiterate shoemaker who only spoke Serbian. I think he cut them out of a magazine because he liked the frilly borders."

Which box contains the treasure?

The point being that in the absence of additional information, there is no reason to believe that the labels give any information about the contents of the boxes, or about labels, or about anything at all. This should not come as a surprise to anyone. It is true not just in annoying puzzles, but in the world in general. A box labeled “fresh figs” might contain fresh figs, or spoiled figs, or angry hornets, or nothing at all.
Order
What is the Name of this Book?
What is the Name of this Book?
with kickback
no kickback

Why doesn't every logic puzzle fall afoul of this problem?

I said as part of the puzzle conditions that there was a treasure in one box. For a fair puzzle, I am required to tell the truth about the puzzle conditions. Otherwise I'm just being a jerk.

Typically the truth or falsity of the labels is part of the puzzle conditions. Here's a typical example, which I took from Raymond Smullyan's What is the name of this book? (problem 67a):

… She had the following inscriptions put on the caskets:
GoldSilverLead
THE PORTRAIT IS IN THIS CASKET THE PORTRAIT IS NOT IN THIS CASKET THE PORTRAIT IS NOT IN THE GOLD CASKET
Portia explained to the suitor that of the three statements, at most one was true.

Which casket should the suitor choose [to find the portrait]?

Notice that the problem condition gives the suitor a certification about the truth of the labels, on which he may rely. In the quotation above, the certification is in boldface.

A well-constructed puzzle will always contain such a certification, something like “one label is true and one is false” or “on this island, each person always lies, or always tells the truth”. I went to _What is the Name of this Book?_ to get the example above, and found more than I had bargained for: problem 70 is exactly the annoying boxes problem! Smullyan says:

Good heavens, I can take any number of caskets that I please and put an object in one of them and then write any inscriptions at all on the lids; these sentences won't convey any information whatsoever.
(Page 65)

Had I known that ahead of time, I doubt I would have written this post at all.

But why is this so surprising?

I don't know.

Final notes

16 people correctly said that the treasure was in the green box. This has to be counted as a lucky guess, unacceptable as a solution to a logic puzzle.

One respondent referred me to a similar post on lesswrong.

I did warn you all that the puzzle was annoying.

I started writing this post in October 2007, and then it sat on the shelf until I got around to finding and photographing the boxes. A triumph of procrastination!

by Mark Dominus ([email protected]) at July 03, 2015 12:15 PM

July 01, 2015

Mark Jason Dominus

The annoying boxes puzzle

Here is a logic puzzle. I will present the solution on Friday.

There are two boxes on a table, one red and one green. One contains a treasure. The red box is labelled "exactly one of the labels is true". The green box is labelled "the treasure is in this box."

Can you figure out which box contains the treasure?

The treasure is in the red box
The treasure is in the green box
There is not enough information to determine the answer
Something else:
Starting on 2015-07-03, the solution will be here.

by Mark Dominus ([email protected]) at July 01, 2015 03:13 PM

Philip Wadler

The Thrilling Adventures of Lovelace and Babbage

Sydney Padua explores an alternate universe wherein Ada Lovelace and Charles Babbage complete the Analytical Engine and use it to (at the order of Queen Victoria) fight crime. I've blogged before about the web comic, but the book is even better.

Padua's tome reconciles hilarity with accuracy. I am not normally a fan of footnotes: if it is worth saying, say it inline; don't force your poor reader to break the flow of thought and eye, and leap to the bottom of the page. But here is the glorious exception, where the footnotes supplement, argue with, and occasionally threaten to overflow the comic. Even the footnotes have footnotes: endnotes cite sources for the dialogue, present pocket biographies of Ada and Charles' contemporaries Isambard Kingdom Brunel, Charles Dodgson, and George Boole, quote at length from original sources, and explain the workings of the Analytic Engine. In the midst of an illustrated fantasia riff on Alice in Wonderland, the footnotes pursue an academic war as to whether or not Babbage truly considered Lovelace to be the Empress of Number. Padua makes pursuit of Victorian arcana a thrilling adventure of its own. Highly recommended!


by Philip Wadler ([email protected]) at July 01, 2015 10:29 AM

Douglas M. Auclair (geophf)

1HaskellADay June 2015 Problems and Solutions

June 2015

  • June 30th, 2015: Count Dracula has just enough time for a quickie, and today's #haskell problem http://lpaste.net/8137099602819022848 
    <iframe allowfullscreen="" class="YOUTUBE-iframe-video" data-thumbnail-src="https://i.ytimg.com/vi/n70vAulsh6I/0.jpg" frameborder="0" height="266" src="https://www.youtube.com/embed/n70vAulsh6I?feature=player_embedded" width="320"></iframe>
    Count Dracula: "Vithd you, never a quickie ... alwayz a longie! Bla-blah-blaaaah!" ... and the solution http://lpaste.net/7601734639496986624
  • June 29th, 2015: Toodle-pip! Word-frequency of a novel purportedly written in 'Hinglish, don't you know!' http://lpaste.net/7805322136641339392 Today's #haskell problem That solution is SO my bag!http://lpaste.net/7435942974816518144
  • June 26th, 2015: THUGs hate code duplication. I bet you didn't know that about THUGs. #thuglife With today's #haskell problem, you do. http://lpaste.net/87111690633609216 The solution is awesome, because reasons. http://lpaste.net/3951774515419152384
  • June 25th, 2015: We solve today's #haskell problem like a Thug. A CANADIAN Thug http://lpaste.net/183406472317632512 … #ThugLife When a THUG wants a cup-o-joe, it just makes sense to give'm dat cup-o-joe when he throws down dat Hamilton http://lpaste.net/8960298568350957568 #thuglife
  • June 24th, 2015: Today's #haskell problem shows us Mad Dad is Sad ... http://lpaste.net/1360790418425380864 … ... AND CANADIAN! AND SO ARE YOU! #whendidthathappen
  • June 23rd, 2015: Banana Fish! I don't know what that means, but: http://lpaste.net/4698665561507233792 (I also don't know what map 'a'-"apple" 'b'-"banana" means, either). Dad even got the banana WITH TAXES! http://lpaste.net/51803352903712768 But is Dad happy? Oh, no! See today's problem (forthcoming)
  • June 22nd, 2015: A couple of range-like thingies for today's #haskell problem http://lpaste.net/9214672078085554176 'Thingies' is a technical term. Arrows for ranges? http://lpaste.net/3818460590272151552 Who knew that could be a 'thing'? (Again, technical term. It means: 'thing.')
  • June 19th, 2015: 
♫ Grease is the word,
is the word,
is the word,
that you heard,..
http://lpaste.net/5444203916235374592
... and is today's #haskell problem. #graph 
O! What a tangled web we weave! http://lpaste.net/1406493831142047744 Contracts between corporations #graph Using #neo4j to show complex interrelationships between corporations #haskell
  • June 18th, 2015: Graph owners of companies ... LIKE A BOSS for today's #haskell problem http://lpaste.net/8745167156892663808 def #NSFW-youtube-link: 
    <iframe allowfullscreen="" class="YOUTUBE-iframe-video" data-thumbnail-src="https://i.ytimg.com/vi/NisCkxU544c/0.jpg" frameborder="0" height="266" src="https://www.youtube.com/embed/NisCkxU544c?feature=player_embedded" width="320"></iframe>
    Take this #graph and shove it; I don' work here anymore! A solution http://lpaste.net/497988783522709504

  • June 17th, 2015: What does Hannibal Lecter have to do with today's #Haskell problem? http://lpaste.net/3911201767555072000 Well, actually nothing. Good for name-dropping ;)
    <iframe allowfullscreen="" class="YOUTUBE-iframe-video" data-thumbnail-src="https://i.ytimg.com/vi/vyGSaTC5rdc/0.jpg" frameborder="0" height="266" src="https://www.youtube.com/embed/vyGSaTC5rdc?feature=player_embedded" width="320"></iframe>
    Ooh! pritti colours! Lines and circles! ME. LIKEY! http://lpaste.net/1108939510487449600 Visualizing relations between companies and their employees in #neo4j #graph database #bigdata

  • June 16th 2015: Business. Commerce. Relationships. And the plot thickens for today's #haskell problem http://lpaste.net/2159896812155043840 You scratched my back, so the solution will scratch yours: http://lpaste.net/6209720607693602816
  • June 15th, 2015: We're told to 'mind our own business.' For today's #haskell problem, however, we don't. http://lpaste.net/409939376974331904 If all the world were 450 businesses ...huh, don't know how to end that couplet, so I'll just share the solution: http://lpaste.net/4134898821270339584
  • June 12th, 2015: Today's Haskell problem is really simple: http://lpaste.net/176873973089304576 Write a Haskell Database. ;)
  • June 11th, 2015: A mapping of a map of categories to various sets of symbols. Not at all a Graph. Nope. Not at all. http://lpaste.net/106990139309293568 So, forewarning: there is wootage to be found in the solution http://lpaste.net/1443717939034324992 
  • June 10th, 2015: FREE LATIN LESSONS with today's #haskell problem! AND curl, but as long as you don't sudo bash you should be okay ... http://lpaste.net/8023684639111512064
  • June 9th, 2015: LET'S PRETEND! that today is yesterday, huh? So 'today's #haskell problem is about Options Tradinghttp://lpaste.net/3308567286981328896 ... not really.
  • June 8th, 2015: Improving the accuracy of the stddev modifier is the topic for today's #haskell problem http://lpaste.net/2181777565994188800
  • June 5th, 2015: Today's #haskell problem is kinda from Haskell by Example http://lpaste.net/1846897956607754240 Maps don't love you like I love you 
<iframe allowfullscreen="" class="YOUTUBE-iframe-video" data-thumbnail-src="https://i.ytimg.com/vi/oIIxlgcuQRU/0.jpg" frameborder="0" height="266" src="https://www.youtube.com/embed/oIIxlgcuQRU?feature=player_embedded" width="320"></iframe>
Hey, did you just make a map from a map and a multimap? http://lpaste.net/1944556995998646272 Is that even allowed? Yes, ... yes, it is.
  • June 4th, 2015: Peano's big TOE has a #haskell problem for you today, rollin' on the river http://lpaste.net/8694895204643110912 Types can be ... helpful in modeling solutions. Yeah. http://lpaste.net/6112991888283795456
  • June 3rd, 2015: As we're not going to do switch for today's #haskell problem (Why? BECAUSE I SAID SO), let's deredundancify an array. http://lpaste.net/2725173830396936192 An array by any other name is just a graph http://lpaste.net/6699309431617748992 ... hey, it's possible!
  • June 2nd, 2015: Today's #haskell problem is called 'twixt' and is inspired from a tweet by @jamestanton http://lpaste.net/4168110918607044608 Betwixt a rock and a prime place lies the solution http://lpaste.net/5331587919524134912
  • June 1st, 2015: These factorials are prime for ... primes. Erhm, yeah. http://lpaste.net/6303441488491577344 Today's #haskell problem from @jamestanton

by geophf ([email protected]) at July 01, 2015 09:38 AM

Thiago Negri

Haskell is just some steps away from Java

Start with Java, then:
  1. Forbid using null;
  2. Use only immutable objects, add "final" modifier to everything;
  3. Swap methods by static functions with the the original "this" as the first argument, e.g. "foo.bar()" turns into "bar(foo)";
  4. Add a lot of features to the type system;
  5. Remove type annotations, i.e. "Foo bar(Foo self)" turns into "bar(self)";
  6. Remove useless parens, i.e. "bar(foo)" turns into "bar foo";
  7. Add call-by-need evaluation;
  8. Done, you have Haskell.
It's not that hard, is it?

One, using null references is a recognized bad practice, see "Null References: The Billion Dollar Mistake." Java 8 already provides the Optional type to stop using nulls.

Two, immutable objects are a win strategy, see posts by Hirondelle Systems, IBM, Yegor, and others.

Three, as you only have immutable objects, there is no reason to use methods instead of static functions, considering you maintain polymorphism (not quite the case for Java, but for the sake of this rant, consider as if it has this feature).

Four, improve the type system. The type system used by Java language misses a lot of features. If you don't feel it, just consider this as an added bonus. When you start using the type system features in your favor, you end up with much better code.

Five, imagine the Java compiler could infer the type of the arguments, so you don't need to type them everywhere. You still have the same static typing language, you just don't need to write the types. Shorter code means less liability to haunt you.

Six, why all those parens? Just drop them. Less code to write, hurray!

Seven, call-by-need just makes a lot of things easier (also makes a lot of things harder), but I really think it is a winner when you talk about productivity. When coding, I feel it a lot easier to express things in terms of values instead of steps (mathematicians have been doing this since long before computers). Expressing things in terms of values in a universe without call-by-need will result in a lot of useless computations, so call-by-need is a must.

Eight, done! This is Haskell. No functors, monads, arrows, categories or lists needed.

Why this post? Well, I don't know. It just occurred to me that if you really go into following good coding practices in Java (e.g. avoid null, use immutable objects), you will eventually feel familiar with functional code. Add some more things to the mix, and you end up with Haskell. I think people feel a bit scared at first contact with Haskell (and family) because of the academic and mathematical atmosphere it has, but in the end it is just a lot of good practices that you are kind of required to comply with.

by Thiago Negri ([email protected]) at July 01, 2015 01:35 AM

June 30, 2015

Functional Jobs

Senior Developer at Elsen, Inc. (Full-time)

Elsen is building the next generation of market simulation software at the intersection of high performance computing, machine learning, and quantitative finance. We're a small, tight-knit team located in the financial district of downtown Boston.

We are looking for a senior software developer to help extend our infrastructure which is written in Haskell, C, and Python. Although substantial knowledge of Haskell is desired, we are primarily looking for individuals with demonstrated experience in financial modeling and the ability to implement ideas quickly and accurately.

Some things we look for in an candidate:

  • Open source involvement
  • Deep understanding of quantitative modeling
  • PostgreSQL or similar database familiarity
  • Understanding of various parallelism techniques (threads, software transactional memory, GPUs, distributed computing)
  • Technical analysis with ta-lib
  • Use of iteratee Haskell libraries (conduit/pipes)
  • Experience with modern C development
  • NumPy/SciPy/Pandas experience
  • Open to playing complex board games from time to time
  • Overall fun-loving personality and good sense of humor

Get information on how to apply for this position.

June 30, 2015 08:36 PM

Dimitri Sabadie

smoothie-0.3, Bézier curves and new user interface

Bezier curves

It’s been a while I’ve been wanting to do that. Now it’s done! smoothie, a Haskell package for dealing with curves and splines, updated to version 0.3.

That version introduces several changes. If you’re a good programmer, you might already have noticed that the major version got incremented. That means there’re compatibility breaking changes. If you don’t know what I’m talking about, you should definitely read this.

The first – non-breaking – change is that the package now supports Bézier interpolation! I’ve been reading about Bézier curves for a while because there’re very present and important for animation purposes – think of Blender. Feel free to dig in the documentation on hackage for further details.

The second – breaking – change is that the interface has changed, especially the implementation of splines. However, the interface is now simpler and doesn’t require a lot of change in your code if you’ve been using older versions.

Feel free to read the CHANGELOG for technical hints.

As always, tell me what you think of the library, and keep the vibe!

by Dimitri Sabadie ([email protected]) at June 30, 2015 05:28 PM

June 29, 2015

Dimitri Sabadie

Mac OS X support in al-0.1.4

Support for Mac users!

This will be a short announcement about al, a Haskell wrapper to the OpenAL C library.

Currently, the wrapper has been successfully tested on Linux – at least it works well on my Archlinux distro. I made a little program that reads from an .ogg file and streams the PCM signal to the wrapper – see libvorbis for further details. I’ll release the program later on if I find the spare time.

The wrapper might also work on Windows as long as you have pkg-config installed. I’d be very happy with feedback from people working on Windows. I don’t want anyone be put apart with my packages.

However, I’ve never tested the wrapper on Mac OS X. I guessed it wouldn’t work out of the box because Mac OS X doesn’t use regular libraries to compile and link – that would have been too easy otherwise, and hell, think different right? They use something called a framework. It’s possible to include a framework in a Haskell project by fulfilling the frameworks field in the .cabal file. I received a simple patch to do that – here, and I merged it upstream.

Then, Mac OS X is now officially supported. The release version is the 0.1.4.

About stackage

There’s something else I’d like to discuss. Quickly after the first release of al, I decided to push it onto stackage. Unfortunately, there’s a problem with the package and Ubuntu. For a very dark reason, Ubuntu doesn’t expose anything when invoking pkg-confg --cflags, even if the files are there – on Ubuntu they can be found in /usr/include/AL.

That’s very silly because I don’t want to hardcode the location – it might be something else on other Linux distro. The problem might be related to the OpenAL support in Ubuntu – the .pc file used by pkg-config might be incomplete. So if you experience that kind of issue, you can fix it by passing the path to your OpenAL headers:

cabal install al --extra-include-dirs=/usr/include/AL

If OpenAL is installed somewhere else, consider using:

find / -name al.h

I’ll do my best to quickly fix that issue.

by Dimitri Sabadie ([email protected]) at June 29, 2015 06:43 PM

Douglas M. Auclair (geophf)

Tabular and Visual Representations of Data using Neo4J

Corporate and Employee Relationships
Both Graphical and Tabular Results

So, there are many ways to view data, and people may have different needs for representing that data, either for visualization (in a graph:node-edges-view) or for tabulation/sorting (in your standard spreadsheet view).

So, can Neo4J cater to both these needs?

Yes, it can.

Scenario 1: Relationships of owners of multiple companies

Let's say I'm doing some data exploration, and I wish to know who has interest/ownership in multiple companies? Why? Well, let's say I'm interested in the Peter-Paul problem: I want to know if Joe, who owns company X is paying company Y for whatever artificial scheme to inflate or to deflate the numbers of either business and therefore profit illegally thereby.

Piece of cake. Neo4J, please show me the owners, sorted by the number of companies owned:

MATCH (o:OWNER)--(p:PERSON)-[r:OWNS]->(c:CORP)
RETURN p.ssn AS Owner, collect(c.name) as Companies, count(r) as Count 
ORDER BY Count DESC


Diagram 1: Owners by Company Ownership

Boom! There you go. Granted, this isn't a very exciting data set, as I did not have many owners owning multiple companies, but there you go.

What does it look like as a graph, however?

MATCH (o:OWNER)--(p:PERSON)-[r:OWNS]->(c:CORP)-[:EMPLOYS]->(p1) 
WHERE p.ssn in [2879,815,239,5879] 
RETURN o,p,c,p1


Diagram 2: Some companies with multiple owners

To me, this is a richer result, because it now shows that owners of more than one company sometimes own shares in companies that have multiple owners. This may yield interesting results when investigating associates who own companies related to you. This was something I didn't see in the tabular result.

Not a weakness of Neo4J: it was a weakness on my part doing the tabular query. I wasn't looking for this result in my query, so the table doesn't show it.

Tellingly, the graph does.

Scenario 2: Contract-relationships of companies 

Let's explore a different path. I wish to know, by company, the contractual-relationships between companies, sorted by companies with the most contractual-relationships on down. How do I do that in Neo4J?

MATCH (c:CORP)-[cc:CONTRACTS]->(c1:CORP) 
RETURN c.name as Contractor, collect(c1.name) as Contractees, count(cc) as Count 
ORDER BY Count DESC


Diagram 3: Contractual-Relationships between companies

This is somewhat more fruitful, it seems. Let's, then, put this up into the graph-view, looking at the top contractor:

MATCH (p:PERSON)--(c:CORP)-[:CONTRACTS*1..2]->(c1:CORP)--(p1:PERSON) 
WHERE c.name in ['YFB'] 
RETURN p,c,c1,p1


Diagram 4: Contractual-Relationships of YFB

Looking at YFB, we can see contractual-relationships 'blossom-out' from it, as it were, and this is just immediate, then distance 1 from that out! If we go out even just distance 1 more in the contracts, the screen fills with employees, so then, again, you have the forest-trees problem where too much data is hiding useful results with data.

Let's prune these trees, then. Do circular relations appear?

MATCH (c:CORP)-[:CONTRACTS*1..5]->(c1:CORP) WHERE c.name in ['YFB'] RETURN c,c1


Diagram 5: Circular Relationship found, but not in YFB! Huh!

Well, would you look at that. This shows the power of the visualization aspect of graph databases. I was examining a hot-spot in corporate trades, YFB, looking for irregularities there. I didn't find any, but as I probed there, a circularity did surface in downstream, unrelated companies: the obvious one being between AZB and MZB, but there's also a circular-relationship that becomes apparent starting with 4ZB, as well. Yes, this particular graph is noisy, but it did materialize an interesting area to explore that may very well have been overlooked with legacy methods of investigation.

Graph Databases.


BAM.

by geophf ([email protected]) at June 29, 2015 06:25 PM

Philip Wadler

Yesod Web Framework

stack support for yesod devel

Since the release of the stack build tool, I think I've received four different requests and bug reports about stack support in Yesod. The sticking point is that yesod devel has not- until now- had support for using stack. The original plan was to wait for Njagi Mwaniki's Google Summer of Code project to finish the new ide-backend based yesod devel. However, demand for this feature was too high, so I'm happy to announce official stack support in yesod-bin-1.4.11.

This blog post should be consider a beta announcement for using Yesod with stack. Please test and report issues. Also, the workflow is not yet perfected. Once we get stack new written and add ide-backend support, things will be much smoother. For now, here's the workflow:

# Install both yesod-bin and cabal-install. Both are still necessary
$ stack install yesod-bin-1.4.11 cabal-install
# Initialize your project
$ stack exec yesod init
$ cd new-directory
# Create stack.yaml
$ stack init
# Build your project to get al dependencies
# Also rebuild yesod-bin with the current GHC, just to be safe
$ stack build yesod-bin-1.4.11 .
# Now run yesod devel
$ stack exec yesod devel

Like I said, this is a little kludgy right now, but will smooth out over time.

Technical details

If you're curious in how I added this support, the commit is really short. And there's not actually anything stack-specific in here, it's just working around a well known limitation in cabal which makes it incompatible with the GHC_PACKAGE_PATH environment variable. All we do in yesod devel is:

  • Detect the GHC_PACKAGE_PATH variable
  • Turn it into --package-db arugments to cabal configure
  • Remove GHC_PACKAGE_PATH from the environment of the cabal process

It would be nice if cabal got this functionality itself in the future, but I believe the current implementation was a design goal of the cabal team.

June 29, 2015 12:00 AM

Danny Gratzer

Proving Cut Admissibility in Twelf

Posted on June 29, 2015
Tags: twelf, types

Veering wildly onto the theory side compared to my last post, I’d like to look at some more Twelf code today. Specifically, I’d like to prove a fun theorem called cut admissibility (or elimination) for a particular logic: a simple intuitionistic propositional sequent calculus. I chucked the code for this over here.

Background

If those words didn’t make any sense, here’ an incomplete primer on what we’re doing here. First of all we’re working with a flavor of logic called “sequent calculus”. Sequent calculus describes a class of logics characterized by using studying “sequents”, a sequent is just an expression Γ ⊢ A saying “A is true under the assumption that the set of propositions, Γ, are true”. A sequent calculus defines a couple things

  1. What exactly A is, a calculus defines what propositions it talks about

    For us we’re only interested in a few basic connectives, so our calculus can talk about true, false, A and B (A ∧ B), A or B (A ∨ B), and A implies B (A ⇒ B).

  2. Rules for inferring Γ ⊢ A holds. We can use these inference rules to build up proofs of things in our system.

    In sequent calculus there are two sorts of inference rules, left and right. A left rule takes a fact that we know and let’s us reason backwards to other things we must know hold. A right rule let’s us take the thing we’re trying to prove and instead prove smaller, simpler things.

    More rules will follow in the Twelf code but for a nice example consider the left and right rules for ,

      Γ, A, B ⊢ C
     ———————————————
      Γ, A ∧ B ⊢ C
    
     Γ ⊢ A    Γ ⊢ B
     ———————————————
        Γ ⊢ A ∧ B

    The left rule says if we know that A ∧ B is true, we can take it apart and try to prove our goal with assumptions that A and B are true. The right rule says to prove that A ∧ B is true we need to prove A is true and B is true. A proof in this system is a true of these rules just like you’d expect in a type theory or natural deduction.

We also tacitly assume a bunch of boring rules called structural rules about our sequents hold, so that we can freely duplicate, drop and swap assumptions in Γ. For a less awful introduction to sequent calculus Frank Pfenning has some good notes.

Now we want to prove a particular (meta)theorem about sequent calculus

  1. if Γ ⊢ A
  2. and Γ, A ⊢ B
  3. then Γ ⊢ B

This theorem means a couple different things for example, our system is consistent and our system also admits lemmas. As it turns out, proving this theorem is hard. The basic complication is that we don’t know what form either of the first two proofs.

The Twelf Stuff

We now formalize our sequent calculus in Twelf. First we declare a type and some constants to represent propositions.

    prop  : type.

    =>    : prop -> prop -> prop. %infix right 4 =>.
    true  : prop.
    false : prop.
    /\    : prop -> prop -> prop. %infix none 5 /\.
    \/    : prop -> prop -> prop. %infix none 5 \/.

Notice here that we use infix to let us write A /\ B => C. Having specified these we now define what a proof is in this system. This is structured a little differently than you’d be led to believe from the above. We have an explicit type proof which is inhabited by “proof terms” which serve as a nice shortcut to those trees generated by inference rules. Finally, we don’t explicitly represent Γ, instead we have this thing called hyp which is used to represent a hypothesis in Γ. Left rules manipulate use these hypotheses and introduce new ones. Pay attention to /‌\/l and /‌\/r since you’ve seen the handwritten equivalents.

    proof   : type.
    hyp     : type.

    init    : hyp -> proof.

    =>/r    : (hyp -> proof) -> proof.
    =>/l    : (hyp -> proof) -> proof -> hyp -> proof.

    true/r  : proof.

    false/l : hyp -> proof.

    /\/r    : proof -> proof -> proof.
    /\/l    : (hyp -> hyp -> proof) -> hyp -> proof.

    \//r1   : proof -> proof.
    \//r2   : proof -> proof.
    \//l    : (hyp -> proof) -> (hyp -> proof) -> hyp -> proof.

The right rules are at least a little intuitive, the left rules are peculiar. Essentially we have a weird CPS-y feel going on here, to decompose a hypothesis you hand the hyp to the constant along with a continuation which takes the hypotheses you should get out of the decomposition. For example for ‌\/ we have to right rules (think Left and Right), then one left rule which takes two continuations and one hyp (think either). Finally, that init thing is the only way to actually take a hypothesis and use it as a proof.

We now want to unite these two pieces of syntax with a typing judgment letting us say that a proof proves some particular prop.

    of         : proof -> prop -> type.
    hof        : hyp   -> prop -> type.

    of/init    : of (init H) A
                  <- hof H A.

    of/=>/r    : of (=>/r F) (A => B)
                  <- ({h} hof h A -> of (F h) B).
    of/=>/l    : of (=>/l C Arg F) U
                  <- hof F (A => B)
                  <- of Arg A
                  <- ({h} hof h B -> of (C h) U).

    of/true/r  : of true/r true.

    of/false/l : of (false/l H) A
                  <- hof H false.

    of//\/r    : of (/\/r R L) (A /\ B)
                  <- of L A
                  <- of R B.
    of//\/l    : of (/\/l C H) U
                  <- hof H (A /\ B)
                  <- ({h}{h'} hof h A -> hof h' B -> of (C h h') U).

    of/\//r1   : of (\//r1 L) (A \/ B)
                  <- of L A.
    of/\//r2   : of (\//r2 R) (A \/ B)
                  <- of R B.
    of/\//l    : of (\//l R L H) C
                  <- hof H (A \/ B)
                  <- ({h} hof h A -> of (L h) C)
                  <- ({h} hof h B -> of (R h) C).

In order to handle hypotheses we have this hof judgment which handles typing various hyps. We introduce it just like we introduce hyps in those continuation-y things for left rules. Sorry for dumping so much code on you all at once: it’s just a lot of machinery we need to get working in order to actually start formalizing cut.

I would like to point out a few things about this formulation of sequent calculus though. First off, it’s very Twelf-y, we use the LF context to host the context of our logic using HOAS. We also basically just have void as the type of hypothesis! Look, there’s no way to construct a hypothesis, let alone a typing derivation hof! The idea is that we’ll just wave our hands at Twelf and say “consider our theorem in a context with hyps and hofs with

    %block someHofs : some {A : prop} block {h : hyp}{deriv : hof h A}.

In short, Twelf is nifty.

The Theorem

Now we’re almost in a position to state cut admissibility, we want to say something like

    cut : of Lemma A
            -> ({h} hyp h A -> of (F h) B)
            -> of ??? B

But what should that ??? be? We could just say “screw it it’s something” and leave it as an output of this lemma but experimentally (an hour of teeth gnashing later) it’s absolutely not worth the pain. Instead let’s do something clever.

Let’s first define an untyped version of cut which works just across proofs without mind to typing derivations. We can’t declare this total because it’s just not going to work for ill-typed things, we can give it a mode though (it’s not needed) just as mechanical documentation.

    cut : proof -> (hyp -> proof) -> proof -> type.
    %mode cut +A +B -C.

The goal here is we’re going to state our main theorem as

    of/cut : {A} of P A
              -> ({h} hof h A -> of (F h) B)
              -> cut P F C
              -> of C B
              -> type.
    %mode of/cut +A +B +C -D -E.

Leaving that derivation of cut as an output. This let’s us produce not just a random term but instead a proof that that term makes “sense” somehow along with a proof that it’s well typed.

cut is going to mirror the structure of of/cut so we now need to figure out how we’re going to structure our proof. It turns out a rather nice way to do this is to organize our cuts into 4 categories. The first one are “principle” cuts, they’re the ones where we have a right rule as our lemma and we immediately decompose that lemma in the other term with the corresponding left rule. This is sort of the case that we drive towards everywhere and it’s where the substitution bit happens.

First we have some simple cases

    trivial : cut P' ([x] P) P.
    p/init1 : cut (init H) ([x] P x) (P H).
    p/init2 : cut P ([x] init x) P.

In trivial we don’t use the hypothesis at all so we’re just “strengthening” here. p/init1 and p/init2 deal with the init rule on the left or right side of the cut, if it’s on the left we have a hypothesis of the appropriate type so we just apply the function. If it’s on the left we have a proof of the appropriate type so we just return that. In the more interesting cases we have the principle cuts for some specific connectives.

    p/=>   : cut (=>/r F) ([x] =>/l ([y] C y x) (Arg x) x) Out'
              <- ({y} cut (=>/r F) (C y) (C' y))
              <- cut (=>/r F) Arg Arg'
              <- cut Arg' F Out
              <- cut Out C' Out'.
    p//\   : cut (/\/r R L) ([x] /\/l ([y][z] C y z x) x) Out'
              <- ({x}{y} cut (/\/r R L) (C x y) (C' x y))
              <- ({x} cut R (C' x) (Out x))
              <- cut L Out Out'.
    p/\//1 : cut (\//r1 L) ([x] \//l ([y] C2 y x) ([y] C1 y x) x) Out
              <- ({x} cut (\//r1 L) (C1 x) (C1' x))
              <- cut L C1' Out.
    p/\//2 : cut (\//r2 L) ([x] \//l ([y] C2 y x) ([y] C1 y x) x) Out
              <- ({x} cut (\//r2 L) (C2 x) (C2' x))
              <- cut L C2' Out.

Let’s take a closer look at p/=>, the principle cut for =>. First off, our inputs are =>/r F and ([x] =>/l ([y] C y x) (Arg x) x). The first one is just a “function” that we’re supposed to substitute into the second. Now the second is comprised of a continuation and an argument. Notice that both of these depend on x! In order to handle this the first two lines of the proof

           <- ({y} cut (=>/r F) (C y) (C' y))
           <- cut (=>/r F) Arg Arg'

Are to remove that dependence. We get back a C' and an Arg' which doesn’t use the hyp (x). In order to do this we just recurse and cut the =>/r F out of them. Notice that both the type and the thing we’re substituting are the same size, what decreases here is what we’re substituting into. Now we’re ready to actually do some work. First we need to get a term representing the application of F to Arg'. This is done with cut since it’s just substitution

              <- cut Arg' F Out

But this isn’t enough, we don’t need the result of the application, we need the result of the continuation! So we have to cut the output of the application through the continuation

              <- cut Out C' Out'.

This code is kinda complicated. The typed version of this took me an hour since after 2am I am charitably called an idiot. However this same general pattern holds with all the principle cuts

  1. The subterms of the target could depend on what we’re substituting for, so get rid of that dependence with a recursive call.
  2. Get the “result”, which is just the term corresponding to the hypothesis the continuation is expecting. This is pretty trivial in all cases except => since it’s just lying about in an input.
  3. Get the actual result by cutting 2. through the continuation.

Try to work through the case for /\ now

    p//\   : cut (/\/r R L) ([x] /\/l ([y][z] C y z x) x) Out'
              <- ({x}{y} cut (/\/r R L) (C x y) (C' x y))
              <- ({x} cut R (C' x) (Out x))
              <- cut L Out Out'.

After principle cuts we really just have a number of boring cases whose job it is to recurse. The first of these is called rightist substitution because it comes up if the term on the right (the part using the lemma) has a right rule first. This means we have to hunt in the subterms to go find where we’re actually using the lemma.

    r/=> : cut P ([x] (=>/r ([y] F y x))) (=>/r ([y] F' y))
            <- ({x} cut P (F x) (F' x)).
    r/true : cut P ([x] true/r) true/r.
    r//\ : cut P ([x] /\/r (R x) (L x)) (/\/r R' L')
            <- cut P L L'
            <- cut P R R'.
    r/\/1 : cut P ([x] \//r1 (L x)) (\//r1 L')
             <- cut P L L'.
    r/\/2 : cut P ([x] \//r2 (R x)) (\//r2 R')
             <- cut P R R'.

Nothing here should be surprising keeping in mind that all we’re doing here is recursing. The next set of cuts is called leftist substitution. Here we are actually recursing on the term we’re trying to substitute.

    l/=>    : cut (=>/l ([y] C y) Arg H) ([x] P x) (=>/l ([x] C' x) Arg H)
               <- ({x} cut (C x) P (C' x)).
    l/false : cut (false/l H) P (false/l H).
    l//\    : cut (/\/l ([x][y] C x y) H) P (/\/l ([x][y] C' x y) H)
               <- ({x}{y} cut (C x y) P (C' x y)).
    l/\/    : cut (\//l ([y] R  y) ([y] L  y) H) ([x] P x)
                  (\//l ([y] R' y) ([y] L' y) H)
               <- ({x} cut (L x) P (L' x))
               <- ({x} cut (R x) P (R' x)).

It’s the same game but just a different target, we’re now recursing on the continuation because that’s where we somehow created a proof of A. This means that on l/=> we’re substation left term which has three parts

  1. A continuation, hyp B to proof of C
  2. An argument of type A
  3. A hypothesis of type A -> B

Now we’re only interesting in how we created that proof of C, that’s the only relevant part of this substitution. The output of this case is going to have that left rule, =>/l ??? Arg H so we have where ??? is a replacement of C that we get by cutting C through P “pointwise”. This comes through on the recursive call

               <- ({x} cut (C x) P (C' x)).

For one more case, consider the left rule for \/

    l/\/    : cut (\//l R L H) P

We start by trying to cut a left rule into P so we need to produce a left rule in the output with different continuations, something like

               (\//l R' L' H)

Now what should R' and L' be? In order to produce them we’ll throw up a pi so we can get L x, a proof with the appropriate type to cut again. With that, we can recurse and get back the new continuation we want.

               <- ({x} cut (L x) P (L' x))
               <- ({x} cut (R x) P (R' x)).

There’s one last class of cuts to worry about, think about the cases we’ve covered so far

  1. The left term is a left rule (leftist substitution)
  2. The right term is a right rule (rightist substitution)
  3. The terms match up and we substitute

So what happens if we have a left rule on the right and a right rule on the left, but they don’t “match up”. By this I mean that the left rule in that right term works on a different hypothesis than the one that the function it’s wrapped in provides. In this case we just have to recurse some more

    lr/=> : cut P ([x] =>/l ([y] C y x) (Arg x) H) (=>/l C' Arg' H)
             <- cut P Arg Arg'
             <- ({y} cut P (C y) (C' y)).
    lr//\ : cut P ([x] /\/l ([y][z] C y z x) H) (/\/l C' H)
             <- ({y}{z} cut P (C y z) (C' y z)).
    lr/\/ : cut P ([x] \//l ([y] R y x) ([y] L y x) H) (\//l R' L' H)
             <- ({y} cut P (L y) (L' y))
             <- ({y} cut P (R y) (R' y)).

When we have such an occurrence we just do like we did with right rules.

Okay, now that we’ve handled all of these cases we’re ready to type the damn thing.

    of/cut : {A} of P A
              -> ({h} hof h A -> of (F h) B)
              -> cut P F C
              -> of C B
              -> type.
    %mode of/cut +A +B +C -D -E.

Honestly this is less exciting than you’d think. We’ve really done all the creative work in constructing the cut type family. All that’s left to do is check that this is correct. As an example, here’s a case that exemplifies how we verify all left-right commutative cuts.

    - : of/cut _ P ([x][h] of/=>/l ([y][yh] C y yh x h) (A x h) H)
         (lr/=> CC CA) (of/=>/l C' A' H)
         <- of/cut _ P A CA A'
         <- ({y}{yh} of/cut _ P (C y yh) (CC y) (C' y yh)).

We start by trying to show that

    lr/=> : cut P ([x] =>/l ([y] C y x) (Arg x) H) (=>/l C' Arg' H)
             <- cut P Arg Arg'
             <- ({y} cut P (C y) (C' y)).

Is type correct. To do this we have a derivation P that the left term is well-typed. Notice that I’ve overloaded P here, in the rule lr/=> P was a term and now it’s a typing derivation for that term. Next we have a typing derivation for [x] =>/l ([y] C y x) (Arg x) H. This is a function which takes two arguments. x is a hypothesis, the same as in lr/=>, however now we have h which is a hof derivation that h has a type. There’s only one way to type a usage of the left rule for =>, with of/=>/l so we have that next.

Finally, our output is on the next line in two parts. First we have a derivation for cut showing how to construct the “cut out term” in this case. Next we have a new typing derivation that again uses of/=>/l. Notice that both of these depend on some terms we get from the recursive calls here.

Since we’ve gone through all the cases already and done all the thinking, I’m not going to reproduce it all here. The intuition for how cut works is really best given by the untyped version with the understand that we check that it’s correct with this theorem as we did above.

Wrap Up

To recap here’s what we did

  1. Define sequent calculus’ syntax
  2. Define typing rules across it
  3. Define how an untyped version of cut works across it
  4. Validate the correctness of cut by

Hope that was a little fun, cheers!

<script type="text/javascript"> var disqus_shortname = 'codeco'; (function() { var dsq = document.createElement('script'); dsq.type = 'text/javascript'; dsq.async = true; dsq.src = '//' + disqus_shortname + '.disqus.com/embed.js'; (document.getElementsByTagName('head')[0] || document.getElementsByTagName('body')[0]).appendChild(dsq); })(); </script> <noscript>Please enable JavaScript to view the comments powered by Disqus.</noscript> comments powered by Disqus

June 29, 2015 12:00 AM

June 27, 2015

Christopher Done

The path package

Here I’d like to announce and explain the motivations behind my path package.

Motivation

It was after working on a number of projects at FP Complete that use file paths in various ways. We used the system-filepath package, which was supposed to solve many path problems by being an opaque path type. It occurred to me that the same kind of bugs kept cropping up:

  • Expected a path to be absolute but it was relative, or vice-versa.
  • Expected two equivalent paths to be equal or order the same, but they did not (/home//foo vs /home/foo/ vs /home/bar/../foo, etc.).
  • Unpredictable behaviour with regards to concatenating paths.
  • Confusing files and directories.
  • Not knowing whether a path was a file or directory or relative or absolute based on the type alone was a drag.

All of these bugs are preventable.

Approach

My approach to problems like this is to make a type that encodes the properties I want and then make it impossible to let those invariants be broken, without compromise or backdoors to let the wrong value “slip in”. Once I have a path, I want to be able to trust it fully. This theme will be seen throughout the things I lay out below.

Solution

After having to fix bugs due to these in our software, I put my foot down and made:

  • An opaque Path type (a newtype wrapper around String).
  • Smart constructors which are very stringent in the parsing.
  • Make the parsers highly normalizing.
  • Leave equality and concatenation to basic string equality and concatenation.
  • Include relativity (absolute/relative) and type (directory/file) in the type itself.
  • Use the already cross-platform filepath package for implementation details.

Implementation

The data types

Here is the type:

newtype Path b t = Path FilePath
  deriving (Typeable)

The type variables are:

  • b - base, the base location of the path; absolute or relative.
  • t - type, whether file or directory.

The base types can be filled with these:

data Abs deriving (Typeable)
data Rel deriving (Typeable)

And the type can be filled with these:

data File deriving (Typeable)
data Dir deriving (Typeable)

(Why not use data kinds like data Type = File | Dir? Because that imposes an extension overhead of adding {-# LANGUAGE DataKinds #-} to every module you might want to write out a path type in. Given that one cannot construct paths of types other than these, via the operations in the module, it’s not a concern for me.)

There is a conversion function to give you back the filepath:

toFilePath :: Path b t -> FilePath
toFilePath (Path l) = l

Parsers

To get a path value, you need to use one of the four parsers:

parseAbsDir  :: MonadThrow m => FilePath -> m (Path Abs Dir)
parseRelDir  :: MonadThrow m => FilePath -> m (Path Rel Dir)
parseAbsFile :: MonadThrow m => FilePath -> m (Path Abs File)
parseRelFile :: MonadThrow m => FilePath -> m (Path Rel File)

The following properties apply:

  • Absolute parsers will reject non-absolute paths.
  • The only delimiter syntax accepted is the path separator; / on POSIX and \ on Windows.
  • Any other delimiter is rejected; .., ~/, /./, etc.
  • All parsers normalize into single separators: /home//foo -> /home/foo.
  • Directory parsers always normalize with a final trailing /. So /home/foo parses into the string /home/foo/.

It was discussed briefly whether we should just have a class for parsing rather than four separate parsing functions. In my experience so far, I have had type errors where I wrote something like x <- parseAbsDir someAbsDirString because x was then passed to a place that expected a relative directory. In this way, overloading the return value would’ve just been accepted. So I don’t think having a class is a good idea. Being explicit here doesn’t exactly waste our time, either.

Why are these functions in MonadThrow? Because it means I can have it return an Either, or a Maybe, if I’m in pure code, and if I’m in IO, and I don’t expect parsing to ever fail, I can use it in IO like this:

do x <- parseRelFile (fromCabalFileName x)
   foo x
   …

That’s really convenient and we take advantage of this at FP Complete a lot.

The instances

Equality, ordering and printing are simply re-using the String instances:

instance Eq (Path b t) where
  (==) (Path x) (Path y) = x == y

instance Ord (Path b t) where
  compare (Path x) (Path y) = compare x y

instance Show (Path b t) where
  show (Path x) = show x

Which gives us for free the following equational properties:

toFilePath x == toFilePath y        ≡ x == y           -- Eq instance
toFilePath x `compare` toFilePath y ≡ x `compare` y    -- Ord instance
toFilePath x == toFilePath y        ≡ show x == show y -- Show instance

In other words, the representation and the path you get out at the end are the same. Two paths that are equal will always give you back the same thing.

Smart constructors

For when you know what a path will be at compile-time, there are constructors for that:

$(mkAbsDir "/home/chris")
$(mkRelDir "chris")
$(mkAbsFile "/home/chris/x.txt")
$(mkRelFile "chris/x.txt")

These will run at compile-time and underneath use the appropriate parser.

Overloaded strings

No IsString instance is provided, because that has no way to statically determine whether the path is correct, and would otherwise have to be a partial function.

In practice I have written the wrong path format in a $(mk… "") and been thankful it was caught early.

Operations

There is path concatenation:

(</>) :: Path b Dir -> Path Rel t -> Path b t

Get the parent directory of a path:

parent :: Path Abs t -> Path Abs Dir

Get the filename of a file path:

filename :: Path b File -> Path Rel File

Get the directory name of a directory path:

dirname :: Path b Dir -> Path Rel Dir

Stripping the parent directory from a path:

stripDir :: MonadThrow m => Path b Dir -> Path b t -> m (Path Rel t)

Review

Let’s review my initial list of complaints and see if they’ve been satisfied.

Relative vs absolute confusion

Paths now distinguish in the type system whether they are relative or absolute. You can’t append two absolute paths, for example:

λ> $(mkAbsDir "/home/chris") </> $(mkAbsDir "/home/chris")
<interactive>:23:31-55:
    Couldn't match type ‘Abs’ with ‘Rel’

The equality problem

Paths are now stringently normalized. They have to be a valid path, and they only support single path separators, and all directories are suffixed with a trailing path separator:

λ> $(mkAbsDir "/home/chris//") == $(mkAbsDir "/./home//chris")
True
λ> toFilePath $(mkAbsDir "/home/chris//") ==
   toFilePath $(mkAbsDir "/./home//chris")
True
λ> ($(mkAbsDir "/home/chris//"),toFilePath $(mkAbsDir "/./home//chris"))
("/home/chris/","/home/chris/")

Unpredictable concatenation issues

Because of the stringent normalization, path concatenation, as seen above, is simply string concatenation. This is about as predictable as it can get:

λ> toFilePath $(mkAbsDir "/home/chris//")
"/home/chris/"
λ> toFilePath $(mkRelDir "foo//bar")
"foo/bar/"
λ> $(mkAbsDir "/home/chris//") </> $(mkRelDir "foo//bar")
"/home/chris/foo/bar/"

Confusing files and directories

Now that the path type is encoded in the type system, our </> operator prevents improper appending:

λ> $(mkAbsDir "/home/chris/") </> $(mkRelFile "foo//bar")
"/home/chris/foo/bar"
λ> $(mkAbsFile "/home/chris") </> $(mkRelFile "foo//bar")
<interactive>:35:1-26:
    Couldn't match type ‘File’ with ‘Dir’

Self-documentation

Now I can read the path like:

{ fooPath :: Path Rel Dir, ... }

And know that this refers to the directory relative to some other path, meaning I should be careful to consider the current directory when using this in IO, or that I’ll probably need a parent to append to it at some point.

In practice

We’ve been using this at FP Complete in a number of packages for some months now, it’s turned out surprisingly sufficient for most of our path work with only one bug found. We weren’t sure initially whether it would just be too much of a pain to use, but really it’s quite acceptable given the advantages. You can see its use all over the stack codebase.

Doing I/O

Currently any operations involving I/O can be done by using the existing I/O library:

doesFileExist (toFilePath fp)
readFile (toFilePath fp)

etc. This has problems with respect to accidentally running something like:

doesFileExist $(mkRelDir "foo")

But I/O is currently outside the scope of what this package solves. Once you leave the realm of the Path type invariants are back to your responsibility.

As with the original version of this library, we’re currently building up a set of functions in a Path.IO module over time that fits our real-world use-cases. It may or may not appear in the path package eventually. It’ll need cleaning up and considering what should really be included.

Doing textual manipulations

One problem that crops up sometimes is wanting to manipulate paths. Currently the way we do it is via the filepath library and re-parsing the path:

parseAbsFile . addExtension "/directory/path" "ext" . toFilePath

It doesn’t happen too often, in our experience, to the extent this needs to be more convenient.

Accepting user input

Sometimes you have user input that contains ../. The solution we went with is to have a function like resolveDir:

resolveDir :: (MonadIO m, MonadThrow m)
           => Path Abs Dir -> FilePath -> m (Path Abs Dir)

Which will call canonicalizePath which collapses and normalizes a path and then we parse with regular old parseAbsDir and we’re cooking with gas. This and others like it might get added to the path package.

Comparing with existing path libraries

filepath and system-filepath

The filepath package is intended as the complimentary package to be used before parsing into a Path value, and/or after printing from a Path value. The package itself contains no type-safety, instead contains a range of cross-platform textual operations. Definitely reach for this library when you want to do more involved manipulations.

The system-filepath package is deprecated in favour of filepath.

system-canonicalpath, canonical-filepath, directory-tree

The system-canonicalpath and the canonical-filepath packages both are a kind of subset of path. They canonicalize a string into an opaque path, but neither distinguish directories from files or absolute/relative. Useful if you just want a canonical path but doesn’t do anything else.

The directory-tree package contains a sum type of dir/file/etc but doesn’t distinguish in its operations relativity or path type.

pathtype

Finally, we come to a path library that path is similar to: the pathtype library. There are the same types of Path Abs File / Path Rel Dir, etc.

The points where this library isn’t enough for me are:

  • There is an IsString instance, which means people will use it, and will make mistakes.

  • Paths are not normalized into a predictable format, leading to me being unsure when equality will succeed. This is the same problem I encountered in system-filepath. The equality function normalizes, but according to what properties I can reason about? I don’t know.

System.Path.Posix> ("/tmp//" :: Path a Dir) == ("/tmp" :: Path a Dir)
True
System.Path.Posix> ("tmp" :: Path a Dir) == ("/tmp" :: Path a Dir)
True
System.Path.Posix> ("/etc/passwd/" :: Path a b) == ("/etc/passwd" :: Path a b)
True
System.Path.Posix> ("/tmp//" :: Path Abs Dir) == ("/tmp/./" :: Path Abs Dir)
False
System.Path.Posix> ("/tmp/../" :: Path Abs Dir) == ("/" :: Path Abs Dir)
False
  • Empty string should not be allowed, and introduction of . due to that gets weird:
System.Path.Posix> fmap getPathString (Right ("." :: Path Rel File))
Right "."
System.Path.Posix> fmap getPathString (mkPathAbsOrRel "")
Right "."
System.Path.Posix> (Right ("." :: Path Rel File)) == (mkPathAbsOrRel "")
False
System.Path.Posix> takeDirectory ("tmp" :: Path Rel Dir)
.
System.Path.Posix> (getPathString ("." :: Path Rel File) ==
                    getPathString ("" :: Path Rel File))
True
System.Path.Posix> (("." :: Path Rel File) == ("" :: Path Rel File))
False
  • It has functions like <.>/addExtension which lets you insert an arbitrary string into a path.

  • Some functions let you produce nonsense (could be prevented by a stricter type), for example:

System.Path.Posix> takeFileName ("/tmp/" :: Path Abs Dir)
tmp

I’m being a bit picky here, a bit unfair. But the point is really to show the kind of things I tried to avoid in path. In summary, it’s just hard to know where things can go wrong, similar to what was going on in system-filepath.

data-filepath

The data-filepath is also very similar, I discovered it after writing my own at work and was pleased to see it’s mostly the same. The main differences are:

  • Uses DataKinds for the relative/absolute and file/dir distinction which as I said above is an overhead.
  • Uses a GADT for the path type, which is fine. In my case I wanted to retain the original string which functions that work on the FilePath (String) type already deal with well. It does change the parsing step somewhat, because it parses into segments.
  • It’s more lenient at parsing (allowing .. and trailing .).

The API is a bit awkward to just parse a directory, requires a couple functions to get it (going via WeakFilePath), returning only an Either, and there are no functions like parent. But there’s not much to complain about. It’s a fine library, but I didn’t feel the need to drop my own in favor of it. Check it out and decide for yourself.

Summary

There’s a growing interest in making practical use of well-typed file path handling. I think everyone’s wanted it for a while, but few people have really committed to it in practice. Now that I’ve been using path for a while, I can’t really go back. It’ll be interesting to see what new packages crop up in the coming year, I expect there’ll be more.

June 27, 2015 12:00 AM

June 25, 2015

Douglas M. Auclair (geophf)

Business Interrelations as a Graph

We look at a practical application of Graph Theory to take a complex representation of information and distill it to something 'interesting.' And by 'interesting,' I mean: finding a pattern in the sea of information otherwise obscured (sometimes intentionally) by all the overwhelming availability of data.

We'll be working with a graph database created from biz.csv, so to get this started, load that table into neo4j:

USING PERIODIC COMMIT
LOAD CSV WITH HEADERS FROM "file:///[...]/biz.csv" AS csvLine
MERGE (b1:CORP { name: csvLine.contractor })
MERGE (b2:CORP { name: csvLine.contractee })

MERGE (b1)-[:CONTRACTS]->(b2)

We got to a graph of business interrelations this past week (see, e.g.: http://lpaste.net/5444203916235374592) showing who contracts with whom, and came to a pretty picture like this from the Cypher query:

MATCH (o:OWNER)--(p:PERSON)-[]->(c:CORP) RETURN o,p,c

diagram 1: TMI

That is to say: the sea of information. Yes, we can tell that businesses are conducting commerce, but ... so what? That's all well and good, but let's say that some businesses want to mask how much they are actually making by selling their money to other companies, and then getting it paid back to them. This is not an impossibility, and perhaps it's not all that common, but companies are savvy to watch dogs, too, so it's not (usually) going to be an obvious A -[contracts]-> B -[contracts] -> A relationship.

Not usually, sometimes you have to drill deeper, but if you drill too deeply, you get the above diagram which tells you nothing, because it shares too much information.

(Which you never want to do ... not on the first date, anyway, right?)

But the above, even though noisy, does show some companies contracting with other companies, and then, in turn being contracted by some companies.

So, let's pick one of them. How about company 'YPB,' for example? (Company names are changed to protect the modeled shenanigans)

MATCH (c:CORP)-[:CONTRACTS]->(c1:CORP) WHERE c.name='YPB' RETURN c, c1

diagram 2: tier 1 of YPB

So, in this first tier we see YPB contracting with four other companies. Very nice. Very ... innocuous. Let's push this inquiry to the next tier, is there something interesting happening here?

MATCH (c:CORP)-[:CONTRACTS*1..2]->(c1:CORP) WHERE c.name='YPB' RETURN c, c1

diagram 3: tier 2 of YPB

Nope. Or what is interesting is to see the network of businesses and their relationships (at this point, not interrelationships) begin to extend the reach. You tell your friends, they tell their friends, and soon you have the MCI business-model.

But we're not looking at MCI. We're looking at YPB, which is NOT MCI, I'd like to say for the record.

Okay. Next tier:

MATCH (c:CORP)-[:CONTRACTS*1..3]->(c1:CORP) WHERE c.name='YPB' RETURN c, c1

diagram 4: tier 3 of YPB

Okay, a little more outward growth. Okay. (trans: 'meh') How about the next tier, that is to say: tier 4?

MATCH (c:CORP)-[:CONTRACTS*1..4]->(c1:CORP) WHERE c.name='YPB' RETURN c, c1

diagram 5: tier 4 of YPB

So, we've gone beyond our observation cell, but still we have no loop-back to YPB. Is there none (that is to say: no circular return to YPB)? Let's push it one more time to tier 5 and see if we have a connection.

MATCH (c:CORP)-[:CONTRACTS*1..5]->(c1:CORP) WHERE c.name='YPB' RETURN c, c1


diagram 6: tier 5 with a (nonobvious) cycle of contracts

Bingo. At tier 5, we have a call-back.

But from whom?

Again, we've run into the forest-trees problem in that we see we have a source of YPB, and YPB is the destination, as well, but what is the chain of companies that close this loop. We can't see this well in this diagram, as we have so many companies. So let's zoom into the company that feeds money back to YPB and see if that answers our question.

MATCH (c:CORP)-[:CONTRACTS]->(c1:CORP)-[:CONTRACTS]->(c2:CORP)-[:CONTRACTS]->(c3:CORP)-[:CONTRACTS]->(c4:CORP)-[:CONTRACTS]->(c5:CORP) WHERE c.name='YPB' AND c5.name='GUB' RETURN c, c1, c2, c3, c4, c5

diagram 7: cycle of contracts from YPB

Aha! There we go. By focusing our query the information leaps right out at us. Behold, we're paying Peter, who pays Paul to pay us back, and it's there, plain as day.

Now, lock them up and throw away the key? No. We've just noted a cyclical flow of contracts, but as to the legality of it, that is: whether it is allowed or whether this is fraudulent activity, there are teams of analysts and lawyers who can sink their mandibles into this juicy case.

No, we haven't determined innocence or guilt, but we have done something, and that is: we've revealed an interesting pattern, a cycle of contracts, and we've also identified the parties to these contracts. Bingo. Win.

The problem analysts face today is diagram 1: they have just too much information, and they spend the vast majority of their time weeding out the irrelevant information to winnow down to something that may be interesting. We were presented with the same problem: TMI. But, by using graphs, we were able to see, firstly, that there are some vertices (or 'companies') that have contracts in and contracts out, and, by investigating further, we were able to see a pattern develop that eventually cycled. My entire inquiry lasted minutes of queries and response. Let's be generous and say it took me a half-hour to expose this cycle.

Data analysts working on these kinds of problems are not so fortunate. Working with analysts, I've observed that:

  1. First of all, they never see the graph: all they see are spreadsheets,
  2. Secondly, it takes days to get to even just the spreadsheets of information
  3. Third, where do they go from there? How do they see these patterns? The learning curve for them is prohibitive, making training a bear, and niching their work to just a few brilliant experts and shunting out able-bodied analysts who are more than willing to help, but just don't see the patterns in grids of numbers
With the graph-representation, you can run into the same problems, but 
  1. Training is much easier for those who can work with these visual patterns,
  2. Information can be overloaded, leaving one overwhelmed, but then one can very easily reset to just one vertex and expand from there (simplifying the problem-space). And then, the problem grows in scope when you decide to expand your view, and if you don't like that expanse, it's very easy either to reset or to contract that view.
  3. An analyst can focus on a particular thread or materialize that thread on which to focus, or the analyst can branch from a point or branch to associated sets. If a thread is not yielding interesting results, then they can pursue other, more interesting, areas of the graph, all without losing one's place.
The visual impact of the underlying graph (theory) cannot be over-emphasized: "Boss, we have a cycle of contracts!" an analyst says and presents a spreadsheet requires explanation, checking and verification. That same analysis comes into the boss' office with diagram 7, and the cycle practically leaps off the page and explains itself, that, coupled with the ease and speed of which these cycles are explored and materialized visually makes a compelling case of modeling related data as graphs.

We present, for your consideration: graphs.



Models presented above are derived from various Governmental sources include Census Bureau, Department of Labor, Department of Commerce, and the Small Business Administration.

Graphs calculated in Haskell and stored and visualized in Neo4J

by geophf ([email protected]) at June 25, 2015 03:17 PM

Yesod Web Framework

Cleaning up the Warp APIs

Cleaning up the Warp APIs

For the last one and a half years, I have been trying to implement HTTP/2 in Warp. Since both HTTP/2 implementations of Firefox and Chrome requires TLS for HTTP/2, I'm also trying to improve the performance of WarpTLS. In the process, I need to change the Connection data type. I felt nervous a bit because Connection is exported from the top module, Network.Wai.Handler.Warp. I believe there are only two users of this data type: Warp itself and WarpTLS. Normal users do not use it. So, Connection should be exported from the Internal module. This motivated me to clean up the Warp APIs.

The APIs of Warp 3.0 has the following issues:

  • The top module exports many internal APIs which are prone to change.
  • The Internal module does not export enough internal APIs.

Michael and I decided to clean up the Warp APIs. The following changes will be made in the version 3.1:

  • Already deprecated APIs (settingsFoo) are removed from the top module.
  • In the documentation of the top module, each API is categorized into either standard or internal.
  • The Internal module exports all internal APIs including the internal APIs in the top module.
  • Stopping exporting the Buffer and Timeout module which have been exported from the top module.

The standard APIs of the top module mainly consist of high-level run functions, Settings related stuff and necessary data types. We try to maintain these stably.

The internal APIs in the top module will be removed in Warp version 3.2. This is just documented. DEPRECATED pragmas are not added since there is no simple way to make an API deprecated in the top moudle but live in the internal module.

Warp version 3.1 is not released yet but is available from github repository. We will wait for a week or two to hear users' opinions.

June 25, 2015 09:00 AM

June 24, 2015

FP Complete

Why is stack not cabal?

This blog post is intended to answer two very frequest questions about stack: how is it different from Cabal? And: Why was it developed as a separate project instead of being worked on with Cabal?

Before we delve into the details, let’s first deconstruct the premises of the questions. There are really three things that people talk about when they say “Cabal”:

  1. a package metadata format (.cabal files) and specification for a “common architecture for building applications and tools”, aka Cabal-the-spec,
  2. an implementation of the spec as a framework, aka Cabal-the-library,
  3. cabal-install, aka Cabal-the-tool, which is a command-line tool that uses Cabal-the-library.

Stack complies with Cabal-the-spec, both in the sense that it groks .cabal files in their entirety and behaves in a way that complies with the spec (insofar as that is relevant since the spec hasn’t seen any updates in recent years). In fact it was easy for Stack to do, because just like Cabal-the-tool, it is implemented using Cabal-the-library. Therefore, a first answer to the questions at hand is that stack is Cabal: it is 100% compatible with the existing Cabal file format for specifying package metadata, supports exactly the same package build harnesses and is implemented on top of the same reference implementation of the spec as cabal-install, which is just one tool among others using Cabal-the-library. cabal-install and stack are separate tools that both share the same framework. A successful framework at that: Haskell’s ecosystem would not be where it is today without Cabal, which way back in 2004, for the first time in the long history of Haskell made it possible to easily reuse code across projects by standardizing the way packages are built and used by the compiler.

Stack is different in that it is a from-the-ground-up rethink of Cabal-the-tool. So the real questions are: why was a new tool necessary, and why now? We’ll tackle these questions step-by-step in the remainder of this post:

  • What problem does stack address?
  • How are stack’s design choices different?
  • stack within the wider ecosystem

The problem

Stack was started because the Haskell ecosystem has a tooling problem. Like any number of other factors, this tooling problem is limiting the growth of the ecosystem and of the community around it. Fixing this tooling problem was born out of a systematic effort of growth hacking: identify the bottlenecks that hamper growth and remove them one by one.

The fact that Haskell has a tooling problem is not a rumour, nor is it a fringe belief of disgruntled developers. In an effort to collect the data necessary to identifying the bottlenecks in the growth of the community, FP Complete conducted a wide survey of the entire community on behalf of the Commercial Haskell SIG. The results are in and the 1,200+ respondents are unequivocal: package management with cabal-install is the single worst aspect of using Haskell. Week after week, Reddit and mailing list posts pop up regarding basic package installation problems using cabal-install. Clearly there is a problem, no matter whether seasoned users understand their tools well, know how to use it exactly right and how to back out gracefully from tricky situations. For every battle hardened power user, there are 10 enthusiasts willing to give the language a try, if only simple things were simple.

Of a package building and management tool, users expect, out-of-the-box (that means, by default!):

  1. that the tool facilitates combining sets of packages to build new applications, not fail without pointing to the solution, just because packages advertize conservative bounds on their dependencies;
  2. that the tool ensures that success today is success tomorrow: instructions that worked for a tutorial writer should continue to work for all her/his readers, now and in the future;
  3. that invoking the tool to install one package doesn’t compromise the success of invoking the tool for installing another package;
  4. that much like make, the UI not require the user to remember what previous commands (s)he did or did not run (dependent actions should be run automatically and predictably).

In fact these are the very same desirable properties that Johan Tibell identified in 2012 and which the data supports today. If our tooling does not support them, this is a problem.

Stack is an attempt to fix this problem - oddly enough, by building in at its core much of the same principles that underlie how power users utilize cabal-install successfully. The key to stack’s success is to start from common workflows, choosing the right defaults to support them, and making those defaults simple.

The design

One of the fundamental problems that users have with package management systems is that building and installing a package today might not work tomorrow. Building and installing on my system might not work on your system. Despite typing exactly the same commands. Despite using the exact same package metadata. Despite using the exact same version of the source code. The fundamental problem is: lack of reproducibility. Stack strives hard to make the results of every single command reproducible, because that is the right default. Said another way, stack applies to package management the same old recipe that made the success of functional programming: manage complexity by making the output of all actions proper functions of their inputs. State explicitly what your inputs are. Gain the confidence that the outputs that you see today are the outputs that you see tomorrow. Reproducibility is the key to understandability.

In the cabal workflow, running cabal install is necessary to get your dependencies. It's also a black box which depends on three pieces of global, mutable, implicit state: the compiler and versions of system libraries on your system, the Cabal packages installed in GHC’s package database, and the package metadata du jour downloaded from Hackage (via cabal update). Running cabal install at different times can lead to wildly different install plans, without giving any good reason to the user. The interaction with the installed package set is non-obvious, and arbitrary decisions made by the dependency solver can lead to broken package databases. Due to lack of isolation between different invocations of cabal install for different projects, calling cabal install the first time can affect whether cabal install will work the second time. For this reason, power users use the cabal freeze feature to pin down exactly the version of every dependency, so that every invocation of cabal install always comes up with the same build plan. Power users also build in so-called “sandboxes”, in order to isolate the actions of calling cabal install for building the one project from the actions of calling cabal install for building this other project.

In stack, all versions of all dependencies are explicit and determined completely in a stack.yaml file. Given the same stack.yaml and OS, stack build should always run the exact same build plan. This does wonders for avoiding accidentally breaking the package database, having reproducible behavior across your team, and producing reliable and trustworthy build artifacts. It also makes it trivial for stack to have a user-friendly UI of just installing dependencies when necessary, since future invocations don’t have to guess what the build plan of previous invocations was. The build plan is always obvious and manifest. Unlike cabal sandboxes, isolation in stack is complete: packages built against different versions of dependencies never interfere, because stack transparently installs packages in separate databases (but is smart enough to reuse databases when it is always safe to do, hence keeping build times low).

Note that this doesn’t mean users have to painstakingly write out all package versions longhand. Stack supports naming package snapshots as shorthand for specifying sets of package versions that are known to work well together.

Other key design principles are portability (work consistently and have a consistent UI across all platforms), and very short ramp-up phase. It should be easy for a new user with little knowledge of Haskell to write “hello world” in Haskell, package it up and publish it with just a few lines of configuration or none at all. Learning a new programming language is challenge enough that learning a new package specification language is quite unnecessary. These principles are in contrast with those of platform specific and extremely general solutions such a Nix.

Modularity (do one thing and do it well), security (don’t trust stuff pulled from Internet unless you have a reason to) and UI consistency are also principles fundamental to the design, and a key strategies to keeping the bug count low. But more on that another time.

These have informed the following "nice to have" features compared to cabal-install:

  • multi-package project support (build all packages in one go, test all packages in one go…),
  • depend on experimental and unpublished packages directly, stored in Git repositories, not just Hackage and the local filesystem,
  • transparently install the correct version of GHC automatically so that you don’t have to (and multiple concurrently installed GHC versions work just fine),
  • optionally use Docker for bullet-proof isolation of all system resources and deploying full, self-contained Haskell components as microservices.

The technologies underpinning these features include:

  • Git (for package index management),
  • S3 (for high-reliability package serving),
  • SSL libraries (for secure HTTP uploads and downloads),
  • Docker,
  • many state-of-the-art Haskell libraries.

These technologies have enabled swift development of stack without reinventing the wheel and have helped keep the implementation stack simple and accessible. With the benefit of a clean slate to start from, we believe stack to be very hackable and easy to contribute to. These are also technologies that cabal-install did not have the benefit of being able to use when it was first conceived some years ago.

Whither cabal-install, stack and other tools

Stack is but one tool for managing packages on your system and building projects. Stack was designed specifically to interoperate with the existing frameworks for package management and package building, so that all your existing packages work as-is with stack, but with the added benefit of a modern, predictable design. Because stack is just Cabal under the hood, other tools such as Halcyon for deployment and Nix are good fits complement stack nicely, or indeed cabal-install for those who prefer to work with a UI that they know well. We have already heard reports of users combining these tools to good effect. And remember: stack packages are cabal-install packages are super-new-fangled-cabal-tool packages. You can write the exact same packages in stack or in another tool, using curated package sets if you like, tight version bounds à la PVP if you like, none or anything at all. stack likes to make common usage easy but is otherwise very much policy agnostic.

Stack is a contributor friendly project, with already 18 contributors to the code in its very short existence, several times more bug reporters and documentation writers, and counting! Help make stack a better tool that suits your needs by filing bug reports and feature requests, improving the documentation and contributing new code. Above all, use stack, tell your friends about it. We hope stack will eliminate a documented bottleneck to community growth. And turn Haskell into a more productive language accessible to many more users.

June 24, 2015 01:00 PM

June 23, 2015

Noam Lewis

In Python, don’t initialize local variables unnecessarily

A common pattern:

def foo():
    x = some value # but do we need this? (short answer: no)
    if something:
        # ... do stuff ...
        x = 'bla'
    else:
        x = 'blo'

The variable x is being initialized before the if/else, but the intention of the programmer is that its value will actually be determined by the if/else itself. If somebody later comes around and mistakenly removes one of the assignments (inside ‘if’ or ‘else’), no runtime error will occur and x will remain initialized to a probably wrong value.

Leaving out the initialization is better – in that case, forgetting to set x in one of the branches will cause an UnboundLocalError:

>>> def foo():
...     if False:
...         x = 0
...     return x
... 
>>> foo()
Traceback (most recent call last):
  File "", line 1, in 
  File "", line 4, in foo
UnboundLocalError: local variable 'x' referenced before assignment

Errors are good! (when they flag buggy code)

Now, what if we also have an x declared in the global scope? Because of how Python handles variable scope, the error will still happen (which is good).

>>> x = 1
>>> def foo():
...     if False:
...         x = 0
...     return x
... 
>>> foo()
Traceback (most recent call last):
..
UnboundLocalError: local variable 'x' referenced before assignment

Summary: In Python, don’t initialize variables until you know what value to assign to them.


by sinelaw at June 23, 2015 06:07 PM

FP Complete

stack 0.1 released

A few weeks ago, we announced the first public beta of stack, a new build tool for Haskell. Since then we've seen a huge amount of work on stack: code contributions, feature requests, bug reports, and design discussions. In other words, the response we've had from the community has been amazing. Thank you for helping us push forward with improved Haskell tooling.

Today we're announcing a new milestone: we believe that stack is now stable enough to be the standard build tool for most Haskell development. We're taking the beta label off of stack, and recommending people dive in. Please keep in mind that stack is still young software, and there are likely corner cases that haven't been worked out fully. However, the feedback we've received from other users has indicated that stack is ready. The stack team itself (both inside and outside of FP Complete) has been using stack for months now as its primary tool. And at FP Complete, we've already moved our biggest projects over to it.

Relevant links:

One question which I've personally held off on addressing until now is a direct comparison between stack and other build tools, cabal being the most obvious comparison. Expect a blog post on the subject in the near future. For now, my recommendation is: try out stack, and see if you like it.

Bringing Haskell to the masses

While stack started with the needs of existing Commercial Haskell users, the goal we've always had in mind for it is a tool that lowers the barrier to entry for non-Haskellers. As we've discussed before, FP Complete has done quite a bit of research on this topic, and the data shows that build tool issues have been an obstacle to adoption. We want stack to solve that, and we want your help.

Firstly: keep doing what you've been doing! Using stack, testing it, providing feedback, reporting bugs; all of these make stack better for both our existing community and for newcomers. But the next step is marketing Haskell outside of our community. All of us Haskellers already know how wonderful a language Haskell is. Let's send a clear message to the rest of the world that it's time they try Haskell. stack's aim is to remove those initial barriers. But now we need to tell people what Haskell has to offer.

If you're interested in getting involved in this kind of a push, please join and discuss on the Commercial Haskell mailing list. There's no preexisting formula for how this should be done. But the basic idea I have right now is:

  • Give users a clear message on how to get up and running with Haskell based on stack
  • Give a good example of a strength Haskell has
  • Make it easy for people to play around with the concept with some sample code

I'm sure others will have better ideas than I on how to accomplish this. If you want to see Haskell take off as not only a successful, powerful language (which it is now), but as a more popular language too, come get involved!

June 23, 2015 05:00 PM

June 22, 2015

Philip Wadler

How badly will Audible misuse my contact list?


In today's world, where our books, music, and photos belong to the Cloud rather than to ourselves, one problem we face is commercial concerns insisting on increased access to personal data.

I received the following note from Audible:

It looks like you may have an older version of Audible app installed on your device which needs to be updated before 6/30/15 to ensure that you enjoy uninterrupted access to your library.
Option 1: Continue to use the older version of the app.
If you receive an error message when you attempt to sign in, look in your emails for a password that you will need for sign in.
OR
Option 2 (Recommended): Upgrade to the latest version.
...

Warmest Regards,
The Audible Team
What the note doesn't mention is that updating the app requires giving Audible access to my contacts list.

Does anyone know how Audible is using the contact list? Worst case scenario is they email advertisements to my friends in my name, telling them what I am currently reading.

Do customers have any legal redress? Changing the terms of service to require access to the customer's contact list is the sort of thing the law should protect against.


by Philip Wadler ([email protected]) at June 22, 2015 04:54 PM

Daniil Frumin

Darcs binaries for OSX with Homebrew

Recently I’ve updated my Darcs homebrew build to Darcs 2.10. You can install it with

brew install http://darcs.covariant.me/darcs.rb

The formula contains a context (--exact-version) and it is a static binary.


Tagged: darcs, haskell, homebrew

by Dan at June 22, 2015 12:33 PM

Mark Jason Dominus

My week at Recurse Center

In late April I served a residency at Recurse Center, formerly known as Hacker School. I want to write up what I did before I forget.

Recurse Center bills itself as being like a writer's retreat, but for programming. Recursers get better at programming four days a week for three months. There are some full-time instructors there to help, and periodically a resident, usually someone notable, shows up for a week. It's free to students: RC partners with companies that then pay it a fee if they hire a Recurser.

I got onto the RC chat system and BBS a few weeks ahead and immediately realized that it was going to be great. I am really wary about belonging to groups, but I felt like I fit right in at RC, in a way that I hadn't felt since I went off to math camp at age 14. Recurse Center isn't that different from math camp now that I think about it.

The only prescribed duty of a resident is to give a half-hour talk on Monday night, preferably on a technical topic. I gave mine on the history and internals of lightweight hash structures in programming languages like Python and Perl. (You can read all about that if you want to.)

Here's what else I did:

  1. I gave a bunch of other talks: two on Git, one on calculating with continued fractions, one on how the Haskell type inferencer works, one on the topology of data types, one on the Unix process model, one on Alien Horrors from the Dawn of Unix. This was too many talks. I didn't have enough energy and time to prepare all of them properly. On the other hand, a lot of people were very complimentary about the talks and said they were very glad that I gave so many. Also, giving talks is a great way to get people familiar with you so that they won't be shy about talking to you or asking you to work with them. But I think I'll cut it down to one per day next time.

  2. Alex Taipale was inspired by my hash talk to implement hashes synthetically in Python, and I paired with her on that for the first part and reviewed her code a couple of times after. It was really fun to see how she went about it.

  3. Libby Horacek showed me around the text adventure game she wrote in Haskell. I had the first of several strokes of luck here. Libby had defined an input format to specify the room layout and the objects, and I observed that it was very similar to Asherah, a project that another Recurser, Michelle Steigerwalt, had done a couple of years before. I found this out because I read everyone's self-posted bio ahead of time and browsed the interesting-sounding links.

  4. Aditya Mukerjee was implementing Git in Go. He wanted help deciphering the delta format. Later I paired with Aditya again and we debugged his implementation of the code that expanded the deltas back into complete files. I hadn't known any Go but it's easy to pick up.

  5. Geoffrey Gilmore had read my ancient article on how to write a regex matcher. He had written his own implementation in Scala and wanted to show it to me. I didn't know any Scala but the code was very clear. Geoffrey had worked out a clever way to visualize the resulting finite automaton: his automaton object had a method that would dump out its graph in the "dot" language, and he could feed that to Graphviz to get it to draw the graph.

  6. I had a conference with Ahmed Abdalla and Joel Burget about SML. The main question they wanted me to answer: Why might they want to look at SML instead of Haskell? This was a stroke of luck: I was unusually well-prepared to answer this question, having written many thousands of lines of SML since about 1993. My answer was unequivocally that there was no reason, SML was obsolete, because it had big problems which had never been solved, and Haskell had been introduced in part to solve, avoid, or finesse these problems.

    For example, nobody knows how to incorporate references into a Hindley-Milner type system. SML has tried at least three methods for doing this over the years. They all suck, and none of them work right. Haskell avoids the whole issue: no references. If you want something like references, you can build a monad that simulates it locally.

    I could probably write a whole blog article about this, so maybe another time.

  7. Libby wanted to pair with me again. She offered me a choice: she was building an e-reader, controlled by a Raspberry Pi, and mounted inside an antique book that she had hollowed out. I would have been willing to try this, although I didn't know anything about Raspberry Pi. But my other choice was very attractive: she was reviving KiSS, an ancient Windows paper-doll app that had been current in the 1990s. people had designed hundreds or thousands of dolls and costumes, which were all languishing because nobody wanted to run the app any more. She wanted to reimplement the dress-up program in Javascript, and port the doll and clothing cels to PNG files. Here I had another stroke of luck. I was already familiar with the program, and I think I have even been into its source code at some point.

    Libby had found that Gimp could load a KiSS cel, so we looked at the Gimp source code to figure out the file format. She had been planning to use libpng to turn the cel into a PNG, but I showed her a better way: convert it into a PPM file and feed to to ppmtopng. This saved a lot of trouble! (I have written a little bit about this approach in the past.) Libby hacked in the Gimp code, grafting her PPM file writing code into the Gimp cel reading code in place of Gimp's internal pixmap operations. It worked!

  8. I talked to Chris Ball about his GitTorrent project. Chris wants to make a decentralized github that doesn't depend on the GitHub company or on their technical infrastructure. He spent a long time trying to make me understand why he wanted to do the project at all and what it was for. I think I eventually got it. It also transpired that Chris knows way more about BitTorrent than I do. I don't think I was much help to Chris.

  9. Jesse Chen paired with me to fix the layout problems that have been troubling my blog for years. We redid the ancient table-based layout that I had inherited from Blosxom ten years ago, converting it mostly to CSS, and fixed a bunch of scrolling problems. We also fixed it to be legible on a phone display, which it previously wasn't. Thanks Jesse!

  10. I had a discussion with Michelle Steigerwalt about big-O notation and how you figure out what an algorithm's big-O-ness is, either from counting lines in the source code or the pseudocode, or from running the algorithm on different-size inputs and timing it. It's fun that you can do the static analysis and then run the program and see it produce the results you predicted.

There was a lot of other stuff. I met or at least spoke with around 90% of the seventy or so Recursers who were there with me. I attended the daily stand-up status meetings with a different group each time. I ate lunch and dinner with many people and had many conversations. I went out drinking with Recursers at least once. The RC principals kindly rescheduled the usual Thursday lightning talks to Monday so I could attend. I met Erik Osheim for lunch one day. And I baked cookies for our cookie-decorating party!

It was a great time, definitely a high point in my life. A thousand thanks to RC, to Rachel Vincent and Dave Albert for essential support while I was there, and to the facilitators, principals, and especially to the other Recursers.

by Mark Dominus ([email protected]) at June 22, 2015 10:49 AM

June 21, 2015

Dimitri Sabadie

HID and MSI keyboards

MSI keyboards

I have a MSI GS60 Ghost Pro 2QE I’m very proud of. It’s sexy and powerful. It comes with a fancy and configurable backlit keyboard.

There’s a tool called SteelSeries Engine for Windows we can use to change the colors of the keyboard. It supports several features:

  • changing colors of three parts of the keyboard (left, middle and right) ;
  • changing modes (normal, breathe, wave, demo, gaming).

Unfortunately, that software doesn’t work on Linux, even with wine. I tried hard to make it work and never actually found a way to run it. Then, I decided to look for alternatives and… found nothing working.

Yesterday, I tried a node.js-powered tool called msi-keyboard. And it worked. However, the interface and user interface was not my cup of tea. I decided to dig in in order to understand how it works, and I decided to write my own tool with a decent interface.

HID access

The key idea is that such keyboards are just HID devices. As a Haskell programmer, I looked for something that would grant me access to such devices, but nothing was working. There’s a hidapi package, but it doesn’t work and has bugs.

I didn’t give up though. I wrote my own Haskell HID API binding, called hid. Several good things about it:

  • it does work ;
  • it’s simple ;
  • I lately wrote a software using it.

Feel free to install and use it!

msi-kb-backlit

Then, I wrote another Haskell package, msi-kb-backlit. It might require super user rights to work. If you’re not a Haskeller, you can find installation details here.

Note: if you use Archlinux, you can directly download msi-kb-backlit through the AUR! Search for msi-kb-backlit with yaourt, or download the tarball.

The software has an embedded documentation to help you tweak with colors and modes. ;)

Feel free to use all those pieces of software. I made them with love for you all!

Enjoy your week end, and keep the vibe!

by Dimitri Sabadie ([email protected]) at June 21, 2015 10:48 PM

Christopher Done

Existentials and the heterogenous list fallacy

An oft-stated argument against static typing is that heterogenous lists are unreasonably difficult to model. Why is static typing being so difficult? Why can’t it just be like dynamic typing? This is a specious argument.

For example, in one article I read, I saw:

In fact you can program heterogeneous lists in dependently typed languages, but it’s unreasonably complicated. Python makes no complaints:

>>> g = lambda x: x**2
>>> [1, 'a', "hello", g]
[1, 'a', 'hello', <function <lambda> at 0x103e4aed8>]

To me this is one methodological weakness of type theory […]

(I’m not sure what “methodological weakness” is supposed to mean, but let’s ignore that.)

There are two problems with this argument and demonstration:

  1. It’s contrived. I’ve written about as much Emacs Lisp and JavaScript as I have written Haskell and C#, and I cannot with all intellectual honesty remember wanting a heterogenous list.1
  2. It’s ill-defined. What is this data structure? What can I assume about the elements so that I can write operations generically? Which, I presume, is the only reason I would be using a list in the first place (otherwise a record would be the correct thing to use); to write algorithms that apply generally to any index.

Even cutting the author some slack and assuming they might want to just temporarily put some things together as a tuple, static languages have tuples, which are heterogenous.

When you look at it beyond the superficial, it’s rather odd.

Regardless, I am sporting. Some people will say, yes, okay, it’s contrived, and never really arises, but if I really wanted this, how could I do it in a statically typed language? So here is the above in Haskell.

Let’s look at the example:

>>> g = lambda x: x**2
>>> [1, 'a', "hello", g]
[1, 'a', 'hello', <function <lambda> at 0x103e4aed8>]

So the list contains a bunch of disparate things and the implicit invariant here is that we can print each of them out. So we can model that with an existential data type Py (for “Python”) that holds some type a that is showable.

data Py = forall a. Show a => Py a
instance Show Py where show (Py s) = show s

(Oh, Haskell doesn’t define an instance for printing functions, so let’s use instance Show (a -> b) where show _ = "<function>" to vaguely match Python.)

I may not know, or care, what the type is, but I at least need to know something about it, in a duck-typing kind of way. If it walks like a duck, quacks like a duck, etc. then it’s a good enough duck for my purposes. In this case, Py says, is it at least showable?

Now we can wrap up any type which is an instance of Show with that:

λ> [Py 1,Py 'a',Py "hello",Py (\x -> x ** 2)]
[1,'a',"hello",<function>]

And we can apply the show method (from the Show class) to each element generically:

λ> map (\(Py p) -> show p) [Py 1,Py 'a',Py "hello",Py (\x -> x ** 2)]
["1","'a'","\"hello\"","<function>"]

So that’s how to do it.

Continuing the discussion, if I extend the type to support also Num (numbers),

data Py = forall a. (Show a,Num a) => Py a

then I can use *, but only for actual numbers. If I try something else I get a type error:

λ> map (\(Py p) -> Py (p*2)) [Py 1,Py 'c']
<interactive>:634:33:
    No instance for (Num Char) arising from a use of ‘Py’
    In the expression: Py 'c'
λ> map (\(Py p) -> Py (p*2)) [Py 1,Py 2.0]
[2,4.0]

Doing the same in Python, we have more or less the same error:

>>> def pow2(x): return x ** 2
...
>>> list(map(pow2,[1,5,'a']))
Traceback (most recent call last):
  File "<stdin>", line 1, in <module>
  File "<stdin>", line 1, in pow2
TypeError: unsupported operand type(s) for ** or pow(): 'str' and 'int'

The difference being the Haskell error was signaled statically at compile-time and the Python error was signalled dynamically at run-time.


  1. To demonstrate my good faith, I have constructed heterogenous lists in Emacs Lisp to model a record, but this is because Emacs Lisp lacks native records. JavaScript, on the other hand, has records.

June 21, 2015 12:00 AM

June 20, 2015

Joachim Breitner

Running circle-packing in the Browser, now using GHCJS

Quite a while ago, I wrote a small Haskell library called circle-packing to pack circles in a tight arrangement. Back then, I used the Haskell to JavaScript compiler fay to create a pretty online demo of that library, and shortly after, I create the identical demo using haste (another Haskell to JavaScript compiler).

The main competitor of these two compilers, and the most promising one, is GHCJS. Back then, it was too annoying to install. But after two years, things have changed, and it only takes a few simple commands to get GHCJS running, so I finally created the circle packing demo in a GHCJS variant.

Quick summary: Cabal integration is very good (like haste, but unline fay), interfacing JavaScript is nice and easy (like fay, but unlike haste), and a quick check seems to indicate that it is faster than either of these two. I should note that I did not update the other two demos, so they represent the state of fay and haste back then, respectively.

With GHCJS now available at my fingertips, maybe I will produce some more Haskell to be run in your browser. For example, I could port FrakView, a GUI program to render, expore and explain iterated function systems, from GTK to HTML.

by Joachim Breitner ([email protected]) at June 20, 2015 08:50 PM

Dominic Steinitz

Some Background on Hidden Markov Models

Introduction

If you look at the wikipedia article on Hidden Markov Models (HMMs) then you might be forgiven for concluding that these deal only with discrete time and finite state spaces. In fact, HMMs are much more general. Furthermore, a better understanding of such models can be helped by putting them into context. Before actually specifying what an HMM is, let us review something of Markov processes. A subsequent blog post will cover HMMs themselves.

Markov Process and Chains

Recall that a transition kernel is a mapping \mu : X \times {\cal{Y}} \rightarrow \overline{\mathbb{R}}_{+} where (X, {\cal{X}}) and (Y, {\cal{Y}}) are two measurable spaces such that \mu(s, \cdot) is a probability measure on {\cal{Y}} for all s \in X and such that \mu(\cdot, A) is a measurable function on X for all A \in {\cal{Y}}.

For example, we could have X = Y = \{a, b\} and {\cal{X}} = {\cal{Y}} = \{\emptyset, \{a\}, \{b\}, \{a,b\}\} and \mu(a,\{a\}) = 0.4, \mu(a,\{b\}) = 0.6, \mu(b,\{a\}) = 0.6, \mu(b,\{b\}) = 0.4. Hopefully this should remind you of the transition matrix of a Markov chain.

Recall further that a family of such transitions \{\mu_t\}_{t \in T} where T is some index set satisfying

\displaystyle  \mu_{t+s}(x, A) = \int_{Y} \mu_s(x, {\mathrm{d}y})\mu_t(y, A)

gives rise to a Markov process (under some mild conditions — see Rogers and Williams (2000) and Kallenberg (2002) for much more detail), that is, a process in which what happens next only depends on where the process is now and not how it got there.

Let us carry on with our example and take T = \mathbb{N}. With a slight abuse of notation and since Y is finite we can re-write the integral as a sum

\displaystyle  \mu_{n+m}(x, z) = \sum_{y \in Y} \mu_m(x, y)\mu_n(y, z)

which we recognise as a restatement of how Markov transition matrices combine.

Some Examples

A Fully Deterministic System

A deterministic system can be formulated as a Markov process with a particularly simple transition kernel given by

\displaystyle  \mu_t(x_s, A) = \delta(f_t(x_s), A) \triangleq  \begin{cases}  1           & \text{if } f_t(x_s) \in    A \\  0           & \text{if } f_t(x_s) \notin A  \end{cases}

where f_t is the deterministic state update function (the flow) and \delta is the Dirac delta function.

Parameters

Let us suppose that the determinstic system is dependent on some time-varying values for which we we are unable or unwish to specify a deterministic model. For example, we may be considering predator-prey model where the parameters cannot explain every aspect. We could augment the deterministic kernel in the previous example with

\displaystyle  \mu_t(\theta_s, {\mathrm{d}\phi}) =  {{\cal{N}} \left( {\mathrm{d}\phi} \,\vert\, \theta_s, \tau^2(t-s) \right)}

where we use Greek letters for the parameters (and Roman letters for state) and we use e.g. {\mathrm{d}\phi} to indicate probability densities. In other words that the parameters tend to wiggle around like Brown’s pollen particles rather than remaining absolutely fixed.

Ornstein-Uhlenbeck

Of course Brownian motion or diffusion may not be a good model for our parameters; with Brownian motion, the parameters could drift off to \pm\infty. We might believe that our parameters tend to stay close to some given value (mean-reverting) and use the Ornstein-Uhlenbeck kernel.

\displaystyle   \mu_t(\theta_s, {\mathrm{d}\phi}) =  {{\cal{N}} \left( {\mathrm{d}\phi} \,\vert\, \alpha + (\theta_s - \alpha)e^{-\beta t},\frac{\sigma^2}{2\beta}\big(1 - e^{-2\beta t}\big) \right)}

where \beta expresses how strongly we expect the parameter to respond to perturbations, \alpha is the mean to which the process wants to revert (aka the asymptotic mean) and \sigma^2 expresses how noisy the process is.

It is sometimes easier to view these transition kernels in terms of stochastic differential equations. Brownian motion can be expressed as

\displaystyle   \mathrm{d}X_t = \sigma\mathrm{d}W_t

and Ornstein-Uhlenbeck can be expressed as

\displaystyle   \mathrm{d}X_t = -\beta(X_t - \alpha)\mathrm{d}t + \sigma\mathrm{d}W_t

where W_t is the Wiener process.

Let us check that the latter stochastic differential equation gives the stated kernel. Re-writing it in integral form and without loss of generality taking s= 0

\displaystyle   X_t = \alpha + (x_0 - \alpha)e^{-\beta t} + \sigma\int_0^t e^{-\beta(t - s)}\mathrm{d}W_s

Since the integral is of a deterministic function, the distribution of X_t is normal. Thus we need only calculate the mean and variance.

The mean is straightforward.

\displaystyle   \mathbb{E}[X_t \,\vert\, X_0 = x_0] =  \mathbb{E}\Bigg[\alpha + (x_0 - \alpha)e^{-\beta t} + \sigma\int_0^t e^{-\beta(t - s)}\mathrm{d}W_s \,\vert\, X_0 = x_0\Bigg] =  \alpha + (x_0 - \alpha)e^{-\beta t}

Without loss of generality assume t \leq u and writing \mathbb{C} for covariance

\displaystyle   \begin{aligned}  \mathbb{C}[X_u, X_t \,\vert\, X_0 = x_0] &=  \mathbb{E}\Bigg[\Bigg( \sigma\int_0^u e^{-\beta(u - s)}\mathrm{d}W_s  \Bigg)                  \Bigg( \sigma\int_0^t e^{-\beta(t - s)}\mathrm{d}W_s  \Bigg)\Bigg] \\  &=  \sigma^2e^{-\beta(u + t)}  \mathbb{E}\Bigg[\Bigg(\int_0^u e^{\beta s}\mathrm{d}W_s\Bigg)            \Bigg(\int_0^t e^{\beta s}\mathrm{d}W_s\Bigg)\Bigg] \\  &=  \sigma^2e^{-\beta(u + t)}  \mathbb{E}\Bigg[\Bigg(\int_0^t e^{\beta s}\mathrm{d}W_s + \int_t^u e^{\beta s}\mathrm{d}W_s\Bigg)            \Bigg(\int_0^t e^{\beta s}\mathrm{d}W_s\Bigg)\Bigg]  \end{aligned}

And now we can use Ito and independence

\displaystyle   \begin{aligned}  \mathbb{C}[X_u, X_t \,\vert\, X_0 = x_0] &=  \sigma^2e^{-\beta(u + t)}\mathbb{E}\Bigg[ \int_0^t e^{2\beta s}\mathrm{d}s  \Bigg] \\  &=  \frac{\sigma^2e^{-\beta(u + t)}}{2\beta}\big(e^{2\beta t} - 1\big)  \end{aligned}

Substituting in t = u gives the desired result.

Bibliography

Kallenberg, O. 2002. Foundations of Modern Probability. Probability and Its Applications. Springer New York. http://books.google.co.uk/books?id=TBgFslMy8V4C.

Rogers, L. C. G., and David Williams. 2000. Diffusions, Markov Processes, and Martingales. Vol. 1. Cambridge Mathematical Library. Cambridge: Cambridge University Press.


by Dominic Steinitz at June 20, 2015 06:20 PM

Neil Mitchell

Announcing the 'extra' library

Summary: I wrote an extra library, which contains lots of my commonly used functions.

When starting to write Bake, my first step was to copy a lot of utility functions from Shake - things like fst3 (select the first element of a triple), concatMapM (monadic version of concatMap), withCurrentDirectory (setCurrentDirectory under bracket). None of these functions are specific to either Bake or Shake, and indeed, many of the ones in Shake had originally came from HLint. Copy and pasting code is horrible, so I extracted the best functions into a common library which I named extra. Unlike the copy/paste versions in each package, I then wrote plenty of tests, made sure the functions worked in the presence of exceptions, did basic performance optimisation and filled in some obvious gaps in functionality.

I'm now using the extra library in all the packages above, plus things like ghcid and Hoogle. Interestingly, I'm finding my one-off scripts are making particularly heavy use of the extra functions. I wrote this package to reduce my maintenance burden, but welcome other users of extra.

My goal for the extra library is simple additions to the standard Haskell libraries, just filling out missing functionality, not inventing new concepts. In some cases, later versions of the standard libraries provide the functions I want, so there extra makes them available all the way back to GHC 7.2, reducing the amount of CPP in my projects. A few examples:

The module Extra documents all functions provided by the library, so is a good place to go to see what is on offer. Modules such as Data.List.Extra provide extra functions over Data.List and also reexport Data.List. Users are recommended to replace Data.List imports with Data.List.Extra if they need the extra functionality.

Which functions?

When selecting functions I have been guided by a few principles.

  • I have been using most of these functions in my packages - they have proved useful enough to be worth copying/pasting into each project.
  • The functions follow the spirit of the original Prelude/base libraries. I am happy to provide partial functions (e.g. fromRight), and functions which are specialisations of more generic functions (whenJust).
  • Most of the functions have trivial implementations. If a beginner couldn't write the function, it probably doesn't belong here.
  • I have defined only a few new data types or type aliases. It's a package for defining new utilities on existing types, not new types or concepts.

Testing

One feature I particularly like about this library is that the documentation comments are tests. A few examples:

Just True ||^ undefined  == Just True
retry 3 (fail "die") == fail "die"
whenJust (Just 1) print == print 1
\x -> fromRight (Right x) == x
\x -> fromRight (Left x) == undefined

These equalities are more semantic equality than Haskell's value equality. Things with lambda's are run through QuickCheck. Things which print to stdout are captured, so the print 1 test really does a print, which is scraped and compared to the LHS. I run these tests by passing them through a preprocessor, which spits out this code, which I then run with some specialised testing functions.

by Neil Mitchell ([email protected]) at June 20, 2015 02:46 PM

June 19, 2015

Cartesian Closed Comic

Neil Mitchell

Maximum Patches, Minimum Time

Summary: Writing a fast continuous integration server is tricky.

When I started writing the continuous integration server Bake, I thought I had a good idea of what would go fast. It turned out I was wrong. The problem Bake is trying to solve is:

  • You have a set of tests that must pass, which take several hours to run.
  • You have a current state of the world, which passes all the tests.
  • You have a stream of hundreds of incoming patches per day that can be applied to the current state.
  • You want to advance the state by applying patches, ensuring the current state always passes all tests.
  • You want to reject bad patches and apply good patches as fast as possible.

I assume that tests can express dependencies, such as you must compile before running any tests. The test that performs compilation is special because it can go much faster if only a few things have changed, benefiting from incremental compilation.

Both my wrong solution, and my subsequent better solution, are based on the idea of a candidate - a sequence of patches applied to the current state that is the focus of testing. The solutions differ in when patches are added/removed from the candidate and how the candidates are compiled.

A Wrong Solution

My initial solution compiled and ran each candidate in a separate directory. When the directory was first created, it copied a nearby candidate to try and benefit from incremental compilation.

Each incoming patch was immediately included in the candidate, compiled, and run on all tests. I would always run the test that had not passed for the longest time, to increase confidence in more patches. Concretely, if I have run test T1 on patch P1, and P2 comes in, I start testing T2 on the combination of P1+P2. After that passes I can be somewhat confident that P1 passes both T1 and T2, despite not having run T2 on just P1.

If a test fails, I bisect to find the patch that broke it, reject the patch, and immediately throw it out of the candidate.

The Problems

There are three main problems with this approach:

  • Every compilation starts with a copy of a nearby candidate. Copying a directory of lots of small files (the typical output of a compiler) is fantastically expensive on Windows.
  • When bisecting, I have to compile at lots of prefixes of the candidate, the cost of which varies significantly based on the directory it starts from.
  • I'm regularly throwing patches out of the candidate, which requires a significant amount of compilation, as it has to recompile all patches that were after the rejected patch.
  • I'm regularly adding patches to the candidate, each of which requires an incremental compilation, but tends to be dominated by the directory copy.

This solution spent all the time copying and compiling, and relatively little time testing.

A Better Solution

To benefit from incremental compilation and avoid copying costs, I always compile in the same directory. Given a candidate, I compile each patch in the series one after another, and after each compilation I zip up the interesting files (the test executables and test data). To bisect, I unzip the relevant files to a different directory. On Windows, unzipping is much more expensive than zipping, but that only needs to be done when bisecting is required. I also only need to zip the stuff required for testing, not for building, which is often much smaller.

When testing a candidate, I run all tests without extending the candidate. If all the tests pass I update the state and create a new candidate containing all the new patches.

If any test fails I bisect to figure out who should be rejected, but don't reject until I've completed all tests. After identifying all failing tests, and the patch that caused each of them to fail, I throw those patches out of the candidate. I then rebuild with the revised candidate and run only those tests that failed last time around, trying to seek out tests where two patches in a candidate both broke them. I keep repeating with only the tests that failed last time, until no tests fail. Once there are no failing tests, I extend the candidate with all new patches, but do not update the state.

As a small tweak, if there are two patches in the queue from the same person, where one is a superset of the other, I ignore the subset. The idea is that if the base commit has an error I don't want to track it down twice, once to the first failing commit and then again to the second one.

Using this approach in Bake

First, the standard disclaimer: Bake may not meet your needs - it is a lot less developed than other continuous integration systems. If you do decide to use Bake, you should run from the git repo, as the Hackage release is far behind. That said, Bake is now in a reasonable shape, and might be suitable for early adopters.

In Bake this approach is implemented in the StepGit module, with the ovenStepGit function. Since Bake doesn't have the notion of building patches in series it pretends (to the rest of Bake) that it's building the final result, but secretly caches the intermediate steps. If there is a failure when compiling, it caches that failure, and reports it to each step in the bisection, so Bake tracks down the correct root cause.

I am currently recommending ovenStepGit as the "best" approach for combining git and an incremental build system with Bake. While any incremental build system works, I can't help but plug Shake, because its the best build system I've ever written.

by Neil Mitchell ([email protected]) at June 19, 2015 06:40 PM

Mark Jason Dominus

Math.SE report 2015-05

A lot of the stuff I've written in the past couple of years has been on math.StackExchange. Some of it is pretty mundane, but some is interesting. My summary of April's interesting posts was well-received, so here are the noteworthy posts I made in May 2015.

  • What matrix transforms into and tranforms into ? was a little funny because the answer is $$\begin{pmatrix}2 & 4 \\ 6 & 8 \end{pmatrix}$$ and yeah, it works exactly like it appears to, there's no trick. But if I just told the guy that, he might feel unnecessarily foolish. I gave him a method for solving the problem and figured that when he saw what answer he came up with, he might learn the thing that the exercise was designed to teach him.

  • Is a “network topology'” a topological space? is interesting because several people showed up right away to say no, it is an abuse of terminology, and that network topology really has nothing to do with mathematical topology. Most of those comments have since been deleted. My answer was essentially: it is topological, because just as in mathematical topology you care about which computers are connected to which, and not about where any of the computers actually are.

    Nobody constructing a token ring network thinks that it has to be a geometrically circular ring. No, it only has to be a topologically circular ring. A square is fine; so is a triangle; topologically they are equivalent, both in networking and in mathematics. The wires can cross, as long as they don't connect at the crossings. But if you use something that isn't topologically a ring, like say a line or a star or a tree, the network doesn't work.

    The term “topological” is a little funny. “Topos” means “place” (like in “topography” or “toponym”) but in topology you don't care about places.

  • Is there a standard term for this generalization of the Euler totient function? was asked by me. I don't include all my answers in these posts, but I think maybe I should have a policy of including all my questions. This one concerned a simple concept from number theory which I was surprised had no name: I wanted to be the number of integers that are no larger than for which . For this is the famous Euler totient function, written .

    But then I realized that the reason it has no name is that it's simply so there's no need for a name or a special notation.

    As often happens, I found the answer myself shortly after I asked the question. I wonder if the reason for this is that my time to come up with the answer is Poisson-distributed. Then if I set a time threshold for how long I'll work on the problem before asking about it, I am likely to find the answer to almost any question that exceeds the threshold shortly after I exceed the threshold. But if I set the threshold higher, this would still be true, so there is no way to win this particular game. Good feature of this theory: I am off the hook for asking questions I could have answered myself. Bad feature: no real empirical support.

  • how many ways can you divide 24 people into groups of two? displays a few oddities, and I think I didn't understand what was going on at that time. OP has calculated the first few special cases:

    1:1 2:1 3:3 4:3 5:12 6:15

    which I think means that there is one way to divide 2 people into groups of 2, 3 ways to divide 4 people, and 15 ways to divide 6 people. This is all correct! But what could the 1:1, 3:3, 5:12 terms mean? You simply can't divide 5 people into groups of 2. Well, maybe OP was counting the extra odd person left over as a sort of group on their own? Then odd values would be correct; I didn't appreciate this at the time.

    But having calculated 6 special cases correctly, why can't OP calculate the seventh? Perhaps they were using brute force: the next value is 48, hard to brute-force correctly if you don't have a enough experience with combinatorics.

    I tried to suggest a general strategy: look at special cases, and not by brute force, but try to analyze them so that you can come up with a method for solving them. The method is unnecessary for the small cases, where brute force enumeration suffices, but you can use the brute force enumeration to check that the method is working. And then for the larger cases, where brute force is impractical, you use your method.

    It seems that OP couldn't understand my method, and when they tried to apply it, got wrong answers. Oh well, you can lead a horse to water, etc.

    The other pathology here is:

    I think I did what you said and I got 1.585times 10 to the 21

    for the case. The correct answer is $$23\cdot21\cdot19\cdot17\cdot15\cdot13\cdot11\cdot9\cdot7\cdot5\cdot3\cdot1 = 316234143225 \approx 3.16\cdot 10^{11}.$$ OP didn't explain how they got so there's not much hope of correcting their weird error.

    This is someone who probably could have been helped in person, but on the Internet it's hopeless. Their problems are Internet communication problems.

  • Lambda calculus typing isn't especially noteworthy, but I wrote a fairly detailed explanation of the algorithm that Haskell or SML uses to find the type of an expression, and that might be interesting to someone.

  • I think Special representation of a number is the standout post of the month. OP speculates that, among numbers of the form (where are prime), the choice of is unique. That is, the mapping is reversible.

    I was able to guess that this was not the case within a couple of minutes, replied pretty much immediately:

    I would bet money against this representation being unique.

    I was sure that a simple computer search would find counterexamples. In fact, the smallest is which is small enough that you could find it without the computer if you are patient.

    The obvious lesson to learn from this is that many elementary conjectures of this type can be easily disproved by a trivial computer search, and I frequently wonder why more amateur mathematicians don't learn enough computer programming to investigate this sort of thing. (I wrote recently on the topic of An ounce of theory is worth a pound of search , and this is an interesting counterpoint to that.)

    But the most interesting thing here is how I was able to instantly guess the answer. I explained in some detail in the post. But the basic line of reasoning goes like this.

    Additive properties of the primes are always distributed more or less at random unless there is some obvious reason why they can't be. For example, let be prime and consider . This must have exactly one of the three forms or for some integer . It obviously has the form almost never (the only exception is ). But of the other two forms there is no obvious reason to prefer one over the other, and indeed of the primes up to 10,000, 611 are of the type and and 616 are of the type .

    So we should expect the value to be distributed more or less randomly over the set of outputs, because there's no obvious reason why it couldn't be, except for simple stuff, like that it's obviously almost always even.

    So we are throwing a bunch of balls at random into bins, and the claim is that no bin should contain more than one ball. For that to happen, there must be vastly more bins than balls. But the bins are numbers, and primes are not at all uncommon among numbers, so the number of bins isn't vastly larger, and there ought to be at least some collisions.

    In fact, a more careful analysis, which I wrote up on the site, shows that the number of balls is vastly larger—to have them be roughly the same, you would need primes to be roughly as common as perfect squares, but they are far more abundant than that—so as you take larger and larger primes, the number of collisions increases enormously and it's easy to find twenty or more quadruples of primes that all map to the same result. But I was able to predict this after a couple of minutes of thought, from completely elementary considerations, so I think it's a good example of Lower Mathematics at work.

    This is an example of a fairly common pathology of math.se questions: OP makes a conjecture that never occurs or that there are no examples with property , when actually almost always occurs or every example has property .

    I don't know what causes this. Rik Signes speculates that it's just wishful thinking: OP is doing some project where it would be useful to have be unique, so posts in hope that someone will tell them that it is. But there was nothing more to it than baseless hope. Rik might be right.

[ Addendum 20150619: A previous version of this article included the delightful typo “mathemativicians”. ]

by Mark Dominus ([email protected]) at June 19, 2015 03:01 AM

Christopher Done

The constraint trick for instances

Ever seen this in a library,

instance (var ~ AType) => ClassName (SomeType var)

and thought, “Shenanigans! Why not just have this?”

instance ClassName (SomeType AType)

Me too!

I only learned of this solution relatively recently, and I know experienced Haskellers who also only understood this recently or still don’t. Hence this quick write up. Here’s the thought process.

We’re writing a trivial pretty printer and we’re using Writer. We write things like:

λ> execWriter (do tell "hello"; tell "world" :: Writer String ())
"helloworld"

Quality. But writing tell every time is so boring! How about we use the IsString class so that we can just write the string literals like this?

do "hello"; "world"

Let’s write the IsString instance:

instance IsString (Writer String a) where
  fromString = tell

What do you say, GHC?

Couldn’t match type ‘a’ with ‘()’

‘a’ is a rigid type variable bound by the instance declaration

Oh. Good point. The type of our tell call results in Writer String (). A small set back. Fine, let’s change the instance declaration to just be ():

instance IsString (Writer String ()) where
  fromString = tell

GHC loves it!

Let’s try using it:

λ> execWriter (do "hello"; "world" :: Writer String ())
<interactive>:42:16:
    No instance for (IsString (WriterT String Identity a))
      arising from the literal ‘"hello"The type variable ‘a’ is ambiguous

This displeases me. But it adds up given the type of (>>):

(>>) :: Monad m => m a -> m b -> m b

In _ >> return () :: Writer String (), the type of _ is Writer String a, so we really need an IsString instance that matches that. But we already tried that. Oh, woe!

Some people reading this will be nodding in recognition of this same problem they had while writing that perfect API that just won’t work because of this niggling issue.

Here comes the trick.1 So let’s go back to a basic instance:

data MyTuple a b = MyTuple a b
instance Show (MyTuple a b) where
  show _ = "MyTuple <some value> <some value>"

Suppose I replace this instance with a new instance that has constraints:

instance (Show a,Show b) => Show (MyTuple a b) where
  show (MyTuple a b) = "MyTuple " ++ show a ++ " " ++ show b

Question: Does that change whether GHC decides to pick this new version of instance over others that may be available, compared to the one above? Have a think.

The answer is: nein! The constraints of an instance don’t have anything to do with deciding whether an instance is picked from the list of instances available. Constraints only apply after GHC has already decided it’s going with this instance.

So, cognizant of this obvious-after-the-fact property, let’s use the equality constraint that was introduced with GADTs and type families (enabling either brings in ~):

instance a ~ () => IsString (Writer String a) where
  fromString = tell

Let’s try it:

λ> execWriter (do "hello" ; "world" :: Writer String ())
"helloworld"

This instance is picked by GHC, as we hoped, because of the a. The instance method also type checks, because the constraint applies when type checking the instance methods, just like if you write a regular declaration like:

foo :: (a ~ ()) => a
foo = ()

That’s it! This crops up in a number of my own libraries and knowing this really helped me. Here is a real example from my lucid library:

instance (a ~ (),Monad m) => Monoid (HtmlT m a) where
  mempty  = return mempty
  mappend = liftM2 mappend

Hope this was helpful!


  1. Actually, it’s a natural consequence to grokking how instance resolution works (but calling it a “trick” makes for a catchy title).

June 19, 2015 12:00 AM

June 17, 2015

Robin KAY

Fast and Slow Sticky Notes in Haskell and Qt

Last year I gave a talk for the London Haskell User Group on building a Sticky Notes application using Haskell, Qt, and the HsQML binding between them. The video has been out for a while now and made the rounds elsewhere, but I've thus far neglected to post it on my own blog! Slides are here. See below for an update on the example program and an answer to the most commonly asked question after the fact.

<iframe allowfullscreen="" frameborder="0" height="270" src="https://www.youtube.com/embed/JCSxWfUvi6o" width="480"></iframe>

Fast and Slow? An update!

For the sakes of simplicity, the original version of the sticky notes program shown in the talk uses an SQLite database to serve the view directly with no in-memory model or caching. This is at least the cause of some sluggishness and at worst pathological performance depending on your machine.

As alluded to in the talk, there is a better albeit more complicated way. This involves moving the slow database accesses onto a separate thread and keeping a fast in-memory model to support the user interface. Changes made by user are now queued up and then flushed to disk asynchronously.

I've now released an updated version (0.3.3.0) of the hsqml-demo-notes package which includes a new faster version of the program illustrating exactly this technique. This hsqml-notes executable is now built using the new code and, for reference, the original code is built into the hsqml-notes-slow executable.

The fast variant uses three MVars to communicate between the UI and database threads. An MVar is kind of synchronisation primitive offered by Haskell akin to a box which may either contain a data value or be empty. Operations on MVars take out or put in values to the box and will block if the MVar is not in the appropriate state to accept or produce a value. Hence, a variety of different constructs such as locks and semaphores can built out of MVars.

The first MVar in the new notes code, modelVar, contains a Map from note IDs to the data associated with each note. This is the in-memory model. It includes all the fields held in the database table plus an additional field which indicates whether there are any pending changes which need flushing to the database (whether the record is "dirty"). The MVar semantics here act as a lock to prevent more than one thread trying to manipulate the model at the same time.

A second MVar, cmdVar, is used as a shallow channel for the UI thread to signal the database thread when there is work to do. The database thread normally waits blocked on this MVar until a new command value is placed in it, at which point it takes out and acts upon it. The first command given to the database thread when the program starts is to populate the model with the data stored on disk. Thereafter, whenever a user makes a change to the model, the dirty bit is set on the altered record and a command issued to the database thread to write those dirty records to the database.

Finally, the third possible type of command causes the database thread to close the SQLite file and cleanly exit. In that case, the third MVar, finVar, is used as a semaphore to signal back to the UI thread once it has shut down cleanly. This is necessary because the Haskell runtime will normally exit once the main thread has finished, and the MVar provides something for it block on so that the database thread has time to finish cleaning up first.


What is the FactoryPool actually for?

QML objects require a relatively explicit degree of handling by Haskell standards because the idea that data values can have distinct identities to one another even if they are otherwise equal is somewhat at odds with Haskell's embrace of referential transparency. This sense of identity is important to the semantics of QML and can't be swept under the rug too easily. Crucially, using signals to pass events from Haskell to QML requires that both the Haskell and QML code are holding on to exactly the same object.

One way to accomplish this is to carefully keep track of the QML objects you create in your own code. The factory-pool is an attempt to provide a convenience layer atop object creation which saves the programmer from having to do this. It is essentially an interning table which enforces the invariant that there is no more than one QML object for each distinct value (according to the Ord type-class) of the Haskell type used to back it. If you query the pool twice with two equal values then it will give you the same object back both times. Importantly, it uses weak references so that objects which are no longer in use are cleared from the intern table and it doesn't grow in size indefinitely.

One of the difficulties people have had with understanding the factory-pool from the notes example is that it's not generally necessary to make it work. Aside from the initial loading of the database, all the activity is driven from the front-end and so displaying a single view isn't strictly reliant on the signals firing correctly. If you replace the code to retrieve an object from the pool with a plain object instantiation, the default QML front-end for the demo would still work the same, albeit more wastefully.

To see the pool doing something useful, try the "notes-dual" front-end (by specifying it on the command line), which I've come to think of as the most interesting of the demos. It displays two front-ends simultaneously backed by the same data model. Changes in one are immediately reflected in the other. This works because when each front-end retrieves the list of notes they both obtains the same ObjRef from the pool for each Note as each other. Hence, when a change is made in one front-end, and a change signal is fired, both the front-ends receive it and remain in sync.

Without the pool, the onus would be on the application code to keep track of the objects in some other fashion. For example, if each read of the notes property created a new set of objects every time it was accessed then many more objects would need to have signals fired on them in order to ensure that every piece of active QML had received notice of the event. Each front-end would still be backed by the same data, methods and properties would still have access to the same set of Note values, but their objects would be distinct from the perspective of signalling and, unless special care was taken, the front-ends wouldn't update correctly.

by Robin KAY ([email protected]) at June 17, 2015 11:09 PM

Kevin Reid (kpreid)

What I've been working on: ShinySDR

As vaguely promised before, another update on what I've been working on for the past couple of years:

ShinySDR (why yes, I am terrible at naming things) is a software-defined radio receiver application.

Specifically, it is in the same space as Gqrx, SDR#, HDSDR, etc.: a program which runs on your computer (as opposed to embedded in a standalone radio) and uses a peripheral device (rtl-sdr, HackRF, USRP, etc.) for the RF interface. Given such a device, it can be used to listen to or otherwise decode a variety of radio transmissions (including the AM and FM broadcast bands everyone knows, but also shortwave, amateur radio, two-way radios, certain kinds of telemetry including aircraft positions, and more as I get around to it).

ShinySDR is basically my “I want my own one of these” project (the UI still shows signs of “I’ll just do what Gqrx did for now”), but it does have some unique features. I'll just quote myself from the README:

I (Kevin Reid) created ShinySDR out of dissatisfaction with the user interface of other SDR applications that were available to me. The overall goal is to make, not necessarily the most capable or efficient SDR application, but rather one which is, shall we say, not clunky.

Here’s some reasons for you to use ShinySDR:

  • Remote operation via browser-based UI: The receiver can be listened to and remotely controlled over a LAN or the Internet, as well as from the same machine the actual hardware is connected to. Required network bandwidth: 3 Mb/s to 8 Mb/s, depending on settings.

    Phone/tablet compatible (though not pretty yet). Internet access is not required for local or LAN operation.

  • Persistent waterfall display: You can zoom, pan, and retune without losing any of the displayed history, whereas many other programs will discard anything which is temporarily offscreen, or the whole thing if the window is resized. If you zoom in to get a look at one signal, you can zoom out again.

  • Frequency database: Jump to favorite stations; catalog signals you hear; import published tables of band, channel, and station info; take notes. (Note: Saving changes to disk is not yet well-tested.)

  • Map: Plot station locations from the frequency database, position data from APRS and ADS-B, and mark your own location on the map. (Caveat: No basemap, i.e. streets and borders, is currently present.)

Supported modes:

  • Audio: AM, FM, WFM, SSB, CW.
  • Other: APRS, Mode S/ADS-B, VOR.

If you’re a developer, here’s why you should consider working on ShinySDR (or: here’s why I wrote my own rather than contributing to another application):

  • All server code is Python, and has no mandatory build or install step.

  • Plugin system allows adding support for new modes (types of modulation) and hardware devices.

  • Demodulators prototyped in GNU Radio Companion can be turned into plugins with very little additional code. Control UI can be automatically generated or customized and is based on a generic networking layer.

On the other hand, you may find that the shiny thing is lacking substance: if you’re looking for functional features, we do not have the most modes, the best filters, or the lowest CPU usage. Many features are half-implemented (though I try not to have things that blatantly don’t work). There’s probably lots of code that will make a real DSP expert cringe.

Now that I've finally written this introduction post, I hope to get around to further posts related to the project.

At the moment, I'm working on adding the ability to transmit (given appropriate hardware), and secondarily improving the frequency database subsystem (particularly to have a useful collection of built-in databases and allow you to pick which ones you want to see).

Side note: ShinySDR may hold the current record for most popular program I've written by myself; at least, it's got 106 stars on GitHub. (Speaking of which: ShinySDR doesn't have a page anywhere on my own web site. Need to fix that — probably starting with a general topics/radio. Eventually I hope to have a publicly accessible demo instance, but there’s a few things I want to do to make it more multiuser and robust first.)

by Kevin Reid (kpreid) ([email protected]) at June 17, 2015 03:22 PM

June 16, 2015

Dimitri Sabadie

Asset management in a real time 3D engine in Haskell

Foreword

In a real time rendering system, it’s not uncommon finding constructs about assets. One famous construct is the resource manager. A resource manager is responsible of several tasks, among:

  • providing a simple interface to load objects from disk (1) ;
  • ensuring we don’t try to load the same object twice (2) ;
  • resolving dependencies between resources (3).

The first point is obvious, but the two others are less intuitive. (2) is important when the user might try to load the same object several times – for instance, a car model, or a character or a weapon. The most known strategy to prevent such a situation from happening is by using a software cache.

A software cache – let’s just say cache – is an opaque object that loads the object on the first request, then just returns that object for future same requests. For instance, consider the following requests and the corresponding cache behavior:

  1. load "wood.png" -> not cached ; loading ; return
  2. load "grass.png" -> not cached ; loading ; return
  3. load "wood.png" -> cached ; return
  4. load "metal.png" -> not cached ; loading ; return
  5. load "metal.png" -> cached ; return
  6. etc.

That behavior is very nice because it will spare a lot of computations and memory space.

(3) is about dependencies. For instance, when you load a car model, you might need to load its textures as well. Well, not really load. Consider the following:

  1. load "car.mesh" -> not cached
    1. load "metal_car.png" -> not cached ; loading ; return
    2. loading ; return
  2. load "metal_car.png" -> cached ; return
  3. load "other_car.mesh" -> not cached
    1. load "metal_car.png" -> cached ; return
    2. return
  4. load "car.mesh" -> cached ; return

You got the idea. (3) needs (2) to be efficient.

Possible implementations

Singleton

In imperative languages and especially in those that support template and/or generics, people tend to implement the cache system with an ugly design pattern – which is actually an anti design pattern : singleton. Each type of resource is assigned a manager by using a template parameter, and then if a manager needs to load a dependency, it just has to reference the corresponding manager by stating the type in the template parameter :

Model & getResource<Model>(std::string const &name) {
Texture &dependency = getResource<Texture>(...);
...
}

That way of doing might sound great, but eh, singletons are just global variables with a unicity constraint. We don’t want that.

Explicit pure store

We can use an explicit store object. That is, some kind of map. For instance, the store that holds textures would have a type like (in Haskell):

textureStore :: Map String Texture

A model store would have the following type:

modelStore :: Map String Model

And each stores is assigned a function; loadTexture, loadModel, and so on.

There are several drawbacks if we go that way. First, we have to carry all stores when using their functions. Some functions might need other stuff in order to resolve dependencies. Secondly, because of explicit state, we need to manually accumulate state! A loading function would have such a following type:

loadTexture :: Map String Texture -> String -> m (Texture,Map String Texture)

That will expose a lot of boilerplate to the user, and we don’t want that.

Implicit pure store

We can enhance the explicit store by putting it into some kind of context; for instance, in MonadState. We can then write loadTexture to make it nicer to use:

loadTexture :: (MonadState (Map String Texture) m,...)
=> String
-> m Texture

There is a problem with that. What happens when we add more types? For instance if we want to handle textures and models? MonadState has a type family constraint that forbids two instances for the pair s m. The following is not allowed and will raise a compiler error:

instance MonadState (Map String Texture) MyState where
...

instance MonadState (Map String Model) MyState where
...

The solution to that problem is to have the carried state a polymorphic type and use typeclass constraint to extract and modify the map we want:

class HasMap a s where
extractMap :: s -> Map String a
modifyMap :: (Map String a -> Map String a) -> s -> s

With that, we can do something like this:

loadTexture :: (MonadState s m,HasMap Texture s,...)
=> String
-> m Texture

loadModel :: (MonadState s m,HasMap Texture s,HasMap Model s,...)
=> String
-> m Model

However, we hit a new issue here. What are s and m? Well, m doesn’t really matter. For simplicity, let’s state we’re using a monad transformer; that is, we use StateT s m as monad.

We still need s. The problem is that s has to be provided by the user. Worse, they have to implement all instances we need so that the loading functions may work. Less boilerplate than the explicit store solution, but still a lot of boilerplate. Imagine you provide a type for s, like Cache. Expending the cache to support new types – like user-defined ones – will be more extra boilerplate to write.

Closures

The solution I use in my engine might not be the perfect solution. It’s not referentially transparent, an important concept in Haskell. However, Haskell is not designed to be used in convenient situations only. We’re hitting a problematic situation. We need to make a compromise between elegance and simplicity.

The solution required the use of closures. If you don’t know what a closure is, you should check out the wikipedia page for a first shot.

The idea is that our loading functions will perform some IO operations to load objects. Why not putting the cache directly in that function? We’d have a function with an opaque and invisible associated state. Consider the following:

type ResourceMap a = Map String a

getTextureManager :: (MonadIO m,...)
=> m (String -> m Texture)
getTextureManager = do
ref <- newIORef empty
pure $ \name -> do
-- we can use the ref ResourceMap to insert / lookup value in the map
-- thanks to the closure!

That solution is great because now, a manager is just a function. How would you implement getModelManager? Well:

getModelManager :: (MonadIO m,...)
=> (String -> m Texture)
-> m (String -> m Model)
getModelManager loadTexture = ...

We can then get the loader functions with the following:

loadTexture <- getTextureManager
loadModel <- getModelManager loadTexture

And you just have to pass those functions around. The cool thing is that you can wrap them in a type in your library and provide a function that initializes them all at once – I do that in my engine. Later on, the user can extend the available managers by providing new functions for new types. In my engine, I provide a few functions like mkResourceManager that hides the ResourceMap, providing two functions – one for lookup in the map, one for inserting into the map.

Conclusion

I truly believe that my solution is a good compromise between elegance and ease. It has a lot of advantages:

  • simple to use ;
  • simple to implement; you just have to play around with closures ;
  • dependencies resolving is easy to add and hidden once the functions are generated ;
  • little runtime overhead (due to closures, might be optimized away by the compiler though) ;
  • can be easily extended by the user to support custom/new types ;
  • if correctly used, implementations can replace IORef with TVar or similar objects for thread-safe implementations ;
  • several replicated functions mean several stores (can be useful in certain cases).

The huge drawback I see in that solution is its opacity. There’s also no way to query the state of each cache. Such a feature could be added by proving a new function, for instance. Same thing for deletion.

I’m one of those Haskellers who love purity. I try to keep my code the purest I can, but there are exceptions, and that cache problem fits that kind of exception.

Feel free to comment, and as always, keep the vibe and happy hacking!

by Dimitri Sabadie ([email protected]) at June 16, 2015 07:01 PM

June 15, 2015

Noam Lewis

Beware of ‘var’ in for loops, JS programmers

Time and time again, I see people using ‘var’ in the initialization part of a for loop. Example from MDN (Mozilla Developer Network):

for (var i = 0; i < 9; i++) {
   console.log(i);
   // more statements
}

What’s wrong with var i = 0 above? The problem is that variables declared in a for initialization have function scope, just like any var declaration does. In other words, they affect the scope of the entire function. Consider the following:

function outer() {
    var x = 'outer';
    function inner() {
        x = 'inner';
        //
        // ... lots o' code
        //
        for (var x = 0; x < 1; x++) {
            // in for
        }
    }
    inner();
}

In the inner function, x shadows the outer variable throughout, not just inside the for loop. So also the initial statement x = 'inner' at the head of ‘inner’ affects only the locally scoped variable.

This is a classic example of var hoisting, which should qualify as one of JavaScript’s awful parts.

Don’t do it! Move all your ‘var’ statements to the head of each function, please.


by sinelaw at June 15, 2015 07:50 PM

Mark Jason Dominus

Math.SE report 2015-04

A lot of the stuff I've written in the past couple of years has been on Mathematics StackExchange. Some of it is pretty mundane, but some is interesting. I thought I might have a little meta-discussion in the blog and see how that goes. These are the noteworthy posts I made in April 2015.

  • Languages and their relation : help is pretty mundane, but interesting for one reason: OP was confused about a statement in a textbook, and provided a reference, which OPs don't always do. The text used the symbol . OP had interpreted it as meaning , but I think what was meant was .

    I dug up a copy of the text and groveled over it looking for the explanation of , which is not standard. There was none that I could find. The book even had a section with a glossary of notation, which didn't mention . Math professors can be assholes sometimes.

  • Is there an operation that takes and , and returns is more interesting. First off, why is this even a reasonable question? Why should there be such an operation? But note that there is an operation that takes and and returns , namely, multiplication, so it's plausible that the operation that OP wants might also exist.

    But it's easy to see that there is no operation that takes and and returns : just observe that although , the putative operation (call it ) should take and yield , but it should also take and yield . So the operation is not well-defined. And you can take this even further: can be written as , so should also take and yield .

    They key point is that the representation of a number, or even an integer, in the form is not unique. (Jargon: "exponentiation is not injective".) You can raise , but having done so you cannot look at the result and know what and were, which is what needs to do.

    But if can't do it, how can multiplication do it when it multiplies and and gets ? Does it somehow know what is? No, it turns out that it doesn't need in this case. There is something magical going on there, ultimately related to the fact that if some quantity is increasing by a factor of every units of time, then there is some for which it is exactly doubling every units of time. Because of this there is a marvelous group homomophism $$\log : \langle \Bbb R^+, \times\rangle \to \langle \Bbb R ,+\rangle$$ which can change multiplication into addition without knowing what the base numbers are.

    In that thread I had a brief argument with someone who thinks that operators apply to expressions rather than to numbers. Well, you can say this, but it makes the question trivial: you can certainly have an "operator" that takes expressions and and yields the expression . You just can't expect to apply it to numbers, such as and , because those numbers are not expressions in the form . I remembered the argument going on longer than it did; I originally ended this paragraph with a lament that I wasted more than two comments on this guy, but looking at the record, it seems that I didn't. Good work, Mr. Dominus.

  • how 1/0.5 is equal to 2? wants a simple explanation. Very likely OP is a primary school student. The question reminds me of a similar question, asking why the long division algorithm is the way it is. Each of these is a failure of education to explain what division is actually doing. The long division answer is that long division is an optimization for repeated subtraction; to divide you want to know how many shares of three cookies each you can get from cookies. Long division is simply a notation for keeping track of removing shares, leaving cookies, then further shares, leaving none.

    In this question there was a similar answer. is because if you have one cookie, and want to give each kid a share of cookies, you can get out two shares. Simple enough.

    I like division examples that involve giving cookies to kids, because cookies are easy to focus on, and because the motivation for equal shares is intuitively understood by everyone who has kids, or who has been one.

    There is a general pedagogical principle that an ounce of examples are worth a pound of theory. My answer here is a good example of that. When you explain the theory, you're telling the student how to understand it. When you give an example, though, if it's the right example, the student can't help but understand it, and when they do they'll understand it in their own way, which is better than if you told them how.

  • How to read a cycle graph? is interesting because hapless OP is asking for an explanation of a particularly strange diagram from Wikipedia. I'm familiar with the eccentric Wikipedian who drew this, and I was glad that I was around to say "The other stuff in this diagram is nonstandard stuff that the somewhat eccentric author made up. Don't worry if it's not clear; this author is notorious for that."

  • In Expected number of die tosses to get something less than 5, OP calculated as follows: The first die roll is a winner of the time. The second roll is the first winner of the time. The third roll is the first winner of the time. Summing the series we eventually obtain the answer, . The accepted answer does it this way also.

    But there's a much easier way to solve this problem. What we really want to know is: how many rolls before we expect to have seen one good one? And the answer is: the expected number of winners per die roll is , expectations are additive, so the expected number of winners per die rolls is , and so we need rolls to expect one winner. Problem solved!

    I first discovered this when I was around fifteen, and wrote about it here a few years ago.

    As I've mentioned before, this is one of the best things about mathematics: not that it works, but that you can do it by whatever method that occurs to you and you get the same answer. This is where mathematics pedagogy goes wrong most often: it proscribes that you must get the answer by method X, rather than that you must get the answer by hook or by crook. If the student uses method Y, and it works (and if it is correct) that should be worth full credit.

    Bad instructors always say "Well, we need to test to see if the student knows method X." No, we should be testing to see if the student can solve problem P. If we are testing for method X, that is a failure of the test or of the curriculum. Because if method X is useful, it is useful because for some problems, it is the only method that works. It is the instructor's job to find one of these problems and put it on the test. If there is no such problem, then X is useless and it is the instructor's job to omit it from the curriculum. If Y always works, but X is faster, it is the instructor's job to explain this, and then to assign a problem for the test where Y would take more time than is available.

    I see now I wrote the same thing in 2006. It bears repeating. I also said it again a couple of years ago on math.se itself in reply to a similar comment by Brian Scott:

    If the goal is to teach students how to write proofs by induction, the instructor should damned well come up with problems for which induction is the best approach. And if even then a student comes up with a different approach, the instructor should be pleased. ... The directions should not begin [with "prove by induction"]. I consider it a failure on the part of the instructor if he or she has to specify a technique in order to give students practice in applying it.

by Mark Dominus ([email protected]) at June 15, 2015 07:38 PM

Gabriel Gonzalez

break-1.0.0: A small library for breaking from loops

I've implemented a small library named break for breaking from loops, based off of a previous post of mine.

This library is simple: you wrap the command you want to loop with a function named loop and you call break when you want to exit from the loop.

import Control.Break
import Control.Monad.State
import Prelude hiding (break)

example :: State Int ()
example = loop (do
n <- lift get -- Inside a `loop`, wrap commands in `lift`
if n < 10
then lift (put (n + 1)) -- You keep looping by default
else break () ) -- Use `break` to exit from the `loop`

The above loop increments n until n is 10 and then exits from the loop. We can verify this by running the State action:

>>> execState example 0
10

By default, you wrap commands other than break with lift. However, for some effects (like State) you can omit the lift:

example :: State Int ()
example = loop (do
n <- get
if n < 10
then put (n + 1)
else break () )

This library uses a Break type which is implemented as ExceptT under the hood:

newtype Break r m a = Break { unBreak :: ExceptT r m a }

The break function just "throws an exception":

break :: Monad m => r -> Break r m a
break r = Break (throwE r)

Here "throwing an exception" doesn't use any sort of out-of-band feature built into the Haskell language. "Exceptions" are just ordinary values implemented within the language:

throwE :: Monad m => e -> ExceptT e m a
throwE = ExceptT (return (Left e))

... and ExceptT's implementation of (>>=) short-circuits when encountering a Left internally, skipping subsequent commands.

loop is just an ordinary function that repeats the loop body indefinitely and only stops when you break from the loop:

loop :: Monad m => Break r m () -> m r
loop m = do
x <- runExceptT (unBreak (forever m))
case x of
Left r -> return r
Right r -> return r

Conceptually we just "catch" the "exceptional value" and return the value. I use quotes because there's no reason to restrict this value to exceptions. You can return any old value from the loop this way:

example :: State Int Bool
example = loop (do
n <- get
if n < 10
then put (n + 1)
else break True )

>>> runState example 0
(True,10)

Notice how I don't have to define a special variation on the forever function that integrates with ExceptT or break to terminate correctly. Instead, break interacts correctly with forever out-of-the-box thanks to Haskell's laziness: forever only lazily evaluates as many actions as necessary and once the internal ExceptT short-circuits the forever function doesn't demand any further command repetitions.

This library also showcases one of Haskell's nifty features: the GeneralizedNewtypeDeriving language extension. Even though I wrap ExceptT in a Break newtype, I can still configure Break to reuse many of the interfaces that were originally implemented for ExceptT, like this:

{-# LANGUAGE GeneralizedNewtypeDeriving #-}

newtype Break r m a = Break { unBreak :: ExceptT r m a }
deriving
( Functor
, Applicative
, Monad
, MonadTrans
, MonadIO
, MonadCont
, MonadState s
, MonadWriter w
)

The GeneralizedNewtypeDeriving extension is clever and knows how to wrap and unwrap the newtype to transparently lift all of these type classes to work on Break.

In fact, the library implementation is remarkably small. Here's the entire implementation if you omit the documentation:

{-# LANGUAGE GeneralizedNewtypeDeriving #-}

import Control.Applicative (Applicative)
import Control.Monad (forever)
import Control.Monad.IO.Class (MonadIO)
import Control.Monad.Trans.Class (MonadTrans(..))
import Control.Monad.Trans.Except (ExceptT, runExceptT, throwE)
import Control.Monad.Cont (MonadCont )
import Control.Monad.State (MonadState )
import Control.Monad.Writer (MonadWriter)
import Prelude hiding (break)

newtype Break r m a = Break { unBreak :: ExceptT r m a }
deriving
( Functor
, Applicative
, Monad
, MonadTrans
, MonadIO
, MonadCont
, MonadState s
, MonadWriter w
)

break :: Monad m => r -> Break r m a
break r = Break (throwE r)

loop :: Monad m => Break r m () -> m r
loop m = do
x <- runExceptT (unBreak (forever m))
case x of
Left r -> return r
Right r -> return r

Newtypes are probably one of the Haskell features I miss the most when programming in other languages. They are free performance-wise (especially with the recent work on Data.Coerce) and you pay very little code to transport interfaces across newtype boundaries. You get all of the benefits of abstraction and precise types at very little cost.

If you would like to use the break library you can find the library on Hackage or Github.

by Gabriel Gonzalez ([email protected]) at June 15, 2015 02:04 PM

optional-args-1.0.0: Optional function arguments

I'm releasing a small library named optional-args to simplify functions that take optional arguments.

Traditionally you would represent an optional argument using Maybe, like this:

greet :: Maybe String -> String
greet (Just name) = "Hello, " ++ name
greet Nothing = "Hello"

Then you would provide a specific value by wrapping the value in pure or Just:

>>> greet (pure "John")
"Hello, John"

... or you can use the default by suppling empty or Nothing:

>>> greet empty
"Hello"

The disadvantage to this approach is that Maybe does not implement the IsString, Num, or Fractional type classes, meaning that you cannot use numeric or string literals in place of Maybe. You have to explicitly wrap them in pure or Just.

The optional-args library provides an Optional type that is equivalent to Maybe, but with additional instances for IsString, Num, and Fractional:

data Optional a = Default | Specific a

instance IsString a => IsString (Optional a)
instance Num a => Num (Optional a)
instance Fractional a => Fractional (Optional a)

Additionally, the constructors are better-named for the task of defining function arguments:

import Data.Optional

greet :: Optional String -> String
greet (Specific name) = "Hello, " ++ name
greet Default = "Hello"

Since Optional implements IsString, you can use a naked string literal anywhere a function expects an Optional string argument as long as you enable the OverloadedStrings extensions:

>>> :set -XOverloadedStrings
>>> greet "John"
"Hello, John"

... and you can still use either Default or empty to use the default:

>>> greet empty
"Hello"

Similarly, any function that accepts an Optional numeric argument:

birthday :: Optional Int -> String
birthday (Specific age) = "You are " ++ show age ++ " years old!"
birthday Default = "You are one year older!"

... will accept naked numeric literals when you invoke the function:

>>> birthday 20
"You are 20 years old!"

For values that are not literals, you can still wrap them in pure:

>>> let age = 20
>>> birthday (pure age)
"You are 20 years old!"

The IsString, Num, and Fractional instances are recursive, so you can wrap your types in a more descriptive newtype and derive IsString or Num:

{-# LANGUAGE GeneralizedNewtypeDeriving #-}

import Data.Optional
import Data.String (IsString)

newtype Name = Name { getName :: String } deriving (IsString)

greet :: Optional Name -> String
greet (Specific name) = "Hello, " ++ getName name
greet Default = "Hello"

newtype Age = Age { getAge :: Int } deriving (Num)

birthday :: Optional Age -> String
birthday (Specific age) = "You are " ++ show (getAge age) ++ " years old!"
birthday Default = "You are one year older!"

... and you would still be able to use naked numeric or string literals as function arguments:

>>> :set -XOverloadedStrings
>>> greet "John"
"Hello, John"
>>> birthday 20
"You are 20 years old!"

The Optional type's Monoid instance also plays nicely with the IsString instance. Specifically, Optional obeys these two laws:

fromString (str1 <> str2) = fromString str1 <> fromString str2

fromString mempty = mempty

... which is a fancy way of saying that this code:

>>> greet ("John " <> "Smith")
"Hello, John Smith"

... will behave the same as this code:

>>> greet "John Smith"
"Hello, John Smith"

Even if we were to implement an IsString instance for Maybe, it would not satisfy the second law.

The Optional type is also the only Maybe-like type I know of that has a recursive Monoid instance:

instance Monoid a => Monoid (Optional a)

These sorts of recursive instances come in handy when chaining Monoid instances as illustrated in my post on scaling equational reasoning.

The optional-args library also comes with documentation explaining intended usage in detail (almost identical to this post), so if the user clicks on the Optional type they will discover clear instructions on how to use the type.

If you would like to use this, you can find the library on Hackage or Github.

by Gabriel Gonzalez ([email protected]) at June 15, 2015 02:03 PM

Don Stewart (dons)

Haskell dev role in Strats at Standard Chartered [London]

The Strats team at Standard Chartered has an open position for a typed functional programming developer, based in London. Strats are a specialized software engineering and quantitative analysis team building software for financial markets users.

You will work on the trading floor, directly with traders, building software to automate their work and improve their efficiency. The role is highly development focused and you will use Haskell for almost all tasks: data analysis, market data publishing, database access, web services, desktop GUIs, large parallel tasks, quantitative models, solvers, everything. This is a fast paced role – code you write today will be deployed within hours to hundreds of users and has to work.

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

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

The role requires physical presence on the trading floor in London. Remote work is not an option. Ideally you have some project and client management skills — you will talk to users, understand their problems and then implement and deliver what they really need. No financial background is required.

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

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

Role posted 2015-06-15


Tagged: jobs

by Don Stewart at June 15, 2015 09:11 AM

Magnus Therning

Using QuickCheck to test C APIs

Last year at ICFP I attended the tutorial on QuickCheck with John Hughes. We got to use the Erlang implementation of QuickCheck to test a C API. Ever since I’ve been planning to do the same thing using Haskell. I’ve put it off for the better part of a year now, but then Francesco Mazzoli wrote about inline-c (Call C functions from Haskell without bindings and I found the motivation to actually start writing some code.

The general idea

Many C APIs are rather stateful beasts so to test it I

  1. generate a sequence of API calls (a program of sorts),
  2. run the sequence against a model,
  3. run the sequence against the real implementation, and
  4. compare the model against the real state each step of the way.

The C API

To begin with I hacked up a simple implementation of a stack in C. The “specification” is

/**
 * Create a stack.
 */
void *create();

/**
 * Push a value onto an existing stack.
 */
void push (void *, int);

/**
 * Pop a value off an existing stack.
 */
int pop(void *);

Using inline-c to create bindings for it is amazingly simple:

{-# LANGUAGE QuasiQuotes #-}
{-# LANGUAGE TemplateHaskell #-}

module CApi
    where

import qualified Language.C.Inline as C
import Foreign.Ptr

C.include "stack.h"

create :: IO (Ptr ())
create = [C.exp| void * { create() } |]

push :: Ptr () -> C.CInt -> IO ()
push s i = [C.exp| void { push($(void *s), $(int i)) } |]

pop :: Ptr () -> IO C.CInt
pop s = [C.exp| int { pop($(void *s)) } |]

In the code below I import this module qualified.

Representing a program

To represent a sequence of calls I first used a custom type, but later realised that there really was no reason at all to not use a wrapped list:

newtype Program a = P [a]
    deriving (Eq, Foldable, Functor, Show, Traversable)

Then each of the C API functions can be represented with

data Statement = Create | Push Int | Pop
    deriving (Eq, Show)

Arbitrary for Statement

My implementation of Arbitrary for Statement is very simple:

instance Arbitrary Statement where
    arbitrary = oneof [return Create, return Pop, liftM Push arbitrary]
    shrink (Push i) = Push <$> shrink i
    shrink _ = []

That is, arbitrary just returns one of the constructors of Statement, and shrinking only returns anything for the one constructor that takes an argument, Push.

Prerequisites of Arbitrary for Program Statement

I want to ensure that all Program Statement are valid, which means I need to define the model for running the program and functions for checking the precondition of a statement as well as for updating the model (i.e. for running the Statement).

Based on the C API above it seems necessary to track creation, the contents of the stack, and even if it isn’t explicitly mentioned it’s probably a good idea to track the popped value. Using record (Record is imported as R, and Record.Lens as RL) I defined it like this:

type ModelContext = [R.r| { created :: Bool, pop :: Maybe Int, stack :: [Int] } |]

Based on the rather informal specification I coded the pre-conditions for the three statements as

preCond :: ModelContext -> Statement -> Bool
preCond ctx Create = not $ RL.view [R.l| created |] ctx
preCond ctx (Push _) = RL.view [R.l| created |] ctx
preCond ctx Pop = RL.view [R.l| created |] ctx
    where
        l = length $ RL.view [R.l| stack |] ctx

That is

  • Create requires that the stack hasn’t been created already.
  • Push i requires that the stack has been created.
  • Pop requires that the stack has been created and that it holds at least one value. (That last bit isn’t explicitly mentioned but seems like a good thing to assume.)

Furthermore the “specification” suggests the following definition of a function for running a statement:

modelRunStatement :: ModelContext -> Statement -> ModelContext
modelRunStatement ctx Create = RL.set [R.l| created |] True ctx
modelRunStatement ctx (Push i) = RL.over [R.l| stack |] (i :) ctx
modelRunStatement ctx Pop = [R.r| { created = c, pop = headMay s, stack = tail s } |]
    where
        c = RL.view [R.l| created |] ctx
        s = RL.view [R.l| stack |] ctx

(This definition assumes that the model satisfies the pre-conditions, as can be seen in the use of tail.)

Arbitrary for Program Statement

With this in place I can define Arbitrary for Program Statement as follows.

instance Arbitrary (Program Statement) where
    arbitrary = liftM P $ ar baseModelCtx
        where
            ar m = do
                push <- liftM Push arbitrary
                let possible = filter (preCond m) [Create, Pop, push]
                if null possible
                    then return []
                    else do
                        s <- oneof (map return possible)
                        let m' = modelRunStatement m s
                        frequency [(499, liftM2 (:) (return s) (ar m')), (1, return [])]

The idea is to, in each step, choose a valid statement given the provided model and cons it with the result of a recursive call with an updated model. The constant 499 is just an arbitrary one I chose after running arbitrary a few times to see how long the generated programs were.

For shrinking I take advantage of the already existing implementation for lists:

    shrink (P p) = filter allowed $ map P (shrink p)
        where
            allowed = and . snd . mapAccumL go baseModelCtx
                where
                    go ctx s = (modelRunStatement ctx s, preCond ctx s)

Some thoughts so far

I would love making an implementation of Arbitrary s, where s is something that implements a type class that contains preCond, modelRunStatement and anything else needed. I made an attempt using something like

class S a where
    type Ctx a :: *

    baseCtx :: Ctx a
    preCond :: Ctx a -> a -> Bool
    ...

However, when trying to use baseCtx in an implementation of arbitrary I ran into the issue of injectivity. I’m still not entirely sure what that means, or if there is something I can do to work around it. Hopefully someone reading this can offer a solution.

Running the C code

When running the sequence of Statement against the C code I catch the results in

type RealContext = [r| { o :: Ptr (), pop :: Maybe Int } |]

Actually running a statement and capturing the output in a RealContext is easily done using inline-c and record:

realRunStatement :: RealContext -> Statement -> IO RealContext
realRunStatement ctx Create = CApi.create >>= \ ptr -> return $ RL.set [R.l| o |] ptr ctx
realRunStatement ctx (Push i) = CApi.push o (toEnum i) >> return ctx
    where
        o = RL.view [R.l| o |] ctx
realRunStatement ctx Pop = CApi.pop o >>= \ v -> return $ RL.set [R.l| pop |] (Just (fromEnum v)) ctx
    where
        o = RL.view [R.l| o |] ctx

Comparing states

Comparing a ModelContext and a RealContext is easily done:

compCtx :: ModelContext -> RealContext -> Bool
compCtx mc rc = mcC == rcC && mcP == rcP
    where
        mcC = RL.view [R.l| created |] mc
        rcC = RL.view [R.l| o |] rc /= nullPtr
        mcP = RL.view [R.l| pop|] mc
        rcP = RL.view [R.l| pop|] rc

Verifying a Program Statement

With all that in place I can finally write a function for checking the validity of a program:

validProgram :: Program Statement -> IO Bool
validProgram p = and <$> snd <$> mapAccumM go (baseModelCtx, baseRealContext) p
    where
        runSingleStatement mc rc s = realRunStatement rc s >>= \ rc' -> return (modelRunStatement mc s, rc')

        go (mc, rc) s = do
            ctxs@(mc', rc') <- runSingleStatement mc rc s
            return (ctxs, compCtx mc' rc')

(This uses mapAccumM from an earlier post of mine.)

The property, finally!

To wrap this all up I then define the property

prop_program :: Program Statement -> Property
prop_program p = monadicIO $ run (validProgram p) >>= assert

and a main function

main :: IO ()
main = quickCheck prop_program

June 15, 2015 12:00 AM

June 11, 2015

Yesod Web Framework

cabal's does not exist error message

I've seen many people confused by this error message, and just ran into it myself, so decided a blog post to explain was in order.

As I was hacking on stack this morning, I pushed and got a build failure from Travis with the following content at the end:

Failed to install asn1-encoding-0.9.0
Last 10 lines of the build log ( /home/travis/.cabal/logs/asn1-encoding-0.9.0.log ):
cabal: /home/travis/.cabal/logs/asn1-encoding-0.9.0.log: does not exist

What the error message means is: I tried to load up the log file containing the output of the build, but the file does not exist. It's possible that there are multiple reasons for this, but I know of only one: when cabal is unable to download the necessary package from Hackage, usually because Hackage is having a temporary blip.

As a user: if you see this message, just try running your command again. If it's a temporary Hackage outage, the second attempt may succeed. Another option (which I'd strongly recommend) is to switch to a more reliable package index; see the blog post on FP Complete's S3 mirror for more details. I've been pushing for a while to make this the default remote-repo used by cabal-install, but unfortunately that hasn't happened. (For the record: stack does use the S3 mirror by default.)

For cabal: I see three steps worth taking:

  1. Fix this confusing error message to say something like "Download of http://... failed". I thought there was a cabal issue opened about this already, which is why I didn't open up a new one right now. If there isn't one, it's worth opening.
  2. Automatically retry a failing download. I'm not convinced this is a good thing to do, but it's a possible mitigation. (We don't do that right now in stack, though I've been toying with the idea. Feedback appreciated.)
  3. Switch to a more reliable mirror for the default remote-repo.

Fixing this instability at the Hackage level would of course also be a good move.

June 11, 2015 12:00 AM

Christopher Done

Stream fusion and composability (Java 8 and Haskell) for newbies

In an online discussion, when Java 8 released their stream API, written about here, you can write e.g.

public List<Article> getAllJavaArticles() {
    return articles.stream()
        .filter(article -> article.getTags().contains("Java"))
        .collect(Collectors.toList());
}

Someone asked, “But my question: would the streams be faster than loops? Or is the only benefit better readability?” Someone answered that the benefit is that streams compose and loops don’t. What does composable mean here? Below is my answer, using two languages I know, JavaScript and Haskell.

Composable in this context means: To be able to compose two things into one without redundancy or overhead. For example, consider you want to map a function f over an array arr to produce a new array, you might do this:

var arr2 = [];
for (var i = 0; i < arr.length; i++)
    arr2.push(f(arr[i]));

If you want to filter the array based on a predicate p, you might do this:

var arr3 = [];
for (var i = 0; i < arr2.length; i++)
    if (p(arr2[i]))
        arr3.push(arr2[i]);

Or maybe you want to take all elements until a a predicate p2 is not satisfied:

var arr4 = [];
for (var i = 0; i < arr3.length; i++)
    if (p2(arr3[i]))
        arr4.push(arr3[i]);
    else
        break;

Now, if you want to do that all in one process you have a few options:

  • Put them all one after the other verbatim as I’ve written above. Redundant, a maintenance issue and inefficient.
  • Merge them all into one clever loop. Also redundant (re-implementing the same concept of mapping, filtering and taking), error prone (it’s easy to get manual loops wrong, especially merging several concepts together), and a maintenance burden.
  • Put them each into a method on your language’s Array type as map(), filter(), and takeWhile() and then write arr.map(f).filter(p).takeWhile(p2). Good abstraction, very low maintenance because the functions are black boxes. But inefficient.

An ideal stream API will give you the last point, but be able to understand concepts like mapping and filtering and know how to merge them together into an efficient loop. This is called stream fusion, which you can google if you want to know more.

I don’t know Java but I can give a Haskell example:

map f . filter p . takeWhile p2

(Note: In Haskell the operations separated by . are run right to left, like map f (filter p (takeWhile p2 …)).)

If I compile this with GHC, e.g.

main = print ((map f . filter p . takeWhile p2) [1..10])
  where p2 = (<5)
        p = even
        f = (+2)

and look at the reduced output called Core, a language the compiler generates code for before generating assembly or byte code, the map f . filter p are both compiled into a single loop (Core output is verbose, so I collapsed it into this more readable form). This just walks over the list, checks whether the item is even, if so, keeps it and adds 2 to it, otherwise skips that item:

mainzugo xs =
  case xs of
    [] -> []
    (x:ys) ->
      case even x of
        False -> mainzugo ys
        True -> x + 2 : mainzugo ys

Which is pretty nifty. Furthermore, if you fold (also called reducing) e.g.

foldr (+) 0 . map f . filter p

Then that whole thing is also compiled into one loop:

mainzugo xs =
  case xs of
    [] -> 0
    (x:ys) ->
      case even x of
        False -> mainzugo ys
        True -> (x + 2) + mainzugo ys

There’re limits to what can compose with what, though.

June 11, 2015 12:00 AM

June 10, 2015

The GHC Team

GHC Weekly News - 2015/06/10

Hi *,

Welcome for the latest entry in the GHC Weekly News. The past week, GHC HQ met up for a quick catch up on 7.10.2 (which you'll want to read up on, see below), and some other technical nonsense about some work we've been doing. As a result the current weekly notes have been slow - the current priority is the next release though, which leads us to...

7.10.2 status

7.10.2 is going to be out soon - our current plan is to have a release candidate on the weekend of Saturday the 13th, and the final release the next week. That means if you want something fixed, you'd better hollar very soon, or we're just not going to get to it!

If you're wondering what's currently been fixed/scheduled, the status page shows the current set of tickets we've fixed and plan on fixing.

List chatter

  • Jan Stolarek asks: in some cases, GHC will generate default instances or values, but that source code has no textual information location (for example, consider an instance clause without the where) - what do people think about fixing this, and are there anythings to look out for? https://mail.haskell.org/pipermail/ghc-devs/2015-June/009202.html
  • David Luposchainsky has opened a new thread - about moving fail out of Monad and into its own typeclass, MonadFail. This change is a request that's very long in the tooth (older than the AMP or FTP changes by a landslide), but David's proposal has a clearly set out goal to tackle compatibility, warnings, and implementation. https://mail.haskell.org/pipermail/ghc-devs/2015-June/009186.html

Noteworthy commits

Closed tickets

#10460, #7672, #9252, #9506, #10294, #5316, #10408, #10386, #9960, #10145, #9259, #10386, #9507, #8723, #10442, #5014, #4215, #10443, #8244, #10499, #10500, #10428, #10488, #10489, #10406, #10501, #10441, #10406, #10502, #9101, #9663, and #9945.

by thoughtpolice at June 10, 2015 09:34 PM

Brent Yorgey

Ally Skills Tutorial at ICFP

I just signed up for the Ally Skills Tutorial at ICFP, and if you are (1) a man who (2) will be at ICFP in Vancouver, I encourage you to sign up, too! From the website:

The Ally Skills Tutorial teaches men simple, everyday ways to support women in their workplaces and communities. Participants learn techniques that work at the office, in classrooms, at conferences, and online. The skills we teach are relevant everywhere, including skills particularly relevant to open technology and culture communities. At the end of the tutorial, participants will feel more confident in speaking up to support women, be more aware of the challenges facing women in their workplaces and communities, and have closer relationships with the other participants.

This sounds super helpful—I suspect there is often a large gap between the extent to which I want to support women and the extent to which I actually know, practically, how to do so. The workshop will be taught by Valerie Aurora, Linux filesystem developer and Ada Initiative co-founder; I expect it will be high quality!


by Brent at June 10, 2015 08:47 PM

Well-Typed.Com

Summer School on Generic and Effectful Programming

I’m one of the lecturers at

Summer School on Generic and Effectful Programming

St Anne’s College, Oxford, 6th to 10th July 2015

(Register here)

Datatype-generic programming was the topic of my PhD thesis many years ago, and it has continued to be a fascinating field of work and research for me since then.

At the upcoming summer school, I will give a three-lecture course on Applying Type-level and Generic Programming in Haskell. In this course, I will describe the state-of-the-art of datatype-generic programming in Haskell/GHC. This means we’ll look at the GHC extension that allows you to generically derive your own type classes, but also at the relatively recent generics-sop library. We will discuss the GHC type system features that make all of this possible, such as data kinds, kind polymorphism, GADTs, higher-rank types, constraint kinds and more, and we will look at a number of real-world applications of generic programming, taken, e.g., from the areas of web programming and databases.

But my course is only one of many. Ralf Hinze, the main organizer, has done an outstanding job and assembled a fantastic lineup of lecturers: I’m honoured to be teaching alongside Edwin Brady, Fritz Henglein, Conor McBride, Don Syme and Tarmo Uustalu. I am sure I will learn a lot from them and their lectures.

If you always wanted to learn more about generic and effectful programming, this is your chance! You can still register for the school! I’d be happy to see you there.

by andres at June 10, 2015 12:36 PM

Don Stewart (dons)

Haskell dev role in Strats at Standard Chartered [London]

The Strats team at Standard Chartered has an open position for a typed functional programming developer, based in London.

You will work on the trading floor, directly with traders, building software to automate their work and improve their efficiency. The role is highly development focused and you will use Haskell for almost all tasks: data analysis, market data publishing, database access, web services, desktop GUIs, large parallel tasks, quantitative models, solvers, everything. This is a fast paced role – code you write today will be deployed within hours to hundreds of users and has to work.

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

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

The role requires physical presence on the trading floor in London. Remote work is not an option. Ideally you have some project and client management skills — you will talk to users, understand their problems and then implement and deliver what they really need. No financial background is required.

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

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

Role posted 2015-06-10


Tagged: jobs

by Don Stewart at June 10, 2015 08:27 AM

June 09, 2015

FP Complete

ANNOUNCING: first public beta of stack

stack is a new, complete, cross-platform development tool aimed at both new and experienced Haskell developers alike, for installing and setting up the compiler, installing packages needed, and building, testing or benchmarking one or more packages in a project at a time. It's the whole stack.

We developed it in collaboration with the Commercial Haskell Group, with two deliberate goals in mind:

  1. Newbie friendliness, ease of setup and doing the right thing by default. Just get people running with Haskell as conveniently as possible.
  2. Catering to the finer points of serious commercial Haskell development. Supporting the modern use-cases of working on large Haskell projects.

In short, it's a program that you run in a directory with a stack configuration file in it (stack.yaml—automatically created if one doesn't exist). That directory may contain one or many packages inside it to be built. Then there are commands to build, test, install dependencies, run GHC, etc.

Here's a rundown of the advantages stack brings to the table. For both newbies and experienced Haskellers:

  • It's really easy to get going with Haskell. You can just run stack build in a package directory and it will automatically download and install GHC, the standard Haskell compiler, for you, download the package index and install packages that are needed.
  • It also caters to newbies reading books who just want to run ghc on a file. You can run stack ghc X.hs and it will download GHC if necessary, etc. until it can run GHC on that file. The same is true for stack ghci, etc.
  • It automatically assumes (and does some figuring out if there's a project Cabal file) the latest LTS Haskell release as its source of packages, or otherwise a nightly release. This means you can just use packages without worrying about what versions match up and trying to think like a package manager thinks.

For experienced Haskellers, there is support for typical use-cases and subtleties of larger projects:

  • This also means you can just put the snapshot release in your version control, via the stack.yaml file, which is important for reliable collaboration.
  • Serious commercial or large scale users of Haskell can build so-called "mega-repos", by adding to the list of packages in your stack.yaml, you can build/test/bench multiple projects at once. stack build will just build everything. stack build this will build this package and rebuild anything that depends on it, and also any of its dependencies that changed.
  • You can enable profiling in the configuration and this will automatically rebuild all packages with profiling turned on for you.
  • Packages are installed into isolated package databases by default. There is a layering of three package databases: The global database, the snapshot database, and your personal project's database. Many projects can share the same global database (base, bytestring, etc.) and the snapshot database (e.g. text, haskell-src-exts, etc.)—which means no unnecessary rebuilding of packages—and yet each project has its own package database, so they are isolated from each other and cannot break each other.
  • Binary installs of your personal projects are also isolated into that directory.
  • In this "local" database, you can also specify newer upstream versions than are available in the snapshot. In fact, the snapshot is optional, you can be based on plain Hackage. This is not the default behaviour and is a configuration option.
  • It also supports docker integration for truly sandboxed environments. By enabling docker in the configuration, running stack build will download the image if necessary and then run the build inside the docker image. There is an array of options available for the docker integration.

We first arrived at this tool based on feedback from our clients at FP Complete and have been using this tool in-house ourselves for around a year, in several iterations. This final iteration has had particular focus on ease of use. We were also motivated by the results of the recent Haskell survey.

Feedback from members of the Commercial Haskell Group has been very helpful in shaping the direction of the tool in a positive way and we now open it up, open source, in beta and for the Haskell community as a whole and welcome your contributions, ideas and feedback!

stack is available on Hackage (cabal install stack), as well as binary downloads for Windows, Mac, and Linux, with Ubuntu and Arch packages. Please note that this is a beta release: we anticipate bugs, and will work to quickly resolve them. Please be sure to report issues on the Github issue tracker.

June 09, 2015 08:00 AM

Magnus Therning

`mapAccum` in monad

I recently had two functions of very similar shape, only difference was that one was pure and the other need some I/O. The former was easily written using mapAccumL. I failed to find a function like mapAccumL that runs in a monad, so I wrote up the following:

mapAccumM :: (Monad m, Traversable t) => (a -> b -> m (a, c)) -> a -> t b -> m (a, t c)
mapAccumM f a l = swap <$> runStateT (mapM go l) a
    where
        go i = do
            s <- get
            (s', r) <- lift $ f s i
            put s'
            return r

Bring on the comments/suggestions/improvements/etc!

June 09, 2015 12:00 AM

June 08, 2015

Ken T Takusagawa

[gszzqvjg] Seeding a PRNG with a string

Some Haskell codes demonstrating how to initialize random number generators (equivalently stream ciphers) with a string (and salt).  The main point of these demonstration codes are to list what modules one needs to import and show how to hook things together.

aes-ctr-demo.hs generates a stream of random bytes using AES-256 in counter mode (CTR).  (This implements option 2 among this enumeration of ways to do counter mode.)  Without arguments, it uses the scrypt key derivation function to convert the password and salt to a 256-bit AES key.  It also demonstrates two alternatives to scrypt: a SHA-512 instance of PBKDF2, and using straight unsalted SHA-256 as a key derivation function (the latter is cryptographically terrible idea because it is relatively easy to mount a dictionary attack against it compared to real KDFs).

mwc-demo.hs demonstrates seeding the non-cryptographic MWC random number generator with 258 words generated with PBKDF2.

tf-demo.hs demonstrates seeding the TF (ThreeFish) random number generator with a 4-tuple of Word64 generated with PBKDF2.

Alternate Source code directory

Disclaimer: I have paid no attention to whether these demonstrations are vulnerable to side-channel attacks.  They almost certainly are vulnerable.

by Ken ([email protected]) at June 08, 2015 04:23 AM

June 07, 2015

Dominic Steinitz

Population Growth Estimation via Hamiltonian Monte Carlo

Here’s the same analysis of estimating population growth using Stan.

data {
  int<lower=0> N; // number of observations
  vector[N] y;    // observed population
}

parameters {
  real r;
}

model {
  real k;
  real p0;
  real deltaT;
  real sigma;
  real mu0;
  real sigma0;
  vector[N] p;
  k      <- 1.0;
  p0     <- 0.1;
  deltaT <- 0.0005;
  sigma  <- 0.01;
  mu0    <- 5;
  sigma0 <- 10;

  r ~ normal(mu0, sigma0);

  for (n in 1:N) {
    p[n] <- k * p0 * exp((n - 1) * r * deltaT) / (k + p0 * (exp((n - 1) * r * deltaT) - 1));
    y[n] ~ normal(p[n], sigma);
  }
}

Empirically, by looking at the posterior, this seems to do a better job than either extended Kalman or vanilla Metropolis.


by Dominic Steinitz at June 07, 2015 06:47 PM

Neil Mitchell

ghcid 0.4 released

Summary: I've released a new version of ghcid, which is faster and works better for Vim users.

I've just released version 0.4 of ghcid. For those who haven't tried it, it's the simplest/dumbest "IDE" that could possibly exist. It presents a small fixed-height console window that shows the active warnings/errors from ghci, which is updated on every save. While that might not seem like much, there are a number of improvements over a standard workflow:

  • You don't have to switch to a different window and hit :reload, just saving in your editor is enough.
  • It includes warnings from modules that successfully compiled previously, as opposed to ghci which omits warnings from modules that didn't reload.
  • It reformats the messages to the height of your console, so you can see several messages at once.

I find it gives me a significant productivity boost, and since there is no editor integration, it adds to my existing tools, rather than trying to replace them (unlike a real IDE).

Version 0.4 offers a few additional improvements:

  • We use fsnotify to watch for changes, rather than polling as in older versions. The result is a significant decrease in battery usage, combined with faster responses to changes.
  • If you change the .cabal or .ghci file then ghcid will restart the ghci session to pick up the changes.
  • If you are a Vim user, then the sequence of temporary files Vim uses on save could upset ghcid. I believe these issues are now all eliminated.
  • The number of errors/warnings is displayed in the titlebar of the console.
  • There is a feature to run a test after each successful save (using --test). I am expecting this to be a niche feature, but feel free to prove me wrong.

Tempted to give it a try? See the README for details.

by Neil Mitchell ([email protected]) at June 07, 2015 09:57 AM