However, when a pattern matching contains only one clause, the typechecker automatically adds a refutation clause by itself. In fact, refutable clause are always needed whenever type information is needed to refute some cases. ) are granting fuel to the exhaustiveness pattern checker to let it try harder when proving that the remaining syntactically correct cases are not well-typed. And this is a common practice when binding with C libraries.Ĭoncerning GADTs, the reason why a heuristic is needed is because checking the exhaustiveness of a pattern match is undecidable. The issue is more than an external function might create a value of this type void. A common alternative is to use universal quantification: type void =. Note that OCaml has a number of different ways to write empty types the empty variant is one of them, but since empty pattern matchings are syntacticaly forbidden in OCaml it wasn’t convenient to use before the addition of the dot syntax (the type definition itself wasn’t allowed before 4.07 anyway, but you could work around that using polymorphic variants). As you can guess, this is not very common. The use of the dot syntax (unreachable branch) nudges the type-checker into spending more time trying to prove that the branch is indeed dead. Its main use is for pattern matches involving GADTs, where one or several inputs are impossible but the type checker can’t prove it using its default heuristics. using the type system to help verify propositional ![]() ![]() Or is it mainly needed for this kind of Curry-Howard-y thing, Is it ever used for, like, normal computer programs that do stuff, So I guess I have two questions about the dot thing.ĭoes it let you do anything you couldn’t otherwise do? Or makeĪnything you might want to do easier? Any backstory on why it wasĪdded to the language would be very interesting to hear. For instance, you could do this instead: # let explosion : void -> 'a = explosion # let f : ('a, 'b) right_material = fun eith a -> match eith with Left not_a -> explosion (not_a a) | Right b -> b īut it also seems like you don’t need the dot to define an ex falso Type ('a, 'b) right_material = ('a -> void, 'b) Either.t -> 'a -> 'b Material implication ((~A / B) -> (A -> B)), for instance: # type ('a, 'b) right_material = (('a -> void), 'b) Either.t -> ('a -> 'b) Propositional intuitionistic logic proofs in your toplevel, which, if ![]() įun! You can then use it for messing around with Curry-Howard-ed # let explosion : void -> 'a = fun impossible -> match impossible with _ ->. Mimram uses it to define an ex falso quodlibet inference rule: # type void = | Me to OCaml’s funny dot syntax for pattern branches the compiler can Reading Samuel Mimram’s delightful Program = Proof, which introduced
0 Comments
Leave a Reply. |