42 votes
Accepted

How does a computer determine the data type of a byte?

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 ...
26 votes
Accepted

Why does Coq include let-expressions in its core language

It is a common misconception that we can translate let-expresions to applications. The difference between let x : t := b in v ...
  • 28.4k
17 votes

Is there any use case for the bottom type as a function parameter type?

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 ...
16 votes
Accepted

Is there a difference between type safety and type soundness?

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

How does a computer determine the data type of a byte?

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 ...
  • 240
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,754
11 votes
Accepted

Why aren't we researching more towards compile time guarantees?

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

What are potential pitfalls with having a minimal kernel that runs managed code?

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 ...
  • 386
8 votes

Can we prove that $1 + 2 + \dots + n = \frac{n(n+1)}{2}$ using a computer program?

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 ...
8 votes
Accepted

Safe way to explicitly define new types instead of using Algebraic data types for my functional language

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 $...
8 votes
Accepted

Reducing products in HoTT to church/scott encodings

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\...
  • 7,754
8 votes

Reducing products in HoTT to church/scott encodings

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 ...
  • 28.4k
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” ...
8 votes
Accepted

Representation of the concatenation at the type level

A major idea of concatenative languages is that the syntax and semantic domain form monoids and the semantics is a monoid homomorphism. The syntax is the free monoid generated by the basic operations, ...
8 votes

Is type-checking "syntactic" or "semantic"?

Although I personally would describe type analysis as semantic, this question seems to start with the assumption that there is a clear, formally-definable dividing line between "syntax" and "semantics"...
  • 11.4k
7 votes

What is a non-contrived example of static type-checking being too conservative?

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

Reference request: optimizing procedures on lists in dynamic languages by performing safety checks in advance

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

Higher-ranked polymorphism without explicit application or subtyping?

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

Does strong typing contribute to better performance optimization by compiler?

I think your friend somewhat presents a false dichotomy. I will just give one example: when it first came out, the Self VM was one of the fastest dynamic language implementations. In fact, the ...
6 votes
Accepted

Decidability of dependent typing on primitive recursive languages

Not only is the answer to this question yes, but this is exactly the strategy that modern implementations like Coq and Agda take! To be precise, the type checker has to preform evaluation when ...
  • 3,738
6 votes
Accepted

Proving preservation under substitution System F Omega

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$ ...
  • 28.4k
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

What's the advantage of typed assembly?

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 ...
  • 14.2k
6 votes

What's the advantage of typed assembly?

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 ...
  • 144k
6 votes
Accepted

LET REC recursive expression static typing rule

It seems you discovered the difference between a set of typing rules and an algorithm for type inference. Typing rules only define a relation among 1) a type environment, 2) a term, and 3) a type. ...
  • 14.2k
6 votes
Accepted

Type system with subtyping on abstract data types?

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

Is there any use case for the bottom type as a function parameter type?

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

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