[Agda] Pie in the sky

[Dan Licata]

Hi Benja, Samuel,

I haven't followed all of the details in this thread, so apologies if
this has been mentioned already.  What you're describing seems close to
the mechanism for scoped instances in

  Modular type classes
  Derek Dreyer, Robert Harper, Manuel M. T. Chakravarty, Gabriele Keller
  http://www.mpi-sws.org/~dreyer/papers/mtc/main-long.pdf

In particular: 

(1) their 'using <instances> in ...' seems analogous to the 'instance'
declarations that Andreas described, which nominate something as
eligible for type class search

(2) their 'canon(S)' (a module expression that stands for what the type
class mechanism infers as an instance for signature S) seems related to
the proposal to implicitly name variables by their type

Personally, I find it clearer to have separate syntax for nominating
something as an instance, rather than trying to reuse the definition
syntax (instance = ...), as was proposed earlier in the thread.  

I also think it would be better to think of canon/default, possibly with
a type annotation (e.g. default(A)), as a language construct, rather
than tying the mechanism to the *names* of variables (I like
alpha-conversion when possible).  What you write as the name (instance
Ord Int) I'd call default(Ord Int).  I think this might just be a
different way of thinking about your proposal.

Third, if you want to distinguish between arguments to functions that
are only filled in by unification, and those that are filled in by type
class search, then it seems like there should be another kind of Pi in
addition to (x : A) -> B and {x : A} -> B.  E.g. {x : A} => B to mimic
the Haskell syntax for a type class premise.  

Sorry for jumping in without having understood your proposal fully.  
Please let me know if I've misunderstood you, or am just recapitulating
things you've already said.  

Thanks!
-Dan




On Sep22, Benja Fallenstein wrote:
> Hi Samuel,
> 
> Glad to see we largely agree after all and even have mostly the same
> sensibilities about the design choices! :-)
> 
> On Tue, Sep 21, 2010 at 11:57 PM, Samuel Gélineau <gelisam at gmail.com> wrote:
> > Your proposal for extending instance parameters makes a lot of sense
> > and might even work,
> 
> Yes, I think that's an acute way of putting it. :)
> 
> > but it is clearly a layer above the basic
> > instance parameter feature. I would like to focus on implementing the
> > basics first.
> 
> Agreed, that makes perfect sense. The basic feature is much clearer at
> this point and should still be quite useful without these
> complications.
> 
> Thanks again,
> - Benja
> 
> > Since we seem to agree on those basics, my question is
> > for the gatekeepers of Agda's codebase:
> >
> > Do the agda gatekeepers have any opposition to a new feature
> > introducing "(instance Foo Bar)" as a new form of valid variable name
> > and using {instance Foo Bar = instance Foo Bar} instead of {instance
> > Foo Bar = _} when a parameter with such a name is omitted?
> >
> > – Samuel
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>