24 votes
Accepted

Automatic Downcasting by Inferring the Type

Upcasts always succeed. Downcasts can result in a runtime error, when the object runtime type is not a subtype of the type used in the cast. Since the second is a dangerous operation, most typed ...
user avatar
  • 14.2k
12 votes
Accepted

Relation between type-checking decidability, typability decidability and strong normalization

I'll give a more focused and technical answer to Martin's. If we're interested in dependent type theories, then neither direction is obvious, but both are generally assumed to hold. However the ...
user avatar
  • 7,744
9 votes
Accepted

Relation between Type Assignment system (TA) and Hindley-Milner system

System F and its subsystem HM have a type former for universal quantification: $$ \tau \quad::=\quad \forall x.\tau \ |\ ... $$ which the system in Hindley/Seldin doesn't have. That is the key ...
user avatar
9 votes
Accepted

Type inference + overloading

I would suggest looking at Geoffrey Seward Smith's dissertation As you probably already know, the way the common type inference algorithms work is that they traverse the syntax tree and for every ...
user avatar
  • 1,604
9 votes

Why isn't the Swift programming language type inference more aggressive?

I don't understand Swift's typing system yet, so I can only speculate, but I imagine that it's for the same reason that Scala doesn't have full type inference: nobody knows how to do it in a ...
user avatar
9 votes
Accepted

Drawbacks of adding type equality to 1ML

Your proposal is an instance of a general design pattern for type systems that some would call a design smell: whenever you are stuck on an inference constraint that you cannot solve, or cannot solve ...
user avatar
  • 499
8 votes

Why isn't the Swift programming language type inference more aggressive?

I must admit I don't know Swift yet, but here are my thoughts. Putting some type annotations in here and there really helps produce better type error messages. Return types and arguments are a great ...
user avatar
  • 546
8 votes
Accepted

Check if a lambda constructor is well-typed

