How about recursive function?

[rhysd]

Hi, thank you for interesting implementations.

These type systems are implemented for tiny language. It contains Var, Call, Fun and Let expressions. While reading your algorithm_w implementation, I noticed that they lack important functional programming feature: recursive functions.

For recursive functions, type inference sometimes needs to care about them. Before applying type inference, type variable for the function should be added to type environment because function body may contain applying itself (recursive call).

For example, assume let rec exists and let's say to write let rec f x = f 10; 42 in f true. When visiting the LetRec node, inferrer makes type variable for f to type environment before apply type analysis to function body f 10; 42 for recursive function call. And then applies type inference to f 10. In function body, the type of f is determined to int -> int. This works for monomorphic function. But in this case, f is a polymorphic function 'a -> int. But function type is determined before generalized. Hence f true will fail after because of int -> int type. I feel some trick is necessary to support recursive function. What do you think about this?

[tomprimozic]

Hey, sorry I missed this. Let me split this in two points.

(1) As far as I'm aware, typing recursive functions is quite simple - you just apply a fixed point operator fix : forall [a] (a -> a) -> a. For example, to type let rec fac n = if n == 0 then 1 else n * f (n - 1), you transform the code (the parser could do this automatically, as syntax sugar) into

let fac' fac_rec n = if n == 0 then 1 else n * fac_rec (n - 1)

which can be inferred to have the type fac' : (int -> int) -> int -> int. You then define let fac = fix fac', which can again be inferred to have the type fac : int -> int. You don't need to actually implement fix - you just need it to infer the type of fac, but you can still compile it normally.

(2) Polymorphic recursion is a different beast. I don't think that any language implements it, it might even be unsound, and in any case it's more likely to be a programming error than not. But it's probably possible to typecheck it using first-class polymorphism algorithm...

[lpil]

(2) Polymorphic recursion is a different beast. I don't think that any language implements it

I recall SJP saying at this year's Haskell eXchange that Haskell implements polymorphic recursion.