Skip to main content
11 votes
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 ...
ThreeFx's user avatar
  • 433
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 ...
Andrej Bauer's user avatar
  • 30.9k
5 votes

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 ...
chi's user avatar
  • 14.6k
4 votes

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 ...
Gilles 'SO- stop being evil''s user avatar
4 votes
Accepted

Types and Types Systems concepts

Yes, exactly. Because you can instantiate the polymorphic type with an infinite amount of (mono)types. For example, the type $a \to a$ (which is a polymrphic type) represents Bool $\to$ Bool Char $\...
Euge's user avatar
  • 630
2 votes

Which type compilers report if they cannot infer a precise type?

Depends on where the type appears. On values (including return values), the lower bounds are the most interesting since it gives you more freedom on where to use them. On parameters, the upper ...
Raphael's user avatar
  • 72.6k
2 votes

Type inference with imports

The first option is to simply process all the imports and see what is in them. This is not what you are asking, because it is equivalent to having everything in a single file, more or less. And it can ...
Andrej Bauer's user avatar
  • 30.9k
2 votes
Accepted

Is $\Gamma \vdash x x : T$ possible in the simply typed lambda calculus?

You are on the right track. The argument you would use is on the lines of size of types defined below: (I am assuming you are in the world of simply typed $\lambda$-calculus) $size(T) = 1$ $size(T \...
Apoorv's user avatar
  • 659
2 votes

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. ...
Gilles 'SO- stop being evil''s user avatar
2 votes

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 ...
Guy Coder's user avatar
  • 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: ...
Andrew K. Hirsch's user avatar
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 $$
axr's user avatar
  • 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....
D.W.'s user avatar
  • 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 ...
chi's user avatar
  • 14.6k

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