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 ...
- 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 ...
- 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 ...
- 8,178
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 ...
- 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 ...
- 8,178
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 ...
- 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 ...
- 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” ...
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 ...
- 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 ...
- 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 ...
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 $\...
- 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:
...
- 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 ...
- 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.
...
- 794
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 ...
- 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 ...
- 8,178
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 ...
- 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
...
- 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. ...
- 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 ...
- 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 ...
- 794
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 ...
- 803
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}}
\...
- 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 ...
- 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 ...
- 8,178
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, ...
- 216
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 ...
- 8,178
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 ...
- 11.8k
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 ...
- 28.4k
Only top scored, non community-wiki answers of a minimum length are eligible