Normal currying describes an isomorphism between functions of type (A x B) -> C and functions of type A -> (B -> C). With dependent types, we can have an isomorphism between functions of type ((a : A) x (b : P(a))) -> Q(a, b) and functions of type (a : A) -> ((b : P(a)) -> Q(a, b)). What your article proves is a bit less generic with Q doesn't vary accoring to a and b; i.e. an isomorphism between ((a : A) x (b : P(a))) -> Q and functions of type (a : A) -> ((b : P(a)) -> Q).
I don't want to make it seem like I'm proving anything novel here, the proof I work through is definitely pretty basic as far as proofs go. It's written somewhat narratively because it reflects a train of thought I went through a few days ago when reading about existential types in Rust. Seeing the theorem ((∃ x. P(x)) → Q) ⇔ (∀ x. (P(x) → Q)) in the blog post made me want see if I still remembered enough Coq to prove it, and then when I was sitting down this morning to write something I thought it would make a good blog post as it explores some deep cuts of what I've been learning in Rust and might make a good introduction for people into Coq. I'll definitely take it on the chin that I titled the blog too ambitiously however and I'll be more modest with my titles in the future.
Comments
Personally, I find the title to be slightly misleading as the proof is essentially just (un)currying for dependently typed function.
I’m not sure I understand the connection to dependent types, would you be able to elaborate?
Normal currying describes an isomorphism between functions of type (A x B) -> C and functions of type A -> (B -> C). With dependent types, we can have an isomorphism between functions of type ((a : A) x (b : P(a))) -> Q(a, b) and functions of type (a : A) -> ((b : P(a)) -> Q(a, b)). What your article proves is a bit less generic with Q doesn't vary accoring to a and b; i.e. an isomorphism between ((a : A) x (b : P(a))) -> Q and functions of type (a : A) -> ((b : P(a)) -> Q).
Yeah that makes sense, thanks for explaining.
I don't want to make it seem like I'm proving anything novel here, the proof I work through is definitely pretty basic as far as proofs go. It's written somewhat narratively because it reflects a train of thought I went through a few days ago when reading about existential types in Rust. Seeing the theorem ((∃ x. P(x)) → Q) ⇔ (∀ x. (P(x) → Q)) in the blog post made me want see if I still remembered enough Coq to prove it, and then when I was sitting down this morning to write something I thought it would make a good blog post as it explores some deep cuts of what I've been learning in Rust and might make a good introduction for people into Coq. I'll definitely take it on the chin that I titled the blog too ambitiously however and I'll be more modest with my titles in the future.