Questions tagged [type-inference]

The tag has no usage guidance.

Filter by
Sorted by
Tagged with
7 votes
3 answers
606 views

Example of a term in system F which is not typable in the simply typed lambda calculus

What is the simplest possible example of a (correctly typed) term in system F that does not correspond to any correctly typed term in the simply typed λ-calculus? More precisely, I am looking for a ...
Gro-Tsen's user avatar
  • 841
4 votes
1 answer
150 views

Free type variables in Hindley-Milner type inference

I'm trying to understand how generalization works in H-M type inference. In order to generalize a function, we: Collect all the free type variables in the type of the function body, Subtract away any ...
Brian Berns's user avatar
9 votes
3 answers
535 views

"Spurious" Type Equivalences in MLSub/Algebraic Subtyping

I have been reading up on Stephen Dolan's "Algebraic Subtyping" in his PhD thesis and also the ICFP 2020 Paper "The simple essence of algebraic subtyping..." by Lionel Parreaux and ...
Max New's user avatar
  • 1,663
11 votes
1 answer
701 views

Swapping arguments of variables in higher-order pattern unification

Pattern unification is a simplified form of higher-order unification in which existential variables only appear applied to distinct universal variables. Thus, for instance, an equation such as $M \,x\...
Mike Shulman's user avatar
3 votes
1 answer
194 views

Counterexample request: ill-scoped metavariable solution

