Thorsten Altenkirch on NaÏve Type Theory and An Interesting and Useful Duality

Who said naῗve?

Subscribe to FOMUS 2016.

There's a thing which, in 1998, Philip Wadler named The Expression Problem. See Tillmann Rendel - Automatic Refunctionalization to a Language with Copattern Matching.

Niklas Broberg: Revisiting the Expression Problem (December 2025): 

See Data types à la carte by Wouter Swierstra and Trees That Grow by Shayan Najd and Simon Peyton Jones. Another oft-cited paper is one published in 1990 entitled Object-oriented programming versus abstract data types by William R. Cook with a follow-up in 2009 entitled On Understanding Data Abstraction, Revisited.

51:01 One neat way to deal with complex boilerplate code is to write a syntactic transform.  See A Syntax for Composable Data Types in Haskell, A User-friendly Syntax for Solving the Expression Problem by Anna Romeborn and Fredrik Albers.

References and recent work: 

So, that's how far 27 years got us, ... 

Subscribe to chalmersfpunit.

In 2004 Subtyping for Session Types in the Pi Calculus by Simon Gay and Malcolm Hole solved a similar problem in communications protocols:

We define a notion of subtyping for session types, which allows protocol specifications to be extended in order to describe richer behaviour; for example, an implemented server can be refined without invalidating type-correctness of an overall system. We formalize the syntax, operational semantics and typing rules of an extended pi calculus, prove that typability guarantees absence of run-time communication errors, and show that the typing rules can be transformed into a practical typechecking algorithm. 

See this note for more references on session types. 

Simon Gay on Linear Logic, Session Types and Deadlock:

Part of a series of talks on Compositionality in 2016.

Subscribe to Simons Institute.

Subscribe to Category Theory Proofs.

I really believe that the only reason these similarities noted above aren't strict isomorphisms with Category theory proofs is that they have not been put in the right context in which they naturally appear as Adjunctions with associated Universal objects. I mean, what's the essential difference between, on the one hand, two pairs of mutually recursive functions, one pair of which deconstructs one data type and constructs another and the other pair of which perform an inverse transformation; and on the other hand a pair of communicating processes connected by a bidirectional channel over which they exchange messages? Of course the answer depends upon what these functions and the communications processes actually do, but having established type disciplines for each, one ought to be able to identify the class of algorithms that could be implemented this way by establishing a natural transformation between the two representations, so you would then have a framework in which you could express composable processes which would be correct by construction. See Programming Paradigms.