Hacker News new | comments | ask | show | jobs | submit login
Unboxed union types in Scala via the Curry-Howard isomorphism (chuusai.com)
44 points by DanielRibeiro on June 9, 2011 | hide | past | web | favorite | 18 comments



This is right up there with most brilliant explorations I have seen in Scala. I am very pleased indeed that the language and its tools are strong enough to support that kind of experiment. It's a different question entirely whether you want to put that into production code. My answer would be almost certainly no, but that's not the point of this blog, as I understood it.


No, of course, the point of the blog is to pester a certain Martin to put it into the compiler :-).


Great feedback. It is always a pleasure to have the Language creator's opinion here on Hacker News.


"And there you have it — an unboxed, statically type safe encoding of union types in unmodified Scala!"

And just about impossible to read.

The fact that it needed a mathematical proof to arrive at that conclusion was a hint that the path was too convoluted to follow.

For the love of all that's holy and good, please don't do this kind of thing in real code. Someone will just be forced to go in after you and make it readable again.


I'm no mathematician and I was able to easily understand the premise and follow most of the reasoning (some Scala idiosyncrasies went above my head at the last step where he adds syntactic sugar).

The proof is as basic as can be. If it helps, you can substitute types with sets, "being a subtype" with "being included in", imagine Venn diagrams and procede from there visually.

Edit: see the first half of this article for an illustration of what I mean.

http://www.ams.org/feature-column/fcarc-venn "Topolgy of Venn Diagrams"


Read the first example. Easy to understand, even if you don't know much scala, yes?

Now read the final code. Can you really make heads or tails of that without reading his whole post? Imagine if the whole program was as arcane as that.

Someone else will have to maintain that code eventually, and without his magic post to clarify it, it's insanely hard to read. I would end up writing tests to determine exactly what it did and didn't do, then rewrite it from scratch so I (and everyone after me) could read it.


1) Who says that this is meant for production code? It is first and foremost a demonstration of the power and flexibility of the Scala type system.

2) I wouldn't mind actually using it in production if the library was written as a litterate program including the whole blog post. Once you wrap your head around the concept, the code becomes clear (and is so simple that you can understand it doesn't have any bug to be fixed anyway)


The important sentence is:

"Obviously it would be nicer if Scala supported union types as primitives, but at least this construction shows that the Scala compiler has all the information it needs to be able to do that. "

Which means the compiler can do this but need syntactic sugar to make it more accessible.


Since when has exploring the nooks and crannies of a programming language not been considered good hacker practice?

Also, read it again. There's no proof involved here - basic logic is all.


The important sentence is: "Obviously it would be nicer if Scala supported union types as primitives, but at least this construction shows that the Scala compiler has all the information it needs to be able to do that. " Which means the compiler can do this but need syntactic sugar to make it more accessible.


Is this more readable?

    def size[T : Union[Int, String]#Value](t : T) = t match {
      case i : Int => i
      case s : String => s.length
    }


> The fact that it needed a mathematical proof to arrive at that conclusion was a hint that the path was too convoluted to follow.

There are some (e.g., Dijkstra) who would argue that the code itself ought to be a mathematical proof of correctness. I'm inclined to agree.


Except that's not possible yet. The pitfalls, limitations, and complexity of languages with advanced type systems such as Scala and Haskell are evidence that the Curry-Howard isomorphism is not useful enough.


Can you name some pitfalls, limitations or complexity in Haskell?

Haskell is not a complicated language, but it may be hard to learn because it is so different. My experience is that people get frustrated trying to learn it, and decide if it was hard to learn, it must be "too difficult".


http://research.microsoft.com/en-us/um/people/simonpj/papers... to understand the tradeoffs involved in building a state-of-the-art type checker for an expressive advanced type system. Look at the Haskell bug list around the type checker.

Also, http://pchiusano.blogspot.com/2011/05/making-most-of-scalas-...

Also, http://www.cis.upenn.edu/~bcpierce/papers/harmful-mfps.pdf

Also, http://people.cs.kuleuven.be/~tom.schrijvers/Research/papers...


Hmm.. I don't know Scala, so I cannot really discuss Scala complexity.

But having no degree whatsoever, I find pretty much all Haskell I encounter understandable and approachable and that has been the case ever since I had around 4-6 months of Haskell experience.

I have never encountered significant bugs in GHC's type checker -- are there any more bugs there than there are in other less advanced type systems?


Personally, I don't have a problem with deep magic that I don't completely understand operating in my code, as long as its semantics are clear and obvious. If I didn't, I doubt I'd code in C, never mind Scala.

I'm more interested in what this compiles to in the JVM, and what its performance overhead is.


The size method from the post compiles to exactly the same bytecode as the unsafe

  def sizeAny(t: Any) = t match {
    case i : Int => i
    case s : String => s.length
  }
The only difference is that the method has an additional unused parameter for the <:< witness [edit: which must be provided at the call site, so there is some overhead (a method call and an object allocation) there] and that the compiler guarantees that it will never throw a MatchError exception.

As proof the disassembly:

   public int size(java.lang.Object, scala.Predef$$less$colon$less);
     Code:
      0:	aload_1
      1:	astore_3
      2:	aload_3
      3:	instanceof	#8; //class java/lang/Integer
      6:	ifeq	16
      9:	aload_3
      10:	invokestatic	#14; //Method scala/runtime/BoxesRunTime.unboxToInt:(Ljava/lang/Object;)I
      13:	goto	30
      16:	aload_3
      17:	instanceof	#16; //class java/lang/String
      20:	ifeq	31
      23:	aload_3
      24:	checkcast	#16; //class java/lang/String
      27:	invokevirtual	#20; //Method java/lang/String.length:()I
      30:	ireturn
      31:	new	#22; //class scala/MatchError
      34:	dup
      35:	aload_3
      36:	invokespecial	#26; //Method scala/MatchError."<init>":(Ljava/lang/Object;)V
      39:	athrow

   public int sizeAny(java.lang.Object);
     Code:
      0:	aload_1
      1:	astore_2
      2:	aload_2
      3:	instanceof	#8; //class java/lang/Integer
      6:	ifeq	16
      9:	aload_2
      10:	invokestatic	#14; //Method scala/runtime/BoxesRunTime.unboxToInt:(Ljava/lang/Object;)I
      13:	goto	30
      16:	aload_2
      17:	instanceof	#16; //class java/lang/String
      20:	ifeq	31
      23:	aload_2
      24:	checkcast	#16; //class java/lang/String
      27:	invokevirtual	#20; //Method java/lang/String.length:()I
      30:	ireturn
      31:	new	#22; //class scala/MatchError
      34:	dup
      35:	aload_2
      36:	invokespecial	#26; //Method scala/MatchError."<init>":(Ljava/lang/Object;)V
      39:	athrow




Applications are open for YC Summer 2019

Guidelines | FAQ | Support | API | Security | Lists | Bookmarklet | Legal | Apply to YC | Contact

Search: