[Agda] Incompatibilities affecting ``Fresh Look''

[Alan Jeffrey]

On 12/15/2010 11:37 AM, Andreas Abel wrote:
> On 12/15/10 6:13 PM, kahl at cas.mcmaster.ca wrote:
>> I had not been fully aware of this (I remember reading it, but so far
>> I have never felt tempted to seriously consider this possibility).
>> Does anybody have a good use case for that?
>> (I come from Haskell...)
>
> Yes.  Since you can have many refinements of the same structures, like
> refining list to vectors, sorted lists, sorted vectors, etc., it is
> convenient to allow them to share the name for nil and cons.
>
> Without overloading, we get nowwhere.  (Imagine a language where there
> are different verbs for eating bread, eating rolls, eating roll with
> butter, eating rolls with butter and jam...) ;-)

Which is why Agda should be object-oriented :-)

A.