4 ms·
What do you mean by local type inference? Things like let? If so even languages without HM like Agda allow that. HM type inference is specifically for finding t
by dependenttypes 6y ago
What do you mean by local type inference? Things like let? If so even languages without HM like Agda allow that. HM type inference is specifically for finding the type of the arguments of functions.
- jhanschoo 6y ago> You just take the type from the right hand side and then put it on the left hand side? That's what they mean by local variable inference
- dependenttypes 6y agoI do not really understand what this means. Something like given y : yt and let x = y we can infer that x : yt?
- jhanschoo 6y agoYeah.