Fighting with type universing

Stream: general

[Cayden Codel]

In my project, I want to include some reasoning from Wadler's "Theorems for Free!" I stated one of his metatheorems as an axiom and then tried to apply it in a theorem but failed. Lean 3 complained about the type of the polymorphic function. I suspect the problem is due to my use of Type* and how Lean 3 handles it, but I don't know how to resolve it. Perhaps something with declaring a universe? Below is a MWE.

-- If a function is polymorphic, it commutes with the map function
axiom wadler {α β : Type*} (f : ∀ {α : Type*}, list α → list α)
  (l : list α) (g : α → β) : f (l.map g) = (f l).map g

theorem fact {α : Type*} (f : ∀ {α : Type*}, list α → list α)
  (g : list bool → bool) (h : α → bool) (l : list α) :
  g (f (l.map h)) = g ((f l).map h) :=
begin
  rw wadler f l,
end

The error in Lean is

type mismatch at application
  wadler f
term
  f
has type
  list ?m_1 → list ?m_1 : Type
but is expected to have type
  Π {α : Type ?}, list α → list α : Type (?+1)

[Yaël Dillies]

Replace f by @f _ to force Lean to remove the {α : Type ?} argument.

[Cayden Codel]

Oh wow. Writing just @f instead of f works (adding the underscore kept the same error). Thanks!

[Yaël Dillies]

Ah right I misparsed the error! :D

[Kevin Buzzard]

import tactic

axiom wadler {α β : Type*} (f : ∀ {α : Type*}, list α → list α)
  (l : list α) (g : α → β) : f (l.map g) = (f l).map g

theorem not_wadler : false :=
begin
  classical,
  let f : ∀ (α : Type*), list α → list α := λ α, if α = ℕ then λ L, [] else λ L, L,
  have := wadler f [unit.star] (λ x, 37),
  simp [f, if_pos] at this,
  have foo : unit ≠ ℕ,
  { intro h,
    have : subsingleton unit := infer_instance,
    rw h at this,
    cases this with this,
    specialize this 0 1,
    cases this,
  },
  rw if_neg foo at this,
  cases this,
end

[Reid Barton]

Turns out, you get what you pay for

[Trebor Huang]

Parametricity is anti-classical, meaning it directly implies the negation of excluded middle. Also, Wadler seems to be in a system where there is no universe levels, and the forall can quantify over every type, including the type you are defining itself. So there isn't much hope doing this in Lean.

[Patrick Massot]

Trebor, Kevin is well-aware of all this. His answer is his way to say: I'm living in the real world, not a world of exotic logic.

[Kevin Buzzard]

I'm living in the world of mathematics departments is perhaps a more accurate way to say it. If you look at the axioms I use in my proof you can see I'm using classical ones. If you are careful you can probably still develop a theory using the wadler axiom in lean 3 but you'll have to be super careful that you check every result for classical axioms because you can't turn them off.

[Kevin Buzzard]

I remember reading the wadler paper and being so confused! I was trying to learn type theory at the time and I was just thinking "but all of these theorems are false!"

[Reid Barton]

The real (classically-valid) theorem is that the parametricity theorems hold for all the terms that you can define without axioms.

[Reid Barton]

It's internal parametricity that's anti-classical.

[Trebor Huang]

Kevin Buzzard said:

I remember reading the wadler paper and being so confused! I was trying to learn type theory at the time and I was just thinking "but all of these theorems are false!"

If you interpret forall as an intersection instead of an infinite product, then it does seem right even to mathematicians. id is the only function (understood in the Eulerian sense, i.e. defined by an expression, not in the modern sense, being defined by a correspondence relation) that is in the intersection of all the types x -> x.

[Reid Barton]

No, this doesn't make sense to mathematicians

[Kevin Buzzard]

For me "if then else" makes a lot of sense, maybe this is the problem

[Chris Hughes]

You also don't need to do weird case splits on equalities of Types to disprove it.

import Mathlib.Data.List.Dedup

axiom wadler {α β : Type _} (f : ∀ {α : Type _}, List α → List α)
  (l : List α) (g : α → β) : f (l.map g) = (f l).map g

theorem not_wadler : False := by
  classical have := @wadler Bool Bool (fun l => l.dedup) [true, false] (fun _ => false)
  rw [@List.dedup_cons_of_not_mem  _ (id _) _ _
      (mt List.mem_singleton.1 (show true ≠ false by decide))] at this
  simp [List.map, List.dedup_cons_of_mem (List.mem_singleton.2 rfl)] at this

[Reid Barton]

The constructivist take on this example is that List.dedup only works on types with decidable equality and so you only get a parametricity theorem that works on functions that preserve equality (i.e., injective functions).