[Agda] Pie in the sky

[Benja Fallenstein]

Hi Dan,

I've only had time for a cursory look at the paper you've cited (and
read Samuel's summary). I *think* I understand, but excuses for not
doing the maximum possible amount of homework right back at you &
please correct me if I'm misunderstanding something! :-)

It seems to me that there is *some* overlap -- "type classes are just
records/signatures, all we need is a mechanism for passing them around
implicitly (and sometimes, explicitly naming the implicitly passed
value)."

But where my idea differs is that I think it would be useful to make
another slight generalization, and think of type classes as an
instance of the pattern that there is often only one interesting value
of a given type in a given context, so that it is annoying to have to
explicitly (a) name this value and (b) pass it around. (After all,
that's mostly what a type class mechanism has to do in our context;
passing records explicitly we can already do.) Functions and
parameters named by lower-casing their types are suggestive of this
pattern...

So basically, my idea is to let *any* type be passed around through
the type class mechanism, and the rest is mostly bikeshedding the
details, or so it seems to me.

Well, given my motivation one detail's particularly important to me:
If you have to name a value before you can declare it to be the
canonical value of its type (i.e., to be used in type class search),
that would defeat my point (a). So I don't like the part about Dreyer
et.al.'s system where you need to create EqInt before you can say
'using EqInt in ...', and I don't like Andreas' variant of the
instance declarations, where you have to give every instance a name.
My opinion is that

- it's a feature of Haskell that you can declare an instance without
naming it; instead of having to name instances, you should be able to
declare a nameless instance and then refer to it through "instance A"
/ "canon(A)" or whatever;

- it's a bug of Haskell that you can't name instances; but we already
have a way to name values of arbitrary values: ordinary assignment
syntax;

- if you want to name an instance *and* make it the canonical value of
its type, it's reasonable to require you to write something to the
effect of,

    namedEqInt : Eq Int
    namedEqInt = blah

    instance Eq Int = namedEqInt

i.e., an ordinary declaration followed by an instance declaration
(whatever the syntax for instance declarations is). Or, of course, you
can use the other way around, if you prefer:

    instance Eq Int = blah

    namedEqInt = instance Eq Int

BTW, note that FWIW, the equivalent of "using EqInt in ..." would be
available as,

   let instance Eq Int = namedEqInt in ...

On Wed, Sep 22, 2010 at 3:28 AM, Dan Licata <drl at cs.cmu.edu> wrote:
> 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.

The "instance TYPE = VALUE" syntax yields a nice symmetry between the
syntax for explicitly specifying implicit parameters and the syntax
for explicitly specifying instance parameters of a function -- well,
and I so happen to find assignment syntax for specifying canonical
values of type perfectly natural :-)

On the other hand, having to give the type in the assignments is kind
of ugly, and it's unclear how to write instances of function types
that way (except as lambdas to the right of the "="). I'd rather write
something like,

    default : TYPE
    default = ...

Also, as suggested in a different part of this thread, we could make

    instance Eq Int where
        ...

an abbreviation for

    instance Eq Int = record {...}

I realize that not having any version that I find fully satisfying
weakens my position on this point somewhat...

(Actually, I notice now that in my other mail with the updated
proposal, I didn't actually specify any top-level declarations for
instances... also forgot to mention importing from modules.)

> 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.

I certainly think of canon/default/instance as a language construct,
even when I think of them as a language construct that constructs
names :-)

Thanks for replying!
- Benja