Questions tagged [type-inference]

The tag has no usage guidance.

Filter by
Sorted by
Tagged with
50 votes
1 answer
8k 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 ...
Victor's user avatar
  • 705
27 votes
1 answer
3k views

What are the strongest known type systems for which inference is decidable?

It's well known that Hindley–Milner type inference (the simply-typed $\lambda$-calculus with polymorphism) has decidable type inference: you can reconstruct principle types for any programs without ...
Joey Eremondi's user avatar
14 votes
1 answer
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 ...
Juan's user avatar
  • 755
14 votes
1 answer
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 ...
mrrusof's user avatar
  • 241
11 votes
3 answers
1k views

Automatic Downcasting by Inferring the Type

In java, you must explicitly cast in order to downcast a variable ...
Sam Washburn's user avatar
11 votes
2 answers
2k views

Define a list using only the Hindley-Milner type system

I'm working on a small lambda calculus compiler that has a working Hindley-Milner type inference system and now also supports recursive let's (not in the linked code), which I understand should be ...
Juan's user avatar
  • 755
11 votes
1 answer
707 views

Inferring refinement types

At work I’ve been tasked with inferring some type information about a dynamic language. I rewrite sequences of statements into nested let expressions, like so: <...
Jon Purdy's user avatar
  • 365
10 votes
3 answers
1k views

Equivalence of data-flow analysis, abstract interpretation and type inference?

@Babou's answer to a recent question reminds me that at one time I think I read a paper about the equivalence (in terms both of the facts that can be inferred or proved and the time complexity of ...
Wandering Logic's user avatar
10 votes
2 answers
2k views

Relation between type-checking decidability, typability decidability and strong normalization

Yo! This is probably a stupid question, however I've never seen it written down explicitly if, for instance, decidability of type-checking is equivalent to the strong normalization property. Therefore ...
user40276's user avatar
  • 211
10 votes
2 answers
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 ...
miniBill's user avatar
  • 419
10 votes
0 answers
827 views

Advantages of algorithm W over algorithm J for type inference in Hindley-Milner type system

According to A modern eye on ML type inference Furthermore, for some unknown reason, W appears to have become more popular than J, even though the latter is viewed—with reason!—by Milner as ...
Alexey Romanov's user avatar
8 votes
1 answer
282 views

Relation between Type Assignment system (TA) and Hindley-Milner system

Recently I started my studies in type theory/type systems and Lambda Calculus. I have already read about Simple Typed Lambda Calculus in Church and Curry style. The last one is also known as Type ...
Rafael Castro's user avatar
8 votes
0 answers
344 views

Type-classes for type inference

I'm creating a semantic analyzer with type inference. For the basics I've got a type variable and a type construct with name and a list of types. I want to support overloading and I know that Haskell ...
Peter Lenkefi's user avatar
7 votes
0 answers
53 views

When does type inference become undecidable in typed lambda calculus?

