Questions tagged [type-inference]

The tag has no usage guidance.

23 questions with no upvoted or accepted answers
Filter by
Sorted by
Tagged with
10
votes
0answers
490 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 ...
8
votes
0answers
280 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 ...
4
votes
0answers
360 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 ...
4
votes
0answers
207 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 ...
3
votes
0answers
155 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 ...
3
votes
0answers
32 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 ...
3
votes
0answers
795 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: ...
2
votes
0answers
37 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 ...
2
votes
0answers
87 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 ...
2
votes
0answers
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 ...
2
votes
0answers
152 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 ...
2
votes
0answers
35 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 ...
2
votes
0answers
26 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 ...
1
vote
0answers
87 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 ...
1
vote
0answers
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: ...
0
votes
0answers
24 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 ...
0
votes
0answers
18 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. ...
0
votes
0answers
65 views

Consistency of a set of bidirectional typing rules

Main Is there any way to algorithmically check the consistency of a set of bidirectional typing rules, e.g. the absence of cycles and the uniqueness of the derivation tree? This problem is naturally ...
0
votes
1answer
36 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 ...
0
votes
0answers
56 views

Is there some place I can find an implementation of the Cartesian Product Algorithm for Type Inference?

Where can I find an implementation of the cartesian product algorithm for type inference? (Preferably in Python/C++, but any language would really do) I've searched the internet many times but there ...
0
votes
0answers
41 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 ...
0
votes
0answers
437 views

Type inference and Type checking

I understand that adding the annotations (dependent typing) may cause the type checking of the programming language to become undecidable. What about type inference ? Whether type checking and type ...
0
votes
0answers
75 views

Type inference example?

In my programming languages course we are reviewing type inference, i didnt get very well how to make this task. I all ready search at the bibliography of my course (PLAI by Shriram krishnamurthi) ...