Skip to content

Types and Programming Languages Chapter 4 An ML Implementation of Arithmetic Expressions

Jump to bottom Edit New page
Simon Woolf edited this page Mar 5, 2017 · 17 revisions

## Our implementations

Before the meeting, a large number of people implemented code based on the material in chapters 3 and 4:

Nominal plan

We started by discussing what we had nominally planned for the meeting. We were going to mob program an implementation of the eval function from chapter 4. We agreed we should reserve plenty of time (a full hour) for show and tell as lots of people had built things.

We considered which language to use. We settled on JavaScript as it was one of the few languages no one had chosen beforehand and the majority of people were loosely familiar with it.

Getting started

We decided we'd like to implement eval by figuring things out for ourselves, rather than basing it on the implementation in the book. We started by considering the boolean rules. Tom wrote them up on the whiteboard:

t ::= true
      false
      if t then t else t

if true then t₂ else t₃ → t₂

if false then t₂ else t₃ → t₃

                   t₁ → t₁′
----------------------------------------------
if t₁ then t₂ else t₃ → if t₁′ then t₂ else t₃

We collectively came up with some test cases relating to these rules, e.g. if true then true else false. We'd use these test cases to drive out a solution in a TDD-esque manner. Paul offered to type.

We decided to use CodePen and opted for some low-fi console.log testing.

How should we represent terms? Functions? Objects? Arrays?

We agreed to use constructor functions for a number of reasons, including:

  • it would be easier to add methods to our objects if we decided to
  • it feels quite natural to think in terms of objects in our programs (Murray)
  • it would be easier to reference their properties, e.g. t.t3 rather than t[2]

Implementing the rules

We focussed on the eval1 function which performs a small-step evaluation of a term. We spoke about how to handle the "no rule applies" case. We agreed to come back to this once we had developed our code a bit further.

We then moved on to eval which needed to call eval1 multiple times. We had two options:

We can either use an explicit looping construct such as a while loop or we could use recursion.

Recursion seemed to be a popular choice. Paul sketched out the code and Leo explained how it worked.

We added more rules to implement, this time including succ, pred and iszero. We still needed to deal with the "no rule applies" problem but decided to keep going. We didn't really have enough implemented to be able to construct good test cases for this yet.

There was a brief interlude. It was generally agreed that adding salt to coffee was a bad idea. Someone pointed out that people seem to add almost anything to coffee, e.g. butter and rum. @tuzz proposed banoffee coffee and toffee coffee. Everyone rolled their eyes applauded profusely.

We briefly talked about whether we should return a new Zero object for E-PredZero or return the existing Zero object from t1. This was quickly cleared up by following the rule literally and returning a new Zero object.

We proceeded to fill in the remaining rules. We were approaching an hour into the meeting so we made the decision to park the implementation in its current state. Things that were left:

  • adding guard conditions around nested eval1 calls for things where "no rule applies"
  • implementing isNumericVal and adding it as a condition to the appropriate rules e.g. (pred (succ true))

A cleaned up version of our code is available on GitHub.

Show and tell

(The implementations are listed at the top of this page.)

Ben

Ben used Swift to implement the eval function. He used indirect enum in a few places. He noted it was more-or-less a literal translation of the code in the book. He used pattern matching in his case statement. There was a brief discussion about the use of where in the case statement. Ben explained that where is part of Swift's pattern matching and can be used outside of case as well. He wasn't sure whether it was idiomatic Swift. He suggested that option types might be more idiomatic.

Simon

Simon used Prolog. There was some discussion about premises being written after the rule. This differs from the style in the book. His implementation referred to eval1 as reduce which some felt was a better name for this function. Simon pointed out that Prolog lends itself well to this kind of problem. So well, in fact, that we're able to run the program backwards to generate terms:

Leo pointed out this this "drives the point home" that we're dealing with an infinite set. We can continually apply the rules to build bigger terms.

Paul

Paul's implementation was in Rust. He hoped, before he started, that Rust would be a good language for this as it supports pattern matching but then 'immediately ran into problems'. Specifically, problems relating to the ownership of objects. We noted that indirect from Ben's Swift implementation was similar to the use of box in Paul's. This is a way to tell the static compiler to use the heap rather than the stack for storing terms. By default, Rust prefers the stack. Paul made use of the option monad to handle eval1 calls on terms that couldn't be evaluated any further.

