Polymorphism and Higher Order Functions

Polymorphic List Definition

Inductive list (A : Type) : Type := nil : list A | cons : A -> list A -> list A. Lists parameterized by element type A, allowing reuse for any type.

map Function Type

map : forall (A B : Type), (A -> B) -> list A -> list B. Takes a function from A to B and a list of A, returns list of B. Higher-order and polymorphic.

Haskell Type Variables

Type variables a,b in signatures like map :: (a -> b) -> [a] -> [b] are prenex universally quantified: map : forall a b. (a -> b) -> [a] -> [b].

Haskell Type Constructor

[_] : Type -> Type (list type constructor). (->) : Type -> Type -> Type (function type constructor). Types themselves are first-class in type system.

Limitation of Haskell Types

Cannot directly type strange g = [g True, g 0] because g would need both Bool → ? and nat → ?. Requires impredicative polymorphism (g : forall A, A → B).

Rocq Strange Function Type

strange : forall (B : Type), (forall (A : Type), A -> B) -> list B. g must work for all argument types A, returning same result type B.

Dependent Types

vec_app : forall (n m : nat) (A : Type), Vec n A -> Vec m A -> Vec (n + m) A. Type depends on value (length n), enabling precise length specifications.

Rocq Type Hierarchy

0 : nat, nat : Set, Set : Type, Prop : Type, Type : Type (with universes to avoid paradoxes). Types themselves have types (sorts).

Rocq vs Haskell Types

Rocq types are terms with t : τ relation. Supports arbitrary quantification, dependent types, while Haskell types are prenex polymorphic only.

Termination in Rocq

Rocq's λ-calculus (Calculus of Inductive Constructions) is terminating, ensuring all functions are total and proofs are consistent.

Polymorphic Map Implementation

Fixpoint map (A B : Type) (f : A -> B) (l : list A) : list B := match l with | nil _ => nil B | cons _ x xs => cons B (f x) (map A B f xs) end. Explicit type arguments.

System F

Haskell's core type system (System F) supports parametric polymorphism with prenex universal quantification. Basis for polymorphic programming.

λ-cube (Barendregt)

Framework classifying type systems by three axes: polymorphism (types depending on types), dependent types (types depending on terms), and operators (terms depending on types). Rocq near the top