Questions tagged [type-inference]
The type-inference tag has no usage guidance.
6
questions
45
votes
1answer
6k views
What makes type inference for dependent types undecidable?
I have seen it mentioned that dependent type systems are not inferable, but are checkable. I was wondering if there is a simple explanation of why that is so, and whether or not there is there a limit ...
14
votes
1answer
2k views
Why will the Hindley-Milner algorithm never yield a type like t1 -> t2?
I'm reading about the Hindley-Milner typing algorithm while writing an implementation, and see that, as long as every variable is bound, you'll always get either atomic types or types where the ...
5
votes
1answer
90 views
What does $ \forall \alpha_1, \dots , \alpha_n . \tau $ mean formally as a type?
I was learning about polymorphic types but I couldn't understand the notation, can someone explain it means (context cs421 UIUC):
$$ \forall \alpha_1, \dots , \alpha_n . \tau $$
its supposed to be a ...
9
votes
2answers
1k views
Type inference + overloading
I'm looking for a type inference algorithm for a language I'm developing, but I couldn't find one that suits my needs because they usually are either:
à la Haskell, with polymorphism but no ad-hoc ...
6
votes
1answer
550 views
Encoding row types
I'm working on a type system with extensible records, similar to ones explained in "A Polymorphic Type System for Extensible Records and Variants - Benedict R. Gaster and Mark P. Jones" and "...
1
vote
1answer
120 views
What is the difference between $ \alpha \to \alpha $ vs $ \forall \alpha. \alpha \to \alpha$?
I was studying polymorphic types and I was finding the distinction with monomorphic types difficult to pin down (context CS 421). From the course I linked the have the following (vague attempt) at a ...
