[Agda] Pie in the sky

[Samuel Gélineau]

On 2010-09-23 at 7:04 PM, Benja Fallenstein wrote:
> I don't get it. I do want the following type signatures to be
> alpha-equivalent (of course?):
>
>    foo : {MyClass : Set -> Set} -> {MyClass Int} -> Int
>    foo : {YourClass : Set -> Set} -> {YourClass Int} -> Int

Recall that {MyClass Int} is just an abbreviation for {instance
MyClass Int : MyClass Int}, where "instance MyClass Int" is a name
like any other. Under alpha-equivalence, I should be allowed to name
it "bar" or "muffin" or even "instance MyClass String" without
changing the meaning of the program.

Since the essence of the name-based version of our proposal is to look
in the environment for a variable with a specific name computed from
the type of the instance class we need, the choice of name matters
very much to the meaning of the program, and therefore the proposal
breaks alpha-equivalence.

I think the essence of the problem is that the name "instance MyClass
Int" actually depends on the names "MyClass" and "Int", which is why I
now want to investigate dependent names.


> So let me update my earlier "other" explanation to the syntax we've
> now agreed on (except that it then makes less sense to allow writing
> {instance Ord Int : Ord Int} instead of {Ord Int}, but surely that's a
> minor detail). Still sketchy, but hopefully clearer.

It's not a minor detail to me. It was the name-based approach which I
was passionate about; the discussion is now mostly about type classes,
which is fine, but isn't what I came to the table for.


Happy type class discussions,
– Samuel, signing off.