Function type inference with recursive calls
f#, type-inference
Solution
F# type checker uses Damas-Hindley-Milner type inference algorithm. The factorial example can be explained roughly as follows:
From declaration of `fact`, we have its type in the form `tx -> ty` and `tx = t(i)` where `t(i)` is type of a value `i`.
From the equality check, because of `val (=): 'T -> 'T -> bool` we also have `t(i) = t(0) = int`.
- From `then` branch, we get another constraint `ty = t(1) = int`.
- From `else` branch, the normal `(*)` operator is `'T -> 'T -> 'T` so we get `t(i) = ty`.
Based on the set of constraints:
tx = t(i)
t(i) = t(0) = int
ty = t(1) = int
t(i) = ty
using unification, we arrive at `tx = ty = int` and infer type of `fact` as `int -> int`. It also means that if you change the order of clauses in `if/then/else` (by reversing conditions), type inference still works fine.
That said, this is a very simple example of the type inference algorithm. You can follow the Wikipedia link above to read more about it.
In order to apply the algorithm to your custom language, you can find an implementation in various functional programming books. Please see this thread Damas-Hindley-Milner type inference algorithm implementation for more details.
Problem
I'm trying to implement a custom language that allows function return type to be inferred from its last statement. However, when a direct or indirect recursive function call is found, the type inference system obviously fails. ``` func factorial(a:int) -> if a == 0 1 else a * factorial(a - 1) ``` For example, F# does this even with argument types unspecified: ``` let rec fact i = if i = 0 then 1 else i * fact (i-1) ``` How does this system work?