Hacker News Reader

Comment by yogthos | Hacker News Reader

The kinds of errors where you have a type mismatch are wholly uninteresting in my experience, and get caught very early on in the development process. What I really care about is semantic correctness.

For example, consider a sort function. The types can tell me that I passed in a collection of a particular type and I got a collection of the same type back. However, what I really want to know is that the collection contains the same elements, and that they’re in order. This is difficult to express using most type systems out there. Even when the type system is powerful enough to encode such semantics, it's both difficult to figure out how to express and understand the resulting specification.

View on HN

I was curious about your example of expressing and validating that a sort function returns a sorted list using the type system. I found this paper [0] by McBride, McKinna, and Altenkirch about using dependent types in the language Epigram to do exactly that. I have only scanned it, and it remains to be seen if it truly is too "difficult to figure out how to express or understand the resulting specification." Hopefully with more research it will only become easier!

[0] http://www.cs.nott.ac.uk/~psztxa/publ/ydtm.pdf

The fact that it's a research topic really says all you need to know in my opinion. It's not a question of whether you can do it in principle, but rather whether it's an effective alternative to other approaches.

I agree, I don’t think dependent typing and validating the correctness of your program using formal proofs is ready for mainstream adoption. I think it might be ready for some domains, like aeronautics, where the cost of errors is very high.

Here's some sort specifications for LiquidHaskell (refinement types) https://github.com/ucsd-progsys/liquidhaskell/blob/master/te...

I have a bit of trouble reading it, but the specs are very terse.

Well, you can create a SortedList type that is only returned from sort functions, so you can write functions that only accept sorted lists.

It's not a question of whether you can do it in principle or not. My point was that I don't think it's an effective approach for creating such specifications compared to the alternatives such as runtime contracts.

Why is that? In fact, I would argue you want both. You want to use a contract to check the incoming data, but once it's been checked, you'd want to wrap it in a type that guarantees the property is set.

Otherwise, you have to iterate over a potentially very large set of data to check if it's sorted every time you want to use a function that has that contract.

Reply on news.ycombinator.com