Как можно доказать эквивалентность двух типов и то, что подпись однократно заселена? - PullRequest
Новая
       83

Как можно доказать эквивалентность двух типов и то, что подпись однократно заселена?

8 голосов
/ 02 сентября 2010

Любой, кто следит за блогом Тони Морриса и упражнениями 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
}

Кроме того, было указано, что тип является однократно обитаемым (т.е. все реализации типа в точности эквивалентны). Я могу догадаться, доказывая эквивалентность двух типов, но на самом деле не знаю, с чего начать утверждение о едином населении. Как это доказать?

1 Ответ

2 голосов
/ 02 сентября 2010

Тип Option вдвойне заселен.Он может содержать что-то или нет.Это ясно из сигнатуры fold в первой черте, в которой вы можете только:

  • вернуть результат применения some, если у вас есть значение типа A сидявокруг (вы Some)
  • верните свой аргумент none (вы None)

Любая данная реализация может выполнять только одну или другуюбез нарушения ссылочной прозрачности.

Так что я считаю ошибкой называть его однобитым.Но любая реализация любой из этих черт должна быть изоморфна одному из этих двух случаев.

РЕДАКТИРОВАТЬ

Тем не менее, я не думаю, что вы действительно можете охарактеризовать "обитаемость" типане зная его конструкторов.Если бы вы расширили одну из этих опций с помощью реализации, которая имела конструктор, например, Tuple12[A], вы могли бы написать 13 различных версий fold.

...