dependent types and parametric polymorphism in lean

Stream: Type theory

[Bulhwi Cha]

Are dependent functions and dependent products in Lean parametrically polymorphic?

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

Parametricity is not provable in Lean, and it's not true in all models of Lean + mathlib axioms; in particular, it's inconsistent with the axiom of choice. Check out also previous discussions here or here.

[Bulhwi Cha]

From https://docs.lean-lang.org/theorem_proving_in_lean4/dependent_type_theory.html:

Suppose you wish to write a function cons which inserts a new element at the head of a list. What type should cons have? Such a function is polymorphic: you expect the cons function for Nat, Bool, or an arbitrary type α to behave the same way.

What does it mean that a function or datatype is parametrically polymorphic? What does the word "polymorphic" mean in the above context? I don't think it means universe polymorphism.

[Bulhwi Cha]

I read a Wikipedia article about parametric polymorphism and thought dependent functions and products in Lean are parametrically polymorphic. It seems I misunderstood the notion of parametric polymorphism. What is it, then?

[Bulhwi Cha]

Wojciech Nawrocki said:

Parametricity is not provable in Lean, and it's not true in all models of Lean + mathlib axioms; in particular, it's inconsistent with the axiom of choice. Check out also previous discussions here or here.

I'm not trying to prove the parametricity theorem; I haven't heard of it until now. I just want to check my understanding of parametric polymorphism.

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

Ah, sorry! I misread this as a question about parametricity, but you are just asking about polymorphism. Yes, dependent functions are polymorphic.

What does it mean that a function or datatype is parametrically polymorphic?

It just means that we have one implementation of cons which works for lists containing elements of any type. That is, consing a Boolean onto a List Bool uses the same function as consing a number onto a List Nat, etc. The way this is formalized in dependent type theory is that the first argument of List.cons is a type, and then List.cons Bool (or List.cons Nat or whatever) is a "monomorphic" function of type Bool -> List Bool -> List Bool (or analogous).

[Bulhwi Cha]

Thanks. One more question: are dependent products (pairs) in Lean polymorphic? It doesn't seem so.

[Marcus Rossel]

Note that "polymorphic" isn't a precise term in this context. Quoting from Types and Programming Languages:

The term polymorphism refers to a range of language mechanisms that allow a single part of a program to be used with different types in different contexts (§23.2 discusses several varieties of polymorphism in more detail).

§23.2

Type systems that allow a single piece of code to be used with multiple types are collectively known as polymorphic systems (poly = many, morph = form). Several varieties of polymorphism can be found in modern languages (this classification comes from Strachey, 1967, and Cardelli and Wegner, 1985).

Parametric polymorphism, [...] allows a single piece of code to be typed “generically,” using variables in place of actual types, and then instantiated with particular types as needed. Parametric definitions are uniform: all of their instances
behave the same.

The most powerful form of parametric polymorphism is the impredicative or first-class polymorphism [...]. More common in practice is the form known as ML-style or let-polymorphism, which restricts polymorphism to top-level let-bindings, disallowing functions that take polymorphic values as arguments, and obtains in return a convenient and natural form of automatic type reconstruction. First-class parametric polymorphism is also becoming popular in programming languages, and forms the technical foundation for the powerful module systems of languages like ML.

Ad-hoc polymorphism, by contrast, allows a polymorphic value to exhibit different behaviors when “viewed” at different types. The most common example of ad-hoc polymorphism is overloading, which associates a single function symbol with many implementations; the compiler (or the runtime system, depending on whether overloading resolution is static or dynamic) chooses an appropriate implementation for each application of the function, based on the types of the arguments.

A generalization of function overloading forms the basis for multi-method dispatch in languages such as CLOS (Bobrow et al., 1988; Kiczales et al., 1991) and Cecil (Chambers, 1992; Chambers and Leavens, 1994). This mechanism has been formalized in the λ-& calculus of Castagna, Ghelli, and Longo (1995; cf. Castagna, 1997).

A more powerful form of ad-hoc polymorphism known as intensional polymorphism (Harper and Morrisett, 1995; Crary, Weirich, and Morrisett, 1998) permits restricted computation over types at run time. Intensional polymorphism is an enabling technology for a variety of advanced implementation techniques for polymorphic languages, including tag-free garbage collection, “unboxed” function arguments, polymorphic marshaling, and space-efficient “flattened” data structures.

Yet more powerful forms of ad-hoc polymorphism can be built from a typecase primitive, which permits arbitrary pattern-matching on type information at run time (Abadi, Cardelli, Pierce, and Rémy, 1995; Abadi, Cardelli, Pierce, and Plotkin, 1991b; Henglein, 1994; Leroy and Mauny, 1991; Thatte, 1990). Language features such as Java’s instanceof test can be viewed as restricted forms of typecase.

The subtype polymorphism of Chapter 15 gives a single term many types using the rule of subsumption, allowing us to selectively “forget” information about the term’s behavior.

By that description, I'd argue that dependent products are polymorphic.