4 ms·
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 McBrid
by smadge 8y ago
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 http://www.cs.nott.ac.uk/~psztxa/publ/ydtm.pdf
- yogthos 8y agoThe 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.
- smadge 8y agoI 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.