And still this type system could be the base for a very interesting and powerfull programming langua...

randomNumber7 • yesterday at 10:21 PM • 3 replies • view on HN

And still this type system could be the base for a very interesting and powerfull programming language imo.

amelius • yesterday at 11:01 PM

Yeah we don't throw programming languages away because they are undecidable.

So why would we throw type systems away if they are undecidable?

➕ show 2 replies

rerdavies • yesterday at 11:49 PM

Presumably with the rather unpleasant side-effect of compiles that may never finish. :-P

solomonb • yesterday at 11:53 PM

This really isn't a big deal as it resolved via type universes.

alt Hacker News