To begin with, if I understand correctly, in a simply typed lambda calculus, typing, type checking and type inference are always decidable. In the "full-fledged" polymorphic (terms depend on ...
P.A.R.T.E.I.'s user avatar
6 votes
1 answer
197 views

Does there exist a type system for a non-let-polymorphic lambda calculus?

I'm wondering if there is a way to extend Hinley-Milner's type system to allow polymorphic types without the need of a let construct, by adding an intersection type (as Dan pointed out) that ...
Juan's user avatar
  • 755
6 votes
1 answer
593 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 "...
sinan's user avatar
  • 223
5 votes
3 answers
1k views

Why isn't the Swift programming language type inference more aggressive?

Couldn't the type inference in Apple's new programming language Swift had been done more aggressive? For instance why can't the return type of a function be deduced? ...
Christian's user avatar
  • 151
5 votes
2 answers
744 views

Check if a lambda constructor is well-typed

In basic type inference for 𝜆-calculus with parametric polymorphism à la Hindley–Milner, when can we say that we cannot give a type to a lambda constructor? For example $$(λx.λy.y(x\ ...
Gallaoui's user avatar
  • 153
5 votes
1 answer
333 views

Drawbacks of adding type equality to 1ML

In the 1ML – Core and Modules United (F-ing First-Class Modules) paper, the author gives the following example for why module types do not form a lattice under subtyping: ...
typesanitizer's user avatar
5 votes
2 answers
655 views

Does the underlying computational calculus in type theories affect decidability?

I'm looking for a high-level explanation although if that isn't possible or difficult, I'd prefer references to books/papers. I understand that modern type theory is inspired by Curry-Howard ...
Bharat Khatri's user avatar
5 votes
1 answer
231 views

Polymorphism restriction on lambda-bound variables in HM

I'm trying to implement the Hindley-Milner type system, following Milner 1978, "A Theory of Type Polymorphism in Programming" (link). In the Hindley-Milner system, a polymorphic let-bound expression ...
feersum's user avatar
  • 313
5 votes
1 answer
376 views

Why injection into sum type apparently leads to ambiguity?

I have been reading Benjamin Pierce's Types and Programming Languages, plus a couple of course notes on type systems and typed $\lambda$-calculus, and there is one thing I don't get: it seems that ...
josh's user avatar
  • 331
5 votes
1 answer
223 views

What's the advantage of "value restriction" over its alternatives?

What is the motivation to pick "value restriction" over other candidates? Examples of alternatives: Enclosing pureness into the function type, for example: ...
weakish's user avatar
  • 151
5 votes
1 answer
208 views

Does Damas-Milner still have principal types if existential type schemata are added?

In the Damas-Milner type system, type schemata can be formed in two ways: $T$ $\forall X. S$ Where $T$ ranges over monotypes and $S$ ranges over type schemata. The type-checking algorithm for this ...
isekaijin's user avatar
  • 405
5 votes
1 answer
120 views

Local type argument synthesis when type variable does not appear in arguments

I am implementing the techniques described in the classic Local Type Inference paper. Specifically, I am implementing the type argument synthesis algorithm from section 3. My algorithm seems to ...
Alexis King's user avatar
5 votes
1 answer
227 views

Free variables in constraint-typing derivation?

In Types and Programming Language's constraint typing rules (Figure 22-1), is it possible for any part of the typing derivation to contain free type variables that aren’t part of the fresh variables? ...
Joshua Grosso's user avatar
5 votes
1 answer
122 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 ...
Charlie Parker's user avatar
5 votes
1 answer
277 views

Hindley-Milner type inference for language with implicit type casting

I've only implemented the HM algorithm on a small academic language with a few primitive types and functions. In that case, the unification algorithm would return a type error if two different ...
jeanluc's user avatar
  • 227
5 votes
1 answer
85 views

Is dependency analysis required in order to type a program?

I have seen stated in various places that in order to allow an "increase in polymorphism," functional dependency analysis should be performed, and type inference should be used for every declaration ...
Bakuriu's user avatar
  • 807
5 votes
0 answers
603 views

Hindley-Milner: How do I separate constraint generation and unification phases in Algorithm W when inferring types of patterns?

I am self-teaching myself Hindley-Milner type inference by writing my own implementation, separating tree traversal and constraint solving. The tutorials that I've been following only allow patterns ...
Del's user avatar
  • 223
4 votes
3 answers
1k views

How can SML infer types like this?

Wikipedia says: fun factorial n = if n = 0 then 1 else n * factorial (n-1) A Standard ML compiler is required to infer the static type int -> int of this ...
Xodarap's user avatar
  • 1,538
4 votes
3 answers
349 views

What is the runtime/time complexity of Coq’s (Dependent) Type Inference?

I remember learning in a class that type inference is decidable but usually takes a long time (e.g. type inference in OCaml is EXPTIME). I was wondering, since Coq allows programs/values themselves to ...
Charlie Parker's user avatar
4 votes
2 answers
440 views

In Hindley-Milner system, how can I prove that let id=\x.x in id id is well-typed?

I am trying to infer the type and prove that this is well-typed: let $f =\lambda x.x$ in $f f$ Obviously the $f$ is the identity function, so it's the same as let $id =\lambda x.x$ in $id$ $id$ I ...
MiragePV's user avatar
4 votes
1 answer
316 views

Meaning of type inference rule for abstraction in lambda-calculus

Below is a snippet about simply typed lambda-calculus from CS152: Programming Languages Lecture 9 | Simply Typed Lambda Calculus, on printed‑page 15, indexed 23. $$ \frac {\Gamma, x: \tau_1 \vdash e: ...
Hibou57's user avatar
  • 233
4 votes
1 answer
98 views

Which language is used to construct a type system?

Typically, OCaml and Scala seem to be used for designing any programming languages tool. But what features offer them an edge over other languages. A related question, is a type system for a language ...
mythbuster's user avatar
4 votes
1 answer
422 views

Type Inference and Generalization

I've been trying to understand type inference for Hindley-Milner-based languages, and I'm struggling to understand how generalization works. Let's say I have the following program in Haskell: ...
user1502040's user avatar
4 votes
1 answer
327 views

Typing rule for binding groups

In "Typing Haskell in Haskell", by Mark P. Jones, is provided a sort of haskell-like specification for typing Haskell. As stated in this paper, binding groups is a area "neglected in most theoretical ...
Rafael Castro's user avatar
4 votes
0 answers
228 views

Updating types during type inference in a Hindley-Milner type system

I'm looking at implementing type inference for a Hindley-Milner type system, and before I have even started to implement the Damas-Milner algorithm, while working through some examples, I hit some ...
beta's user avatar
  • 141
3 votes
2 answers
303 views

Which type compilers report if they cannot infer a precise type?

In the presence of subtyping, a type checker can usually infer only some inequality constraints on the type rather than the exact type. Of course, internally it will store the full constraints. But ...
max's user avatar
  • 381
3 votes
1 answer
263 views

Curry-Howard, void, and type checking in Haskell

I am trying to understand an example of theorem proving via type checking in Haskell given here. The example is as follows. Using the Curry-Howard isomorphism, construct an inhabitant of the type and ...
Tonita's user avatar
  • 565
3 votes
1 answer
124 views

How to statically type polymorphic lambdas using hindley milner style type inference

I am playing with a simple implicitly typed functional language and have implemented type checking using a Hindley Milner style system. In order to guide code generation, I want to tag each term with ...
Johannes Luong's user avatar
3 votes
1 answer
268 views

Assertion of Type Inference Rules/Type Checking

I have a problem in a book I am trying to accomplish. I understand the overall type of the expression is boolean and how it derives. (y * x) will be rule 4 (counting from top right). (y * x) + x when ...
Frank Duckworth West's user avatar
3 votes
2 answers
198 views

How does a compiler infer a value's type?

From A Swift Tour — The Swift Programming Language (Swift 5): var myVariable = 42 myVariable = 50 let myConstant = 42 A constant or variable must have the same ...
Curious's user avatar
  • 273
3 votes
2 answers
2k views

Lambda Calculus Type Inference

I'm currently trying to learn how to infer most general types on lambda calculus, and due to the lack of information on the subject I could find on Google I'm forced to attempt what I think is logical ...
Chapi's user avatar
  • 55
3 votes
2 answers
947 views

System f-sub, how to do type checking?

I was reading that system f-sub (polymorphic lambda calculus with sub-typing) and I was quite confused with its one checking rule called "T-TAPP". This rule as following (ctx denotes the typing ...
alim's user avatar
  • 994
3 votes
1 answer
337 views

Top-down typing strategy - is there a name for this?

In most statically typed languages, each expression has an intrinsic type. E.g. in Java, 3 is an int, 3.0 is a double, ...
Bernát's user avatar
  • 131
3 votes
1 answer
311 views

Is the type inference here really complicated?

There's a question on SO asking why in Java the right type doesn't get picked in a concrete case. I know that Java can't do it in such "complicated" cases, but I'm asking myself WHY? The (for ...
maaartinus's user avatar
3 votes
2 answers
177 views

Get term type during evaluation using Hindley-Milner type system

I've implemented a lambda calculus evaluator and use the Hindley-Milner algorithm to infer terms types and ensure type correctness without the user having to explicitly annotate types. But now I'd ...
Juan's user avatar
  • 755
3 votes
1 answer
424 views

ML - Type Interface

From my recitation class - Can you please explain why does operator $"+"$ signature is $ int \rightarrow (int \rightarrow int)$ ? How does this graph is build ? And what is mean $t=u \...
URL87's user avatar
  • 765
3 votes
1 answer
272 views

Partial type inference for dependent types

I'm looking for resources on (partial) type inference for dependent types. For example there could be a type inference scheme that fails if the term doesn't have a principal type, or a scheme that ...
fread2281's user avatar
  • 161