如何证明两种类型的等价性以及一个签名是单独存在的？

【问题标题】：How does one prove the equivalence of two types and that a signature is singly-inhabited?如何证明两种类型的等价性以及一个签名是单独存在的？
【发布时间】：2011-04-07 01:16:40
【问题描述】：

任何一直关注Tony Morris' blog 和scala 练习的人都会知道这两种类型签名是等价的：

trait MyOption1[A] {
  //this is a catamorphism
  def fold[B](some : A => B, none : => B) : B 
}

还有：

trait MyOption2[A] {
  def map[B](f : A => B) : MyOption2[B]
  def getOrElse[B >: A](none : => B) : B
}

此外，已经声明该类型是单独存在的（即该类型的所有实现都是完全等价的）。我可以猜测证明这两种类型的等价性，但真的不知道从哪里开始单居声明。如何证明这一点？

【问题讨论】：

cstheory.stackexchange.com 可能是解决这个问题的更好地方。

标签： scala functional-programming type-theory

【解决方案1】：

Option 类型是双重居住的。它可以包含或不包含某些内容。从第一个特征中fold 的签名中可以清楚地看出这一点，您只能：

返回应用some的结果，如果你有一个A类型的值坐在周围（你是Some）
返回您的 none 参数（您是 None）

任何给定的实现只能做一个或另一个，而不会违反引用透明性。

所以我认为将其称为单独居住是错误的。但是这些特征中的任何一个的任何实现都必须与这两种情况中的一种同构。

编辑

也就是说，如果不知道它的构造函数，我认为你无法真正描述一个类型的“可居住性”。例如，如果您要使用具有 Tuple12[A] 的构造函数的实现来扩展这些选项特征之一，您可以编写 13 个不同版本的 fold。

【讨论】：