Polymorphism and Higher Order Functions

Polymorphic List Definition

• Inductive list (A : Type) : Type

• nil : list A

• cons : A -> list A -> list A

• Parameterized by element type A

• Allows 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
• Operates on a list of A
• Returns a list of B
• Higher-order and polymorphic.

Haskell Type Variables

• Type variables a, b in signatures like map :: (a -> b) -> [a] -> [b]
• Prenex universally quantified
• Expressed as map : forall a b. (a -> b) -> [a] -> [b].

Haskell Type Constructor

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

Limitation of Haskell Types

• Cannot directly type strange g = [g True, g 0]
• 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
• Returns 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)
• Enables 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
• Haskell types are prenex polymorphic only.

Termination in Rocq

• Rocq's λ-calculus (Calculus of Inductive Constructions) is terminating
• Ensures all functions are total
• Guarantees 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)
• Operators (terms depending on types)
• Rocq near the top.