Fri Aug 21 08:14:26 CEST 2009

PF interpreter in Ocaml

I'd like to encode the interpreter data types in something more rigid,
to see if I missed some corner case.

The first thing to realize is to distinguish types and constructors.

      SEQ = (SUB : SUB)            ;; `:' is graph CONS
      SUB = PRIM | QUOTE | SEQ
      K   = HALT | (SUB . K)      ;; `.' is linear CONS

type sub  = 
  | Quote
  | Seq   of sub * sub ;;

type k = 
  | Frame of sub * k ;;

The second thing is to realize that dynamic typing is a _lot_ less
restrictive than the ML type system.  Especially the wrapping
necessary make unions of other types.  Dave Herman describes it
here[2] in relation to the way it's done in Typed Scheme[3].

type sub  = 
    Prim  of prim
  | Quote of datum
  | Seq   of sub * sub

and k = 
  | Frame of sub * k

and datum =
    Number of int
  | Code of sub 
  | Pair of pair

and prim =
    Address of int

and pair =
  | Cons of datum * datum


Now I'm trying to express the interpreter.  Ocaml's syntax is weird.
Constructors have different syntax from functions?

Aha.  Ok I understand.  Constructors can take multiple inputs, but
functions always take a signle one.  Multiple inputs are handled using
currying.  A constructor seems to be a function that takes a tuple.

Next: how do you put a function in a datatype?  I.e. the prim type is
actually state -> state.  Looks like I want GADTs[4][5][6].  This
looks like a can of worms I don't want to get into yet.  Let's use
simple enumeration.

Good.  It's running.  See code here [7].

I've added 'Run' which leads to some arbitrariness in encoding the
types.  Is Run a prim or a special case of code?  I'd say the latter
since it operates on the whole machine state instead of just the
parameter stack.

Quite revealing to have to specify things a bit tighter..  From a
first real contact, I think I like OCaml, even if it is more
restrictive.  It is definitely more easy to get things right once they
pass the type checker.  I should have a closer look at Typed

Now, getting the 'fac' example running. In factor:

  : fac ( n -- n! ) dup 1 = [ 1 ] [ dup 1 - fac ] if * ;

What is necessary is a way to define a cyclic data structure.
Apparently `let rec' does not allow this:

let rec _fac =
  Seq(lit 1,
  Seq(quot (lit 1),  
  Seq(quot ((Seq(_dup,
             Seq(lit 1,

=> Error: This kind of expression is not allowed as right-hand side of `let rec'

How to solve this?  In Scheme it's easy: just dump a symbol at first,
then walk the data structure and set! the value.

[1] http://lambda-the-ultimate.org/node/983
[2] http://calculist.blogspot.com/2008/09/true-unions-revisited.html
[3] http://www.ccs.neu.edu/home/samth/typed-scheme/
[4] http://www.haskell.org/haskellwiki/Generalised_algebraic_datatype
[5] http://okmij.org/ftp/ML/GADT.ml
[6] http://www.haskell.org/haskellwiki/GADTs_for_dummies
[7] http://zwizwa.be/darcs/libprim/pf/pf.ml
[8] http://caml.inria.fr/pub/ml-archives/caml-list/2008/12/460de486fcbbc2eca13e5c77d014da17.en.html