3 ms·
> λ 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 "./te
by AnaniasAnanas 8y ago
> λ 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 8y agoThanks 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 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 8y agoI 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.