Path, a program transformation system for haskell
Mark Tullsen, Paul Hudak · 2002
PATH (Programmer Assistant for Transforming Haskell) is a user-directed program transformation system for Haskell. This dissertation describes PATH and the technical contributions made in its development. PATH uses a new method for program transformation in which 1) total correctness is preserved, i.e., transformations can neither introduce nor eliminate non-termination; 2) infinite data structures and partial functions can be transformed; 3) generalization of programs can be done as well as specialization of programs; 4) neither an improvement nor an approximation relation is required to prove equivalence of programs—reasoning can be directly about program equivalence. Current methods (such as fold/unfold, expression procedures, and the tick calculus) all lack one or more of these features. PATH uses a more expressive logic for proving equivalence of programs than previous transformation systems. A logic more general than two-level horn clauses (used in the CIP transformation system) is needed but the full generality of first order logic is not required. This logic used in PATH lends itself to the graphical manipulation of program derivations (i.e., proofs of program equivalence). PATH incorporates a language extension which makes programs and derivations more generic: programs and derivations can be generic with respect to the length of tuples; i.e., a function can be written that works uniformly on 2-tuples, 3-tuples, and etc. iii ivCopyright c ○ 2002 by Mark Anders Tullsen All rights reserved. v viAcknowledgments I wish to thank my advisor Paul Hudak for many years of constructive criticism, guidance, and encouragement. I also wish to thank the other readers of this dissertation: John Peterson, Zhong Shao, and Tim Sheard. To my wife, Teresa, and my children Andrew, Rachel, Zachary, and Jonathan: a heartfelt thanks for your support and patience while I have been working on this dissertation. Soli Deo Gloria. vii viiiContents