Reading Samuel Mimram’s delightful Program = Proof, which introduced
me to OCaml’s funny dot syntax for pattern branches the compiler can
verify to be impossible. Apparently it was introduced in 4.07:
Mimram uses it to define an ex falso quodlibet inference rule:
# type void = |;;
type void = |
# let explosion : void -> 'a = fun impossible -> match impossible with _ -> .;;
val explosion : void -> 'a = <fun>
Fun! You can then use it for messing around with Curry-Howard-ed
propositional intuitionistic logic proofs in your toplevel, which, if
I’m being honest, is kind of addictive. Like a proof of rightward
material implication ((~A \/ B) -> (A -> B)), for instance:
# type ('a, 'b) right_material = (('a -> void), 'b) Either.t -> ('a -> 'b);;
type ('a, 'b) right_material = ('a -> void, 'b) Either.t -> 'a -> 'b
# let f : ('a, 'b) right_material = fun eith a -> match eith with Left not_a -> explosion (not_a a) | Right b -> b;;
val f : ('a, 'b) right_material = <fun>
But it also seems like you don’t need the dot to define an ex falso
quodlibet inference rule. For instance, you could do this instead:
# let explosion : void -> 'a = explosion;;
val explosion : void -> 'a = <fun>
So I guess I have two questions about the dot thing.
Does it let you do anything you couldn’t otherwise do? Or make
anything you might want to do easier? Any backstory on why it was
added to the language would be very interesting to hear.
Is it ever used for, like, normal computer programs that do stuff,
or is it mainly needed for this kind of Curry-Howard-y thing,
i.e. using the type system to help verify propositional
intuitionistic logic formulas?
You can see one use of it here: https://ocamlpro.com/blog/2017_04_01_ezsudoku (The blog post is a bit long, and the use of dot only comes at the end, but it also gives some context that you might find interesting).
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. 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. As you can guess, this is not very common.
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). A common alternative is to use universal quantification: type void = { v : 'a. 'a }.
Wow, that’s a really cool example! Thanks. It makes sense that type
inference involving GADTs would need a nudge now and again, since
GADTs introduce a lot of additional complexity into the type inference
process. I’ll have to play around with more toy examples to develop a
feel for how I’d use the dot in that context.
Re: alternate definitions of void, I used to do it in the following
somewhat Haskell-y way, like this:
# type void;;
type void
# let rec explosion : void -> 'a = fun impossible -> explosion impossible;;
val explosion : void -> 'a = <fun>
On the other hand, in OCaml, that syntax makes void into an abstract
type, which I guess could be problematic? For example, that might
theoretically let you fill void in later via the with type :=
… syntax, which seems bad?
another way to define an uninhabited type which a. only relies on gadts, and b. the compiler is still able to prove false is:
type (_, _) eq = Refl : ('a, 'a) eq
type void = (int, float) eq
if you’re using type void = { absurd : 'a. 'a }, the compiler can’t trim branches where it may appear.
and the problem with divergent computations is that they can prove anything, not just ex falso.
Haskell does have an empty cases syntax extension in which:
absurd :: Void -> a
absurd f = case f of {}
(FYI: fun x -> match x with C -> ... <-> function C -> ...)
The issue is more than an external function might create a value of this type void. And this is a common practice when binding with C libraries.
Concerning GADTs, the reason why a heuristic is needed is because checking the exhaustiveness of a pattern match is undecidable. Under the hood, refutation clauses (... -> .) 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.
In fact, refutable clause are always needed whenever type information is needed to refute some cases. However, when a pattern matching contains only one clause, the typechecker automatically adds a refutation clause by itself. Thus,
let f (None:void option) = ()
is the same thing as
let f: void option -> unit = function
| None -> ()
| _ -> .
As soon as a pattern matching contains more cases
type 'a ternary =
| No
| Nothing
| Just of 'a
one needs to add an explicit clause to avoid an exhaustiveness warning. For instance,
let none: void ternary -> unit = function
| No -> ()
| Nothing -> ()
emits
Warning 8 [partial-match]: this pattern-matching is not exhaustive.
Here is an example of a case that is not matched:
Just _
Consequently, my experience is that refutation clause are quite frequently needed when using GADTs since one of the most common use case is to restrict the set of valid values to make it a better approximation of the set of meaningful values.