=Paper=
{{Paper
|id=Vol-3009/abstract4
|storemode=property
|title=The Yoneda Reduction of Polymorphic Types (Abstract)
|pdfUrl=https://ceur-ws.org/Vol-3009/abstract4.pdf
|volume=Vol-3009
|authors=Paolo Pistone,Luca Tranchini
|dblpUrl=https://dblp.org/rec/conf/kr/PistoneT21
}}
==The Yoneda Reduction of Polymorphic Types (Abstract)==
https://ceur-ws.org/Vol-3009/abstract4.pdf
The Yoneda Reduction of Polymorphic Types
(Abstract)‹ ‹‹
Paolo Pistone1 and Luca Tranchini2
1
DISI, Università di Bologna, Mura Anteo Zamboni,7, I-40126, Bologna
2
Wilhelm-Schickard-Institut, Universität Tübingen, Sand 13, D-72076, Tübingen
paolo.pistone2@unibo.it
luca.tranchini@gmail.com
Abstract. We explore a family of type isomorphisms in System F whose
validity corresponds, semantically, to some form of the Yoneda isomor-
phism from category theory. These isomorphisms hold under theories of
equivalence stronger than βη-equivalence, like those induced by para-
metricity and dinaturality. We show that the Yoneda type isomorphisms
yield a rewriting over types, that we call Yoneda reduction, which can be
used to eliminate quantifiers from a polymorphic type, replacing them
with a combination of monomorphic type constructors. We establish
some sufficient conditions under which quantifiers can be fully elimi-
nated from a polymorphic type, and we show some application of these
conditions to count the inhabitants of a type and to compute program
equivalence in some fragments of System F.
Keywords: Type isomorphism · Yoneda Lemma · Propositional quan-
tification.
1 Introduction
The study of type isomorphisms is a fundamental one both in the theory of
programming languages and in logic, through the well-known proofs-as-programs
correspondence: type isomorphisms supply programmers with transformations
allowing them to obtain simpler and more optimized code, and offer new insights
to understand and refine the syntax of type- and proof-systems.
‹
This extended abstract is an excerpt from the long version of a paper which the
authors have recently published in the proceedings of CSL 21 [21]. The long version of
the paper (available at https://arxiv.org/abs/1907.03481) contains more detailed
proofs and some additional results compared to [21].
‹‹
We thank the anonymous reviewers for interesting insights, and in particular for
pointing us to a similarity between the type isomorphisms studied in this paper
and a result known as Ackermann’s Lemma in the field of second-order quantifier
elimination (see [11], section 6).
Copyright © 2021 for this paper by its authors. Use permitted under Creative
Commons License Attribution 4.0 International (CC BY 4.0).
The Yoneda Reduction of Polymorphic Types 93
Roughly speaking, two types A, B are isomorphic when one can transform
any call by a program to an object of type A into a call to an object of type
B, without altering the behavior of the program. Thus, type isomorphisms are
tightly related to theories of program equivalence, which describe what counts as
the observable behavior of a program, so that programs with the same behavior
can be considered equivalent.
The connection between type isomorphisms and program equivalence is of
special importance for polymorphic type systems like System F (hereafter Λ2).
In fact, while standard βη-equivalence for Λ2 and the related isomorphisms are
well-understood [7,8], stronger notions of equivalence (as those based on para-
metricity or free theorems [29,16,1]) are often more useful in practice but are
generally intractable or difficult to compute, and little is known about the type
isomorphisms holding under such theories.
A cornerstone result of category theory, the Yoneda lemma, is sometimes
invoked [3,13,5,27,14] to justify some type isomorphisms in Λ2 like e.g.
@X.pA ñ Xq ñ pB ñ Xq ” B ñ A @X.pX ñ Aq ñ pX ñ Bq ” A ñ B
(‹)
which do not hold under βη-equivalence, but only under stronger equivalences.
Such isomorphisms are usually justified by reference to the interpretation of
polymorphic programs as (di)natural transformations [3], a well-known seman-
tics of Λ2 related to both parametricity [23] and free-theorems [28], and yielding
a not yet well-understood equational theory over the programs of Λ2 [12,17,20],
that we call here the ε-theory. Other isomorphisms, like those in Fig. 1, can be
justified in a similar way as soon as the language of Λ2 is enriched with other
type constructors like 1, 0, `, ˆ, ñ and least/greatest fixpoints µX.A, νX.A.
All such type isomorphisms have the effect of eliminating a quantifier, replac-
ing it with a combination of monomorphic type constructors, and can be used to
test if a polymorphic type has a finite number of inhabitants (as illustrated in
Fig. 2) or, as suggested in [5], to devise decidable tests for program equivalence.
In this paper we develop a formal study of the elimination of quantifiers from
polymorphic types using a class of type isomorphisms, that we will call Yoneda
type isomorphisms, which generalize the examples above. Then, we explore the
application of such type isomorphisms to establish properties of program equiv-
alence for polymorphic programs.
2 A Type-Rewriting Theory of Polymorphic Types
In the first part of the paper we investigate the type-rewriting arising from
Yoneda type isomorphisms and its connection with proof-theoretic techniques
to count type inhabitants.
2.1 Counting type inhabitants with type isomorphisms.
Examples like the one in Fig. 2 suggest that, while arising from a categorical read-
ing of polymorphic programs, Yoneda Type Isomorphisms have a proof-theoretic
94 Paolo Pistone and Luca Tranchini
@X.X ñ X ñ A ” ArX ÞÑ 1 ` 1s (˚)
@X.pA ñ Xq ñ pB ñ Xq ñ C ” CrX ÞÑ µX.A ` Bs (˚˚)
@X.pX ñ Aq ñ pX ñ Bq ñ D ” DrX ÞÑ νX.A ˆ Bs (˚ ˚ ˚)
Fig. 1: Other examples of Yoneda type isomorphisms, where X only occurs positively
in A, B, C and only occurs negatively in D.
flavor. To demonstrate this, we show that the use of such isomorphisms to count
type inhabitants can be compared with some well-known proof-theoretic suffi-
cient conditions for a simple type A to have a unique or finitely many inhabitants
[2,6], namely the balancedness, negatively-non duplicated and positively-non du-
plicated conditions. We show that whenever an inhabited simple type A satisfies
any of the first two conditions (resp. a special case of the third), then its uni-
versal closure @X1 . . . @Xn .A can be converted to 1 by applying Yoneda type
isomorphisms and usual βη-isomorphisms, and when A satisfies a special case
of the third, then it can be converted to 1 ` ¨ ¨ ¨ ` 1. Furthermore, we suggest
that the appearance of the fixpoints in isomorphisms like p˚˚q can be related
to a well-known approach to counting type inhabitants by solving systems of
polynomial fixpoint equations [30].
2.2 Eliminating Quantifiers with Yoneda Reduction
We then turn to investigate in a more systematic way the quantifier-eliminating
rewriting over types arising from the left-to-right orientation of Yoneda type
isomorphisms. A major obstacle here is that the rewriting must take into account
possible applications of βη-isomorphisms, whose axiomatization is well-known to
be challenging in presence of the constructors `, 0 [10,15] (not to say of µ, ν). For
this reason we introduce a family of rewrite rules, that we call Yoneda reduction,
defined not directly over types but over a class of finite trees which represent the
types of Λ2 (but crucially not those made with 0, `, . . . ) up to βη-isomorphism.
Using this rewriting we establish some sufficient conditions for eliminating
quantifiers, based on elementary graph-theoretic properties of such trees, which
in turn provide some new sufficient conditions for the finiteness of type inhabi-
tants of polymorphic types. First, we prove quantifier-elimination for the types
satisfying a certain coherence condition which can be seen as an instance of the
2-SAT problem. We then introduce a more refined condition by associating each
polymorphic type A with a value κpAq P t0, 1, 8u, that we call the characteristic
of A, so that whenever κpAq ‰ 8, A rewrites into a monomorphic type, and
when furthermore κpAq “ 0, A converges to a finite type. In the last case our
method provides an effective way to count the inhabitants of A.
The computation of κpAq is somehow reminiscent of linear logic proof-nets,
as it is obtained by inspecting the existence of cyclic paths in a graph obtained
by adding some “axiom-links” to the tree-representation of A.
The Yoneda Reduction of Polymorphic Types 95
@X.X ñ X ñ @Y.p@Z.pZ ñ Xq ñ p@W.pW ñ Zq ñ W ñ Xq ñ Z ñ Y q ñ pX ñ Y q ñ Y
p˚q
” @Y.p@Z.pZ ñ 1 ` 1q ñ p@W.pW ñ Zq ñ W ñ 1 ` 1q ñ Z ñ Y q ñ p1 ` 1 ñ Y q ñ Y
(‹)
” @Y.p@Z.pZ ñ 1 ` 1q ñ pZ ñ 1 ` 1q ñ Z ñ Y q ñ p1 ` 1 ñ Y q ñ Y
p˚˚˚q
” @Y.ppνZ.p1 ` 1q ˆ p1 ` 1qq ñ Y q ñ p1 ` 1 ñ Y q ñ Y
p˚˚q
” µY.pνZ.p1 ` 1q ˆ p1 ` 1qq ` p1 ` 1q ” 1 ` 1 ` 1 ` 1 ` 1 ` 1
Fig. 2: Short proof that a Λ2-type has 6 inhabitants, using type isomorphisms.
3 Program Equivalence in System F with Finite
Characteristic
In the second part of the paper we direct our attention to programs rather
than types, and we exploit our results on type isomorphisms to establish some
non-trivial properties of program equivalence for polymorphic programs in some
suitable fragments of Λ2.
3.1 Computing equivalence with type isomorphisms
Computing program equivalence under the ε-theory can be a challenging task,
as this theory involves global permutations of rules which are difficult to detect
and apply [17,20,26,22,28]. Things are even worse at the semantic level, since
computing with dinatural transformations can be rather cumbersome, due to
the well-known fact that such transformations need not compose [3,18].
Nevertheless, our approach to quantifier-elimination based on the notion
of characteristic provides a way to compute program equivalence without the
appeal to ε-rules, free theorems and parametricity, since all polymorphic pro-
grams having types of finite characteristic can be embedded inside well-known
monomorphic systems. To demonstrate this fact, we introduce two fragments
Λ2κď0 and Λ2κď1 of Λ2 in which types have a fixed finite characteristic, and we
prove that these are equivalent, under the ε-theory, respectively, to the simply
typed λ-calculus with finite products and co-products (or, equivalently, to the
free bicartesian closed category B), and to its extension with µ, ν-types (that is,
to the free cartesian closed µ-bicomplete category µB [24,4]). Using well-known
facts about B and µB [25,4,19], we finally establish that the ε-theory is decidable
in Λ2κď0 and undecidable in Λ2κď1 .
3.2 Program equivalence and predicativity
We provide an example of how the correspondence between polymorphic types
of finite characteristic and µ, ν-types can be used to prove non-trivial properties
of program equivalence. A main source of difficulty with Λ2 is that polymorphic
programs are impredicative, that is, a program of universal type @X.A can be
instantiated at any type B, yielding a program of type ArB{Xs. It is thus useful
to be able to predict when a complex type instantiation can be replaced by a
one of smaller complexity, without altering the program behavior.
96 Paolo Pistone and Luca Tranchini
Using the fact that a universal type @X.A of finite characteristic in which A
is of the form A1 ñ . . . ñ An ñ X is isomorphic to the initial algebra µX.T
of some appropriate functor T , we establish a sufficient condition under which
a program containing an instantiation of @X.A as ArB{Xs can be transformed
into one with instantiations of types strictly less complex than B.
We finally use this condition to provide a simpler proof of a result from [22],
showing that all programs in a certain fragment of Λ2κď0 (the fragment freely
generated by the embedding of finite sums and products) can be transformed
into predicative programs only containing atomic type instantiations, a result
related to some recent investigations on atomic polymorphism [9].
References
1. Ahmed, A., Jamner, D., Siek, J.G., Wadler, P.: Theorems for free for free: para-
metricity, with and without types. In: Proceedings of the ACM on Programming
Languages. ICFP, vol. 1, p. Article No. 39. New York (2017)
2. Aoto, T.: Uniqueness of normal proofs in implicational intuitionistic logic. Journal
of Logic, Language and Information 8, 217–242 (1999)
3. Bainbridge, E., Freyd, P.J., Scedrov, A., Scott, P.J.: Functorial polymorphism.
Theoretical Computer Science 70, 35–64 (1990)
4. Basold, H., Hansen, H.H.: Well-definedness and observational equivalence for
inductive-coinductive programs. Journal of Logic and Computation exw091 (2016)
5. Bernardy, J.P., Jansson, P., Claessen, K.: Testing Polymorphic Properties. In:
ESOP 2010: Programming Languages and Systems. Lecture Notes in Computer
Science, vol. 6012, pp. 125–144. Springer Berlin Heidelberg (2010)
6. Broda, S., Damas, L.: On long normal inhabitants of a type. Journal of Logic and
Computation 15, 353–390 (2005)
7. Bruce, K.B., Di Cosmo, R., Longo, G.: Provable isomorphisms of types. Mathe-
matical Structures in Computer Science 1, 1–20 (1991)
8. Di Cosmo, R.: A short survey of isomorphisms of types. Mathematical Structures
in Computer Science 15, 825–838 (2005)
9. Ferreira, F., Ferreira, G.: Atomic polymorphism. Journal of Symbolic Logic 78(1),
260–274 (2013)
10. Fiore, Di Cosmo, R., Balat, V.: Remarks on isomorphisms in typed lambda calculi
with empty and sum types. Annals of Pure and Applied Logic 141(1–2), 35–50
(2006)
11. Gabbay, D.M., Schmidt, R., Szalas, A.: Second-order Quantifier Elimination. Col-
lege publications (2008)
12. Girard, J.Y., Scedrov, A., Scott, P.J.: Normal forms and cut-free proofs as natural
transformations. In: Moschovakis, Y. (ed.) Logic from Computer Science, vol. 21,
pp. 217–241. Springer-Verlag (1992)
13. Hasegawa, R.: Categorical data types in parametric polymorphism. Mathematical
Structures in Computer Science 4(1), 71–109 (1994)
14. Hinze, R., James, D.W.: Reason isomorphically! In: WGP 2010. pp. 85–96 (2010)
15. Ilik, D.: Axioms and decidability for type isomorphism in the presence of sums.
In: Proceedings of the Joint Meeting of the Twenty-Third EACSL Annual Confer-
ence on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE
Symposium on Logic in Computer Science (LICS) (2014)
The Yoneda Reduction of Polymorphic Types 97
16. Johann, P.: On proving the correctness of program transformation based on free
theorems for higher-order polymorphic calculi. Mathematical Structures in Com-
puter Science 15, 201–229 (2005)
17. de Lataillade, J.: Dinatural terms in System F. In: Proceedings of the Twenty-
Fourth Annual IEEE Symposium on Logic in Computer Science (LICS 2009). pp.
267–276. IEEE Computer Society Press, Los Angeles, California, USA (2009)
18. McCuscker, G., Santamaria, A.: On compositionality of dinatural transformations.
In: CSL 2018. LIPIcs, vol. 119, pp. 33:1–33:22. Schloss Daghstuhl–Leibinz-Zentrum
fuer Informatik, Dagstuhl, Germany (2018)
19. Okada, M., Scott, P.: A note on rewriting theory for uniqueness of iteration. Theory
and Applications of Categories 6, 47–64 (1999)
20. Pistone, P.: On dinaturality, typability and βη-stable models. In: fuer Informatik,
S.D.L.Z. (ed.) 2nd International Conference on Formal Structures for Computa-
tion and Deduction (FSCD 2017). Leibniz International Proceedings in Informatics
(LIPIcs), vol. 84, pp. 29:1–29:17. Dagstuhl, Germany (2017)
21. Pistone, P., Tranchini, L.: The Yoneda Reduction of Polymorphic Types. In: Com-
puter Science Logic 2021 (CSL 2021). LIPIcs–Leibniz International Proceedings in
Informatics, vol. 183, pp. 35:1–35:22 (2021)
22. Pistone, P., Tranchini, L., Petrolo, M.: The naturality of natural deduction (II).
On atomic polymorphism and generalized propositional connectives. Studia Logica
(2021). https://doi.org/10.1007/s11225-021-09964-z
23. Plotkin, G., Abadi, M.: A logic for parametric polymorphism. In: TLCA ’93, In-
ternational Conference on Typed Lambda Calculi and Applications. Lecture Notes
in Computer Science, vol. 664, pp. 361–375. Springer Berlin Heidelberg (1993)
24. Santocanale, L.: Free µ-lattices. Journal of Pure and Applied Algebra 9, 166–197
(2002)
25. Scherer, G.: Deciding equivalence with sums and the empty type. In: Proceedings
of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages.
pp. 374–386. POPL 2017, ACM, New York, NY, USA (2017)
26. Tranchini, L., Pistone, P., Petrolo, M.: The naturality of natural deduction. Studia
Logica 107(1), 195–231 (2019)
27. Uustalu, T., Vene, V.: The Recursion Scheme from the Cofree Recursive Comonad.
Electronic Notes in Theoretical Computer Science 229(5), 135–157 (2011)
28. Voigtländer, J.: Free theorems simply, via dinaturality. In: Declarative Program-
ming and Knowledge Management. pp. 247–267. Springer International Publishing,
Cham (2020)
29. Wadler, P.: Theorems for free! In: Proceedings of the fourth international confer-
ence on functional programming languages and computer architecture - FPCA ’89
(1989)
30. Zaoinc, M.: Fixpoint technique for counting terms in typed lambda-calculus. Tech.
rep., State University of New York (1995)