Seminar

Wednesday, February 10th, 2021, 16:30, on Zoom.

Paolo Pistone (Bologna)
The Yoneda Reduction of Polymorphic Types (joint work with Luca Tranchini)

Abstract:

We explore a family of type isomorphisms in System F whose validity corresponds, semantically, to some form of the Yoneda isomorphism from category theory. These isomorphisms hold under theories of equivalence stronger than βη-equivalence, like those induced by parametricity and dinaturality. Based on such isomorphisms, we investigate 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 then demonstrate some applications of this rewriting to problems like counting the inhabitants of a type or characterizing program equivalence in some fragments of System F.

The seminar will be held on Zoom. In order to get access to the Zoom meeting, please contact Peter Schuster or Giulio Fellin.