37
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'
38.9k7 gold badges103 silver badges167 bronze badges
15
In this answer, I'll stick to a core ML fragment of the language, with just lambda-calculus and polymorphic let following Hindley-Milner. The full OCaml language has additional features such as row polymorphism (which if I recall correctly doesn't change the theoretical complexity, but with which real programs tend to have larger types) and a module system (...
answered Nov 11 '12 at 20:23
Gilles 'SO- stop being evil'
38.9k7 gold badges103 silver badges167 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'
38.9k7 gold badges103 silver badges167 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
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
You've stumbled on the fact that inference of static invariants for higher-order languages is quite difficult in practice, in addition to being undecidable in theory. I'm not sure what the definitive answer to your question is, but note several things:
Polymorphism and refinement types behave poorly together, as you have noted, in particular the notion of ...
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. ...
8
The classic Hindley-Milner type inference algorithm requires each literal value to be unambiguously inferable to a type: 0 is an int, while 0.0 is a real. Haskell's type system has been enhanced to include a certain kind of bounded polymorphism, so that 0 can have any type that is a number (more precisely, of any type that is an instance of the Num type ...
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 ...
8
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 ...
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
I think it is important to realise what the type $\mathtt{int \rightarrow int}$ means and does not mean.
It
does not mean that a program P having that type must return an
integer, contrary to what the original poster said. Instead it means
if P terminates on a given input (of type int), P terminates by returning an integer.
This way the halting problem is ...
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'
38.9k7 gold badges103 silver badges167 bronze badges
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)\ ...
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
[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 ...
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
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
Working with types is not as "hard" as working with values with respect to computability. You can know statically that a function will return a bool without knowing statically that it will return true, for example. Moreover, it's entirely possible and sometimes trivially easy to prove that a specific given function halts with a certain input, but this is a ...
Only top voted, non community-wiki answers of a minimum length are eligible
