Programming languages

From Spivey's Corner
Jump to: navigation, search

This is a kind of log of my work on a prospective book that explores the landscape of programming languages via purely functional interpreters written in Haskell.

The programs are formatted using a literate programming system of my own devising, implemented in a mixture of C/Lex and TCL and supported by Plain TeX macros. Part of the point is that large parts of the interpreters for many languages can be shared, without the heavy type machinery that would be needed to make generic implementations. For example, I can make a set of <Standard clauses for eval> that work with any suitable monad, and can be pasted into the text of many interpreters, without having some clunky mechanism for extensible recursive function definitions. I like the results, but am happy to hear suggestions for improvement. (Please don't ask for a copy of the tools, because they are completely undocumented and seriously flaky.)

7th October 2016

Why pipeline components can't terminate

Consider the definition of the pipe operator:

pipe :: Pipe ι η ???  Pipe η ο ???  Pipe ι ο ???
pipe xm ym =
 MkPipe (λk ik ok 
  apPipe ym k0 (MkInCont (λok'  apPipe xm k0 ik ok')) ok)
 where k0 x ik" ok" = error "terminated"

If we want to allow the components xm and ym to terminate then we must replace the continuation k0 with something else – possibly different continuations for xm and ym if that helps. When the exit continuation of ym (say) is called, we have access to the following quantities of note:

  • The continuation k to be called when the pipe exits.
  • The original continuation ik and ok passed to the pipe; these capture the state of the left and right context of the pipe at the time it was created, but are out of date now.
  • The continuations ik" and ok" that are the current context of ym. Note that ik" has type InCont η and doesn't even have the right type to be passed to k, which expects an input continuation of type InCont ι. Surely, buried inside ik'' there is a continuation of the appropriate kind, representing the left context of whatever xm has evolved into; but even if we could peel off the frames one by one, there is no knowing (if xm has become a pipeline in its own right) how many frames should be discarded.

It seems to me that we can't implement the rule that the whole pipe terminates when either xm or ym do. An alternative rule might be that both xm and ym must terminate, and then their values are combined somehow; this seems hopeless, because typically once one of these processes has stopped communicating, then the other will soon be deadlocked.

What can be implemented is that when either process terminates, the value it returns is discarded, and the process to its right receives a special value on its input channel – perhaps Nothing in place of Just a normal value. This is not so hard to implement.

6th October 2016

5th October 2016

From Matthew Pickering:

There is at least one library implemented in terms of continuations: https://hackage.haskell.org/.../Conduit-Simple-Core.html

And the authors of other popular libraries provide functions to convert between the two representations. https://github.com/Gabriel439/Haskell-Pipes-Extras-Library/commit/95b33460b016c5ed6348c9046ab8701161f22d2d

3rd October 2016

  • Valery Trifonov, Simulating quantified class constraints, Proceedings of the 2003 ACM SIGPLAN workshop on Haskell, ACM 2003.

After several hours of fruitless footling around, I discovered that the definition

forever :: Monad m  m a  m b
forever xm = ym where ym = do xm; ym

makes a benchmark 10 times faster than writing

forever xm = do xm; forever xm

It is used at the hot end of the pipeline, but that amount of difference is surprising.

28th September 2016

Best references for Pipes and Conduits?

27th September 2016

The road to hell was paved with good intentions as regards keeping this blog going ...

  • I read Voigtländer's paper about the codensity optimisation. It explains partly what's going on with the faster >>=, but there's another ingredient in the treatment of pipe
http://www.janis-voigtlaender.eu/papers/AsymptoticImprovementOfComputationsOverFreeMonads.pdf

14th September 2016

  • Replaced the lists of continuations with single input and output continuations, and dropped the restriction to Int channels. The types work out nicely if you keep your wits about you.
  • Performance-wise, the continuations are a win in terms of order of growth for deeply nested programs using either >>= or pipe, and a good fraction faster for the primes program too.
  • Mostly rewrote the paper for the new implementation.
  • Also made a defunctionalised implementation (which needs GADTs) that seems a bit faster still. Like many defunked programs, it looks like a program that can be derived but not explained.

13th September 2016

  • In some programs, the performance of sequential composition is much better for the continuation-based coroutines, but for parallel composition the two implementations are about comparable. I'm now tempted to think about operating-system-like data structures for process scheduling, but I don't think they will be easy or elegant.
  • Pursuing this idea, I made an implementation that passes around the left and right contexts of a process as two lists of continuations. This is back to the idea that contexts will be passed around everywhere: you can drop the universal quantifier. To keep the types sane, I had to specialize all channels to type Int, so some more deep type stuff will be needed when I drop that restriction.
  • And after all, the lists of continuations are an unnecessary implementation detail, aren't they? They can surely be packaged up as a single continuation.
  • Oh, and by the way, I also had to make it an error for any process to terminate after it has been joined in a pipeline with others: it's too hard to make (p >> q) terminate when either p or q does. But I suppose I could forbid p from terminating but allow q to do so – in that case only the rightmost link in a chain would be allowed to return.

(It seems no accident that I am going round in circles on many aspects of this.)

11-12th September 2016

  • Working on a paper on coroutines, with comparison with a direct-style implementation. Lennart Augustson suggests this image for Russell's paradox:
You are leaving Y

9th September 2016

  • Fixed a bug with interpretation of <Abbreviated chunk names...> by htangle
  • More editing of exercises, including taking out boilerplate code from the answers that should not appear in the book, and fixing things so the code will compile.
Two coroutines circle the whirlpool of impredicativity

8th September 2016

  • A chapter about coroutines implemented with continuations.

7th September 2016

Sorted through about 50 exercises from old problem sheets, updating them technically and improving some wording. Ground to a halt when I reached the later exercises about continuations, which seem like they could be improved in the light of my experience with the parser combinators.

Early September

As a warm-up, revisited the appendix where an implementation of parser combinators appears. Parsers can initially work with only the first line of the input, and can suspend themselves and prompt for more input if it's needed; producing the prompt takes us outside what can be done with a lazy input stream, and continuations are the key.

Personal tools

Variants
Actions
Navigation
Tools