如何在模式匹配的右侧考虑枚举的所有情况答案

【问题标题】：How to account for all cases of an enum on the right-hand side of a pattern match如何在模式匹配的右侧考虑枚举的所有情况
【发布时间】：2013-02-17 21:36:30
【问题描述】：

详尽的模式匹配很棒，但它似乎只适用于 case (=>) 运算符的左侧。

我很好奇是否有一种方法可以验证函数（或表达式）的输出是否可以绑定到该枚举。目标是让编译器在我忘记从枚举中输出项目时告诉我。

在我的示例中，我使用了以下包含三个项目的枚举：

object MyEnum { 
    sealed trait t 
    case object E1 extends t
    case object E2 extends t
    case object E3 extends t
}

这是一个模式匹配表达式，它会产生编译时警告（我们已经知道）：

def foo( e : MyEnum.t ) : Boolean =
    e match {
        case MyEnum.E1 => true
        case MyEnum.E2 => false
        case MyEnum.E3 => true   // if we leave this line out, we get a warning
    }

如果我们将MyEnum.E3 排除在模式匹配表达式之外，Scala 会抱怨，因为它引用了非详尽的模式匹配。这是非常有益的，但我想知道是否可以反过来。

我们能否说明=> 右侧的所有MyEnum.t 情况？

这是一个突出显示这一点的示例：

def bar( s : String ) : Option[MyEnum.t] = 
    s match {
        case "a" => Some(MyEnum.E1)
        case "b" => Some(MyEnum.E2)
        case "c" => Some(MyEnum.E3)  // if we leave this out, no warning
        case _ => None
    }

在这个例子中，如果我们省略了MyEnum.E3 这一行，那么编译器就会继续运行，就好像没有任何问题一样。我想说的是：

forall MyEnum.t (aliased as e) there exists Some(e) | None

我知道这可以通过运行时测试轻松解决，但我很好奇是否有办法静态检查。

谢谢。

【问题讨论】：

您可以轻松地在依赖类型语言中静态地检查这个，但是您必须编写会被检查的证明。在上面的示例中，您只需要简单的满射性证明，在建设性设置中，这相当于给出反函数的一半。您的问题的自动“推断”形式是不可能的，因为可能有任意复杂的逻辑掩盖您的 E1-E3 返回值。

标签： scala pattern-matching dependent-type

【解决方案1】：

我要靠运气并声称这是不可能的（让我们对 Odersky 保密）。如果 Scala 编译器能够检测到这种情况，我认为它会比现在更慢;)

我能看到的唯一方法是定义 foo 类似于您所做的方式，并通过使其迭代 foo 来制作反向映射来定义 bar ，但这对我来说没有多大意义，并且可能不起作用在您的具体情况下。

我认为你的案例是一个很好的例子，说明单元测试何时有用，那么为什么不写一个呢？

【讨论】：

哦，是的，它可能非常慢。我只是预感到这是可能的。

【解决方案2】：

不，这是不可能的，因为这相当于停机问题，该问题在 1936 年被证明是无法解决的。

【讨论】：