TAPL in Julia

New to Julia
1

Hello!
I am reading the book “Types and Programming Languages” by B.Pierce and I’m trying to implement the various models in Julia. The code I am trying to translate is the following (in Ocaml):

type term =
    TmTrue of info
  | TmFalse of info
  | TmIf of info * term * term * term
  | TmZero of info
  | TmSucc of info * term
  | TmPred of info * term
  | TmIsZero of info * term
 let rec isnumericval t = match t with
    TmZero(_) -> true
  | TmSucc(_,t1) -> isnumericval t1
  | _ -> false

let rec isval t = match t with
    TmTrue(_)  -> true
  | TmFalse(_) -> true
  | t when isnumericval t  -> true
  | _ -> false

let rec eval1 t = match t with
    TmIf(_,TmTrue(_),t2,t3) ->
      t2
  | TmIf(_,TmFalse(_),t2,t3) ->
      t3
  | TmIf(fi,t1,t2,t3) ->
      let t1' = eval1 t1 in
      TmIf(fi, t1', t2, t3)
  | TmSucc(fi,t1) ->
      let t1' = eval1 t1 in
      TmSucc(fi, t1')
  | TmPred(_,TmZero(_)) ->
      TmZero(dummyinfo)
  | TmPred(_,TmSucc(_,nv1)) when (isnumericval nv1) ->
      nv1
  | TmPred(fi,t1) ->
      let t1' = eval1 t1 in
      TmPred(fi, t1')
  | TmIsZero(_,TmZero(_)) ->
      TmTrue(dummyinfo)
  | TmIsZero(_,TmSucc(_,nv1)) when (isnumericval nv1) ->
      TmFalse(dummyinfo)
  | TmIsZero(fi,t1) ->
      let t1' = eval1 t1 in
      TmIsZero(fi, t1')
  | _ -> 
      raise NoRuleApplies

My attempt in Julia is the following

abstract type Info end
abstract type Term <:Info end
abstract type TmTrue <:Info end
abstract type TmFalse <:Info end
abstract type TmZero<:Info end
struct TmSucc 
  t::Term
end

struct TmPred 
  t::Term
end

struct TmIf 
  fi::Info
  tmcond::Term
  tmthen::Term
  tmelse::Term
end

struct NoRuleApplies <:Exception end

function is_numerical(t::TmZero) 
  true
end

function is_numerical(x::TmSucc)
  is_numerical(x.t)
end

function is_numerical(x)
  false
end

function is_val(x::TmTrue)
  true
end
 
function is_val(x::TmFalse)
  true
end

function is_val(x)
  is_numerical(x)
end

I’m stuck at the definition of eval1.
Thanks

2

This OCaml code is not complete, so I added this at the top to make it work. Probably these values are defined elsewhere in the book.

type info = string
let dummyinfo : info = ""
exception NoRuleApplies

My impression from reading your attempted translation is that you either don’t understand how types are defined in OCaml or you don’t know how they are defined in Julia. So… you need to get that squared away.

Also, I’d much rather use OCaml for building this kind of evaluator than Julia, since OCaml can verify that it’s correct at compile-time. Nonetheless, this is what I came up with:

const Info = String
const dummyinfo = ""

struct NoRuleApplies <: Exception end

abstract type Term end

struct TmTrue <: Term
    i::Info
end
struct TmFalse <: Term
    i::Info
end
struct TmIf <: Term
    i::Info
    t1::Term
    t2::Term
    t3::Term
end
struct TmZero <: Term
    i::Info
end
struct TmSucc <: Term
    i::Info
    t::Term
end
struct TmPred <: Term
    i::Info
    t::Term
end
struct TmIsZero <: Term
    i::Info
    t::Term
end

isnumericval(::TmZero) = true
isnumericval(t::TmSucc) = isnumericval(t.t)
isnumericval(::Term) = false

isval(::TmTrue) = true
isval(::TmFalse) = true
isval(t::Term) = isnumericval(t)  # the ocaml code is redundant in this case.

eval1(t::TmIf) =
    t.t1 isa TmTrue ? t.t2 :
    t.t1 isa TmFalse ? t.t3 :
    TmIf(t.i, eval1(t.t1), t.t2, t.t3)
eval1(t::TmSucc) = TmSucc(t.i, eval1(t.t))
eval1(t::TmPred) =
    t.t isa TmZero ? TmZero(dummyinfo) :
    t.t isa TmSucc && isnumericval(t.t) ? t.t :
    TmPred(t.i, eval1(t.t))
eval1(t::TmIsZero) =
    t.t isa TmZero ? TmTrue(dummyinfo) :
    t.t isa TmSucc && isnumericval(t.t.t) ? TmFalse(dummyinfo) :
    TmIsZero(t.i, eval1(t.t))
eval1(::Term) = raise NoRuleApplies

I haven’t checked to see if it does anything useful, so there may be mistakes.

3

Thank you! I am little embarrassed as I should made my homework better. The type info is defined in an additional file available from the book’s website, basically as a tuple:

type info = FI of string * int * int | UNKNOWN

and used mostly for parsing. Anyways your answer was extremely useful. Thank you again.

1 Like