# Tag Info

Accepted

### Types as first class Citizen

First class types enable something called dependent typing. These allow the programmer to use values of types at type level. For example, the type of all pairs of integers is a regular type, while the ...
• 433
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 ...
• 30.9k

### What's the difference between the rank and the degree of a type function?

The book states that the rank of a term is the number of $\Pi$'s in its (normal) form. But doesn't the number of such $\Pi$'s correspond exactly to the number of arguments it takes? That is, if a type ...
• 14.6k

### What's the difference between the rank and the degree of a type function?

The degree of a type function is its arity, i.e. the number of parameters that it takes. This is the simple concept that you're familiar with, independent of what kind of objects the function ...
Accepted

• 659

### Is order important in Structural Equivalence?

A type constructor is a way to build a type from other types (possibly zero other types), in the same way that a value constructor is a way to build a value from (possibly 0) other values. ...

### Is there a notation for types?

In looking at int op int→int my focus is immediately drawn to . If you have ever studied Lambda Calculus and how it forms the ...
• 5,101
1 vote
Accepted

### How are conflicts between free and bound de Bruijn indices resolved?

The best way to view this, in my opinion, is by looking at the abstract syntax tree. For λw. b w, this would be something like: ...
1 vote

### Is there a notation for types?

You can write a new union type as $$\mathrm{type} \; number = int \; | \; float$$ Then, you can write down your function $$addition : number \rightarrow number \rightarrow number$$
• 296
1 vote

### Is there a notation for types?

One approach is to use union/intersection types: https://stackoverflow.com/q/5653678/781723. Haskell type classes can be used to support this, but with some significant restrictions: https://www....
• 162k
1 vote

### What is the type system (or class of type systems) that that ensures all your tree Branches end in Leaves?

To be honest, I'm unsure about whether this is a CS question or a programming question. There is a strong programming part to it, yet encoding requirements in types requires reasoning on types which ...
• 14.6k

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