← back

Spring 2013 Problem 2

1 February 2016

Question

Why does this function only deal with ints instead of generic data types? The current method definition is as follows: val ith : int list -> int -> int -> int = <fun> how do I make it match val ith: 'a list -> int 0> 'a -> 'a = <fun>?

let rec ith l i d =
  match l with
  | [] -> d
  | h::t ->
    let f baseV elem = if baseV = 0 then elem else (baseV - 1) in
    let base = i in
    List.fold_left f base l;;

Answer

It inferred this type

val ith : int list -> int -> int -> int = <fun>

because of the following reasoning:

let rec ith l i d = match l with
| []-> d
| h::t -> List.fold_left (fun a x -> if a = 0 then x else a-1) i l;;
  1. Think of the function type as a bunch of unknowns:
l : 'a

i : 'b

d : 'c

res : 'd
  1. Now you match on l with list constructors, so you know l is a list. Plus, the first case returns d of type 'c, so the result type of the whole function is 'c
l : 'a list

i : 'b

d : 'c

res : 'c
  1. Next notice that you fold over the list, with accumulator i of type 'b. So 'b == 'c
l : 'a list

i : 'c

d : 'c

res : 'c
  1. The fold function can replace the accumulator with an element x of the list (first branch), so the list must contain elements of type 'c
l : 'c list

i : 'c

d : 'c

res : 'c
  1. Finally, note that the other branch of the fold function decrements the accumulator, therefore the accumulator (variable i, of type 'c) is an int. We have 'c == int.

[Alternatively notice that you compare the accumulator with 0, therefore it must be an int.]

l : int list

i : int

d : int

res : int

You can't have any other type if you write this function this way, because of how the type inference algorithm works.