Comment

Comment by 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`.

Discussion