English 中文(简体)
How does one prove the equivalence of two types and that a signature is singly-inhabited?
原标题:

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?

问题回答

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.





相关问题
Are there type signatures which Haskell can t verify?

This paper establishes that type inference (called "typability" in the paper) in System F is undecidable. What I ve never heard mentioned elsewhere is the second result of the paper, namely that "type ...

Where s the contravariance?

A canonical example of patching up an otherwise covariant class is as follows: abstract class Stack[+A] { def push[B >: A]( x: B ) : Stack[B] def top: A def pop: Stack[A] Now, if I remove the ...

Books for beginning type system theory [closed]

I want to study type system theory. I don t have any background in type system theory so I m more or less a beginner (except the articles I ve read on the subject and which I find intimidating because ...

Typing the Y combinator

http://muaddibspace.blogspot.com/2008/01/type-inference-for-simply-typed-lambda.html is a concise definition of the simply typed lambda calculus in Prolog. It looks okay, but then he purports to ...

A question about logic and the Curry-Howard correspondence

Could you please explain me what is the basic connection between the fundamentals of logical programming and the phenomenon of syntactic similarity between type systems and conventional logic?

热门标签