Questions tagged [type-inference]
The type-inference tag has no usage guidance.
5
questions
26
votes
2answers
2k views
Context Sensitive Grammars and Types
1) What, if any, is the relationship between static typing and formal grammars?
2) In particular, would it be possible for a linear bounded automaton to check whether, say, a C++ or SML program was ...
12
votes
3answers
2k views
Type inference for imperative statements other than assignment
In my search for research papers about type systems for imperative languages, I only find solutions for a language with mutable references but without genuine imperative control structures such as ...
10
votes
2answers
243 views
Decidability of type inference and type checking in MLTT
In Martin-Löf's An Intuitionistic Theory of Types: Predicative Part it is proved that type checking $a \colon A$ is decidable subject to $a$ being typeable in the first place, by proving a ...
9
votes
1answer
455 views
In System F à la Church, can we automatize type inference for the for-all elimination?
The question is the following. Generally when one have a term like $\Lambda X.t$, we can eliminate the forall by applying this term to a type, as instance $(\Lambda X.t)[T]\to t[X:=T]$.
Now, suppose ...
6
votes
1answer
276 views
Can type inference be classified in two groups: unification-based and control-flow-based?
I recently came across the 1995 paper Safety analysis versus type inference (pdf link) by Palsberg and Schartzbach that contrasts unification-based type inference and static analysis methods based on ...
