ocaml, ability to trigger compile error on value change

user_2936110 0
Viewed 45

I'd like to express, in a compile time way, that my code operates under the assumption of a value being a certain constant. For simplicity, let's say I have this module

module Lib : sig
  type t = A|B|C|D
  val default : t
  val f : t option -> unit
end = struct
  type t = A|B|C|D
  let default = B
  let f _ = ()
end

And I write code outside of Lib and want to assert in a compile time way, that I need the default to be B. Meaning that I want a compile error when Lib.default is different from B, in that case I want to review if my code is good with the differet value. This way I wouldn't have to read release notes of the lib, the compiler would call me back.

I have some control over Lib, so I can change it if needed. I'm interested in other ways of structuring it if that makes this compile time assertion easier let alone possible.

I have other parts of the code which doesn't depend on this, eg

let config : Lib.t option =
  match Lib.default with
  | A
  | B
  | C -> None
  | D -> Some C

I was thinking about doing subtypes, like in

type t = [`A|`B|`C|`D]
val default : [`B]

but then I drop the info that default might change to other constructors of t, and then this would compile error saying that matching A is impossible.

let config : Lib.t option =
  match Lib.default with
  | `A
  | `B
  | `C -> None
  | `D -> Some `C

Thanks

compile-time ocaml type-safety
1 Answers

The subtypes might be a solution, though I have to admit that I didn't get the full understanding of what you want. But later on it, let's first embrace polymorphic variants and subtyping. Your attempt is not using subtypes yet, as there is no polymorphism in your type, i.e., type t = ['A|'B|'C|'D]1 is a ground type. What we need is the following,

module Lib : sig
  type 'a t = [< `A|`B|`C|`D] as 'a
  val default : [ `B] t
  val f : 'a t option -> unit
end = struct
  type 'a t = [< `A|`B|`C|`D] as 'a
  let default = `B
  let f _ = ()
end

So we say that 'a Lib.t is a family of types, and a value of type 'a t could be ['A] or 'B or ['A|'B] or ['A|'B|'C] or ... with the [A|B|C|D] being the top type, aka the supertype.

With the default type we have options, we can post that it has type ['B] t, which is the same as ['B], but indicates more clearly that it is a part of a hierarchy, so the users should expect it to change to any other type. From the type system perspective, it doesn't matter, because the OCaml type system is not nominal but structural.

This solution will give you a type error here,

let config : _ Lib.t option =
  match Lib.default with
  | `A  (* default is not polymorphic and can be only `B *)
  | `B
  | `C -> None
  | `D -> Some `C

since we clearly stated that default is B and only B.

Alternatively, we can say that default could be [> 'B], i.e., that it is a polymorphic type that at least is B but could be anything else. With this solution, you will not get any errors in the config function. You will not either get any errors if you will change from [> 'B] to [> 'A], for example. So it is probably not what you're looking for, so let's go back and use the monomorphic ['B] type for the default and try to deal with it on the user side. We can explicitly say, that we want to upcast the ground default to the all possible values, e.g.,

module Lib : sig
  type 'a t = [< `A|`B|`C|`D] as 'a
  val default : [`B] t
  val f : 'a t option -> unit
end = struct
  type 'a t = [< `A|`B|`C|`D] as 'a
  let default = `B
  let f _ = ()
end

let config : _ Lib.t option =
  match (Lib.default : [`B] Lib.t :> [> `B] Lib.t) with
  | `A
  | `B
  | `C -> None
  | `D -> Some `C

Now, if we change the default to A, we will have the desired type error. The only caveat is that we need to specify the currently verified default at every use case, so let's move it to the Lib instead, e.g.,

module Lib : sig
  type 'a t = [< `A|`B|`C|`D] as 'a
  type verified = [`B]
  val default : [`B] t
  val f : 'a t option -> unit
end = struct
  type 'a t = [< `A|`B|`C|`D] as 'a
  type verified = [`B] t
  let default = `B
  let f _ = ()
end

open Lib
let config : _ Lib.t option =
  match (default : verified t :> [> verified ] t) with
  | `A
  | `B
  | `C -> None
  | `D -> Some `C

So now, when you would like to try a new default value, you change the type of default (and the value of course) but do not change the verified type and go through all use-cases until you're ready to add the newly added type to the verified set. Yes, set, because we can upgrade the verified type to accept a set of variants, e.g.,

module Lib : sig
  type 'a t = [< `A|`B|`C|`D] as 'a
  type verified = [`A |`B]
  val default : [`B] t
  val f : 'a t option -> unit
end = struct
  type 'a t = [< `A|`B|`C|`D] as 'a
  type verified = [`A|`B] t
  let default = `B
  let f _ = ()
end

open Lib
let config : _ Lib.t option =
  match (default : [< verified] t :> [> verified ] t) with
  | `A
  | `B
  | `C -> None
  | `D -> Some `C

So now, we will get an error if Lib.default has any variant other than A or B. And as a bonus, you don't need to change anything on the use site.

And as the final refinement, I would suggest to get rid of nominal (in all senses of the word) 'a t type and just have to polymorphic types, one for the blessed set of verified constructors and another for the set of all possible constructors, e.g.,

module Lib : sig
  type 'a default = [> `A|`B|`C|`D] as 'a
  type 'a verified = [< `A |`B] as 'a
  val default : [`B]
  val f : 'a default option -> unit
end = struct
  type 'a default = [> `A|`B|`C|`D] as 'a
  type 'a verified = [< `A|`B] as 'a
  let default = `B
  let f _ = ()
end

open Lib
let config : _ option =
  match (default : _ verified :> _ default) with
  | `A
  | `B
  | `C -> None
  | `D -> Some `C

or

let config : 'b option =
  match (default : 'a verified :> 'b default) with
  | `A
  | `B
  | `C -> None
  | `D -> Some `C

1)) forgive me the wrong backticks, the right one do not play nice with SO markup

user_26254420
Related