[AnaniasAnanas]

> λ calculus, with Forall and simple types

Just fyi, this is called System F.

I do not remember any OCaml and I get an error when trying to run it (File "./test.ml", line 123, characters 6-7: Error: Syntax error: operator expected.) so I do not know if I can be of much help. What is the result of typ_of_expr [] (app k_intint (Int 1))? I presume that you expect it to be IntTy -> IntTy, right?

[eiurafhlfie]

Thanks for your reply.

It is indeed system F I'm trying to implement :-)

My formatting for HN seems to have screwed the program up. You'll find the contents of systemf.ml in this paste: https://pastebin.com/gw20LBNR

Here is the result from my OCaml repl:

  # typ_of_expr [] (app k_intint (Int 1));;
  - : (typ, string) result =
  Error "Type mismatch. t0_0: SymbolTy a, t0_1: Arrow, t1: IntTy"

You are correct about what `(k_intint (Int 1))` should be. I hope for `k_intint` to be `IntTy -> IntTy -> IntTy`.

[AnaniasAnanas]

I am pretty sure that the type variable is not binded properly (when type checking App on the part where it says "(Ok (ClosureTy (ctx, Arrow (t0_0, t0_1)))," I get a symbol for t1, you are doing t1 = t0_0 which would be false in any case but the thing is that even when I use lookup in the enviroment I do not find said symbol). I would suggest instead of having closures to replace every occurrence of the type variable (or any variable really) during evaluation. So if you have something like ((\Lambda t (\lambda x t x)) int) to evaluate it into (\lambda x int x) directly instead of (\lambda x (sym "t") x) + a separate environment thing. I can give you my System F implementation in haskell that uses this method if you want.