将类型与数据构造函数关联的ADT编码有什么问题？(比如Scala.)

Question

在Scala中,代数数据类型被编码为sealed一级类型层次结构.例:

-- Haskell
data Positioning a = Append
                   | AppendIf (a -> Bool)
                   | Explicit ([a] -> [a]) 

// Scala
sealed trait Positioning[A]
case object Append extends Positioning[Nothing]
case class AppendIf[A](condition: A => Boolean) extends Positioning[A]
case class Explicit[A](f: Seq[A] => Seq[A]) extends Positioning[A]

随着case classES和case objectS,斯卡拉产生了一堆东西一样equals,hashCode,unapply(通过模式匹配使用)等这使我们的许多关键特性和传统的ADT功能.

但是有一个关键的区别 - 在Scala中,"数据构造函数"有自己的类型.比较以下两个例子(从相应的REPL复制).

// Scala

scala> :t Append
Append.type

scala> :t AppendIf[Int](Function const true)
AppendIf[Int]

-- Haskell

haskell> :t Append
Append :: Positioning a

haskell> :t AppendIf (const True)
AppendIf (const True) :: Positioning a

---

我一直认为Scala的变化是有利的.

毕竟,不会丢失类型信息.AppendIf[Int]例如是一个子类型Positioning[Int].

scala> val subtypeProof = implicitly[AppendIf[Int] <:< Positioning[Int]]
subtypeProof: <:<[AppendIf[Int],Positioning[Int]] = <function1>

实际上,您获得了有关该值的额外编译时间不变量.(我们可以将此称为依赖类型的限制版本吗？)

这可以很好地使用 - 一旦你知道使用了什么数据构造函数来创建一个值,相应的类型就可以通过流的其余部分传播,以增加更多的类型安全性.例如,播放JSON,使用这个斯卡拉编码,将只允许你提取fields的JsObject,而不是任意的JsValue.

scala> import play.api.libs.json._
import play.api.libs.json._

scala> val obj = Json.obj("key" -> 3)
obj: play.api.libs.json.JsObject = {"key":3}

scala> obj.fields
res0: Seq[(String, play.api.libs.json.JsValue)] = ArrayBuffer((key,3))

scala> val arr = Json.arr(3, 4)
arr: play.api.libs.json.JsArray = [3,4]

scala> arr.fields
<console>:15: error: value fields is not a member of play.api.libs.json.JsArray
              arr.fields
                  ^

scala> val jsons = Set(obj, arr)
jsons: scala.collection.immutable.Set[Product with Serializable with play.api.libs.json.JsValue] = Set({"key":3}, [3,4])

在Haskell中,fields可能会有类型JsValue -> Set (String, JsValue).这意味着它将在运行时失败JsArray等等.这个问题也以众所周知的部分记录访问器的形式出现.

Scala对数据构造函数的处理错误的观点已多次表达 - 在推特,邮件列表,IRC,SO等等.不幸的是我没有任何链接,除了一对 - Travis Brown的回答,和Argonaut,一个用于Scala的纯函数JSON库.

Argonaut 有意识地采用Haskell方法(通过privatecase类,并手动提供数据构造函数).你可以看到我用Haskell编码提到的问题也存在于Argonaut中.(除非Option用于表示偏倚.)

scala> import argonaut._, Argonaut._
import argonaut._
import Argonaut._

scala> val obj = Json.obj("k" := 3)
obj: argonaut.Json = {"k":3}

scala> obj.obj.map(_.toList)
res6: Option[List[(argonaut.Json.JsonField, argonaut.Json)]] = Some(List((k,3)))

scala> val arr = Json.array(jNumber(3), jNumber(4))
arr: argonaut.Json = [3,4]

scala> arr.obj.map(_.toList)
res7: Option[List[(argonaut.Json.JsonField, argonaut.Json)]] = None

我一直在思考这个问题,但仍然不明白是什么让Scala的编码错误.当然它有时会妨碍类型推断,但这似乎不足以说明它是错误的.我错过了什么？

Answer 1

据我所知,Scala的案例类的惯用编码可能有两个原因:类型推断和类型特异性.前者是语法上的便利问题,而后者则是推理范围扩大的问题.

子类型问题相对容易说明:

val x = Some(42)

x原来的类型,Some[Int]可能不是你想要的.您可以在其他更有问题的领域生成类似问题:

sealed trait ADT
case class Case1(x: Int) extends ADT
case class Case2(x: String) extends ADT

val xs = List(Case1(42), Case1(12))

类型xs是List[Case1].这基本上保证不是你想要的.为了解决这个问题,容器List需要在其类型参数中协变.不幸的是,协方差引入了一大堆问题,实际上降低了某些结构的稳健性(例如Scalaz Monad通过允许协变容器对其类型和几个monad变换器进行妥协,尽管事实上这样做是不合理的).

因此,以这种方式编码ADT会对代码产生一定程度的病毒影响.您不仅需要处理ADT本身的子类型,而且您编写的每个容器都需要考虑到您在不合适的时刻登陆ADT的子类型这一事实.

不使用公共案例类对ADT进行编码的第二个原因是避免使用"非类型"来混淆类型空间.从某个角度来看,ADT案例并不是真正的类型:它们是数据.如果你以这种方式推理ADT(这没有错!),那么为每个ADT案例提供一流的类型会增加你需要携带的一些东西来推理你的代码.

例如,考虑ADT上面的代数.如果你想推理使用这个ADT的代码,你需要不断思考"好吧,如果这种类型是Case1什么？" 这不是任何人真正需要问的问题,因为Case1是数据.它是特定副产品案例的标签.就这样.

就个人而言,我并不关心以上任何一点.我的意思是,协方差的不健全问题是真实的,但我通常只是希望使我的容器不变并指示我的用户"吮吸它并注释你的类型".它很不方便而且很笨,但我觉得它更接近替代方案,它是很多样板折叠和"小写"数据构造器.

作为通配符,这种类型特异性的第三个潜在缺点是它鼓励(或者更确切地说,允许)更"面向对象"的样式,其中您将特定于案例的函数放在各个ADT类型上.我认为用这种方式混合你的隐喻(案例类和子类型多态)是一个很糟糕的问题.但是,这种结果是否是打字案件的错误是一个悬而未决的问题.