Where/how is never_returns defined?

Learning
1

Hi, noob here

  • how does one generally define an uninhabited type like never_returns?
  • where is never_returns itself defined?

Searching online and on github did not help…

1 Like
2

I assume you’re referring to Core.never_returns? It is defined as an empty variant type:

type t = |

https://github.com/janestreet/core_kernel/blob/master/src/never_returns.ml shows the definition of never_returns, which is an alias to Nothing.t: https://github.com/janestreet/core_kernel/blob/master/src/nothing.mli.

Trivia: before the introduction of empty variant types, Nothing.t used to be defined as a (unit, int) Type_equal.t, which can be made uninhabitable using GADT features:

1 Like
3

Thx a bunch @bcc32! Nice avatar :wink:

If I can pick your brain a bit more, how do I read

type t = |
val unreachable_code : t -> _

or for that matter the older version of

 let unreachable_code = function
      | (_ : t) -> .
    ;;

this underscore and this dot… what do they even mean?..

compiler figures out the type is uninhabited and they are just some kind of placeholders? but why two of them? _ and . ?

…and finally was it some sort of a convention in old times to use ;; in .ml files? These days I understand ;; are only used in interactive top level?..

4

The underscore and dot are called a refutation case. It basically asks the compiler to check that the pattern cannot be inhabited.

;; is still common in ml files, but they are optional. One advantage is that they prevent a trailing ; from producing a syntax error very far away from where the fix needs to be:

let f x =
  <many lines of code>;
  last statement;

let g x =
  <many more lines of code>

let h x =
^ syntax error reported here
2 Likes
5

ahh… finally got it… nothing.mli says

val unreachable_code : t -> _

while nothing.ml says

let unreachable_code = function
  | (_ : t) -> .
;;

and the resulting type of unreachable_code according to utop is

Core.Nothing.t -> 'a

So that _ in .mli seems to indicate that it can be any type… There probably is a clever name for such use of _ and one day I’ll find it :slight_smile: