Hacker News new | past | comments | ask | show | jobs | submit login

It doesn't say "type checking", though. It says "the language", which I think of as including the respective preludes.



The core theory (and implementation) is much simpler for almost all dependent type theories. At least this is my personal feeling after having read a lot of GHC code, written an Idris backend, the native backend for Lean, and significant portions of `rustc`.


It's generally (or maybe universally) more difficult to "get" dependent typing than plain old ML-family static typing. I mean, this HN comments page alone has multiple threads where people don't think that the "x > y" proof example even works. For most programmers, that's how non-obvious the possibility of proving nontrivial properties of code is. Maybe I should change the wording in the OP to make it clear that I'm talking about the set of ideas required to use the language, not the characters that need to be typed into a computer to make it work.


> It's generally (or maybe universally) more difficult to "get" dependent typing than plain old ML-family static typing.

That's true, but Haskell has come a long way since a direct comparison like that would make sense.

> I mean, this HN comments page alone has multiple threads where people don't think that the "x > y" proof example even works.

I think this is because people have some preconceived idea about what dependent typing is before they come to dependently typed languages. So, not only are they learning about dependent types, but they are also fighting their preconceived notions. That was certainly the case for me.

It's an interesting facet of the human condition; every time we learn a new tool, we have to be reminded that it's not magic.

Now, having become proficient, I have a better intuition for how to get my complex Idris programs to type check than my complex Haskell ones. Idris is actually simpler, it's not just about line counts.




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

Search: