Polymorphism and Higher-Order Functions

polymorphism, polymorphic lists, polymorphic functions, type annotations, type inference, implict arguments, polymorphic pairs, polymorphic options, higher-order functions, filter, map, fold, anonymous functions, Church numerals, Arguments, @ for explicit arguments.

Polymorphism avoids us from having to create separate defintions for boolean lists, integer lists, and so on. Here is an example.

Inductive list (X:Type) : Type :=
  | nil
  | cons (x : X) (l : list X).

list is typed: Type -> Type. cons is now a polymorphic constructor.

Accordingly, the type of cons and nil are quantified over all types X.

Check nil : forall X : Type, list X.
Check cons : forall X : Type, X -> list X -> list X.

Note that each constructor of =list= takes a =Type=. e.g.

Check (cons nat 3 (nil nat)) : list nat.

Notice the constant use of nat. This seems redundant.

You don’t need to always pass the type to the constructor.

Check (cons nat 2 (cons nat 1 (nil nat)))
      : list nat.

Fixpoint repeat' X x count : list X :=
  match count with
  | 0        => nil X
  | S count' => cons X x (repeat' X x count')
  end.

Instead of simply omitting the types of some arguments to a function, like

      repeat' X x count : list X :=

we can also replace the types with holes

      repeat' (X : _) (x : _) (count : _) : list X :=

to tell Coq to attempt to infer the missing information.

This seems redundant, still. Indeed, the chapter states:

In fact, we can go further and even avoid writing [_]’s in most cases by telling Coq always to infer the type argument(s) of a given function.

The Arguments directive specifies the name of the function (or constructor) and then lists the (leading) argument names to be treated as implicit, each surrounded by curly braces.

There are two ways to do this.

Arguments nil {X}.
Arguments cons {X}.
Arguments repeat {X}.

Now we don’t have to supply any type arguments at all in the example:

Definition list123'' := cons 1 (cons 2 (cons 3 nil)).

Alternatively, we can declare an argument to be implicit when defining the function itself, by surrounding it in curly braces instead of parens. For example:

Fixpoint repeat''' {X : Type} (x : X) (count : nat) : list X :=
  match count with
  | 0        => nil
  | S count' => cons x (repeat''' x count')
  end.

Note that you can mark an inductive type with an implict argument, but it’s a step too far:

Inductive list' {X:Type} : Type :=
  | nil'
  | cons' (x : X) (l : list').

because adding this makes the X be implicit for not only the constructors but for the type itself.

i.e. [5,5] : list' and [true, false] : list' insread of list' nat and list' bool respectively.

We can have anonymous functions, which are useful to work with higher-order functions.

The syntax is as follows. #+BEGIN_SRC coq Example test_anonfun’: doit3times (fun n => n * n) 2 = 256. Proof. reflexivity. Qed. #+END_SRC coq

A Church numeral is a way of defining natural numbers using lambda calculus. Specifically, a natural number n is represented as a function that takes a function f and applies f n times.

So, have:

Definition one : cnat :=
  fun (X : Type) (f : X -> X) (x : X) => f x.

Definition zero : cnat :=
  fun (X : Type) (f : X -> X) (x : X) => x.

Note that zero is represented by applying f 0 times, i.e. just returning x.

Consider a Church numeral n. That is, some function fun X f x => f ( f (... f x) ). We can then also write it as fun X f x = f^n x.

Church numerals are typed forall X : Type. (X -> X) -> X -> X - they are functions.

What does n X f x represent?

Passing X f x to n means to “apply f (starting with x) n times”.

We can then think of Church numerals in this way: the function f represents the successor operation, and the value x represents the zero element of X.

We can build the Peano natural numbers as a result, by letting f = S (successor) and x = 0.

The interesting thing is that Church numerals represent the natural numbers without inductive datatypes. We can represent numbers just with functions.

Also, with Church numerals, we can define addition and multiplication elegantly.

This was done in the exercises.

plus is just fun (n m : cnat) => fun X (f : X -> X) (x : X) => m X f (n X f x). As in, n X f x (apply f n times starting with x), and m X f (n X f x) (apply f m times starting with (n X f x) (the earlier result)).

mult is similar, just making the repeating adding n m times (letting the “successor” function or f be fun (x : X) => plus f n).

It’s a bit odd looking though. It’ll look better in lambda calculus notation.

Definition mult (n m : cnat) : cnat :=
  fun X (f : X -> X) (x : X) =>
    m X (fun (y : X) => (plus n
                           (fun X (f': X -> X) (x' : X) => x')
                        ) X f y )
      x.

\f.\x.m (\y. plus n (\f'.x'.x') f y) x

Or not.

• mumble_grumble : Determine well-typed values. (2 stars) (Optional)
• poly_exercises: Prove app_nil_r, app_assoc, app_length. (2 stars each)
• more_poly_exercises: Prove rev_app_distr and rev_involutive. (2 stars each, especially useful)

• combine_checks : Analyze the behavior and type of combine. (1 star) (Optional)
• split: Implement the inverse of combine. (2 stars)

• hd_error_poly: Define a polymorphic version of hd_error. (1 star) (Optional)

• filter_even_gt7: Filter even numbers greater than 7 from a list. (2 stars)
• partition: Split a list into two sublists based on a predicate using filter. (3 stars)
• map_rev: Prove that map and rev commute. (3 stars)
• flat_map: Define a flat_map function. (2 stars)

• implicit_args Replace implicit arguments with explicit arguments. (2 stars, optional)

  implicit_args is tedious and does not involve code.

• fold_length: Define length using fold and prove its correctness. (2 stars)
• fold_map: Implement map using fold and prove its correctness. (3 stars)
• fold_types_different: Written question: why does fold typed f : X -> Y -> Y instead of f : X -> X -> X? (1 star, optional)

• prod_curry and prod_uncurry: Define and prove that currying and uncurrying are inverses. (2 stars)
• nth_error_informal: Informal proof about nth_error. (2 stars, advanced)

• church_scc: Define the successor function for Church numerals. (2 stars, advanced)
• church_plus: Define addition for Church numerals. (3 stars, advanced)
• church_mult: Define multiplication for Church numerals. (3 stars, advanced)

• church_exp: Define exponentiation for Church numerals. (3 stars, advanced)

  I am a bit stuck with church_exp.

This is an answer to an exercise. Line 708-729.

Definition filter_even_gt7 (l : list nat) : list nat :=
  filter (fun n => andb (even n) (leb 7 n)) l.

Example test_filter_even_gt7_1 :
  filter_even_gt7 [1;2;6;9;10;3;12;8] = [10;12;8].
Proof.
  simpl. reflexivity.
Qed

Before, and after running simpl, the goal is

filter_even_gt7 [1; 2; 6; 9; 10; 3; 12; 8] = [10; 12; 8]

That is, simpl doesn’t simplify the left side.

Why does reflexivity able to do it and not simpl?

ANSWER:

The book, for an exercise, states that:

Prove the correctness of fold_length. (Hint: It may help to know that reflexivity simplifies expressions a bit more aggressively than simpl does – i.e., you may find yourself in a situation where simpl does nothing but reflexivity solves the goal.

Here’s my solution to that exercise, where reflexivity is indeed able to simplify more than simpl.

Theorem fold_length_correct : forall X (l : list X),
  fold_length l = length l.
Proof.
  intros X l. induction l as [| x l' IHl'].
  - reflexivity.
  - simpl. rewrite <- IHl'. reflexivity.
Qed.

So, reflexivity is simply more aggressive than simpl.

This is an unsatisfying answer, since it doesn’t talk about what aggressive simplification means, nor why reflexivity is more aggressive than simpl but it’s okay.

In one of the exercises, it is written that:

Warning: Coq will not let you pass [cnat] itself as the type [X] argument to a Church numeral; you will get a “Universe inconsistency” error. That is Coq’s way of preventing a paradox in which a type contains itself. So leave the type argument unchanged.

Can you tell us more about the error?

System F was introduced by Girard (of linear logic, Girard’s paradox) in 1972 in the context of proof theory.

Reynolds (of CMU, ALGOL, separation logic, continuations) independently discovered System F under the name polymorphic lambda calculus and also stated the parametricity theorem (an idea first developed by Strachey (of denotational semantics)) under the name abstraction theorem in 1983.

While going through polymorphism, I recalled PFPL/15-312’s discussion of System F.

Here are some notes from Chapter 16 and 17 of PFPL.

The languages so far have been monomorphic: each expression has a unique type.

Generic expressions codify type-independent behaviors. Such expressions are polymorphic.

Unfortunately I don’t know how to insert complex LaTeX yet. But a definition for F is given.

Typ tau is either a variable t, an arrow type t_1 -> t_2, or a polymorphic type denoted forall t. tau

Exp e is composed of the usual ones, but we add in System F - type abstractions and type applications.

A type abstraction Lam(t.e) is an expression with a value of type t somewhere in e. The statics types type abstractions with the polymorphic type, as expected.

A type application applies a polymorphic function to a specified type App{tau}(e). Here, per the statics, e is a polymorphic expression and tau is some type.

All (lazy) finite products, sums, inductive and coinductive types are definiable in System F.

We show “definability” through definitional equality - we encode other systems like T in F by making some “replacements”.

The book goes over the details of encoding. As seen in this SF chapter too, (lazy) natural numbers are expressible in System F - these are Church numerals.

Showing that natural numbers can be encoded in F shows that F is at least as expressive as T.

A remarkable property of F is that polymorphic types severely constrain the behavior of their elements.

We may prove useful theorems about an experssion knowing only their type.

Consider i : \forall.(t.t->t). It must be the case that i is the identity function.

Consider b : \forall(t.t -> t -> t). There are only two possible expressions b can be equivalent to. We elide the expressions, but intuitively, given two arguments t, b can do nothing but return one of them.

These findings, properties of programs in F that are proved knowing only their type, are called parametricity properties,

They are called free theorems, in the sense that we can prove non-trivial results in System F without even looking at the program code (only types).

This allows the type system to “pre-verify” broad ranges of programs (with the same type).

These properties arise from proving parametricity in System F.

Casually, PFPL states:

Parametricity Theorem:

If a piece of code typechecks, then it “just works”.

Parametricity narrows the space of well-typed programs sufficiently enough that the opportunities for programmer error are reduced to almost nothing.

The formal explanation of the parametricity theorem is a bit technically involved and beyond me. There is a long treatment of the theorem in Chapter 46.

System F has the normalization property, as in, the evaluation of every well-typed program terminates. This is shared with System T. Apparently, normalization is very hard to prove, which is impressive for System F, given that you can define substantial code like sorting functions in it. The normalization of System F was proven by Girard in his doctoral thesis.

Given untyped term m, can we find a typed term in System F that “erases” to m?

Type erasure simply removes all the type annotations of an expression.

Type reconstruction is undecidable for System F (Wells, 1994). This was a long-standing open problem in the 70s. Type reconstruction of partial type erasure (type erasure except type annotations for type applications) is undecidable (Pfenning, 1993).

The lack of type reconstruction causes some cons to System F. Often, type reconstruction is valued, so some programming languages (like ML) work with a restricted System F.

• The operational semantics of System F is a type-passing semantics - the type is actually substituted into the body of the function. This imposes a significant cost.

  To avoid this cost, most polymorphic languages use a type-erasing semantics - where after typechecking, all the types are erased and the untyped terms are then interpreted or compiled.

  The presence of features like casts forces a type-passing semantics, although there are compiler workarounds.

System F’s type system is often called impredicative. A definition of impredicativity is when quantifiers whose domain includes the thing being defined itself.

For example, the type X = \forall tau. tau -> tau ranges over all types, including X itself.

Impredicativity is a terminology from logic and it is quite confusing.

• ML uses a fragment of System F (?) called let-polymorphism.
• Girard extended System F with higher-order polymorphism, yielding System F_omega.

I haven’t read beyond the abstract, but it’s related to parametricity, System F, and System F_omega.

They introduce the dependency core calculus for studying dependency analyses (secure information flow). The key property provided by DCC is noninterference, guaranteeing that a low-level observer does not distinguish high-level computations from low-level ones.

They then present a translation from DCC into F_omega, and prove that the translation prserves non-intereference.

The proof of noninterference for DCC suggests a connection to parametricity in System F, which suggests that it should be possible to implement dependency analyses in languages with parametric polymorphism.

I don’t really know what that means.