Compiler basics: Lisp to Assembly (notes.eatonphil.com)

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 con...