5

我正在用 scala 实现一些常见的算法。在尝试重新创建冒泡排序时，我遇到了这个问题

这是一个内部循环的实现，它将值冒泡到顶部：

def pass(xs:List[Int]):List[Int] = xs match { 
  case Nil => Nil 
  case x::Nil => x::Nil 
  case l::r::xs if(l>r) => r::pass(l::xs)
  case l::r::xs => l::pass(r::xs)
}

我的问题是 case Nil => Nil。我知道我需要这个是因为我可以申请Nil这个功能。有没有办法确保Nil不能以满足编译器的方式作为参数提供，以便我可以消除这种情况？

4

3 回答 3

4

List 有两个子类型，Nil 和 ::，所以 :: 表示一个至少有一个元素的列表。

def pass(xs: ::[Int]):List[Int] = xs match { 
  case x::Nil => x::Nil 
  case l::r::xs if(l>r) => r::pass(new ::(l,xs))
  case l::r::xs => l::pass(new ::(r, xs))
}
于 2012-09-30T16:09:19.837 回答
2

这大致对应于对原始类型的改进，您将编写一个类型，其成员是初始类型的子集。然后，您将证明，对于x您的函数的每个输入，它x都是 non Nil。由于这需要大量的证明（您可以在 Coq 中使用子集类型使用依赖类型来实现这一点），在这种情况下最好的做法是引入一个新类型，它是一个没有Nil构造函数的列表，只有一个cons 和单个元素的构造函数。

编辑：由于 Scala 允许您在 List 类型上使用子类型来强制执行此操作，因此您可以在类型系统中确定地使用该子类型来证明它。这仍然是一个证明，从某种意义上说，任何类型检查都对应于证明程序确实存在某种类型的证明，这只是编译器可以完全证明的东西。

于 2012-09-30T15:55:30.993 回答
2

在这种情况下，您可以简单地使用case子句顺序：

def pass(xs:List[Int]):List[Int] = xs match { 
  case l::r::xs if(l>r) => r::pass(l::xs)
  case l::r::xs => l::pass(r::xs)
  case xs => xs
}

前两个子句将仅匹配具有一个或多个元素的列表。最后一个子句将在其他地方匹配。

于 2012-09-30T16:34:48.357 回答