Type inferencing help in OCaml

Question

How would I proceed with proving these two functions are well typed? I am a bit lost with this question.

  let rec reduce f lst u =
     match lst with
     | [] -> u
     | (h::t) -> f h (reduce f t u) 

 let rec forall2 p l1 l2 =
     match (l1,l2) with
     | ([],[]) -> true
     | ([],_) -> false
     | (_,[]) -> false
     | ((h1::t1),(h2::t2)) ->
          (p h1 h2) && (forall2 p t1 t2)

Answer 1

I won't give a fully-fledged solution since the question looks like an assignment.

To do the type-inference yourself, all you have to do is look at the source and make deductions. Then, from your deductions, deduce more and more types until all types are known, or until you've found a discrepancy.

To get you started:

• In reduce, you're pattern-matching lst against patterns of type 'a list. Thus, lst must be typed as 'a list.
• The values after each pattern must have the same type, so u has the same type as f h (reduce f t u).

Et cætera, et cætera...