Dmitry

Dmitry used Kotlin which he explained is a relatively new language that's related to Scala and Java. He didn't go into too much detail, but explained he had implemented the eval function as well.

Leo

Leo used Haskell and pointed out it was a straightforward implementation (no need for 'indirect' or 'box'). He implemented the eval function which used the small-step semantics. He then explained he'd experimented with QuickCheck, which is a property testing framework. He took the theorems from chapter 3 and generated random terms which he fed through these property tests.

In cases where a violation of some property was found, Leo implemented a custom shrinking function which attempts to find the simplest possible counter-example that demonstrates the problem. He pointed out that you don't have to write your own shrinking function. He'd had a go at implementing the E-Funny rules from chapter 3 to demonstrate that they violated some of the theorems. He also implemented eval using big-step semantics then used QuickCheck to demonstrate that the two implementations were equivalent.

Rich

Rich's implementation was in Python. He explained it was similar to the other implementations. He explicitly threw exceptions and used an explicit while loop rather than recursion for the eval function. He implemented a constructor function to build Term classes and explained it was a bit unusual to define classes inside a function. He then refactored his code to use functions for each rule rather than the case statement.

Rich implemented the 'funny' rules as well and showed they violated the theorems. He then spoke about how he used yield to replace the explicit error handling. In cases where no further evaluation could take place, nothing would be yielded (an analogy was made to an empty list). He then moved on to attempting to write a pattern matching framework in Python.

Finally, Rich explained that he'd used Jupyter which is a tool that is commonly used when scientists work with large data sets. It allows you to evaluate expressions in real time and display their derivation trees. He'd used nested html tables for this. The isNumerivVal condition became just another rule in these derivation trees.

Laura

Laura used Racket. She was hesitant at first to demo her implementation, but Leo was keen to see some Racket code. She explained she'd used Racket's pattern matching features as well as guard clauses.

Chris P

Chris had implemented eval in Ruby and took the book's implementation quite literally. He explained he'd have liked to implement a polymorphic solution which moved behaviour onto the term subclasses. He briefly showed a graph that represents his Turing machine implementation.

Chris had implemented the rules for a Turing machine that evaluated terms. He explained the online environment he'd used only supported single-letter symbols which made it quite difficult to make sense of. He showed the Turing machine running to reduce a non-trivial expression to false.

He explained that his Turing machine operated in a right-left direction of the input. Much of the implementation was taken up with the monotony of copying symbols around on the tape. He demonstrated an example that used lots of pred and succ and showed this copying process.

Chris Z

Chris used Elixir and had made use of its pattern matching features and guard clauses. He'd tried to change eval to work without throwing exceptions.

Simon

Simon also used Elixir with a very simple lexer and parser to parse a string input into nested tuples, and a small step and big step evaluator. Each used a different workaround to the problem in Elixir of not being able to have arbitrary recursive functions in guard clauses for is_numeric etc. (the small-step capped the maximum recursion depth; the big-step used a custom conditional macro rather than the built-in case clause).

Tom

Tom had implemented a parser and evaluator for the metalanguage used in the book for defining grammars. He'd then used this metalanguage to define the specific grammar defined in chapters 3 and 4. Like Rich, he needed to define a syntactic category for nv.

We discussed the possibility of using Tom's metalanguage in future meetings for other grammars the book defines. He suggested it might just work without additional changes.

John

John had implemented eval in Ruby through the use of parslet. He explained that he'd exploited parslet's support for transforming trees in order to actually perform the evaluation of expressions.

Retrospective

At the end of the meeting, we held a very brief retrospective as we'd already overrun. We agreed we should:

  • timebox show and tells so that everyone has an equal amount of time to present
  • be more prepared for mobbing, e.g. set up a simple test harness ahead of time

We questioned whether mob programming will work with more complicated chapters. John noted that we'll likely be ok for a little while longer as the next chapters are about the lambda calculus, which we collectively have some knowledge of.

Tom explained that he felt encouraged by this meeting. It's a challenging book and we seem to have collectively got a grip on the main concepts.

Finally, we talked about when to hold the next meeting as some people are away. Deferred to Slack.

## Pub

A few of us went to the pub.

Add a custom footer
Clone this wiki locally