Zainab Ali - Recursion Schemes from First Principles

This is about a paper published in 1991: Functional programming with bananas, lenses, envelopes and barbed wire by Erik Meijer, Maarten Fokkinga & Ross Paterson. Other references to articles and papers by Milewski, Wadler and Gibbons at 32:48. I also came across this paper by Wadler: The Girard-Reynolds Isomorphism.

I wish I had known about this, it would have saved me several years of work! Mike Gordon presumably didn't know about it either: see Emily Riehl and Terrence Tau on The Future of Mathematics.

Subscribe to Lambda World.

And I just found this 2016 ICFP talk by Dan Licata on Functional programming and Homotopy Type Theory.

At 45:54 there is an example of taking this idea of higher inductive types to verify interpreters.

Subscribe to ICFP.

This was  given in 2019. See Cubical Agda: A Dependently Typed Programming Language with Univalence and Higher Inductive Types:

The principle of univalence is the major new addition in Homotopy Type Theory and Univalent Foundations (HoTT/UF) (Univalent Foundations Program, 2013). However, these new type-theoretic foundations add univalence as an axiom which disrupts the good constructive properties of type theory. In particular, if we transport addition on binary numbers to the unary representation we will not be able to compute with it as the system would not know how to reduce the univalence axiom. Cubical type theory (Cohen et al., 2018) addresses this problem by introducing a novel representation of equality proofs and thereby providing computational content to univalence. This makes it possible to constructively transport programs and properties between equivalent types. This representation of equality proofs has many other useful consequences, in particular function and propositional extensionality (pointwise equal functions and logically equivalent propositions are equal), and the equivalence between bisimilarity and equality for coinductive types (Vezzosi, 2017). 

Subscribe to ACM SIGPLAN.

Thorsten Altenkirch on Equality Types and the Uniqueness of Identity Proofs

 

And part II where he demonstrates how to prove properties of functional programs in Agda:

 

Subscribe to Computerphile.

See About Logic - Interview with Steve Awodey:

 

My comment:

What great discussion. For a long time I have thought all philosophers should learn to use functional programming languages and this proves my point. At 40:06 about isomorphism being the only relation on types which behaves like an equality: what about bisimulation? I am not sure what a bisimulation relation between two types would look like apart from the obvious case of graphs, but still, ... non-well-founded set theory is really just an embedding into graph theory, isn't it? I think Cubical Agda uses an intuition about computing "the equivalence between bisimilarity and equality for coinductive types" and apparently it's explained in "Vezzosi, A. (2017) Streams for Cubical Type Theory." I found this reference in "Cubical Agda: A Dependently Typed Programming Language with Univalence and Higher Inductive Types" by Vezzosi, Mortberg and Abel. 

See also this 1999 paper by R. Hennicker and A. Kurz: (Ω, Ξ)-Logic: On the Algebraic Extension of Coalgebraic Specifications. I wonder whether there is some more general notion of bisimilarity which uses simulation relations as left and right adjoints in a Galois connection. This might give a distinct notion of trisimilarity which would not necessary reduce to transitivity of a pairwise bisimilarity relation. It is structures like this which I think lie behind some of the puzzling observational features of quantum mechanical systems and special relativity. See this comment by Tim Maudlin talking about Sydney Shoemaker's Time Without Change and this paper: Elements of the General Theory of Coalgebras by H. Peter Gumm.

At 22:42 in the talk about Cubical Agda above, there is a question about coinductive "sized types" and equality.  According to Google, sized types "... annotate inductive and coinductive data types with ordinal sizes to track structural depth, enabling the compiler's termination checker to accept a wider range of recursive and corecursive functions. They ensure that recursive calls operate on smaller sub-structures (termination) or produce finite observations of infinite structures (productivity)". See also Three Equivalent Ordinal Notation Systems in Cubical Agda by Fredrik Nordvall Forsberg, Chuangjie Xu and Neil Ghani:

We present three ordinal notation systems representing ordinals below ε₀ in type theory, using recent type-theoretical innovations such as mutual inductive-inductive definitions and higher inductive types. We show how ordinal arithmetic can be developed for these systems, and how they admit a transfinite induction principle. We prove that all three notation systems are equivalent, so that we can transport results between them using the univalence principle. All our constructions have been implemented in cubical Agda.

Now go back up and watch that talk by Zainab Ali about Peeling the Banana again! 

Subscribe to About Logic.