# Questions tagged [type-inference]

The tag has no usage guidance.

23 questions with no upvoted or accepted answers
Filter by
Sorted by
Tagged with
579 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 ...
297 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 ...
422 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 ...
211 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 ...
203 views

### Type inference for System F-omega

There have been some nice papers about simple type inference for System F: "HMF: Simple Type Inference for First-Class Polymorphism", "Practical type inference for arbitrary-rank types", and "Complete ...
36 views

### Is the expression (λx.xx)(λy.y) typeable in the following system?

We are given a simple functional language: $e ::= x | n | e_{1}e_{2}|\lambda(x:\tau).e$ with types: $\tau ::= \text{int} | \tau_{1} \rightarrow \tau_{2}| \tau_{1} \land \tau_{2}$ Is the ...
826 views

### Row polymorphism, union and intersection types

It seems that row polymorphism with union types can be used in dynamic languages to approximate overloading, e.g. given the following python function: ...
42 views

### Understanding least common generalization (or anti-unification) of types

I am learning how to extend a basic Hindley-Milner type system to support overloaded variables by following Geoffrey Seward Smith's dissertation. The proposed type inference algorithm makes use of the ...
40 views

### Substitution of monomorphic type variables in generalized Hindley–Milner

I am trying to understand the constraints-based Hindley–Milner type inference algorithm described in the Generalizing Hindley-Milner paper. The function $\text{S}\small{\text{OLVE}}$ is defined as ...
112 views

### How could 'Complete and Easy Bidirectional Type Checking' handle invariant parameters on type constructors

The paper Complete and Easy Bidirectional Typechecking for Higher-Rank Polymorphism provides examples for checking if one function type is a subtype of another, which I think demonstrates checking ...
41 views

### Real world example of contraction and weakening

Can you provide me a real world example of contraction and weakening in the type system of a popular language like Java, Kotlin, etc.? I heard that Rust has got explicit contraction but I don´t ...
153 views

### Proving that the failure of algorithm W implies that the program is not typable

How one does prove that if algorithm W failed for a given program $e$ and context $\Gamma$, then there is no substitution $S$ and type $\tau$ such that $S\Gamma \vdash e : \tau$ ? The original paper ...
36 views

### Question about let syntax in type systems

I'm on the Wikipedia page for Hindley-Milner type systems, on the section about "let polymorphism": https://en.wikipedia.org/wiki/Hindley%E2%80%93Milner_type_system#Let-polymorphism I'm a bit ...
28 views

### How does the free program identifiers (fpi) extend over constraints and type schemes in $HM(X)$?

Chapter 10 of Advanced Topics in Types and Programming Languages; gives a very comprehensive description of type inference by constraints solving. They introduce the free program indentifiers of an ...
107 views

### Is it possible to write a fully-decidable type system for the J language?

I'm experimenting with the J array language, a dynamically-typed array language with mutable assignment, subtyping, and function overloading (just like traditional APL). It is unclear to me whether ...
2k views

### How does C# do type inference?

Sometimes the C# compiler can do some type inference when you have to specify the generic parameters of some methods, like: ...
35 views

### Is there a static type system (implemented or not) that can detect ignored parameters and re-type them to increase generality?

I came across this question while playing with the SKI combinators. (Skip to the bottom for the question, if you don't care about the motivation.) You can implement the combinators in Haskell as ...
28 views

### Is type unification a kind of search for alpha equivalence?

I was reading about type unification and it moves through of substitution of variables. To me it looks like a search for an alpha equivalence... I mean, two types are unifiable if they are alpha ...
19 views

### RDF | If something is a rdfs:subClassOf of :Q can you infer it is also rdf:type :Q?

Given: :P rdfs:subClassOf :Q Can you infer the following?: :P rdf:type :Q I do not think you can, but I am not fully sure. ...
56 views

### Inference and Unification algorithm provided to a Unification graph of two expressions

I am trying to unify two expressions given a unification algorithm $unify$ applied to the unification graph of the two expressions. However, I struggle a lot in understanding how exactly the steps of ...
42 views

### Inferring the type of (f .) in Haskell

If we have the following in Haskell: f x y = x + y :type f f :: Num a => a -> a -> a then GHC would report ...