mietek / epigram2

Mirror of Epigram 2, by Conor McBride, et al.
https://code.google.com/p/epigram
MIT License
48 stars 7 forks source link

Preventing clashes in the |Operators.OpName| name-space #71

Open GoogleCodeExporter opened 9 years ago

GoogleCodeExporter commented 9 years ago
This is a silly hack: the references of operators are hard-coded into the 
@Operators.OperatorName@ name-space (in Evidences.Operators). Therefore, in a 
development, one should not declare things in a such a way to end up polluting 
this name-space. 

A solution to this would be to "firewall" the |NameSupply| such as to avoid the 
definition of an |Operators| root name. But who would be stupid enough to 
pollute the operator name-space anyway?

Original issue reported on code.google.com by pedag...@gmail.com on 1 Sep 2010 at 9:52

GoogleCodeExporter commented 9 years ago
This arises with axioms and primitives as well. The principled way to do avoid 
clashes would be to make everything the user does live in a particular 
namespace, rather than at the root. Since we have no principles, we might as 
well do this when defining the source language rather than protecting Cochon 
users from this particular danger.

Original comment by adamgundry on 3 Sep 2010 at 7:47