Streaming Metamorphisms in Agda

Josh Ko

Tuesday 11 June 2019
11:15 - 12:15
Room 1.83 , Earl Mountbatten Building


A metamorphism is a fold followed by an unfold, the former consuming a data structure to compute an intermediate value and the latter producing a codata structure from that value. Bird and Gibbons considered streaming metamorphisms on lists, which, under a commutativity condition, can possibly start producing the output without having to consume all the input. In Agda, we can encode a metamorphic specification in a type such that any program with that type correctly implements the metamorphism. In addition, for streaming metamorphisms, type information can help us find out the commutativity condition as we program the streaming algorithm in Agda’s interactive development environment.

LAIV/DSG joint seminar.

Hosts: Sven-Bodo Scholz and Katya Komendantskaya