Questions tagged [type-inference]
The type-inference tag has no usage guidance.
69
questions
2
votes
2answers
36 views
Are type variables really only used in mathematical conversation about types?
Are type variables really only used in mathematical conversation about types? i.e. are type variables (meta-variables that only contain the type classification label) only exist in proofs for types ...
0
votes
1answer
56 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 ...
5
votes
1answer
73 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 ...
6
votes
1answer
530 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 "...
0
votes
0answers
32 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 ...
2
votes
0answers
37 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 ...
3
votes
0answers
87 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 ...
2
votes
0answers
150 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
26 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 ...
1
vote
0answers
51 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 ...
2
votes
2answers
85 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 ...
1
vote
1answer
34 views
Add type checking/inference to my programming language
I am currently creating my own compiled programming language, and I have come to a point where I would like to start working on the type system and introduce some type checking. Ideally I would like ...
4
votes
2answers
136 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\ ...
Gilles 'SO- stop being evil'
37.4k7 gold badges100 silver badges166 bronze badges
0
votes
0answers
35 views
Projection operator for constraints
I was looking at HM(X) framework, Hindley-Milner parameterized by a constraint system X, and I was struggling to understand what does the projection operator $\exists \alpha$ does for a constraint. ...
3
votes
1answer
75 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 ...
1
vote
1answer
51 views
Isoecursive Types When to Fold and Unfold
I'm trying to implement recursive types into my programming language. I've implemented extensible rows and was hoping to add some recursive typing in order to get something like ...
2
votes
0answers
32 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
25 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 ...
4
votes
1answer
177 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 ...
3
votes
1answer
299 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:
...
5
votes
3answers
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?
...
5
votes
1answer
117 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 ...
1
vote
2answers
98 views
Symbolic Evaluation for Type Inference in a Dynamic Language
Say I have the following contrived example code:
...
3
votes
2answers
185 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 ...
Gilles 'SO- stop being evil'
37.4k7 gold badges100 silver badges166 bronze badges
10
votes
0answers
336 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 ...
2
votes
1answer
119 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 ...
22
votes
1answer
2k 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 ...
4
votes
0answers
210 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 ...
42
votes
1answer
5k 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 ...
2
votes
1answer
45 views
Typing by value
I wondered if there was a generalized name for typing a variable by assigning a specific value to it. For instance
a = 4
This would make the variable ...
1
vote
0answers
1k 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:
...
2
votes
2answers
29 views
Inferring used fields in return type
A common issue in app development is avoiding over-fetching of data, such as in this naive (pseudocode) example:
...
3
votes
2answers
494 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 ...
4
votes
1answer
82 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:
...
4
votes
1answer
256 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:
...
3
votes
1answer
132 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 ...
8
votes
0answers
249 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 ...
8
votes
2answers
866 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 ...
3
votes
2answers
288 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 ...
5
votes
1answer
97 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 ...
5
votes
1answer
186 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 ...
1
vote
1answer
142 views
Comparison Procedure in Robinson's Unification Algorithm
I'm studying the Principal Type (PT) Algorithm in Basic Simple Type Theory by J. Roger Hindley.
One step to find the PT of a term is the Unification of types. The Robinson's Unification Algorithm uses ...
11
votes
3answers
962 views
Automatic Downcasting by Inferring the Type
In java, you must explicitly cast in order to downcast a variable
...
2
votes
2answers
1k 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 ...
Gilles 'SO- stop being evil'
37.4k7 gold badges100 silver badges166 bronze badges
8
votes
1answer
196 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 ...
3
votes
2answers
137 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 ...
5
votes
1answer
175 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 ...
3
votes
2answers
425 views
The Hindley-Milner type system plus polymorphic recursion is undecidable or semidecidable?
I have often read that Hindley-Milner extended to allow polymorphic recursion is undecidable. However is the term used what is actually meant? Or do people actually mean semidecidable when they ...
6
votes
1answer
176 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 ...
9
votes
2answers
958 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 ...
Gilles 'SO- stop being evil'
37.4k7 gold badges100 silver badges166 bronze badges
