4 ms·
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
by 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 agoYes, sorry I meant in the context of GADTs. Is it really full type erasure if that GADT information is passed aorund?
- octachron 5y agoNo 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 agoI 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.