search

diprism / perpl

The PERPL Compiler
MIT License
10 stars 5 forks source link

== for recursive datatypes too restrictive #135

Open colin-mcd opened 1 year ago

colin-mcd commented 1 year ago

Currently, doing == comparison on a recursive datatype ends up forcing both sides to have the same tags, though this is not actually necessary. As a consequence, using == on a datatype unnecessarily prevents refunctionalization. If you were to write out a comparison function for List A, the compiler would allow the two args to have different tags and in many cases would be able to refunctionalize them.

See tagged_rec_eq.ppl for an example of what we'd like to be able to do.

colin-mcd commented 1 year ago

I think solving this would involve splitting monomorphization into two steps: monomorphizing datatype parameters, and then datatype tags. Then, we would need to put the RecEq phase between the two steps, so that it happens after datatype parameters have been monomorphized (e.g. the A in List #n A but before the #n goes away), and generalizing RecEq to work with tags (right now it assumes tags are gone).