유형을 데이터 생성자와 연결하는 ADT 인코딩의 문제점은 무엇입니까?

유형을 데이터 생성자와 연결하는 ADT 인코딩의 문제점은 무엇입니까? (예 : Scala.)

---

Scala에서 대수 데이터 유형은 sealed1 단계 유형 계층 으로 인코딩됩니다 . 예:

-- 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 object의 스칼라는 같은 것들을 잔뜩 생성 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의 데이터 생성자 처리가 잘못되었다는 견해는 Twitter, 메일 링리스트, IRC, SO 등에서 여러 번 표현되었습니다 . 불행히도 저는 몇 가지를 제외하고는 링크가 없습니다. Travis Brown의 답변입니다 . 그리고 Scala를위한 순전히 기능적인 JSON 라이브러리 인 Argonaut .

Argonaut는 의식적 으로 Haskell 접근 방식을 취합니다 ( private케이스 클래스를 지정하고 데이터 생성자를 수동으로 제공). 내가 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

I have been pondering this for quite some time, but still do not understand what makes Scala's encoding wrong. Sure it hampers type inference at times, but that does not seem like a strong enough reason to decree it wrong. What am I missing?

---

To the best of my knowledge, there are two reasons why Scala's idiomatic encoding of case classes can be bad: type inference, and type specificity. The former is a matter of syntactic convenience, while the latter is a matter of increased scope of reasoning.

The subtyping issue is relatively easy to illustrate:

val x = Some(42)

The type of x turns out to be Some[Int], which is probably not what you wanted. You can generate similar issues in other, more problematic areas:

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

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

The type of xs is List[Case1]. This is basically guaranteed to be not what you want. In order to get around this issue, containers like List need to be covariant in their type parameter. Unfortunately, covariance introduces a whole bucket of issues, and in fact degrades the soundness of certain constructs (e.g. Scalaz compromises on its Monad type and several monad transformers by allowing covariant containers, despite the fact that it is unsound to do so).

So, encoding ADTs in this fashion has a somewhat viral effect on your code. Not only do you need to deal with subtyping in the ADT itself, but every container you ever write needs to take into account the fact that you're landing on subtypes of your ADT at inopportune moments.

The second reason not to encode your ADTs using public case classes is to avoid cluttering up your type space with "non-types". From a certain perspective, ADT cases are not really types: they are data. If you reason about ADTs in this fashion (which is not wrong!), then having first-class types for each of your ADT cases increases the set of things you need to carry in your mind to reason about your code.

For example, consider the ADT algebra from above. If you want to reason about code which uses this ADT, you need to be constantly thinking about "well, what if this type is Case1?" That just not a question anyone really needs to ask, since Case1 is data. It's a tag for a particular coproduct case. That's all.

Personally, I don't care much about any of the above. I mean, the unsoundness issues with covariance are real, but I generally just prefer to make my containers invariant and instruct my users to "suck it up and annotate your types". It's inconvenient and it's dumb, but I find it preferable to the alternative, which is a lot of boilerplate folds and "lower-case" data constructors.

As a wildcard, a third potential disadvantage to this sort of type specificity is it encourages (or rather, allows) a more "object-oriented" style where you put case-specific functions on the individual ADT types. I think there is very little question that mixing your metaphors (case classes vs subtype polymorphism) in this way is a recipe for bad. However, whether or not this outcome is the fault of typed cases is sort of an open question.

참고URL : https://stackoverflow.com/questions/25330359/what-are-the-problems-with-an-adt-encoding-that-associates-types-with-data-const