Questions tagged [type-inference]
The type-inference tag has no usage guidance.
88
questions
0
votes
1
answer
63
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 ...
CommunityBot
- 1
5
votes
1
answer
346
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 ...
- 5,002
0
votes
0
answers
18
views
What is the general flow of the type inference algorithm in these cases where there is very little type information?
For a state of the art compiler, can they successfully do type inference on all of these cases, or are there some in which they can't? If there is a place which collects a bunch of test cases which a ...
- 1,873
0
votes
1
answer
42
views
How to think about typing inference rules when thinking about typechecking?
I am trying to build an imperative programming language with a type system that will allow for proofs. I just found kind lang, which implements all the ideas that I have been meaning to use (plus more)...
- 28.1k
2
votes
1
answer
126
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 ...
- 5,002
5
votes
1
answer
131
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? ...
- 5,002
4
votes
3
answers
135
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 ...
- 7,744
2
votes
0
answers
76
views
What is the runtime (time complexity) of Type Inference in Simply Typed Lambda Calculus?
I was told that the runtime of OCAML or Scala is EXPTIME - which seems really bad! However, since people use type inference (deciding the type of a term or program or expression) in practice - it must ...
- 2,910
0
votes
0
answers
41
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 ...
- 1
2
votes
0
answers
50
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 ...
0
votes
0
answers
30
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 ...
- 219
3
votes
1
answer
53
views
Annotated type system problem about conditional branch
I am reading the book "Principle of Program Analysis" by Flemming Nielson for annotated type systems. In the first chapter, section 1.6 they mentioned the simple type system for various ...
- 151
4
votes
1
answer
81
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 ...
- 29.1k
0
votes
0
answers
21
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. ...
- 146
3
votes
1
answer
166
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 ...
- 555
2
votes
1
answer
80
views
Type-checking function calls with functional subtyping
I'm relatively new to the topic. Suppose that you want to type-check an expression of the form f(a), i.e. a function call. Assuming that all the declarations are ...
- 2,050
26
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 ...
2
votes
0
answers
44
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 ...
- 21
1
vote
1
answer
68
views
Type inference with overloading
I am working on a type system supporting overloading. I have a rough idea of how type inference is usually implemented in such a scenario, but I am wondering how - after type inference is completed - ...
- 28.1k
5
votes
2
answers
614
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 ...
- 141
2
votes
1
answer
57
views
Type inference with imports
I understand how a type inference algorithm infers types within a single file by building on top of already inferred types and identified constraints (e.g. in the Hindley-Milner type system).
I am ...
- 28.1k
2
votes
1
answer
76
views
Hindley-Milner system with let expansion
I'm reading these slides that present Hindley-Milner type inference. In the system HM, we have the following let rule:
$\dfrac{\Gamma \vdash t:S \;\; \Gamma,x:S \vdash t':T }{\Gamma \vdash \text{let} ...
- 7,744
2
votes
0
answers
129
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 ...
- 21
2
votes
2
answers
77
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 ...
- 794
1
vote
1
answer
160
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 ...
- 2,050
5
votes
1
answer
104
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 ...
- 340
6
votes
1
answer
570
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 "...
CommunityBot
- 1
0
votes
0
answers
43
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 ...
- 593
2
votes
0
answers
43
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 ...
- 121
3
votes
0
answers
226
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 ...
- 535
2
votes
0
answers
155
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 ...
- 479
3
votes
0
answers
40
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 ...
- 207
2
votes
0
answers
116
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 ...
CommunityBot
- 1
3
votes
2
answers
132
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 ...
- 4,108
1
vote
1
answer
61
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 ...
- 24.9k
5
votes
2
answers
474
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\ ...
3
votes
1
answer
115
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 ...
- 133
2
votes
0
answers
37
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 ...
- 121
2
votes
0
answers
29
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 ...
- 27
4
votes
1
answer
281
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 ...
- 14.1k
5
votes
1
answer
325
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:
...
- 499
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?
...
- 24.9k
5
votes
1
answer
225
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 ...
- 227
1
vote
2
answers
144
views
Symbolic Evaluation for Type Inference in a Dynamic Language
Say I have the following contrived example code:
...
- 227
4
votes
2
answers
338
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 ...
10
votes
0
answers
649
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 ...
- 3,107
3
votes
1
answer
201
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 ...
5
votes
0
answers
447
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 ...
- 223
48
votes
1
answer
7k
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 ...
- 7,744
2
votes
1
answer
48
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 ...
- 70.8k