これはML Advent Calendar 2020 11日目の記事です。
OCamlでUninhabited type（値の存在しない型）を書くための方法をいくつか紹介します。
空のバリアント型を使う
現在書くならいちばん素直な方法。
type void = |
refutation caseを使うと absurd 関数が書ける。
let absurd : void -> 'a = function _ -> .
ちなみに空の多相バリアント型は書けない。間違って下のように書くと、 [] という唯一のデータコンストラクタを持つ void 型が定義されてしまう（OCaml 4.03.0 から [] と (::) をユーザー定義型のコンストラクタとして使えるようになった）。
type void = []
GADTを使う
GADTで型の等価性述語をつくり、それでありえない等価性を表現しようとする。
type (_, _) eq = Eq : ('a, 'a) eq
type void = (int, string) eq
型チェッカーは int ≠ string なことを知っているので refutation case で納得してくれる。
let absurd : void -> 'a = function _ -> .
レコードの多相フィールドを使う
∀a. a で⊥を表現するやつ。
type void = { v : 'a. 'a }
let absurd x = x.v
🙅♂️type void = Void of void
実は let rec でふつうに値が作れてしまう（リファレンスマニュアルの 8.1 Recursive definitions of values の節を参照）。
type void = Void of void
let rec absurd (Void x) = absurd x
let rec void = Void void
レコードの多相フィールドの場合は、同じことをすると（当然）型エラーになる。
let rec void = {v = void}
(*
Line 1, characters 20-24:
Error: This field value has type 'b which is less general than 'a. 'a
*)
🙅♂️type void
type void
type void は一見よさそうだが、OCaml的には型定義の実体をシグネチャで隠蔽した場合と区別できない。Standard MLのようにdatatype宣言が分かれていればどうにかなったのだろうが。
おまけ: Haskellの場合
Haskell 2010からdata宣言の右辺が必須でなくなったので data Void でよい。
data Void
absurd :: Void -> a
absurd a = case a of {}