Questions tagged [type-inference]
The type-inference tag has no usage guidance.
8
questions
47
votes
1answer
7k 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
100 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 ...
14
votes
1answer
3k views
Concise example of exponential cost of ML type inference
It was brought to my attention that the cost of type inference in a functional language like OCaml can be very high. The claim is that there is a sequence of expressions such that for each expression ...
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
563 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
0answers
48 views
What is the runtime (time complexity) of Type Inference in Simply Typed Lambda Calculus?
I was told that the runtime of OCAML or Scala is EXPTIME - which seems really bad! However, since people use type inference (deciding the type of a term or program or expression) in practice - it must ...
1
vote
1answer
149 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 ...