This is a question on metavariable (aka holes) resolution in (dependent) type theories. In many referential implementations (such as Andras Kovacs' elaboration-zoo), there is one step called 'scope ...
ice1000's user avatar
  • 965
3 votes
2 answers
255 views

Bidirectional typing for dependent types: Why are Sigma, Pi synthesized?

According to the Pfenning philosphy of bidirectional typing, as also explained by Dunfield and Krishnaswamy 2013, constructors should be checked, while eliminators should be synthesized. Cconvention ...
Siddharth Bhat's user avatar
8 votes
2 answers
335 views

Does the Hindley-Milner type system (i.e. STLC with prenex polymorphism) have a category-theoretic model?

It is well known that any CCC (cartesian closed category) is a model of the simply-typed $\lambda$-calculus. It is less well known that System F admits a categorical model, but it is also well studied ...
xrq's user avatar
  • 1,175
6 votes
1 answer
240 views

Decidability of rank-k polymorphism vs. System F

There's a paper by Kfoury from 1992, "Type Reconstruction in Finite Rank Fragments of the Second-Order $\lambda$-Calculus", that proves that type inference for Curry-style rank-$k$ polymorphic lambda ...
ionchy's user avatar
  • 325
1 vote
0 answers
59 views

A substitution to add variables in the context

I'm doing type-inference in a dependently typed language, using (as is commonly done) a λ-calculus with explicit substitutions like that of Abadi (with a representation based on debruijn indices) in ...
Stefan's user avatar
  • 390
6 votes
1 answer
169 views

Conservative Approximation of Kleene-Mycroft Iteration for Polymorphic Recursion?

To perform type inference in the presence of polymorphic recursion, one can use a Kleene-Mycroft iteration to compute the principal type of an expression. To type $\mathsf{fix}\ f\ldotp e$, we define $...
Joey Eremondi's user avatar
3 votes
1 answer
164 views

Verified type checkers

Most of the work on programming language metatheory mechanization focus on the declarative properties of the languages (e.g., type soundness), but fail to address the algorithmic side, i.e. the type ...
xrq's user avatar
  • 1,175
10 votes
1 answer
494 views

Can Isorecursive types capture mutually recursive data types?

I've been reading TAPL, and reached the section on recursive types. I understand the type operator $\mu$. For example, the two type expressions are equivalent ...
Enrico Borba's user avatar
4 votes
2 answers
528 views

Extending Hindley-Milner to type mutable references

I have been trying to implement a programming language from scratch, and have gotten reasonably far. It reads just like Python, other than the fact that let is used ...
Enrico Borba's user avatar
3 votes
1 answer
375 views

Universe polymorphism: the inference of universes and their constraints

When making a universe polymorphic definition in Coq, universes and their constraints are automatically inferred. Are they somewhat the most general ones (in a sense similar to the principal type ...
Bob's user avatar
  • 381
6 votes
1 answer
286 views

General Induction Principle

Let us suppose that we want to provide for each inductive type an axiom describing the associated elimination/induction principle. For example, given a definition for the naturals: ...
jackb's user avatar
  • 175
10 votes
2 answers
460 views

Decidability of type inference and type checking in MLTT

In Martin-Löf's An Intuitionistic Theory of Types: Predicative Part it is proved that type checking $a \colon A$ is decidable subject to $a$ being typeable in the first place, by proving a ...
Josh's user avatar
  • 203
7 votes
1 answer
464 views

Avoiding Cycles with Unification and Subtyping

Context I realize that subtyping often doesn't admit principle types, and that inference in the presence of subtypes is undecidable. I'm working in a context where typechecking should simply fail ...
Joey Eremondi's user avatar
10 votes
1 answer
2k views

What is the difference between System F and Hindley-Milner type system?

Hindley-Milner type system is some restriction of System F, which allows type inference. But from simple descriptions I cannot see, what is the difference between them?
uhbif19's user avatar
  • 305
13 votes
3 answers
1k views

What should a proof of correctness for a typechecker actually be proving?

I've been programming for several years, but am very unfamiliar with theoretical CS. I've recently been trying to study programming languages, and as part of that, type checking and inference. My ...
Vivek Ghaisas's user avatar
6 votes
1 answer
371 views

Recursive types and the empty type

In John Mitchell's book "The Foundations of Programming Languages", he considers a typed lambda calculus with unit, exponential, product, (binary) coproduct types, and arbitrary recursive types (p126)....
Andrew Bacon's user avatar
7 votes
2 answers
338 views

Efficiently ordering typed programs

Sometimes it is useful to enumerate in increasing order programs that have a given type. A simple example is test generation for compilers: we want to test a new optimising phase and are ...
Martin Berger's user avatar
10 votes
2 answers
520 views

Higher-rank polymorphism over unboxed types

I have a language in which types are unboxed by default, with type inference based on Hindley–Milner. I’d like to add higher-rank polymorphism, mainly for working with existential types. I think I ...
Jon Purdy's user avatar
  • 353
11 votes
2 answers
938 views

Subtypes as subsets of SML datatypes

One of the few things that I dislike about Okasaki's book on purely functional data structures is that his code is littered with inexhaustive pattern matching. As an example, I'll give his ...
isekaijin's user avatar
  • 501
2 votes
0 answers
44 views

Abduction in a Herbrand Constraint System

I have a simple constraint system with a finite set $C$ of constant symbols, an infinite set $V$ of variables, and two relation symbols - $R_1$, a preorder, and $R_2$, an equivalence relation. ...
Gowtham Kaki's user avatar
7 votes
1 answer
390 views

Decidability of parametric higher-order type unification

I'm making a language that has higher-kinded types (like Haskell) and allows type synonyms to appear partially applied in type expressions (unlike Haskell). As an example, consider the following ...
isekaijin's user avatar
  • 501
5 votes
1 answer
658 views

Can all linear lambda calculi be linearity checked syntactically?

Given a lambda calculus with explicit linearity and usual application and abstraction, can the linearity check be done on an untyped syntax tree if we keep track of the structural types? Are the ...
Gus O'Hanley's user avatar
1 vote
1 answer
70 views

Why is the polymorphic weight 1

I am reading through through a paper called HMF: Simple Type Inference for First-Class Polymorphism by Daan Leijen of Microsoft Research. In the paper it describes how to calculate the polymorphic ...
t123's user avatar
  • 121
7 votes
1 answer
383 views

Can type inference be classified in two groups: unification-based and control-flow-based?

I recently came across the 1995 paper Safety analysis versus type inference (pdf link) by Palsberg and Schartzbach that contrasts unification-based type inference and static analysis methods based on ...
hugomg's user avatar
  • 173
5 votes
1 answer
574 views

Is this behavior in a programming language inconsistent?

I'm developing a tiny programming language to try to wrap my head around type inference, and I'm trying to figure out if its behavior makes sense or not. Here's the problem: The identity function <...
Benjamin Kovach's user avatar
8 votes
1 answer
1k views

Practical implementation of Hindley–Milner with typeclasses — matching vs most general unifier

I'm trying to get a deep understanding of a (great) paper "Typing Haskell in Haskell". I'm having difficulties understanding the implementation of two methods there — the ...
kgadek's user avatar
  • 211
4 votes
1 answer
795 views

Generalization and instantiation of types in Hindley-Milner type inference

I’m currently reading Heeren, B., Hage, J., & Swiestra, D. (2002). Generalizing Hindley-Milner Type Inference Algorithms in an attempt to understand Hindley-Milner-style type inference. I'm ...
beta's user avatar
  • 293
3 votes
1 answer
932 views

Occurs check in type inference

I'm reading about type inference in chapter 30 of Programming Languages: Application and Interpretation and I'm trying to understand exactly how the occurs check works in an example I came up with. ...
beta's user avatar
  • 293
22 votes
1 answer
1k views

What are the practical issues with intersection and union types?

I'm designing a simple statically typed functional programming language as a learning experience. It appears that the type system I have implemented so far could (with a little extra work) ...
mikera's user avatar
  • 323
10 votes
1 answer
607 views

A simple proof that decidability of typability in System F ($\lambda 2$) implies decidability of type checking?

Suppose we don't know Joe B. Wells's result from 1994 that both typability and type checking are undecidable in System F (AKA $\lambda 2$). In Barendregt's Lambda calculi with types (1992) I found a ...
Petr's user avatar
  • 2,581
0 votes
1 answer
138 views

How to generalize a map of type for many operators?

I am formalizing the type system for a small language, and thus writing inference rules. Taking unary - operator for example, its entry may be a number as well as ...
SoftTimur's user avatar
9 votes
2 answers
413 views

Research on call-site based type inference?

I'm trying to learn more about whole-program type checking and type inferencing systems that use information from function call sites to compute type information (in addition to the standard approach ...
Derek Thurn's user avatar
12 votes
3 answers
2k views

Type inference for imperative statements other than assignment

In my search for research papers about type systems for imperative languages, I only find solutions for a language with mutable references but without genuine imperative control structures such as ...
nponeccop's user avatar
  • 301
9 votes
1 answer
573 views

What is the role of the Bicolored Calculus of Constructions?

So, I'm reading a bit about elaboration, particularly, algorithms based on the Bicolored Calculus of Construction, and I'm a bit confused. I don't understand what exactly the purpose of the $CC^{bi}$ ...
Anthony's user avatar
  • 710
5 votes
2 answers
439 views

the type system does not tell the whole story due to "exception"

I am wondering whether it is a bad style to use "exception". For example, in Ocaml, the exception does not appear as the .mli file. So it appears to me that "exception" is something that cannot be ...
zell's user avatar
  • 265
7 votes
1 answer
364 views

Implications of the rule of cumulativity in the Calculus of Constructions

Please help me understand some type theory research. As suggested in "Type Checking with Universes" by Robert Harper and Robert Pollack, we can add the following rule to our otherwise standard COC or ...
Anthony's user avatar
  • 710
6 votes
2 answers
701 views

With equirecursive types are there downsides to making all types potentially recursive?

By this I mean to ask, is it a bad idea to have all type constructor term expressions abstracted with $\mu$ just in case they need to be recursive? For example, $Bool : Type;$ $Bool = (\mu Bool' ...
Anthony's user avatar
  • 710
26 votes
2 answers
2k views

Context Sensitive Grammars and Types

1) What, if any, is the relationship between static typing and formal grammars? 2) In particular, would it be possible for a linear bounded automaton to check whether, say, a C++ or SML program was ...
Diogenes Creosote's user avatar
5 votes
1 answer
178 views

Nested automatization of type inference of forall elimination

Following a previous question about how to automatize the type inference in a forall elimination of an application, now suppose we want to do the same but for a nested forall, say $(\Lambda X_1.\...
Alejandro DC's user avatar
9 votes
1 answer
470 views

In System F à la Church, can we automatize type inference for the for-all elimination?

The question is the following. Generally when one have a term like $\Lambda X.t$, we can eliminate the forall by applying this term to a type, as instance $(\Lambda X.t)[T]\to t[X:=T]$. Now, suppose ...
Alejandro DC's user avatar
8 votes
0 answers
439 views

Type inference with subtype constraints and polymorphism using Trifonov and Smith's constraint maps

Trifonov and Smith's Subtyping Constrained Types (1996) introduces constraint maps to represent consistent closed constraint sets (such maps providing sets of lower and upper bounds to each variable ...
sclv's user avatar
  • 1,379