Hacker News Reader

Yeah, I definitely wouldn't want to argue against having type inference at all. I agree that you don't want to annotate every single local definition (although I'd probably lean towards annotating more often than most).

I'm more saying that I'm fine with type system features that break global inference, as long as there's still local inference that's usually good enough in practice.

View on HN

Right, but local inference is also complicated. So the question is how much of it Idris manages to do without manual annotations. It's not even limited to local definitions with names. If you fully annotate "a=b+2" you get something like "a:int = a:int +:(int->int->int) 2:int". The compiler makes an expression tree and every node in the tree has to get an annotation, either from the source text (i.e. manually) or through inference.

Reply on news.ycombinator.com