Compiler basics: Lisp to Assembly
Hi Hacker News PL enthusiasts. This is off topic, but I hope you will have mercy on me.<p>I&#x27;m reaching out for some help from you. I&#x27;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&#x27;m writing a couple of interpreters every week, trying out new ideas. But there is one hurdle I&#x27;ve been unable to overcome for a long time.<p>I&#x27;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&#x27;ve been stuck at this point for months. Have read all I can find on the internet, and have read TAPL many times.<p>Am honestly feeling really stupid for not having been able to complete this.<p>What I&#x27;m struggling with beta reducing expressions that are type lambdas (i.e. the expression related to `Forall`).<p>Λ means type lambda, i.e. the set of expressions indexed by type<p>λ means expression lambda, i.e. the set of expressions indexed by expression<p>E.g. Λa.λx:a.x is the polymorphic &quot;identity&quot; function, which in javascript looks like `x =&gt; x`<p>k = ΛA.ΛB.λx:A.λy:B.x<p>k_intint = ((k IntTy) IntTy)<p>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.<p>I&#x27;ll paste the source code of my latest attempt below, the function in question is `typ_of_expression`. I&#x27;ve written this in OCaml, but would be very thankful for a response in any language, or pseudocode, or just explained in English.<p>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&#x27;d be happy to pay €100 for any help that lets me solve this (SEPA, Bitcoin).<p><pre><code>  (* λ calculus, with Forall and simple types *)
  type &#x27;a binding =
    | SymBind of &#x27;a
    | QuantifierBind

  type &#x27;a context = (string * &#x27;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&#x2F;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&#x2F;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
    | [] -&gt; Error &quot;No result&quot;
    | (k, QuantifierBind) :: rest -&gt; lookup rest key
    | (k, SymBind v) :: rest -&gt; if key = k
                                then Ok v
                                else lookup rest key
  
  let str = String.concat &quot;&quot;
  
  let rec string_of_typ t = match t with
    | UnitTy -&gt; &quot;UnitTy&quot;
    | IntTy -&gt; &quot;IntTy&quot;
    | Arrow _ -&gt; &quot;Arrow&quot;
    | Forall (s, t) -&gt; str [&quot;Forall &quot;; s; &quot; &quot;; string_of_typ t]
    | ClosureTy (_ctx, t) -&gt; str [&quot;Closure &quot;; string_of_typ t]
    | SymbolTy s -&gt; str [&quot;SymbolTy &quot;; s]
  
  let string_of_expr e = match e with
    | Unit -&gt; &quot;Unit&quot;
    | Closure _ -&gt; &quot;Closure&quot;
    | Symbol s -&gt; str [&quot;Symbol &quot;; s]
    | Int i -&gt; str [&quot;Int &quot;; string_of_int i]
    | Lam _ -&gt; &quot;Lam&quot;
    | App _ -&gt; &quot;App&quot;
    | TLam _ -&gt; &quot;TLam&quot;
    | TApp _ -&gt; &quot;TApp&quot;
  
  (* 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
    | [] -&gt; acc
    | (x, QuantifierBind) :: rest -&gt;
       convert_context rest ((x, QuantifierBind) :: acc)
    | (x, SymBind e) :: rest -&gt;
       (match converter_fn original_context e with
        | Ok t -&gt; convert_context rest ((x, SymBind t) :: acc)
        | Error e -&gt; failwith (str [&quot;typ_context error: &quot;; e]))
  
  let rec typ_of_expr context e =
    match e with
    | Unit -&gt; Ok UnitTy
    | Int i -&gt; Ok IntTy
    | Closure (ctx, e) -&gt;
       let new_context = convert_context typ_of_expr context ct  x context in
       typ_of_expr new_context e
    | Symbol s -&gt; lookup context s
    | Lam (x, in_typ, body) -&gt;
       (let new_context = (x, SymBind in_typ) :: context in
        match typ_of_expr new_context body with
        | Ok return_typ -&gt; Ok (Arrow (in_typ, return_typ))
        | Error e -&gt; Error (str [ &quot;Error finding return type of   lambda. Error: &quot;
                                ; e]))
    | App (e0,
           e1) -&gt;
       (match (typ_of_expr context e0,
               typ_of_expr context e1) with
        | (Ok (Arrow (t0_0, t0_1)),
           Ok t1) -&gt; if t1 = t0_0
                     then Ok t0_1
                     else Error (str [&quot;Type mismatch&quot;])
        | (Ok (ClosureTy (ctx, Arrow (t0_0, t0_1))),
           Ok t1) -&gt; if t1 = t0_0
                     then Ok t0_1
                     else Error
                            (str
                               [&quot;Type mismatch. t0_0: &quot;
                               ;string_of_typ t0_0
                               ;&quot;, t0_1: &quot;
                               ;string_of_typ t0_1
                               ;&quot;, t1: &quot;
                               ;string_of_typ t1
                            ])
        | (Ok t, _) -&gt; Error (str [&quot;Not given a lambda as first   thing to App. &quot;
                                  ;string_of_typ t])
        | _ -&gt; Error (str [&quot;Error getting typ of expr App&quot;]))
    | TLam (a, body) -&gt;
       (let new_context = (a, QuantifierBind) :: context in
        match typ_of_expr new_context body with
        | Ok body_type -&gt; Ok (ClosureTy (new_context,
                                         Forall (a,
                                                 body_type)))
        | Error e -&gt; Error (str [ &quot;Failed to get typ of TLam, a  nd thus can not construct Forall. Error: &quot;
                                ; e]))
    | TApp (TLam (a, body),
            t1) -&gt; let new_context = (a, QuantifierBind) :: con  text in
                   typ_of_expr new_context body
    | TApp (e0, t1) -&gt;
       (match typ_of_expr context e0 with
        | Ok (ClosureTy (ctx,
                         Forall (a, body))) -&gt;
           let new_context = (a, SymBind t1) :: ctx @ context i  n
           Ok (ClosureTy (new_context,
                          body))
        | Ok (ClosureTy(ctx,
                        t)) -&gt;
           Error (str [&quot;TApp given ClosureTy with non-forall on   left-hand-side. IS: &quot;
                      ;string_of_typ t])
        | Ok (Forall (a, body)) -&gt; Error &quot;TApp given naked Fora  ll as first argument&quot;
        | Ok _ -&gt; Error &quot;TApp given non-Forall first argument&quot;
        | Error e -&gt; Error (str [&quot;Error in TApp - error: &quot;
                                ;e]))
  
  let rec eval context e =
    let context: (expr context) = context in
    match e with
    | Unit -&gt; Ok Unit
    | Closure (ctx, e) -&gt; eval (List.append ctx context) e
    | Int i -&gt; Ok (Int i)
    | Lam (x, t, body) -&gt; Ok (Closure (context,
                                       Lam (x, t, body)))
    | Symbol s -&gt; lookup context s
    | App (Closure(ctx,
                   Lam (x, t, body)),
           e1) -&gt;
       let new_context = (x, SymBind e1) :: ctx @ context in
       eval new_context body
    | App (e0, e1) -&gt;
       (match eval context e0 with
        | Ok (Closure (ctx,
                       Lam (x, t, body))) -&gt;
           eval (ctx @ context) (App (Lam (x,
                                           t,
                                           body),
                                      e1))
        | Ok _ -&gt; Error &quot;Can&#x27;t apply non-Lam&quot;
        | Error e -&gt; Error (str [&quot;Apply error: &quot;
                                ;e]))
    | TLam (a, body) -&gt; Ok (TLam (a, body))
    | TApp (TLam (a, body),
            given_typ) -&gt;
       let new_context = (a, QuantifierBind) :: context in
       eval new_context body
    | TApp (e0, t) -&gt;
       (match eval context e0 with
        | Ok (TLam (a, body)) -&gt;
           let _ = failwith &quot;Not gonna happen&quot; in
           eval context (TApp (TLam (a, body), t))
        | Ok (Closure (ctx,
                       TLam (a,
                             body))) -&gt;
           eval (ctx @ context) body
        | Ok _ -&gt; Error &quot;Can&#x27;t type-apply non-Λ&quot;
        | Error e -&gt;
           Error (str [ &quot;Error applying type lambda. Error: &quot;
                      ; 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 &quot;a&quot; (lam &quot;x&quot;
   *                      (SymbolTy &quot;a&quot;)
   *                      (Symbol &quot;x&quot;))) *)
  
  let k_combinator = (tlam &quot;a&quot; (tlam &quot;_b&quot;
                                  (lam
                                     &quot;x&quot;
                                     (SymbolTy &quot;a&quot;)
                                     (lam
                                        &quot;_y&quot;
                                        (SymbolTy &quot;_b&quot;)
                                        (Symbol &quot;x&quot;)))))
  
  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))</code></pre>