A term $M$ is well-typed if and only if there is a type derivation that leads to a judgement of the form $\Gamma \vdash M : \tau$ for some context $\Gamma$ and some type $\tau$. (I use the word “type” ...
user avatar
7 votes

What are the strongest known type systems for which inference is decidable?

[EDIT: Voilà a few words on each] There are several ways of extending HM type inference. My answer is based on many, more or less successful, attempts at implementing some of them. The first one I ...
user avatar
  • 179
7 votes

Check if a lambda constructor is well-typed

No, that term can not be typed in Hindley Milner, or any other "standard" type system. Here's a rough sketch of a proof. Suppose by contradiction it had a type. Since type is preserved under beta ...
user avatar
  • 14.2k
7 votes

What is the runtime/time complexity of Coq’s (Dependent) Type Inference?

There are actually two questions here. Is the Coq type system decidable? Long answer short, we hope so, as in it would be a bug if it were not. It is not a universal requirement for a type theory to ...
user avatar
6 votes

Why injection into sum type apparently leads to ambiguity?

I think the key point here is $\sigma$, $\tau$ and $\phi$ are type variables, and not specific types. So, what the typing rule for $\operatorname{inl}$ says is that $\operatorname{inl} M$ is of type $\...
user avatar
  • 1,846
6 votes
Accepted

Polymorphism restriction on lambda-bound variables in HM

Yes, you are restricting it too much. The second code is perfectly fine. For the record, Haskell has no issue with your code: ...
user avatar
  • 14.2k
6 votes
Accepted

Which type compilers report if they cannot infer a precise type?

It is important to keep in mind that this is a question about human-computer interaction and not about compilers. As far as the machine is concerned, the constraints are the constraints, and the ...
user avatar
  • 28.4k
6 votes
Accepted

In Hindley-Milner system, how can I prove that let id=\x.x in id id is well-typed?

If I understand you question correctly, you are wondering how the typing judgment $f : \forall \alpha. \alpha \to \alpha \vdash f\;f : \beta$ can be proved, where $\beta$ is some (yet unknown) type. ...
user avatar
6 votes
Accepted

Curry-Howard, void, and type checking in Haskell

I would find a different tutorial because the author of that one is fundamentally confused. They wrongly claim that $\neg a$ and $\bot\to a$ are equivalent ($a\to\bot$ would be correct), and also ...
user avatar
  • 1,451
5 votes
Accepted

Does Damas-Milner still have principal types if existential type schemata are added?

Yes, adding existentials doesn't add many complications for type inference, if quantifier alternation is controlled carefully. This is not surprising since universals and existentials are dual and the ...
user avatar
5 votes

The Hindley-Milner type system plus polymorphic recursion is undecidable or semidecidable?

The answer you gave is right, but I'd like to stress the relationship between the two terms. A formal language is decidable if and only if there exists an algorithm which correctly accepts or rejects ...
user avatar
  • 51
5 votes
Accepted

Meaning of type inference rule for abstraction in lambda-calculus

The problem is that whatever the context $\Gamma$ may imply about the variable $x$ is irrelevant. This rule is intended to type a $\lambda$-abstraction, and the variable $x$ may be changed to another ...
user avatar
  • 19.1k
5 votes
Accepted

Equivalence of data-flow analysis, abstract interpretation and type inference?

Data flow analysis and type inference are specific instances of abstract interpretation. Data flow analysis and abstract interpretation look similar since they are both about computing a fix point. ...
user avatar
  • 1,604
5 votes

What's the advantage of "value restriction" over its alternatives?

I'm sure that this isn't the only advantage, but I think the primary advantage is simplicity. This is even identified in the original paper introducing the value restriction: previous solutions all ...
user avatar
  • 29.2k
5 votes
Accepted

Assertion of Type Inference Rules/Type Checking

Well, you need to construct a typing derivation which has what you want to prove as a conclusion, and no open premise (i.e., leaves must be axioms, or rules with no premises). In the case of your ...
user avatar
5 votes
Accepted

How to statically type polymorphic lambdas using hindley milner style type inference

You should use a polymorphic lambda calculus, e.g. System F for representing typed terms. Then, when you generalize a let binding, you also insert lambdas which abstract over types, and when you check ...
user avatar
5 votes

What is the difference between $ \alpha \to \alpha $ vs $ \forall \alpha. \alpha \to \alpha$?

$$\newcommand{\expr}{\mathsf{expr}} \newcommand{\int}{\mathbf{Int}} \newcommand{\List}{\mathbf{List}} \newcommand{\let}{\mathbf{let}} \newcommand{\id}{\mathsf{id}} \newcommand{\in}{\mathbf{in}} \...
user avatar
  • 2,135
4 votes

Top-down typing strategy - is there a name for this?

There is no top-down or bottom-up typing strategy when defining a language. It is an implementation issue. A type system will only define operator operand constraints on your AST. The kind constraints ...
user avatar
  • 19.1k
4 votes

Equivalence of data-flow analysis, abstract interpretation and type inference?

A good place to learn about these three approaches and how the relate is the book Principles of Program Analysis by Nielson, Nielson and Hankin. I don't think it's correct to say that data-flow ...
user avatar
4 votes

Equivalence of data-flow analysis, abstract interpretation and type inference?

I consider them as basically the same. They just had initially different goals and were coined by different computer science factions. Data flow analysis comes from the compiler engineering faction, ...
user avatar
4 votes

Relation between type-checking decidability, typability decidability and strong normalization

(1) False. Counter example: Java, Scala, Haskell, ... (2) No general relations hold, really depends on the details of the language/typing system. There is one exception: for sane languages and ...
user avatar
4 votes
Accepted

Local type argument synthesis when type variable does not appear in arguments

As a prelude, there is some terminological confusion in your question. The issue is about a type variable occurring in a result type of a function. This is fairly minor. A more serious one is when ...
user avatar
4 votes
Accepted

Lambda Calculus Type Inference

Let me assume that you are asking about basic type inference for $\lambda$-calculus with parametric polymorphism a la Hindley-Milner (it's not entirely clear from your question). I would recommend the ...
user avatar
  • 28.4k

Only top scored, non community-wiki answers of a minimum length are eligible