4 ms·

Non-exhaustive matches are always detected statically in OCaml. However, such matches are considered valid code: "non-exhaustive match" is a warning by default

Non-exhaustive matches are always detected statically in OCaml. However, such matches are considered valid code: "non-exhaustive match" is a warning by default, even if most people advise to turn that warning into an error. In other words, the `Match_failure` exception is part of OCaml non-typed semantics and there is no soundness issue involved here.

whimsicalism 5y ago
But how is Match_failure detected at runtime unless type information is passed around?
- octachron 5y ago
  There is no type information at runtime at all in OCaml. Once the program has been typed, the program is translated into an untyped lambda-calculus and all type information is throw away. In particular, pattern matching is compiled into this untyped lambda-calculus using if/then/else (and switch statement, and exception and exceptions handlers, ...). The type system is sufficient to detect before this compilation if the pattern is total or if it need to add a failure case. In this case, the `Match_failure` is just a catch-all term in this conditional expression. For instance let f x = match x with | [] -> () is translated into (is_empty/267 = (function x/269 : int (if x/269 (raise (makeblock 0 (global Match_failure/18!) [0: "r.ml" 1 17])) 1))) where you can see the exception being build and raised in the `then` branch of the test. Contrarily, the total function let is_empty x = match x with | [] -> true | _ :: _ -> false becomes (let (is_empty/267 = (function x/269 : int (if x/269 0 1))) And since the function doesn't need to handle the failure case, it doesn't have that `(raise ...)` case. Another important point is that type system information is only needed to check the exhautiveness of pattern matching in presence of GADTs. Otherwise the exhautiveness of pattern matching can be checked using syntatic criteria on the pattern matching and type definitions.
  - whimsicalism 5y ago
    Yes, sorry I meant in the context of GADTs. Is it really full type erasure if that GADT information is passed aorund?
    - octachron 5y ago
      No type information is ever passed to a compilation phase lower than the typechecker in the OCaml compiler pipeline. In the GADTs case, the type system is only used to remove the failure branch. For instance, type 'a t = A: int t | B: float t let always_a (x:int t) = match x with | A -> () | _ -> . is translated to (let (always_a/270 = (function x/272[int] : int 0)) because the typechecker can prove that the `B` case is impossible. In other words, GADTs are yet another instance where the type system can be used to eliminate dead code in the untyped IR.
      - whimsicalism 5y ago
        I see, so you can never really get a match_failure due to type level mismatch with GADT because it would be caught by the compiler. Makes sense to me.

whimsicalism 5y ago

But how is Match_failure detected at runtime unless type information is passed around?

octachron 5y ago
There is no type information at runtime at all in OCaml. Once the program has been typed, the program is translated into an untyped lambda-calculus and all type information is throw away. In particular, pattern matching is compiled into this untyped lambda-calculus using if/then/else (and switch statement, and exception and exceptions handlers, ...). The type system is sufficient to detect before this compilation if the pattern is total or if it need to add a failure case. In this case, the `Match_failure` is just a catch-all term in this conditional expression. For instance let f x = match x with | [] -> () is translated into (is_empty/267 = (function x/269 : int (if x/269 (raise (makeblock 0 (global Match_failure/18!) [0: "r.ml" 1 17])) 1))) where you can see the exception being build and raised in the `then` branch of the test. Contrarily, the total function let is_empty x = match x with | [] -> true | _ :: _ -> false becomes (let (is_empty/267 = (function x/269 : int (if x/269 0 1))) And since the function doesn't need to handle the failure case, it doesn't have that `(raise ...)` case. Another important point is that type system information is only needed to check the exhautiveness of pattern matching in presence of GADTs. Otherwise the exhautiveness of pattern matching can be checked using syntatic criteria on the pattern matching and type definitions.
- whimsicalism 5y ago
  Yes, sorry I meant in the context of GADTs. Is it really full type erasure if that GADT information is passed aorund?
  - octachron 5y ago
    No type information is ever passed to a compilation phase lower than the typechecker in the OCaml compiler pipeline. In the GADTs case, the type system is only used to remove the failure branch. For instance, type 'a t = A: int t | B: float t let always_a (x:int t) = match x with | A -> () | _ -> . is translated to (let (always_a/270 = (function x/272[int] : int 0)) because the typechecker can prove that the `B` case is impossible. In other words, GADTs are yet another instance where the type system can be used to eliminate dead code in the untyped IR.
    - whimsicalism 5y ago
      I see, so you can never really get a match_failure due to type level mismatch with GADT because it would be caught by the compiler. Makes sense to me.