39
For a rather simple version of dependent type theory, Gilles Dowek gave a proof of undecidability of typability in a non-empty context:
Gilles Dowek, The undecidability of typability in the $\lambda\Pi$-calculus
Which can be found here.
First let me clarify what is proven in that paper: he shows that in a dependent calculus without annotations on the ...
24
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 programming languages require the programmer to explicitly ask for it. Essentially, the programmer is telling the compiler "trust me, I know better -- this will be ...
16
In the lambda calculus with no constants with the Hindley-Milner type system, you cannot get any such types where the result of a function is an unresolved type variable. All type variables have to have an “origin” somewhere. For example, the there is no term of type $\forall \alpha,\beta.\; \alpha\mathbin\rightarrow\beta$, but there is a term of type $\...
answered Jan 1 '14 at 4:32
Gilles 'SO- stop being evil'
40.6k7 gold badges108 silver badges171 bronze badges
13
Pairs
This encoding is the Church encoding of pairs. Similar techniques can encode booleans, integers, lists, and other data structures.
Under the context x:a; y:b, the term pair x y has the type (a -> b -> t) -> t. The logical interpretation of this type is the following formula (I use standard mathematical notations: $\to$ is implication, $\vee$ ...
answered Jan 31 '14 at 11:28
Gilles 'SO- stop being evil'
40.6k7 gold badges108 silver badges171 bronze badges
12
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 direction Decidable $\Rightarrow$ Normalizing is open, I believe, even for relatively well understood systems, though we do have partial results. This question ...
9
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 difference.
Now System F doesn't have decidable type-inference, and HM is a way of combining type-inference with reasonably expressive parametric polymorphism. ...
9
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 subexpression they generate a type constraint. Then, they take this constraints, assume conjunction between them, and solve them (typically looking for a most ...
9
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 pragmatically viable way. The combination of parametric polymorphism and subtyping is deadly from the point of view of algorithmic complexity.
9
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 in a principal way, include it in the resulting type. "It's not a problem, it's in the solution."
This solution can be made to work, but in general it may run ...
8
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 checkpoint that'd use for this. Given a type inconsistency in a function application, a full type inference system doesn't know if you messed up the argument ...
7
Oddly enough, Haskell itself is perfectly nearly capable of your example; Hindley-Milner is totally fine with overloading, so long as it's well-bounded:
{-# LANGUAGE OverlappingInstances, MultiParamTypeClasses,
FunctionalDependencies, FlexibleContexts,
FlexibleInstances #-}
import Prelude hiding ((*))
class Times a b c | a b -> ...
7
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” in its general sense which can include quantified variables; in the terminology commonly used with Hindler-Milner, that's a type scheme.) So, to prove that you ...
answered Mar 23 '19 at 23:33
Gilles 'SO- stop being evil'
40.6k7 gold badges108 silver badges171 bronze badges
6
[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 stumbled upon is parametric polymorphism. Type systems trying to extend HM in this direction tend toward System F and so require type annotations. Two notable ...
6
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 $\sigma + \tau$ for any $\tau$. The names of type variables don't matter, what matters is where else are you using the same type variable.
6
Yes, you are restricting it too much. The second code is perfectly fine.
For the record, Haskell has no issue with your code:
> let myid = (\x->x)(\x->x) in (myid 'a', myid True)
('a',True)
and Ocaml as well works fine, after eta-expansion:
let myid y = (fun x -> x)(fun x -> x) y in (myid 'a', myid true);;
- : char * bool = ('a', true)
...
6
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 obvious thing to do is just to show all the constraints to the user. However, when the user is a human, they may find the constraints too complex to process, and so ...
6
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.
As we are dealing with an application, the only rule that applies is T-App, so we end up with the following (partial) typing derivation, where $\gamma$ is yet ...
6
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 reduction (by the subject reduction theorem) we would get that all these terms also have the same type
$$
\begin{array}{l}
(λx.λy.y(x\ y))(λz.z) \\
(λy.y((λz.z)\ ...
6
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 wrongly claim that you can't write a function of type $\texttt{Void}\to a$.
$\texttt{Void}\to a$ is vacuously true. In principle a function of that type should ...
5
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 the function space operator gives a form of negation. Small type annotations that can help regaining type-inference are discussed in (4).
Adding existentials ...
5
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 every input in finite time. We also say it's computable.
A formal language is undecidable if and only if it is not decidable.
A formal language is ...
5
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
variable by $\alpha$-conversion, without changing the semantics of the
$\lambda$-abstraction, and thus without changing its type.
By writing $\Gamma, x: \...
5
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. Data flow analyses typically have finite-height abstract domains which ensures termination. In general, abstract interpretation does not assume such abstract ...
5
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 existed, but the complexity of annotations made them undesirable.
The majority of value that people want to give polymorphic types are functions, which are ...
5
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 example, the conclusion will be
$$ int\;x,\,int\;y\;\vdash\;(x < (x \times y) + x) : bool $$
so the proof will start by
$$ {int\;x,\,int\;y\;\vdash\;x : int \...
5
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 a function application, you also insert type applications as needed. This is precisely what GHC Haskell does, and is the standard solution.
Now, your concrete ...
5
$$\newcommand{\expr}{\mathsf{expr}}
\newcommand{\int}{\mathbf{Int}}
\newcommand{\List}{\mathbf{List}}
\newcommand{\let}{\mathbf{let}}
\newcommand{\id}{\mathsf{id}}
\newcommand{\in}{\mathbf{in}}
\newcommand{\map}{\mathsf{map}}
\newcommand{\string}{\mathbf{String}}
$$
It's not really possible to answer this without being a little more precise about the status ...
4
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 is fixed by the type system and is part of the design of
the language. It can be very simple as in older languages, or be a
sophisticated logical system. Even ...
4
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 analysis, abstract interpretation and type inference are the same thing. While there are many similarities, and maybe more than would expect, given that the three ...
4
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, trying to talk about their optimization algorithms and proofing upper bounds on their complexity etc.
Abstract interpretation comes from the formal, ...
Only top voted, non community-wiki answers of a minimum length are eligible
