Parametericity

Stream: lean4

[Alex Meiburg]

I'm wondering if these types of statements are provable in Lean:

import Mathlib

--If I can make a β from an α and an (α→β), it must be the function applied.
theorem func_eq_apply (F : (α β : Type*) → α → (α → β) → β) : F = (fun _ _ a f ↦ f a) := by
  sorry

--If I can make a β from an (α→β), it must be a particular value plugged in.
theorem exists_domain {α : Type*} (F : (β : Type*) → (α → β) → β) :
    ∃ a, F = (fun _ f ↦ f a) := by
  sorry

--A function that compares elements of any DecidableEq type must be either a constant,
-- the equality function, or the nonequality function.
theorem compare_four_options (F : (α : Type*) → [DecidableEq α] → α → α → Bool) :
    F ∈ ({
        fun _ _ _ _ ↦ true,
        fun _ _ _ _ ↦ false,
        fun _ i x y ↦ by exact (let _ := @instBEq _ i; x == y),
        fun _ i x y ↦ by exact (let _ := @instBEq _ i; x != y)}
      : Set _)
    := by
  sorry

example:

--Example usage of func_eq_apply: knowing what "applier" must be based on its type signature.
opaque applier (a : α) (f : α → β) : β :=
  f a

theorem must_be_applier {α β : Type*} (a : α) (f : α → β) : applier a f = f a := by
  rw [func_eq_apply @applier]

I know that these are provable in some type systems; I've been told repeatedly by different people that, for instance, the Haskell compiler knows theorems like this about its type system

[Alex Meiburg]

These theorems become false if, for instance, you allow functions to "inspect" arbitrary data they know nothing about. For instance, I could make a function that takes two αs with [DecidableEq α], looks at the first bit of their representation in memory, and then returns true if either of those bits is a one. That would contradict compare_four_options. But I think that with the functions you can 'normally' build in Lean those three examples all hold.

[Alex Meiburg]

If Lean doesn't support proving those statements as-is, is there maybe a (finite list of) axioms that one could add that would all these statements provable...?

[Kyle Miller]

It looks like you're thinking along the lines of Wadler's paper "Theorems for free!" https://people.mpi-sws.org/~dreyer/tor/papers/wadler.pdf

[Kyle Miller]

In Lean, I'm pretty sure each of your examples are false, because you can make a function that does different things depending on what the type equals.

You need some sort of naturality condition on the function (I don't know exactly what I'm talking about, so I can't say exactly what I mean), or know something about the syntax of the function to be able to deduce that.

[Kyle Miller]

Here's a contradiction:

axiom func_eq_apply (F : (α β : Type*) → α → (α → β) → β) : F = (fun _ _ a f ↦ f a)

open scoped Classical in
noncomputable def badF (α β : Type) (x : α) (f : α → β) : β :=
  if h : β = Bool then
    h ▸ true
  else
    f x

example : False := by
  have := func_eq_apply badF
  have := congrFun (congrFun (congrFun (congrFun this Unit) Bool) ()) (fun _ => false)
  simp [badF] at this

[Alex Meiburg]

I was actually just writing something almost identical to try myself. :)

opaque bad_applier (a : α) (f : α → β) : β := by
  by_cases h : α = Nat
  · exact f (h ▸ 0)
  · exact f a

[Alex Meiburg]

