# Tag Info

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 ...
• 271k
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

### 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 ...
• 11.8k
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 ...
• 11.8k

### 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
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
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 ...
• 535
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,188
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
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

### 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 ...
• 17.8k
Accepted

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

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

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