Encodings In Polymorphism, revisited

We consider encodings in polymorphism with finite product types. These encodings are given in terms of I-algebras. They have the property that all canonical terms (ground terms) are normal terms. We transplant the proof of a well-known result to our setting and show why weak recursion is admissible. We also show how to carry out the dual encodings using the existential quantifier. Copyright c fl1993. All rights reserved. Reproduction of all or part of this work is permitted for educational or research purposes on condition that (1) this copyright notice is included, (2) proper attribution to the author or authors is made and (3) no commercial gain is involved. Technical Reports issued by the Department of Computer Science, Manchester University, are available by anonymous ftp from m1.cs.man.ac.uk (130.88.13.4) in the directory /pub/TR. The files are stored as PostScript, in compressed form, with the report number as filename. Alternatively, reports are available by post from The Comput..