Here is a link to the "Pierce Book" or Benjamin Pierce's draft transcript of (the first part of) "Types and Programming Languages".

On PDF page 28 you'll see an OCaml implementation of eval1. Which I assumed is like a recursive single-step evaluator?

See the directory Dots' first tutorial / project D code. As you see I have a fully functioning grammar at least of the syntax. Now I'm wondering if we convert the pegged ParseTree into some other internal format? Or do we try to operate on ParseTree's themselves and then finally pretty print a result?

For example, one evaluation rule is E-BetaBoolT: if true then s:Term else t:Term |-> s, where here |-> is the evalutation relation.

So if for example I decided to convert true to a bool and throw away the pegged ParseTree, then it seems like it would 1) harder to implement because you have to write a 1-1 correspondence of classes with your grammar rules at least. And 2) it's going to be full of bugs and error prone, thus making your math kernel buggy which can't happen as is enforced in practice.

On the other hand manipulating someone else's ParseTree seems tacky. Though, it seems like an efficient enough structure. So I'm wondering, what would be the advantages of converting to a second type or layer of software? Would the ParseTree method be significantly slower?

      Term <- IfThenElse(Term) / Successor(Value) / 
              Predecessor(Value) / IsZero(Value) / Value
      IfThenElse(T) < "if" T "then" T "else" T
      Successor(V) < "succ" V
      Predecessor(V) < "pred" V    
      IsZero(V) < "iszero" V     
      Value <- True / False / Zero
      True <- "true"
      False <- "false"
      Zero <- "0"

There is my grammar, and I am able to produce parse trees from it. But I don't know what to do with the parse trees to "evaluate" them.

How I'm currently implementing if-then-else evaluator:

// Inside class IfThenElse that inherits from Term abstract class
override Value evaluate() const {
      if (if_cond.evaluate().is_true)
         // Pierce book: if true then t2 else t3 -> t2 (E-BOOLBETAT)
         return then_part.evaluate();
      else {
         // Pierce book: if false then t2 else t3 -> t3 (E-BOOLBETAF)
         return else_part.evaluate();
  • 1
    $\begingroup$ It's not clear what you are asking, at leat to me. Are you asking how to implement an interpreter? $\endgroup$ Oct 28, 2022 at 18:25
  • $\begingroup$ @AndrejBauer yes, something like that would be sufficient for this exercise. I simply need to take input expressions and evaluate them using the one (or many) step evaluation rules from the book. And I know how to walk the parse tree produced. Just not sure what to do to "evaluate" the parse tree "expressions". Also see my questions in the post concerning efficiency and robustness. $\endgroup$ Oct 29, 2022 at 19:21
  • 1
    $\begingroup$ Yes, you're evaluating the conditional using the standard computation rules. My point was that the $\eta$-rule if b then t else t ≡ t is not something that would appear in such a straightforward manner in an interpreter. $\endgroup$ Oct 31, 2022 at 20:40

1 Answer 1


Faithfully implementing textbook small-step semantics is not necessarily the best way to implement an interpreter. Large step semantics is often more intuitive and direct, as it amounts to a straightforward recursive fold of the syntax tree.

As for organizing datatypes, it is often a good idea to evaluate (pre-processed) syntax trees to values, which are defined as a separate datatype. For example, a common technique for evaluating λ-abstractions is to form closures (terms together with their local runtime environment), and those are not expressible in the original syntax.

The Programming languages zoo has simple examples of techniques:

  • Small-step semantics for a functional language miniml evaluates syntax trees back to syntax trees, see eval.ml. (There is also a separate compiler.)

  • Large-step semantics for a functional language minihaskell evaluates syntax trees to a value datatype, see interpret.ml

For more advanced techniques I highly recommend Andras Kovacs's work:

  • smalltt demonstrating techniques for high-performance elaboration with dependent types.
  • The elaboration zoo includes a series of Haskell implementations for elaborating dependently typed languages. There are accompanying videos.
  • $\begingroup$ What are the advantages of converting to a different (from the parse tree) internal data type? You just say "often a good idea" :). $\endgroup$ Oct 30, 2022 at 17:11
  • $\begingroup$ Also I have a tertiary question. How do I implement this so that I have distinguished / separate "inference rules". The evaluator then appeals to or calls these inference rules for each case? Alternatively, the inference rules are implicit / embedded / hardcoded into the evaluation (interpreter) code. $\endgroup$ Oct 30, 2022 at 17:28
  • $\begingroup$ For example "if true then t else t'" evaluates to t by a certain inference rule. Do I check that the if-condition is true inside an inference rule function or outside of it? $\endgroup$ Oct 30, 2022 at 18:54
  • 1
    $\begingroup$ I added one reason for having a separate datatype, but there are many more. The rule for the conditional that you give is not one that you commonly find in an operational semantics or a normalization procedure, because it is quite tricky and complicated, and it breaks things. So just forget about it for now. $\endgroup$ Oct 30, 2022 at 19:17
  • $\begingroup$ Thank you! See addendum to my post for how I'm currently handling if-then-else. I'm wondering though, when in the book will the inference rules be coded in the constructed language itself. $\endgroup$ Oct 30, 2022 at 19:29

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.