在允许解构的同时保留不变量

Mik*_*uel 6 ocaml invariants pattern-matching

我想定义一个类型,以便所有构造都通过可以保留不变量的模块成员,但允许对模式匹配进行解构.

我只是学习OCaml但是以下几乎适用于一个带有不变量的int对,左边应该严格小于右边

module Range : sig
  type t = private { left:int; right:int }
  exception InvalidRange of (int*int)
  val make : int -> int -> t
end = struct
  type t = { left:int; right:int }
  exception InvalidRange of (int*int)
  let make left right = if left < right
    then { left; right }
    else raise (InvalidRange (left, right))
end
Run Code Online (Sandbox Code Playgroud)

这是有效的

# let p = Range.make 1 2;;
val p : Range.t = {Range.left = 1; Range.right = 2}
# let q = Range.make 2 1;;
Exception: Range.InvalidRange (2, 1).
Run Code Online (Sandbox Code Playgroud)

和时尚后的解构工作

# let {Range.left=x; Range.right=y} = p;;
val x : int = 1
val y : int = 2
Run Code Online (Sandbox Code Playgroud)

而构建失败

# let badp = {Range.left = 2; Range.right = 1};;
  let badp = {Range.left = 2; Range.right = 1};;
Error: Cannot create values of the private type Range.t
# open Range;;
# let badp = {left = 2; right=1};;
  let badp = {left = 2; right=1};;
Error: Cannot create values of the private type Range.t
Run Code Online (Sandbox Code Playgroud)

但我真正想做的是具有解构元组的语法方便性.以下不起作用:

module Range : sig
  type t = private int*int
  exception InvalidRange of (int*int)
  val make : int -> int -> t
end = struct
  type t = int*int
  exception InvalidRange of (int*int)
  let make left right = if left < right
    then (left, right)
    else raise (InvalidRange (left, right))
end
Run Code Online (Sandbox Code Playgroud)

但后来我无法使用元组模式对其进行解构:

# let r = Range.make 1 2 ;;
val r : Range.t = (1, 2)
# let (a, b) = r;;
  let (a, b) = r;;
Error: This expression has type Range.t
       but an expression was expected of type 'a * 'b
Run Code Online (Sandbox Code Playgroud)

我可以改变类型,type t = R of (int * int)但我需要这些尽可能轻量级记忆.有任何想法吗?

eso*_*ope 9

手册中所述,您需要明确强制:

# let (a, b) = (r :> int*int);;
val a : int = 1
val b : int = 2
Run Code Online (Sandbox Code Playgroud)

  • 1)透明类型,2)抽象类型,3a)私有变体或记录类型3b)私有类型缩写之间存在差异.因为1)强制可能是双向的,也是隐含的.2)根本不可能有任何强制.对于3a)强制是可能的一种方式,似乎是隐含的.对于3b)强制也是可能的一种方式,似乎是明确的.重要的是要注意强制没有计算内容(它们在运行时被擦除). (2认同)