# Tag Info

11

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 pair of all integers with the left number smaller than the right number is a dependent type. The standard introductory example of this is length encoded lists (...

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

5

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 function takes $n$ arguments, then doesn't that just mean there must be $n$ $\Pi$ symbols to capture those $n$ arguments? Nope. Let $\sigma, \tau$ be types (i....

4

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 manipulates. Rank-0 types are types of base objects like integers, strings, and more complex data structures. The atomic type constants of degree $0$ would be things ...

4

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 $\to$ Char (Char $\to$ Int) $\to$ (Char $\to$ Int) etc...

2

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 bounds are more relevant since they tell you what kinds of values you may pass into the function.

2

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 be prety expensive to process all the dependencies. What you are looking for is the notion of interface, also known as signature. To simplify things, an ...

1

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 \to T') = size(T) + size(T')$ Unification will only work if the size of types is equal, and in this case $size(T \to T') > size(T)$ hence there cannot be ...

1

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 is more on the CS side. Anyway, here is an answer. There are several options to encode that requirement into types. Basically, we need to encode that each ...

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