Compiler basics: Lisp to Assembly

I can't remember the name of the paper. Any ideas? It was such an elegant way of walking through a compiler implementation.

I'm reaching out for some help from you. I've been working on interpreters this whole year, taking on no more work for pay than needed for rent and food, so that I can realize my programming language dream. I'm writing a couple of interpreters every week, trying out new ideas. But there is one hurdle I've been unable to overcome for a long time.

I'm trying to write a typechecker for a simple lambda calculus with polymorphic functions. My acceptance criteria is being able to typecheck the K combinator. I've been stuck at this point for months. Have read all I can find on the internet, and have read TAPL many times.

Am honestly feeling really stupid for not having been able to complete this.

What I'm struggling with beta reducing expressions that are type lambdas (i.e. the expression related to `Forall`).

Λ means type lambda, i.e. the set of expressions indexed by type

λ means expression lambda, i.e. the set of expressions indexed by expression

E.g. Λa.λx:a.x is the polymorphic "identity" function, which in javascript looks like `x => x`

k = ΛA.ΛB.λx:A.λy:B.x

k_intint = ((k IntTy) IntTy)

What I have yet been unable to do is type_of k_intint, and this because beta reduction should return an expression, but type_of should return a type.

I'll paste the source code of my latest attempt below, the function in question is `typ_of_expression`. I've written this in OCaml, but would be very thankful for a response in any language, or pseudocode, or just explained in English.

