[Agda] Pie in the sky

[Benja Fallenstein]

Hi Samuel, all,

I didn't reply earlier because I haven't had time to digest the paper
-- thanks for the summary! -- but,

On Thu, Sep 23, 2010 at 11:47 PM, Samuel Gélineau <gelisam at gmail.com> wrote:
> Speaking of which, AAARGL! You have managed to find an obvious and
> true reason why our name-based proposal can never work. I really like
> the idea of using canonical names to identify canonical
> implementations, but I am not willing to sacrifice alpha-equivalence
> for it.

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

and if anybody feels uncomfortable with calling these
alpha-equivalent, then that's an argument for adopting a different
informal interpretation of the proposal, but as Dan suspects I think
this is just a question of how to think about it. Or did you have a
different problem with alpha-equivalence in mind? A parameter named
"instance Eq Int" should not be alpha-equivalent to a parameter named
"instance Ord Int", but again if this seems uncomfortable that's just
an argument about ways to think about the proposal.

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.

[Actually, while writing I realized there is another minor difference,
see below.]


Introduce a new kind of entry in contexts: in addition to (VAR :
TYPE), have (instance TYPE). This means that a default instance for
TYPE is available in the current context. TYPE can of course contain
variables declared earlier in the context, and when you change the
name of these variables by alpha conversion, you also need to change
them in TYPE. TYPE is also subject to beta- and eta-conversion. On the
other hand, (instance TYPE1) can never be alpha-, beta- or
eta-converted to (VAR : TYPE2) for any TYPE1, VAR, TYPE2.

Introduce a new kind of lambda for instance defaults, written {TYPE1}
-> TYPE2. In TYPE2, the context is extended by (instance TYPE1). We
can of course bikeshed about whether this should be written TYPE1 =>
TYPE2, but note that the proposed syntax is already illegal in current
Agda.

Introduce a new kind of term, (instance TYPE), which names the default
instance of a given type. Again, TYPE is subject to the usual
conversion rules. We have

    Gamma |- instance TYPE : TYPE

if Gamma contains an entry (instance TYPE).

Introduce a new kind of pattern, (instance TYPE), which has type TYPE
and matches all values of this type. This pattern adds an entry
(instance TYPE) into the context in the same way that a pattern VAR of
type TYPE brings an entry (VAR : TYPE) into the context.

Introduce syntax for declaring instance-lambda functions: The
parameter of a {TYPE1} -> TYPE2 function can be explicitly matched on
by writing {PATTERN} or {instance TYPE1 = PATTERN}. Alternatively, it
can be omitted; this is equivalent to writing {instance TYPE1 =
instance TYPE1}.

Introduce syntax for calling instance-lambda functions: The parameter
of a {TYPE1} -> TYPE2 function can be explicitly specified by writing
{TERM} or {instance TYPE1 = TERM}. Alternatively, it can be omitted;
this is equivalent to writing {instance TYPE1 = instance TYPE1}.


I noted above that I found a second difference to (how I interpreted)
the previous proposal: Under the old proposal, you could presumably
write

    foo : (instance Ord Int : Ord Int) -> 0 <= 0

which would introduce an *explicit* parameter "named instance Ord
Int", causing an instance of Ord Int to be available in the rest of
the pattern (specifically, as an argument to _<=_, which I here assume
to be a predicate). Similarly, you could write anonymous functions

    \(instance Ord Int) -> ...

which would bring an instance of Ord Int into scope in the body of the
lambda. Both of these are illegal under my proposal above, because
these aren't instances of pattern matching in Agda -- you can only
bind names in these places, not arbitrary patterns. (I think I'm
probably happier with disallowing these edge-cases anyway.) Note that
I *am* still proposing that you can bind to (instance TYPE) in any
place where you can pattern match.


In the interests of allowing other people to follow more easily, I'll
stop with having stated the proposal and leave arguments for a
different mail :-)

Samuel, does this relate at all to the issues with alpha-conversion
you have in mind, or were you thinking about something else?

Thanks,
- Benja