But both triggers warning 8 (non-exhaustive pattern matching). It prevents me from using let matching as I don’t like having warnings in a finished code, so I go for a match ... with ... | _ -> assert false.
The warning seems irrelevant to me in the first case, since I tend to use let matching when I am certain it won’t go wrong. And in practice, since let matching can contain only one pattern, it is impossible to make let matching exhaustive.
I know that in Haskell there is no warning on incomplete let matching. Why not do the same in OCaml? Unless there are difficulties I’m not seeing.
If you have a proof that f x only returns a list of two elements, it seems better to state this proof in the type system by making f x returns a 2-tuple. If you don’t have such a proof, then it seems a good idea to make it explicit that this is only an assumption by expanding the pattern to match ... with ... | _ -> assert false with an explanation of the underlying assumption.
The warning seems irrelevant to me in the first case, since I tend to use let matching when I am certain it won’t go wrong.
The point is that humans makes mistake, and the typechecker is here to help to avoid some of them. In fact, I would rather make warning 8 a error than disable it on let-binding.
since let matching can contain only one pattern, it is impossible to make let matching exhaustive.
It is perfectly possible to have exhaustive pattern in let pattern, even if it mostly happens with tuple pattern.
For me such pattern seems mostly convenient when applying the same function (or a composition of functions) to multiple values of the same type and then binding the results to different variable names. Tuples don’t work well here as there has to be a distinct mapping function for each tuple size. I use the following trick:
module F_list = struct
type ('a, 'b) t =
| [] : ('a, [`Z]) t
| (::) : 'a * ('a, [< `Z | `S of _] as 'b) t -> ('a, [`S of 'b]) t
module T = struct
type ('a, 'b) f_list = ('a, 'b) t =
| [] : ('a, [`Z]) f_list
| (::) : 'a * ('a, [< `Z | `S of _] as 'b) t -> ('a, [`S of 'b]) f_list
end
let rec map : type a. _ -> (_, a) t -> (_, a) t = fun f ->
function
| [] -> []
| x :: xs -> f x :: map f xs
end;;
open F_list.T;;
let [c0; c1; c2; c8] =
F_list.map (fun n -> Some (`Const (string_of_int n))) [0; 1; 2; 8];;
No warning here since there’s a proof that the lengths of the lists match (due to GADT exhaustiveness).
Out of sheer curiosity, do you happen to know if there’s any significant run-time overhead in using this method to construct lists - ie can I reasonably have a list of 2000 elements encoded like this?
These GADTs-enhanced lists are exactly the same thing as classical lists at the runtime level. Standard lists could be defined with
type 'a list =
| []
| ( :: ) of 'a * 'a list
Contrarily, having an integer as big as 2000 encoded in unary in the type system will visibly slow down the typechecker. For instance, in a program that merely create such a list
type ('a,'e) t =
| []: ('a,'a) t
| (::): 'a * ('b,'c) t -> ('a * 'b, 'c) t
let rec ( @ ): type a b c. (a,b) t -> (b,c) t -> (a,c) t = fun x y ->
match x with
| a :: q -> a :: ( q @ y )
| [] -> y
let ( $ ) x y = fun () -> x () @ y ()
let x = [1; "two"; 3.; ()] (* 4 *)
let y () = x @ x @ x @ x (* 16 *)
let z () = (y $ y $ y $ y) () (* 64 *)
let w () = (z $ z $ z $ z) () (* 256 *)
let a () = (w $ w $ w $ w) () (* 1024 *)
let b () = ( a $ a $ a $ a) () (* 4096 *)
typechecking starts to dominate the compilation time; and the typechecker even segfaults with really large unary type-level integers.
Back in the Camlp4 days I wrote a pa_refutable syntax extension that allows one to write let refutable p = ... and not have a warning even when p is refutable. OCaml 3.10!
I think that a ppx transforming let[@admit] or let[@refutable] to an [@warning "-8"] attribute on the let-binding and a [@warning "+8"] on the body would be even simpler.
It is generally possible to increase the stack size to push the typechecker a little further, but the typechecker is not really designed to be well behaved for programs of which the type size grows exponentially with the code size. In those case, both time and space complexity tends to become problematic