Many thanks for taking the time to read this. For any reply or pointer in the right direction I would be greatly thankful. You know what, I'd be happy to pay €100 for any help that lets me solve this (SEPA, Bitcoin).

  (* λ calculus, with Forall and simple types *)
  type 'a binding =
    | SymBind of 'a
    | QuantifierBind

  type 'a context = (string * 'a binding) list
  
  type typ =
    | UnitTy
    | IntTy
    | Arrow of typ * typ
    | Forall of string * typ
    (* Thought it simpler to separate Closure and Lambda, for w  hen I later add records/unions etc *)
    | ClosureTy of (typ context) * typ
    | SymbolTy of string
  
  type expr =
    (* again thought it simpler to separate Closure and Lambda,   for when I later add records/unions etc *)
    | Closure of (expr context) * expr
    | Unit
    | Symbol of string
    | Int of int
    | Lam of string * typ * expr  (* turns into Arrow. Takes ex  pr as argument, returns expr *)
    | App of expr * expr
    | TLam of string * expr       (* expr version of Forall. Ta  kes typ as argument, returns expr *)
    | TApp of expr * typ
  
  let rec lookup context key =
    match context with
    | [] -> Error "No result"
    | (k, QuantifierBind) :: rest -> lookup rest key
    | (k, SymBind v) :: rest -> if key = k
                                then Ok v
                                else lookup rest key
  
  let str = String.concat ""
  
  let rec string_of_typ t = match t with
    | UnitTy -> "UnitTy"
    | IntTy -> "IntTy"
    | Arrow _ -> "Arrow"
    | Forall (s, t) -> str ["Forall "; s; " "; string_of_typ t]
    | ClosureTy (_ctx, t) -> str ["Closure "; string_of_typ t]
    | SymbolTy s -> str ["SymbolTy "; s]
  
  let string_of_expr e = match e with
    | Unit -> "Unit"
    | Closure _ -> "Closure"
    | Symbol s -> str ["Symbol "; s]
    | Int i -> str ["Int "; string_of_int i]
    | Lam _ -> "Lam"
    | App _ -> "App"
    | TLam _ -> "TLam"
    | TApp _ -> "TApp"
  
  (* Convert between context types, such as (expr context) or (  typ context) *)
  let rec convert_context converter_fn original_context exprcon  text acc = (* カリたべたい *)
    let convert_context = convert_context converter_fn original  _context in
    match exprcontext with
    | [] -> acc
    | (x, QuantifierBind) :: rest ->
       convert_context rest ((x, QuantifierBind) :: acc)
    | (x, SymBind e) :: rest ->
       (match converter_fn original_context e with
        | Ok t -> convert_context rest ((x, SymBind t) :: acc)
        | Error e -> failwith (str ["typ_context error: "; e]))
  
  let rec typ_of_expr context e =
    match e with
    | Unit -> Ok UnitTy
    | Int i -> Ok IntTy
    | Closure (ctx, e) ->
       let new_context = convert_context typ_of_expr context ct  x context in
       typ_of_expr new_context e
    | Symbol s -> lookup context s
    | Lam (x, in_typ, body) ->
       (let new_context = (x, SymBind in_typ) :: context in
        match typ_of_expr new_context body with
        | Ok return_typ -> Ok (Arrow (in_typ, return_typ))
        | Error e -> Error (str [ "Error finding return type of   lambda. Error: "
                                ; e]))
    | App (e0,
           e1) ->
       (match (typ_of_expr context e0,
               typ_of_expr context e1) with
        | (Ok (Arrow (t0_0, t0_1)),
           Ok t1) -> if t1 = t0_0
                     then Ok t0_1
                     else Error (str ["Type mismatch"])
        | (Ok (ClosureTy (ctx, Arrow (t0_0, t0_1))),
           Ok t1) -> if t1 = t0_0
                     then Ok t0_1
                     else Error
                            (str
                               ["Type mismatch. t0_0: "
                               ;string_of_typ t0_0
                               ;", t0_1: "
                               ;string_of_typ t0_1
                               ;", t1: "
                               ;string_of_typ t1
                            ])
        | (Ok t, _) -> Error (str ["Not given a lambda as first   thing to App. "
                                  ;string_of_typ t])
        | _ -> Error (str ["Error getting typ of expr App"]))
    | TLam (a, body) ->
       (let new_context = (a, QuantifierBind) :: context in
        match typ_of_expr new_context body with
        | Ok body_type -> Ok (ClosureTy (new_context,
                                         Forall (a,
                                                 body_type)))
        | Error e -> Error (str [ "Failed to get typ of TLam, a  nd thus can not construct Forall. Error: "
                                ; e]))
    | TApp (TLam (a, body),
            t1) -> let new_context = (a, QuantifierBind) :: con  text in
                   typ_of_expr new_context body
    | TApp (e0, t1) ->
       (match typ_of_expr context e0 with
        | Ok (ClosureTy (ctx,
                         Forall (a, body))) ->
           let new_context = (a, SymBind t1) :: ctx @ context i  n
           Ok (ClosureTy (new_context,
                          body))
        | Ok (ClosureTy(ctx,
                        t)) ->
           Error (str ["TApp given ClosureTy with non-forall on   left-hand-side. IS: "
                      ;string_of_typ t])
        | Ok (Forall (a, body)) -> Error "TApp given naked Fora  ll as first argument"
        | Ok _ -> Error "TApp given non-Forall first argument"
        | Error e -> Error (str ["Error in TApp - error: "
                                ;e]))
  
  let rec eval context e =
    let context: (expr context) = context in
    match e with
    | Unit -> Ok Unit
    | Closure (ctx, e) -> eval (List.append ctx context) e
    | Int i -> Ok (Int i)
    | Lam (x, t, body) -> Ok (Closure (context,
                                       Lam (x, t, body)))
    | Symbol s -> lookup context s
    | App (Closure(ctx,
                   Lam (x, t, body)),
           e1) ->
       let new_context = (x, SymBind e1) :: ctx @ context in
       eval new_context body
    | App (e0, e1) ->
       (match eval context e0 with
        | Ok (Closure (ctx,
                       Lam (x, t, body))) ->
           eval (ctx @ context) (App (Lam (x,
                                           t,
                                           body),
                                      e1))
        | Ok _ -> Error "Can't apply non-Lam"
        | Error e -> Error (str ["Apply error: "
                                ;e]))
    | TLam (a, body) -> Ok (TLam (a, body))
    | TApp (TLam (a, body),
            given_typ) ->
       let new_context = (a, QuantifierBind) :: context in
       eval new_context body
    | TApp (e0, t) ->
       (match eval context e0 with
        | Ok (TLam (a, body)) ->
           let _ = failwith "Not gonna happen" in
           eval context (TApp (TLam (a, body), t))
        | Ok (Closure (ctx,
                       TLam (a,
                             body))) ->
           eval (ctx @ context) body
        | Ok _ -> Error "Can't type-apply non-Λ"
        | Error e ->
           Error (str [ "Error applying type lambda. Error: "
                      ; e]))
  
  (* helper functions *)
  let tlam a body = TLam (a, body)
  let lam x t body = Lam (x, t, body)
  let app e0 e1 = App (e0, e1)
  let tapp e0 tyT1 = TApp (e0, tyT1)
  
  (* eval [] (tlam "a" (lam "x"
   *                      (SymbolTy "a")
   *                      (Symbol "x"))) *)
  
  let k_combinator = (tlam "a" (tlam "_b"
                                  (lam
                                     "x"
                                     (SymbolTy "a")
                                     (lam
                                        "_y"
                                        (SymbolTy "_b")
                                        (Symbol "x")))))
  
  let k_intint = (TApp (TApp (k_combinator,
                              IntTy),
                        IntTy))
  
  (* DEAR HN READER: This is what is failing me. *)
  let applied_k = typ_of_expr [] (app k_intint (Int 1))