# Tag Info

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
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
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
Accepted

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

### 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
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

### 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
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” ...

### 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

### 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