在Scala中使用GADT进行穷举检查的简洁方法？

ryoqjall 于 2023-03-08 发布在 Scala

关注(0)|答案(1)|浏览(137)

我在寻找与下面的OCaml代码相同的行为，其中编译器理解匹配是穷举的，因为我们已经表示了两个scuteine必须具有相同的类型：

type circle
type rectangle

type _ figure =
    | Circle : int -> circle figure
    | Rectangle : int * int -> rectangle figure

let equal_figure : type a. a figure -> a figure -> bool = fun f1 f2 -> match (f1, f2) with
| Circle r1, Circle r2 -> Int.(r1 = r2)
| Rectangle (x1, y1), Rectangle (x2, y2) -> Int.(x1 = x2 && y1 = y2)
(* the compiler knows this match is exhaustive *)

我可以将这个例子直接移植到Scala，穷举检查器会做正确的事情：

sealed trait CircleMarker
sealed trait RectangleMarker

enum Fig[T]:
  case Circle(r: Int) extends Fig[CircleMarker]
  case Rectangle(x: Int, y: Int) extends Fig[RectangleMarker]

def equalFig[T](f1: Fig[T], f2: Fig[T]): Boolean = (f1, f2) match
  case (Fig.Circle(r1), Fig.Circle(r2))               => r1 == r2
  case (Fig.Rectangle(x1, y1), Fig.Rectangle(x2, y2)) => x1 == x2 && y1 == y2
  (* the compiler knows this match is exhaustive *)

scastie
在Scala中，有没有更简洁的方式来表达这一点，而不使用虚幻的CircleMarker和RectangleMarker特性？

scala

来源：https://stackoverflow.com/questions/75635063/succinct-way-to-use-gadts-for-exhaustiveness-checking-in-scala

1条答案

按热度按时间

t2a7ltrp1#

你可以试试F界限

enum Fig[T <: Fig[T]]:
  case Circle(r: Int) extends Fig[Circle]
  case Rectangle(x: Int, y: Int) extends Fig[Rectangle]

// sealed trait Fig[T <: Fig[T]]
// object Fig:
//   case class Circle(r: Int) extends Fig[Circle]
//   case class Rectangle(x: Int, y: Int) extends Fig[Rectangle]

def equalFig[T <: Fig[T]](f1: Fig[T], f2: Fig[T]): Boolean = (f1, f2) match
  case (Fig.Circle(r1), Fig.Circle(r2))               => r1 == r2
  case (Fig.Rectangle(x1, y1), Fig.Rectangle(x2, y2)) => x1 == x2 && y1 == y2

// def equalFig[T <: Fig[T]](f1: Fig[T], f2: Fig[T]): Boolean = f1 == f2

equalFig(Fig.Circle(1), Fig.Circle(1)) // true
equalFig(Fig.Circle(1), Fig.Circle(2)) // false
equalFig(Fig.Rectangle(1, 2), Fig.Rectangle(1, 2)) // true
equalFig(Fig.Rectangle(1, 2), Fig.Rectangle(1, 3)) // false
// equalFig(Fig.Circle(1), Fig.Rectangle(1, 2)) // doesn't compile

赞(0）回复(0）举报 2023-03-08

我来回答

在Scala中使用GADT进行穷举检查的简洁方法？

1条答案

相关问题

热门标签

最新问答