How does one prove the equivalence of two types and that a signature is singly-inhabited?

Question

Anyone who has been following Tony Morris' blog and scala exercises, will know that these two type signatures are equivalent:

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

And:

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

Furthermore, it has been stated that the type is singly-inhabited (i.e. all implementations of the type are exactly equivalent). I can guess at proving the equivalence of the two types but don't really know where to start on the single-inhabitance statement. How does one prove this?

Answer 1

The Option type is doubly-inhabited. It can either contain something or not. This is clear from the signature of fold in the first trait, in which you can only:

• return the result of applying some, if you have a value of type A sitting around (you're a Some)
• return your none argument (you're a None)

Any given implementation can only do one or the other, without violating referential transparency.

So I believe it's a mistake to call it singly-inhabited. But any implementation of either of these traits must be isomorphic to one of these two cases.

EDIT

That said, I don't think you can really characterize the "inhabitedness" of a type without knowing its constructors. If you were to extend one of these option traits with an implementation that had a constructor which took a Tuple12[A], for instance, you could write 13 different versions of fold.