0
$\begingroup$

In Types and Programming Languages by Pierce, Chapter 23 Universal Types has a summary of System F in the following figure, in particular, "type abstraction values" and their types "universal types".

In all the examples I have seen so far in the chapter, in particular Section 23.4 Examples, (not sure if I miss any example):

  • all the type abstraction values are parametrically polymorphic functions, by allowing the types of their arguments to have any type, and
  • all the universal types, i.e. the types of type abstraction values, are types of parametrically polymorphic functions.

Are type abstraction values and their universal types not for non functions, but only for functions?

More specifically, in any type abstraction value, say $\lambda X.t$, must $t$ have a function type, not a non-function type?

In Section 23.4 Examples, values of base types and of recursive types are type abstraction values, because their definitions in the section are functions by Church encodings.

Thanks.

enter image description here

$\endgroup$
2
$\begingroup$

Short Answer: In λX₁. λX₂. ... λXₙ. t it doesn't matter if t is not a function, but if so, it may not be an interesting example for introduction.

Long Answer:

First of all, technically speaking, the type system defined in Figure 23-1 does NOT have any base types such as Bool or Nat. A type of t in λX. t is either a type variable X, a function type T → T, or a universal type ∀X. T.

Section 23.4, however, takes Nat as an example. So let's consider an extended type system by adding some base types and its values, terms, typing rules, etc. like Section 11.1 does.

Then we can consider, for example, a term λX. 42. This is a well-typed term. Proof:

\[ \cfrac{}{ \cfrac{\mathrm{X} ⊢ \mathrm{42} : \mathrm{Nat}}{ ∅ ⊢ \mathrm{λ X. 42} : \mathrm{∀ X. Nat} }} \]

This term, however, is not very interesting; polymorphism doesn't play any important role here.

Also, we can consider a type ∀X. X. But there is no term of type ∀X. X (i.e. there is no inhabitant of ∀X. X). This can be proved through the Curry-Howard correspondence. But this example may not be suitable for introduction of System F.

Section 23.7 writes a bit more interesting example. If we extend the type system by adding errors, we can consider a term λX. error. This term doesn't throw an error during an evaluation because of the type-abstraction. This observation gives an idea of a new type erasure method, described in Section 23.7.

$\endgroup$
  • $\begingroup$ Thanks. "In λX₁. λX₂. ... λXₙ. t it doesn't matter if t is not a function, but if so, it may not be an interesting example for introduction." "λX. 42, however, is not very interesting; polymorphism doesn't play any important role here." If t in λX. t is not a function, does polymorphism always not play any important role here? $\endgroup$ – Tim Sep 5 at 2:21
  • $\begingroup$ @Tim I wrote "may". There is no formal definition of "interesting". Formally we can only confirm the fact that t can be not a function, and cannot confirm whether it's interesting or not. That is only my opinion; others may say it's interesting. $\endgroup$ – nekketsuuu Sep 5 at 5:47
  • 1
    $\begingroup$ Is (λX. []) : ∀X. List X interesting? $\endgroup$ – Dan Doel Sep 5 at 13:00
  • $\begingroup$ @DanDoel How is your List X defined? Is it by Church encoding in Section 24.3 of the book? If yes, a value with type List X is a polymorphic function. $\endgroup$ – Tim Sep 5 at 20:22
  • $\begingroup$ Is that how $\mathrm{Nat}$ and $42$ are defined? If you insist on everything being Church encoded, then you will have nothing but functions, trivially. But that's not how most practical languages work. $\endgroup$ – Dan Doel Sep 5 at 22:10

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.