In the Type Classes chapter we can read "Lean does not allow case analysis of types" and "polymorphic functions implement operations that are uniform for any choice of type argument":
|
Because Lean does not allow case analysis of types, polymorphic functions implement operations that are uniform for any choice of type argument; for example, {name}`List.map` does not suddenly compute differently depending on whether the input list contains {name}`String`s or {name}`Nat`s. |
In the Axioms chapter we can read "parametricity is [...] not compatible with Lean's standard axioms":
|
For example, parametricity is a powerful reasoning technique when used in languages that support it, but it is not compatible with Lean's standard axioms. |
It also has an example that does case analysis on whether a type is Nat
|
if α = Nat then [] else xs |
I believe the intent in the Type Classes chapter was for computable functions only (in particular functions that don't use the axiom of choice). But the text as currently written is a bit misleading (since it doesn't mention computability or the absence of axiom of choice explicitly).
In the Type Classes chapter we can read "Lean does not allow case analysis of types" and "polymorphic functions implement operations that are uniform for any choice of type argument":
reference-manual/Manual/Classes.lean
Line 42 in 5d2a1e3
In the Axioms chapter we can read "parametricity is [...] not compatible with Lean's standard axioms":
reference-manual/Manual/Axioms.lean
Line 74 in 5d2a1e3
It also has an example that does case analysis on whether a type is
Natreference-manual/Manual/Axioms.lean
Line 90 in 5d2a1e3
I believe the intent in the Type Classes chapter was for computable functions only (in particular functions that don't use the axiom of choice). But the text as currently written is a bit misleading (since it doesn't mention computability or the absence of axiom of choice explicitly).