Hacker News new | ask | show | jobs
by catnaroek 4688 days ago
As noted by masklinn, the compiler will complain about the non-exhaustive match. Stuff like this makes me want a dependently typed language for practical programming, in which I can express the concept of "this case ought to be impossible", and convince the compiler by supplying a proof. Also, this would eliminate the false dichotomy between "fast, unchecked, unsafe array indexing" and "slow, checked, safe array indexing", which would be a huge win for safe systems programming.
3 comments
doublec 4688 days ago
There are some languages heading towards this. ATS [1] provides a restricted form of dependent types [2] that allows you to do what you want and is designed for systems programming. You can do safe pointer arithmetic for example.

Idris [3] is another language with dependent types (and is more Rust-like) designed for systems programming. I don't think Idris has type level presberger arithmetic though making some things a bit verbose.

[1] http://www.ats-lang.org/ [2] http://bluishcoder.co.nz/2010/09/01/dependent-types-in-ats.h... [3] http://www.idris-lang.org/

link
Locke1689 4688 days ago
I assume you're familiar with ATS? What don't you like about it?
link
rdtsc 4688 days ago
I am not the original poster but I'll respond to this one:

I am familiar with ATS and I don't like that I am only familiar with it from the Language Shootout contest website. I haven't heard of it used in production, no blogs, no news on HN.

It is a bad excuse and rather sad but my main charge against it is that it is not popular enough.

link
doublec 4687 days ago
I agree not much is heard about it. I blog about it a fair amount on [1]. There's also /r/ats [2]. I use it in production. The backend of my bitcoin mining pool [3] is written in ATS and has about 1% of the total bitcoin mining capacity and has been operating for a couple of years. The front end of the pool is written in Ur/Web.

[1] http://bluishcoder.co.nz/tags/ats/ [2] http://www.reddit.com/r/ATS/ [3] http://mmpool.bitparking.com

link
catnaroek 4688 days ago
No tactics.
link
anon3132 4687 days ago
Dependent typing would be throwing out the entire type system, and also be incredibly ambitious. Dependent type systems are great, but I think the Rust team made the right decision here.
link