38

Your suspicion is correct. The CPU doesn't care about the semantics of your data. Sometimes, though, it does make a difference. For example, some arithmetic operations produce different results when the arguments are semantically signed or unsigned. In that case you need to tell the CPU which interpretation you intended. It is up to the programmer to make ...


17

One of the defining properties of the $\bot$ or empty type is that there exists a function $\bot \to A$ for every type $A$. In fact, there exists a unique such function. It is therefore, fairly reasonable for this function to be provided as part of the standard library. Often it is called something like absurd. (In systems with subtyping, this might be ...


14

As others have already answered, today's common CPUs do not know what a given memory position contains; the software decides. However, there are other possibilities. Lisp Machines for example used a tagged architecture which stored the type of each memory position; that way the hardware itself could do some of the work of high-level languages. And even now,...


13

Most research does not actually publish the type checking algorithms for full blown programming languages. You will find some formalisations of a large part of the type systems for full programming languages, such as the work done by Drossopoulou and Eisenbach for Java or Nipkov et al's work on C++. More often, though, you will only find the type systems for ...


13

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 (...


12

Type safety and type soundness are synonyms in most theoretical work. Type soundness is often formulated with respect to an operational semantics as (type) preservation and progress. Preservation states that if an expression has some type, then after a step of evaluation (via the operational semantics), the resulting expression can be given the same type. ...


11

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


10

I am not in a position to tell how much more research should be done on the topic, but I can tell you that there is research being done, for example the Verisoft XT program funded by the german government. The concepts which I think you are looking for are called formal verification and contract based programming, where the latter is a programmer-friendly ...


10

A language in which automatic type checking is not available, an operation would make assumptions about the types of its operands. On the event that these assumptions are false, the operation, not knowing anything about this, may produce nonsense results. Assembly is such language. It has, for instance, separate addition operations for integers and floats. ...


9

The following rank-2 type $$\text{compose}:\forall ABC\delta. \delta\ (\forall \alpha.\alpha\ A\to \alpha B)\ (\forall \beta.\beta\ B\to \beta C) \to \delta\ (\forall \gamma.\gamma\ A\to \gamma C)$$ seems to be sufficiently general. It is much more polymorphic than the type proposed in the question. Here variable quantify over contiguous chunks of stack, ...


9

Your characterization of dynamically typed languages¹ is broadly correct. However, it is somewhat incomplete. Types go beyond type checking: they also characterize values. In Python, this is a fundamental part of the language. In Python, every value is an object, and the type of a value is for the most part determined by the methods it supports. This is ...


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

Depending on the language, there can be many development challenges: Pointers: If a language doesn't have pointers, it will be a challenge to do relatively-easy tasks. For example, you can use pointers to write to VGA memory for printing to the screen. However, in a managed language, you will need some kind of "plug" (from C/C++) to do the same. Assembly: ...


8

In order with the explicit questions: Yes Yes No To answer the question I think you're attempting to ask, we can prove many things using type checking, but not everything. What does this have to do with programs? That's what the Curry-Howard correspondence tells us. The Curry-Howard correspondence is a relationship between logic and computational models. ...


8

You're on the right track: people have come up with the same way to do this. The general concept is known as abstract types. With the Church encoding, the type of a pair of elements of types $a$ and $b$ is polymorphic: it has the type $\forall x, \mathtt{Pair} \, a \, b \, x$ where $x$ is the type of the destructor's continuation. The type family you're ...


7

I've always viewed it more as a matter of convenience, than about whether an algorithm can or can not be expressed at all. If I really wanted to run programs like Mitchell's contrived one, I'd just write the appropriate Turing Machine simulator in my statically typed language. The trick with a static type system is to offer the right kinds of flexibility ...


7

I'm not aware of anything exactly like this, but there are some things that are arguably related. For specifically sorting this is related to the Schwartzian transform, though with a very different goal. In the Schwartzian transform, you run through the input applying an expensive function and pairing the input and output together, then sorting on the ...


7

The Dunfield & Krishnaswami paper's introduction refers to Practical type inference for arbitrary-rank types As can be seen, it scales well to advanced type systems; moreover, it is easy to implement, and yields relatively high-quality error messages (Peyton Jones et al. 2007) In System F-ish approach there is also a "subtyping" relation. See ...


7

The standard reference I often give is Induction is not derivable in second order dependent type theory by Herman Geuvers, which says that there is no type $$N : \mathrm{Type}$$ with functions $$Z:N\qquad S:N\rightarrow N $$ such that $$\mathrm{ind}:\Pi P:N\rightarrow \mathrm{Type}.P\ Z\rightarrow (\Pi m:N.P\ m\rightarrow P\ (S\ m))\rightarrow \Pi n:N. P\...


7

To get your idea working you need something extra, as was pointed out in @cody's answer. Sam Speight worked under the supervision of Steve Awodey to see what can be achieved in HoTT using an impredicative universe, see Impredicative Encodings of Inductive Types in HoTT blog post.


7

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

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


6

Throughout $y$ should have type $T_1$ instead of $T_2$. Let us be more careful about step 3. We are going to apply the following induction hypothesis: If $\Gamma, y : T_1, x : S \vdash t_1 : T_2$ and $\Gamma, y : T_1 \vdash s : S$ then $\Gamma, y : T_1 \vdash [x \mapsto s] t_1 : T_2$. After that we will use abstraction to get $\Gamma \vdash (\lambda y : ...


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 the compiler/runtime are capable of passing the types down to the CPU, then aren't they are capable of emitting equivalent checks in assembly? It could be done, but then we move those checks from compile time to run time, impacting performance we detect type errors at runtime instead of compile time, losing all the benefits of a type system Bloating ...


6

One of the benefits of typed assembly language is that it can reduce the TCB, not expand it. The type checker in the assembler for type-checking the typed assembly language can be fairly simple, and thus potentially fairly trustworthy. In contrast, a compiler is a much more complex beast, and putting a type-checker in a compiler typically involves trusting ...


6

You want to write some executable code (is_left_restartable) and use it inside a type annotation. This is, by definition, a dependent type. The problem when you have dependent types is that it's hard to keep type checking usable for a programming language. It's generally desirable to keep the type system decidable, because programmers tend to be annoyed ...


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

To add to what has been said about the function absurd: ⊥ -> a I have a concrete example of where this function is actually useful. Consider the Haskell data-type Free f a which represents a general tree structure with f-shaped nodes and leaves containing as: data Free f a = Op (f (Free f a)) | Var a These trees can be folded with the following ...


5

I think what you are looking for is type inference for record types. Let me give you a bit of an overview on each of those; but those keywords should help you find a lot more on those topics. Type inference means that you don't need to declare the type of everything. Instead, the compiler figures out the types where it can, from context. For instance if ...


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