Ralf adds a construct

Ralf’s assignment does not revolve around Huttons Razor. After all, Hutton has a patent (which he graciously grants every language researcher free use of). Rather, Ralf augments the razor with a Exit construction:

data Exp : Set where
  Const : ℕ -> Exp
  Plus  : Exp -> Exp -> Exp
  Exit  : Exp -> Exp

The informal meaning of Exit is this: Exit e will evaluate the computation e and then abort the rest of the program, returning e as its value. To reflect the idea that the program may be in two possible states now, either computing, or exiting, we need a way to tag what state we are in. Haskell people have the Either a b type, but in Agda, this is a disjoint sum:

R = ℕ ⊎ ℕ

Ralf generously provided some helper functions defining an algebra for how to compute with the disjoint sum so we translate these to Agda. Constant expressions are injected to the left in the sum:

const : ℕ -> R
const i = inj₁ i

Addition compares the two sides. It propagates right injections up, but computes on left injections. This is as Ralf does in his post.

add : R -> R -> R
add (inj₁ x) (inj₁ x') = inj₁ (x + x')
add (inj₁ x) (inj₂ y) = inj₂ y
add (inj₂ y) y' = inj₂ y

Finally, if we want to exit, we convert a left injection to a right one, and just pass on the right injection.

exit : R -> R
exit (inj₁ x) = inj₂ x
exit (inj₂ y) = inj₂ y

The neat thing about defining an algebra like this for R-computations is that now the evaluation function is almost as simple as in the Razor:

eval : Exp -> R
eval (Const y) = const y
eval (Plus y y') = add (eval y) (eval y')
eval (Exit e) = exit (eval e)

The only new thing is the Exit case which formalizes our informal definition above: compute eval e and exit with it.

Task 1, continuations

Next, we CPS-transform our semantics. We could naively transform the language, above into CPS and then provide that, but that is a boring solution. Nay, the cool thing about CPS is that it makes the control flow of the program explicit. We can exploit this explicit control-flow to optimize the case of Exit expressions in the program.

module NotNaive where

Ok, so we throw everything into a submodule, NotNaive, to limit what is in our scope at any point in time so naming is not going to trip us up later.

  constK : ℕ -> (ℕ -> ℕ) -> ℕ
  constK i k = k i

This is part of our algebra as before. If we have a constant, how do we handle it? We add another parameter, the k above which is the kontinuation. In the case of the Razor-extension, we can regard k as “the rest of the program”. It has type (ℕ -> ℕ) which sort-of makes it a transformer on natural numbers. So if we are to deliver the natural number i to the kontinuation, we apply k i.

Additions take two values and delivers the addition to the kontinuation (which still is, intuitively, the rest of the program):

  addK : ℕ -> ℕ -> (ℕ -> ℕ) -> ℕ
  addK v1 v2 k = k (v1 + v2)

In the Exit case comes the trick. We do the following

  exitK : ℕ -> (ℕ -> ℕ) -> ℕ
  exitK i k = i

which is to not deliver the value to k but just return it straight away. This means that we will abort the evaluation of “the rest of the program” and just return the exit value straight away.

We now turn our attention in this language towards the evaluation function in the language. Constants are handled in the obvious way by using the algebra directly, but the two other cases are handled differently:

  evalK : Exp -> (ℕ -> ℕ) -> ℕ
  evalK (Const y) k = constK y k
  evalK (Plus y y') k = evalK y (\v1 -> evalK y' (\v2 -> addK v1 v2 k))
  evalK (Exit y) k = evalK y (\v1 -> exitK v1 k)

Take the Exit-case first. We evaluate the y like in the direct case. But then, we need to supply a continuation which says what the rest of the program does. Our continuation assumes it gets passed a value v1 which is the result of the y computation. It then exits with this value. The Plus case is similar, but there are two continuations to juggle. We evaluate y and deliver it to a continuation that first evaluates y' and then delivers to the final continuation, using our addK function from above.

