Code review: Pretty-printing and Display term of Anchor

mietek / epigram2

Mirror of Epigram 2, by Conor McBride, et al.

https://code.google.com/p/epigram

MIT License

47 stars 7 forks source link

Code review: Pretty-printing and Display term of Anchor #61

Open GoogleCodeExporter opened 8 years ago

GoogleCodeExporter commented 8 years ago

In Features.Anchor, I wanted to have some Anchor-specific pretty-printing. 
However, I don't really understand the subtle difference between defining a 
CanPretty; or defining a display version of a term and explaining how to 
distill this object.

I think that what I did with Anchor/DAnchor is a mistake: I should have defined 
everything in term of CanPretty. Isn't it?

Original issue reported on code.google.com by pedag...@gmail.com on 29 Aug 2010 at 1:15

GoogleCodeExporter commented 8 years ago

Defining a new constructor for display terms is only necessary when the display 
language needs to represent something differently to the evidence language. For 
example, DEqBlue is defined so it can take two DExTms (instead of type-term 
pairs, as with EqBlue). Otherwise, one should just use the CanPretty aspect. I 
do not think anchors need a different representation, so they should use a 
single canonical constructor.

Original comment by adamgundry on 31 Aug 2010 at 1:21