There can be more to static semantics than type checking.
let bad_empty lst =
match lst with
| [] -> true
File "[1]", lines 2-3, characters 1-13: 2 | .match lst with 3 | | [] -> true Warning 8: this pattern-matching is not exhaustive. Here is an example of a case that is not matched: _::_
val bad_empty : 'a list -> bool = <fun>
See that warning? That's because we're missing anything match with a non empty list. What happens if our pattern doesn't match?
bad_empty [];;
- : bool = true
bad_empty [1; 2; 3;];;
Exception: Match_failure ("[1]", 2, 1).
Raised at bad_empty in file "[1]", line 2, characters 1-29
Called from Toploop.load_lambda in file "toplevel/toploop.ml", line 212, characters 17-27
Uh oh! That's a bad exception!
We can fix our empty function by making our matching exhaustive:
let better_empty lst =
match lst with
| [] -> true
| _ -> false;;
val better_empty : 'a list -> bool = <fun>
better_empty [1; 2; 3];;
- : bool = false
What about this code?
let rec bad_sum lst =
match lst with
| h :: t -> h + bad_sum t
| [x] -> x
| [] -> 0
File "[6]", line 4, characters 3-6:
4 | | [x] -> x
^^^
Warning 11: this match case is unused.
val bad_sum : int list -> int = <fun>
Our match case [x] is unused! But why? [x] can also be written as x :: [] (pronounced "x cons nils"), so it will always match the first pattern before the second.
bad_sum [1; 2; 3];;
- : int = 6
In this case, as shown above, our code still works, but it's ugly :(. We should fix this:
let rec better_sum lst =
match lst with
| h :: t -> h + better_sum t
| _ -> 0;;
val better_sum : int list -> int = <fun>
better_sum [1; 2; 3];;
- : int = 6
There! No error, and our code is prettier!
let rec another_bad_sum lst =
List.hd lst + another_bad_sum (List.tl lst);;
val another_bad_sum : int list -> int = <fun>
another_bad_sum [1; 2; 3];;
Exception: Failure "tl".
Raised at Stdlib.failwith in file "stdlib.ml", line 29, characters 17-33
Called from another_bad_sum in file "[10]", line 2, characters 31-44
Called from another_bad_sum in file "[10]", line 2, characters 15-44
Called from another_bad_sum in file "[10]", line 2, characters 15-44
Called from another_bad_sum in file "[10]", line 2, characters 15-44
Called from Toploop.load_lambda in file "toplevel/toploop.ml", line 212, characters 17-27
What's happening here? Well, the functions List.hd and List.tl return the head and tail of a list; however, there's no head and tail of an empty list so these functions throw an exception. Here, the programmer forgets that the list might be empty. This is why it's dangerous to use List.hd and List.tl, and better as a practice to use pattern matching.
Static checking helps us write better code.
The OCaml compiler checks for, in addition to type correctness,
This is another example of static semantics.
Do not ignore these warnings The compiler is finding errors for you and giving you a chance to fix them!