a few STLCs

safestlc.ml

(* components for type-level lists *)
type tnil = |
type ('head, 'tail) tcons = |

(* singletons for types in our system *)
type _ sty =
  | IntTy : int sty
  | FnTy : 'a sty * 'b sty -> ('a -> 'b) sty

(* binary operations on integer expressions *)
type op =
  | Add
  | Sub
  | Div
  | Mul

(* a heterogeneous list *)
type _ hlist =
  | HNil : tnil hlist
  | HCons : ('head * 'tail hlist) -> (('head, 'tail) tcons) hlist

(* a safe index into a heterogeneous list *)
type (_, _) ix =
  | IxZ : ('head, ('head, _) tcons) ix
  | IxS : ('a, 'tail) ix -> ('a, ('head, 'tail) tcons) ix

(* safely index an hlist *)
let rec hget : type a tylist. (a, tylist) ix -> tylist hlist -> a = fun ix xs ->
  match ix, xs with
  | (IxZ, HCons(x, _)) -> x
  | (IxS(i), HCons(_, xs)) -> hget i xs
  | (_, _) -> . (* impossible! *)

(* expressions, indexed by the types they evaluate to and the required
 * type context
 *)
type (_, _) expr =
  | Lit : int -> (int, 'ctx) expr
  | Var : ('a, 'ctx) ix -> ('a, 'ctx) expr (* de bruijn notation! *)
  | OpApp : (op * (int, 'ctx) expr * (int, 'ctx) expr) -> (int, 'ctx) expr
  | Lam : 'tyIn sty * ('tyOut, (('tyIn, 'ctx) tcons)) expr
          -> ('tyIn -> 'tyOut, 'ctx) expr
  | App : ('a -> 'b, 'ctx) expr * ('a, 'ctx) expr -> ('b, 'ctx) expr

(* look ma no typechecker! *)
let rec eval' : type ctx a. ctx hlist -> (a, ctx) expr -> a = fun ctx ex ->
  match ex with
  | Lit(n) -> n
  | Var(ix) -> hget ix ctx
  | OpApp(op, lhs, rhs) -> begin match op, eval' ctx lhs, eval' ctx rhs with
                           | (Add, x, y) -> x + y
                           | (Sub, x, y) -> x - y
                           | (Div, x, y) -> x / y
                           | (Mul, x, y) -> x * y
                           end
  | Lam(ty, body) -> fun x -> eval' (HCons(x, ctx)) body
  | App(lhs, rhs) -> (eval' ctx lhs) (eval' ctx rhs)

let eval = eval' HNil

let main () =
  let expr1 = App(Lam(IntTy, OpApp(Add, Var(IxZ), Lit(3))), Lit(4)) in
  (* this won't compile!
   * we get:
     File "safestlc.ml", line 64, characters 18-36:
     64 |                   Lam(IntTy, Lit(3))) in
                            ^^^^^^^^^^^^^^^^^^
     Error: This expression has type ('a -> 'b, 'c) expr
            but an expression was expected of type (int, 'd) expr
            Type 'a -> 'b is not compatible with type int

  let expr2 = App(Lam(IntTy, OpApp(Add, Var(IxZ), Lit(3))),
                  Lam(IntTy, Lit(3))) in
  *)
  Printf.printf "%d\n" (eval expr1)

let _ = main ()

Stlc.fs

open System

// types in our system
type Type =
    | IntTy
    | FnTy of Type * Type

// binary operations on integer expressions
type Op =
    | Add
    | Sub
    | Div
    | Mul

// expressions in our system
type Expr =
    | Lit of int
    | Var of string
    | OpApp of Op * Expr * Expr
    | Lam of string * Type * Expr
    | App of Expr * Expr

// a fully-evaluated value in our system
type Value =
    | Int of int
    | Fn of (Value -> Value)

(* a "type context" or "value context" - in other words, the static
 * or dynamic lexical scope of an expression, represented as a stack.
 * we'll do lookup by name - this is not an efficient implementation!
 *)
type Ctxt<'a> = string * 'a list

// look up a variable in a context, innermost-to-outermost
let rec lookup var ctxt =
    match ctxt with
    | [] -> None
    | ((v, x)::xs) -> if var = v then Some(x) else lookup var xs

// typecheck an expression in a typing context
let rec check' ctxt expr =
    match expr with
    | Lit(_) -> Some(IntTy)
    | Var(v) -> lookup v ctxt
    | OpApp(_, lhs, rhs) -> match (check' ctxt lhs, check' ctxt rhs) with
                            | (Some(IntTy), Some(IntTy)) -> Some(IntTy)
                            | _ -> None
    | Lam(v, fromTy, e) -> match check' ((v, fromTy)::ctxt) e with
                           | Some(toTy) -> Some(FnTy(fromTy, toTy))
                           | _ -> None
    | App(lhs, rhs) -> match (check' ctxt lhs, check' ctxt rhs) with
                       | (Some(FnTy(tyFrom, tyTo)), Some(ty)) ->
                               if tyFrom = ty then Some(tyTo) else None
                       | _ -> None

// check a "closed" term
let check = check' []

(* evaluate an expression in a dynamic context
 * we'll throw exceptions in the event of "stuck" evaluation
 * because these are type errors which the type checker should
 * catch beforehand!
 *)
let rec eval' ctxt expr =
    match expr with
    | Lit(n) -> Int(n)
    | Var(v) -> match lookup v ctxt with
                | Some(value) -> value
                | None -> failwith "did you typecheck this?"
    | OpApp(op, lhs, rhs) -> match (op, eval' ctxt lhs, eval' ctxt rhs) with
                             | (Add, Int(x), Int(y)) -> Int(x + y)
                             | (Sub, Int(x), Int(y)) -> Int(x - y)
                             | (Mul, Int(x), Int(y)) -> Int(x * y)
                             | (Div, Int(x), Int(y)) -> Int(x / y)
                             | _ -> failwith "did you typecheck this?"
    | Lam(v, _, e) -> Fn(fun x -> eval' ((v, x)::ctxt) e)
    | App(lhs, rhs) -> match (eval' ctxt lhs, eval' ctxt rhs) with
                       | (Fn(f), x) -> f x
                       | _ -> failwith "did you typecheck this?"

// evaluate a closed term
let eval = eval' []

// check and (if successful) evaluate an expression, printing the result
let doExpr expr =
    match check expr with
    | Some(ty) -> printfn "%A : %A" expr ty
                  printfn "-> %A" (eval expr)
    | None -> printfn "%A : type error!" expr

[<EntryPoint>]
let main argv =
    let expr1 = App(Lam("x", IntTy, OpApp(Add, Var("x"), Lit(3))), Lit(4));
    let expr2 = App(Lam("x", IntTy, OpApp(Add, Var("x"), Lit(3))),
                    Lam("y", IntTy, Lit(3)));
    doExpr expr1
    doExpr expr2
    0 // return an integer exit code

stlc.ml

(* types in our system *)
type ty =
  | IntTy
  | FnTy of ty * ty

let rec print_ty ppf = function
  | IntTy -> Printf.fprintf ppf "IntTy"
  | FnTy(fromTy, toTy) -> Printf.fprintf ppf "%a -> (%a)"
      print_ty fromTy print_ty toTy

(* binary operations on integer expressions *)
type op =
  | Add
  | Sub
  | Div
  | Mul

let rec print_op ppf = function
  | Add -> Printf.fprintf ppf "Add"
  | Sub -> Printf.fprintf ppf "Sub"
  | Div -> Printf.fprintf ppf "Div"
  | Mul -> Printf.fprintf ppf "Mul"

(* expressions in our system *)
type expr =
  | Lit of int
  | Var of string
  | OpApp of op * expr * expr
  | Lam of string * ty * expr
  | App of expr * expr

let rec print_expr ppf = function
  | Lit(n) -> Printf.fprintf ppf "%d" n
  | Var(v) -> Printf.fprintf ppf "%s" v
  | OpApp(op, lhs, rhs) -> Printf.fprintf ppf "%a(%a, %a)"
      print_op op
      print_expr lhs
      print_expr rhs
  | Lam(v, ty, body) -> Printf.fprintf ppf "λ(%s : %a) => %a"
      v
      print_ty ty
      print_expr body
  | App(lhs, rhs) -> Printf.fprintf ppf "(%a)(%a)"
      print_expr lhs
      print_expr rhs

(* a fully-evaluated value in our system *)
type value =
    | Int of int
    | Fn of (value -> value)

let print_value ppf = function
  | Int(n) -> Printf.fprintf ppf "%d" n
  | Fn(_) -> Printf.fprintf ppf "<function>"

(* a "type context" or "value context" - in other words, the static
 * or dynamic lexical scope of an expression, represented as a stack.
 * we'll do lookup by name - this is not an efficient implementation!
 *)
type 'a ctxt = string * 'a list

(* look up a variable in a context, innermost-to-outermost *)
let rec lookup var = function
  | [] -> None
  | ((v, x)::xs) -> if var = v then Some(x) else lookup var xs

(* typecheck an expression in a typing context *)
let rec check' cx = function
  | Lit(_) -> Some(IntTy)
  | Var(v) -> lookup v cx
  | OpApp(_, lhs, rhs) -> begin match (check' cx lhs, check' cx rhs) with
                          | (Some(IntTy), Some(IntTy)) -> Some(IntTy)
                          | _ -> None
                          end
  | Lam(v, fromTy, e) -> begin match check' ((v, fromTy)::cx) e with
                         | Some(toTy) -> Some(FnTy(fromTy, toTy))
                         | _ -> None
                         end
  | App(lhs, rhs) -> begin match (check' cx lhs, check' cx rhs) with
                     | (Some(FnTy(tyFrom, tyTo)), Some(ty)) ->
                             if tyFrom = ty then Some(tyTo) else None
                     | _ -> None
                     end

(* check a "closed" term *)
let check = check' []

(* evaluate an expression in a dynamic context
 * we'll throw exceptions in the event of "stuck" evaluation
 * because these are type errors which the type checker should
 * catch beforehand!
 *)
let rec eval' ctxt = function
  | Lit(n) -> Int(n)
  | Var(v) -> begin match lookup v ctxt with
              | Some(value) -> value
              | None -> failwith "did you typecheck this?"
              end
  | OpApp(op, lhs, rhs) -> begin match (op, eval' ctxt lhs, eval' ctxt rhs) with
                           | (Add, Int(x), Int(y)) -> Int(x + y)
                           | (Sub, Int(x), Int(y)) -> Int(x - y)
                           | (Mul, Int(x), Int(y)) -> Int(x * y)
                           | (Div, Int(x), Int(y)) -> Int(x / y)
                           | _ -> failwith "did you typecheck this?"
                           end
  | Lam(v, _, e) -> Fn(fun x -> eval' ((v, x)::ctxt) e)
  | App(lhs, rhs) -> begin match (eval' ctxt lhs, eval' ctxt rhs) with
                     | (Fn(f), x) -> f x
                     | _ -> failwith "did you typecheck this?"
                     end

(* evaluate a closed term *)
let eval = eval' []

(* check and (if successful) evaluate an expression, printing the result *)
let doExpr expr =
    match check expr with
    | Some(ty) -> Printf.printf "%a : %a\n" print_expr expr print_ty ty;
                  Printf.printf "-> %a\n" print_value (eval expr)
    | None -> Printf.printf "%a : type error!\n" print_expr expr

let main () =
  let expr1 = App(Lam("x", IntTy, OpApp(Add, Var("x"), Lit(3))), Lit(4)) in
  let expr2 = App(Lam("x", IntTy, OpApp(Add, Var("x"), Lit(3))),
                  Lam("y", IntTy, Lit(3))) in
  doExpr expr1;
  doExpr expr2;
  exit 0 (* return an integer exit code *)

let _ = main ();