To run the program:

run2 : Exp -> ℕ
run2 e = NotNaive.evalK e id

note we pass in the id identity function to “start up” the evaluation. This is in balance with what Ralf did. Again, Agda’s termination checker immediately provides termination guarantees for program.

Task 2: A Taste of dependent types

The main reason I set out to do this however, was to utilize the dependent types Agda has built-in. There are something eternally pleasing in defining programs which do not need to compute to answer questions, and here we will see an example of it.

The task is to create a function pure taking an expression and returning true if the expression is pure and false otherwise. Purity is defined as absence of an Exit expression. New module:

module DepAnalysis where

Now, dependent types are more than what the following claims it to be, I am aware. But as a first foray, it is quite mind-boggling in itself and serves as a great simple introduction. If we define

  data Exp' : Bool -> Set where

we have declared a dependent datatype Exp' which has a Bool value attached to it. This means we have two types of expressions: Exp' true and Exp' false. These are different types from the view of the type checker. You can read Bool -> Set as “if we supply a boolean value to an Exp', then it will yield a Set - Set being the elements of the Agda”world" we are working in. So we can just assume in our world, that if an expression is pure, it is Exp' true and otherwise, it is Exp' false.

    Const : ℕ -> Exp' true

This constructor tells Agda that if we supply the Const constructor with a natural number, it will hand us a pure expression. Seems in order, sir! Next constructor:

    Exit  : ∀ {c} -> Exp' c -> Exp' false

This can be read as “if you give my any expression, pure or not - I don’t care - then I will give you a non-pure expresssion”. This makes sense. There is an Exit in the expression, so it better not be pure. It doesn’t matter what the internal expression is.

    Plus  : ∀ {c1 c2} -> Exp' c1 -> Exp' c2 -> Exp' (c1 ∧ c2)

In the final case, Plus we get to supply two expressions. These two expressions have c1 and c2 as their purity-values. Agda will hand us back an expression which is pure if and only if both subexpressions are - due to the conjunction (logical and) in the returned expression.

What have we done here? We have created a dependent data type which will itself track if an expression is pure or not. As we build up the abstract syntax tree, the system will make the calculations necessary. Notice, that if the whole AST is known at compile time, then so is the purity of the expression - right away.

For completeness, we supply the required function pure. Here is the type:

  pure : {b : Bool} -> Exp' b -> Bool

It introduces a new concept, namely implicit parameters. The type {b : Bool} names a parameter which is implicit. We can normally omit implicit parameters when writing functions because it can be extracted from another type in the specification (in this case from Exp' b which contains the b). However, if we need access to the implicit parameter, we can positionally match it by wrapping it in brackets like this:

  pure {x} e = x

So the purity of the expression is already there, we just need to return it! I personally think this is awfully neat.

I want to play more

The Agda wiki contains tutorials, the Agda implementation, and all the other cool information on how to play with Agda. The development here is in a gist on github should you want to play with. Note that the development I made hardly qualifies to show off the really cool features of Agda but only scratches (barely) the surface of what is possible. My intuition is, however, that we will see much more dependently typed programming in the future, when everyone is programming functionally :)

Commentary is as always welcome.

Processing

Clustering

Looking forward

{riak_err,
 [{log_mf, true},
  {error_logger_mf_dir, "log/mf"},
  {error_logger_mf_maxbytes, 10240000},
  {error_logger_mf_maxfiles, 10}
 ]},

Final words

• Enables error reports above 16Kb in size. No limit-function is employed yet, though it would be preferable. I could imagine a report with the state of a large heap being pushed.
• Use compression on terms. Disk IO is slow compared to in-memory compression.
• Fixes some redundancy in the rb grep code by making the code into a match compiler. This patch can probably flow into OTP after some more testing.
• Use binary notation. The rb and log_mf_h code is probably so old Erlang did not have binaries at that time.