(That doesn't compile because it needs to be marked noncomputable)

[Alex Meiburg]

I think the only "naturality" condition needed is that it's all computable.

[Kyle Miller]

I think it's possible to avoid choice and make it computable.

[Alex Meiburg]

Ah, that would be interesting to see. I'm skeptically disagreeing atm but would love to see an example if you can!

[Alex Meiburg]

If you can do it with computable functions then I accept that this is not a thing that should be provable in Lean because it's wrong :P

[Alex Meiburg]

if you computable functions are safe, then I guess my question becomes "is it possible to prove these things for computable functions" and in particular "is it even possible to add syntactic constraints that functions are computable"

[Alex Meiburg]

Kyle Miller said:

It looks like you're thinking along the lines of Wadler's paper "Theorems for free!" https://people.mpi-sws.org/~dreyer/tor/papers/wadler.pdf

and yes that's what I was thinking of, forgot the name. It looks like there might be relevant axioms in there, now I have some search terms I'll see what I can glean

[Kyle Miller]

There's at least the problem that you can prove a contradiction:

axiom func_eq_apply (F : (α β : Type*) → α → (α → β) → β) : F = (fun _ _ a f ↦ f a)

example : False := by
  classical
  let badF (α β : Type) (x : α) (f : α → β) : β :=
    if h : β = Bool then
      h ▸ true
    else
      f x
  have := func_eq_apply badF
  have := congrFun (congrFun (congrFun (congrFun this Unit) Bool) ()) (fun _ => false)
  simp [badF] at this

let bindings inside of proofs don't need to pass the computability checker.

[Alex Meiburg]

Right yeah, I see that, so func_eq_apply is clearly false as written. That's why I'm asking if it's possible to write something like

axiom func_eq_apply (F : (α β : Type*) → α → (α → β) → β) (hF : Computable F) : F = (fun _ _ a f ↦ f a)

that might work instead.

[Kyle Miller]

That certainly seems plausible to me. Computable F could be defined by saying that F is could be put into a particular form that you can use to inductively prove this statement. (It could be a theorem, not an axiom.)

[Alex Meiburg]

Mm. And then we'd either need (1) a bunch of instances generating instances enough to synthesize that wherever needed; or (2) an axiom / something in the kernel to automatically synthesize Computable F whenever F isn't noncomputable.

[Kyle Miller]

noncomputable is a concept that's outside Lean's type theory (and outside the kernel). It's whether the compiler was able to figure out how to lower the definition down into something that can be compiled to C

[Alex Meiburg]

Alright. I guess that's what I was afraid to hear (esp the "outside the type theory") part.

[Kyle Miller]

but that's not to say that you can't formalize something that says "these functions are [insert the name of the right notion for getting theorems for free]" yourself and make some automation to try to derive proofs from definitions

[Alex Meiburg]

Right. Might be a fun thing to try... I've been writing some Decidability instances for fun, maybe this could be a fun thing to try and see if it's scalable or just pain

[Kyle Miller]

I guess a first step is to figure out how to write that predicate so that you get theorems for free. One element I was imagining is an inductive type that represents all the kinds of expressions you can deal with, along with an evaluation function. Then the predicate would be that there exists an expression of this type whose evaluation is equal.

[Kyle Miller]

(I've never done this before, so take this suggestion with a grain of salt.)

[Alex Meiburg]

Yeah. I think "constant functions" and "func_eq_apply" as two constructors might get 80% of the way there. (In that sense, func_eq_apply is sort of being used an 'axiom'). Terms and functions, right? :P

[Alex Meiburg]

I'mma try this and report back :saluting_face:

[Alex Meiburg]

... brain melted, giving up for now. Side question: is there a good way to prove stupid "type confusion" questions like

⊢ ¬(Prop → Prop) = (Empty → Empty)

or (equivalently, probably)

⊢ ¬(Bool → Bool) = (Nat → Nat)

[Kyle Miller]

I think you can only prove those using a cardinality argument.

[Kyle Miller]

Though it'd be best if you could avoid needing to prove any types are not equal to each other!

[Alex Meiburg]

I agree! This is coming from a stupid (and probably not actually working) attempt at a proof by contradiction on a certain toy case. It's not promising, but, I was stuck there anyway and curious

[Alex Meiburg]

I could prove that Prop ≠ Empty I think but wasn't sure how to turn my thing into that

[Kyle Miller]

Here's using congr quotations to apply Fintype.card (congr quotations are a mathlib extension that makes it easy to create congruences, even if there are complexities, like typeclass synthesis in this case).

example : ¬(Prop → Prop) = (Empty → Empty) := by
  intro h
  have := congr(Fintype.card $h)
  simp at this

[Kyle Miller]

I guess this works too

example : ¬(Prop → Prop) = (Empty → Empty) := by
  intro h
  have := congrArg Nat.card h
  simp at this

[Kyle Miller]

(this is in a file with import Mathlib)

[Alex Meiburg]

Nice! Thanks.

[Alex Meiburg]

Reading more about it, it seems like there's a decent attempt in Coq at this kind of stuff (by way of custom tactics to synthesize proofs from syntax trees) here: https://github.com/mit-plv/reification-by-parametricity/
accompanying paper at http://adam.chlipala.net/papers/ReificationITP18/ReificationITP18.pdf

[James Gallicchio]

That's very cool!

[Kim Morrison]

I've always wished I understood https://golem.ph.utexas.edu/category/2013/04/scones_logical_relations_and_p.html, but still don't. :-)

[Alex Meiburg]

but I hope I’ve convinced you that at least one reasonable possibility to consider for is the scone of : the comma category of IdSet over the global sections functor �=hom(1,−):Syn�→Set.

I'm sure he would have convinced me if I knew what that meant! :sweat_smile:

[Robert Maxton]

@Alex Meiburg I'm pretty sure your func_eq_apply is exactly the statement of the Yoneda lemma in Type for the functor Id. (Note that the type signature of F is just a curried functorial map with the arguments swapped.) I'm still working on formalizing the proof, but if I'm right, the requirements you need are the category theory axioms for functors -- namely that they map identity to identity and compositions to compositions. In practical terms, in addition to rigorizing "naturality", that also means no side effects, no global state, and a very restricted subset of dependent functions... though that seems like it might prove too much, since I think Haskell also has dependent functions and otherwise Lean is largely pure-functional?

(It does also rule out both of the contradictions above; the bad_appliers above don't map identity to identity on all types, which can then be detected purely at the type level via composition. It's not a coincidence that both of @Kyle Miller 's counterexamples derive False through applications of congrFun.)

[Robert Maxton]

Right, here you go:

import Mathlib.CategoryTheory.Types
import Mathlib.CategoryTheory.Yoneda

open CategoryTheory Opposite

structure LawfulEvaluator (F : Type u ⥤ Type u) (α : Type u) where
  eval {β : Type u} : (α → β) → F.obj β
  map_comp : ∀ {β γ : Type u} {f : α → β} {g : β → γ}, eval (g ∘ f) = F.map g (eval f)


theorem yoneda_Types (F : Type u ⥤ Type u) : LawfulEvaluator F α ≃ F.obj α := by
  let F' := unopUnop (Type u) ⋙ F
  have yoneda := yonedaEquiv (F := F') (X := op α)
  unfold_let F' at yoneda; unfold yoneda at yoneda; simp at yoneda
  apply Equiv.trans _ yoneda
  unfold unopUnop Functor.comp; simp
  refine ⟨
      λ eval' ↦
        ⟨λ ⟨⟨β⟩⟩ f ↦ eval'.eval (f.unop),
        λ ⟨⟨β⟩⟩ ⟨⟨γ⟩⟩ f ↦ ?nat⟩,
      λ η ↦ ⟨
        @λ β f ↦ η.app (op (op β)) ((↾f).op),
        @λ β γ f g ↦ ?map_comp⟩, ?left_inv, ?right_inv⟩
  case map_comp =>
    simp at η ⊢
    erw [op_comp]; eta_reduce
    let naturality :=
      FunctorToTypes.naturality (X:= op <| op β)
        (CategoryTheory.yoneda.obj <| op α) F' η ((↾g).op.op) ((↾f).op)
    simp [F'] at naturality
    rw [←naturality]
  case nat =>
    ext g
    simp at f g ⊢
    rw [types_comp, LawfulEvaluator.map_comp eval']
  case left_inv => aesop_cat
  case right_inv => aesop_cat

[Robert Maxton]

If we impose the additional restriction that a LawfulEvaluator be compatible with composition and the .map of a functor F, then the type of valid evaluators on α is equivalent to the type F.obj α, i.e they're basically just "hiding" a value of F.obj α and evaluating on it. In particular, if F is the identity functor, the extra constraint map_comp reduces to eval (g ∘ f) = g ∘ eval f), and there is exactly one lawful evaluator for every value of α, which evaluates all functions on that fixed value. More interestingly: even if F is not the identity, as long as F.obj is the identity (it sends α to α for all α : Type u), it is still true that any eval' can only differ from eval in a functorial (i.e. composable) way.

Nevermind, that doesn't quite prove what I wanted it to prove -- it just says that you have to be evaluating some function, calculated from f in functorial manner.