[Agda] Pie in the sky

[Samuel Gélineau]

On Tue, Sep 21, 2010 at 3:51 PM, Benja Fallenstein
<benja.fallenstein at gmail.com> wrote:
> On Tue, Sep 21, 2010 at 6:28 PM, Samuel Gélineau <gelisam at gmail.com> wrote:
> > I guess Benja and I have both looked in the sky, but the pie he has
> > seen is not the same pie as the one I have seen after all...
>
> I'm not so sure! Modulo initial misunderstandings, it seems to me that
> the difference comes down to details and bikeshedding, though I might
> of course still be misunderstanding what you want.

Yes, after reading your message, I now agree that our proposals are
variants on the same basic idea.


> IIUC, you originally thought I wanted the {Ord Int} notation to
> introduce a variable named by the string "Ord Int", and I originally
> thought you were suggesting that arbitrary normal forms could be
> variables of arbitrary types, as in 'zero : String.

Oh, I did imagine that arbitrary normal forms could be variables of
arbitrary types, but I don't insist on this at all. I simply didn't
bother to restrict the sub-feature "normal-forms-as-names" more than I
needed to.


> And in fact, I've already come around to the view that on the user
> level, having an explicit name for the variable like in your proposal
> is better than my original idea of "assigning to _" -- after all, as I
> said earlier, I *think* of these as type-named variables. Now, I think
> it looks better to write the name
>
>  instance Ord Int
>
> instead of
>
>  '(Ord Int)
>
> but that's pure bikeshedding.

I do not think that '(Ord Int) is a particularly good notation either,
I just picked a temporary one until a better notation was found. Let's
use (instance Ord Int) from now on.


> I also think it's sensible then to interpret the type signature
>
> liftM : ∀ {M A B} → {Monad M} → (A -> B) → (M A -> M B)
>
> as
>
> liftM : ∀ {M A B} → {instance Monad M : Monad M} → (A -> B) → (M A -> M B)
>
> which, modulo the bikeshedding (instance Monad M) vs. '(Monad M) seems
> to be your suggestion, too.

I also think this abbreviation would be handy, but I'm glad you
realize that it is just an abbreviation, and not the core feature.


> My suggestion would be simply that if you have an implicit type-named
> parameter '(Ord a) in the signature, and you do not mention that
> implicit parameter in the pattern, then this will be interpreted as an
> implicit {instance Ord a = instance Ord a}.

I think this second abbreviation would also be handy, and I'm glad you
realize that this one is also just an abbreviation.


> I don't see the point of making _ behave differently from omitted
> arguments. My idea was that if (a) an argument of type (Foo bar) is
> omitted, or (b) a _ is used in a place where a (Foo bar) is expected,
> the same thing happens: Try to solve the meta. If the meta cannot be
> solved, behave as if default was given at this location.
>
> So I would just write _ where you write default. Could you explain why
> you don't want this?

I was trying to make the sub-feature "lookup-by-expected-type"
orthogonal to the rest of the language, but I don't insist on this
either.


> When an implicit type-named argument {instance Ord Int} of a function
> foo is not explicitly given in a call to foo, insert {instance Ord Int
> = instance Ord Int} in that position.

I think this is a great idea! This would preserve the meaning of _
while avoiding the need for a new default-like keyword. This is even
more orthogonal than my meta-then-default proposal, excellent!


> > Proof search would allow the user to omit even
> > more, but I don't think we're ready for that yet.
>
> I agree!
>
> However, I *am* coming to think that we probably should be able to do
> what Haskell is able to do, as in Andreas' snippet above; not being
> able to give an Eq instance for Prod would be supremely annoying.

Your proposal for extending instance parameters makes a lot of sense
and might even work, but it is clearly a layer above the basic
instance parameter feature. I would like to focus on implementing the
basics first. 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