[Agda] Pie in the sky

[Benja Fallenstein]

Hi Samuel,

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.

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

> [...] My '(...) notation gives a canonical name for a value of a given type, which is
> useful in the common case when there is only one interesting value of
> the given type in the current context.

I understand that's not what you meant.

So according to your proposal, we can have variables like '(Ord Int) :
Ord Int in the context, which is accessed by the normal form Ord Int;
and according to my original thinking, we can have anonymous variables
like _ : Ord Int in the context, which is accessed by the normal form
of its type, i.e. Ord Int. Up to this point, we seem to be saying
precisely the same thing, only writing it differently.

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

So let me try to enumerate the details where I think we still differ;
please correct me if I'm still wrong about what your position is.

(I) Should the type signature be able to bring the type-named
parameter into context if the pattern doesn't mention it?

You think that, in keeping with the current scoping rules, the pattern
should always have mention the parameter to bring it into context:

liftM {M} {'(Monad M) = '(Monad M)} f m = m >>= λ x → return (f x) where
 open Monad default

I think it's sensible to have different scoping rules for the
type-named variables. I really like how lightweight it is in Haskell
to call a function that uses a type class:

rsort :: Ord a => [a] -> [a]
rsort xs = reverse (sort xs)

I really don't like the {'(Ord a) = '(Ord a)} noise you want to inject
into this definition.

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}. This way, you can still do

foo : ∀ {A} -> {Ord a} -> Blah
foo {instance Ord a = ordA} = ...

which would *not* bring the type-named variable into scope in the body of foo.

This seems perfectly sensible to me because of the normal use case for
the type-named parameters, vs. ordinary implicit parameters. Most of
the time, normal implicit parameters appear in the type of some later
explicit parameter or in the type of the return value. This explains
why most of the time, you don't need to bind them in patterns --
you're making use of them implicitly through the types of the other
parameters.

The type-named parameters will surely very rarely appear in the types
of explicit parameters, so if you don't match on them in the pattern,
they will simply be thrown away and not affect anything. It seems to
me that this would only exceedingly rarely be more useful behavior
than bringing the type class instance into scope in the function body,
and if you do really need it, you can always write

foo {instance Ord a = _} = ...


(II) Should we have a 'default' keyword for cases where we need to
mention a type-named parameter explicitly?

>From your earlier mail:

> [...] When (default) is put in a context where a value of type (Foo bar) is
> expected, '(Foo bar) is looked up in the current environment, causing
> a compile error if none is found.
>
> When an argument of type (Foo bar) is omitted, first behave as if _
> was given at this location. If the meta cannot be solved, behave as if
> default was given at this location.

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?


Though this has given me an idea for modifying my proposal to make it
hopefully much simpler. The fishiest part of my proposal seems to me
the interaction with solving metas. I've had a cursory look at Ulf's
PhD chapter about the metas a few weeks ago, and my idea for using
type-named parameters when a meta cannot be solved didn't seem to
*obviously* fit anywhere in the inference algorithm.

But do we really need to use type-named variables for arbitrary
implicit parameters? How about only using them to fill in implicit
type-named parameters? After all, we already can set implicit
parameters by name (foo {X = Int}), so we already have the notion that
the type of a function with implicit parameters contains the names of
these parameters.

So I'm now suggesting the following rule, mirroring my rule for
patters above, and completely decoupling type-named parameters from
type inference:

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.

(Of course this will give an error if there is no (instance Ord Int)
in the current context.) So given the type signatures

  return : ∀ {M A} → {Monad M} → A → M A
  _>>=_ : ∀ {M A B} → {Monad M} → M A → (A → M B) → M B


the declaration

  liftM : ∀ {M A B} → {Monad M} → (A → B) → (M A → M B)
  liftM f m = m >>= \x → return (f x)

would be simply an abbreviation for

  liftM : ∀ {M A B} → {instance Monad M : Monad M} → (A → B) → (M A → M B)
  liftM {instance Monad M = instance Monad M} f m =
    _>>=_ {instance Monad M = instance Monad M} \x →
      return {instance Monad M = instance Monad M} (f x)

What do you think?


(We could still have 'default', or without it you could always write
'instance Monad M' instead. Also, to have the more complex instances
Andreas was talking about, we might want a more complex interpretation
of 'instance Monad M' when used as a term; see below.)


>>  instance
>>     blurp : forall {a} -> Eq a -> Eq b -> Eq (Prod a b)
>>     blurp (record ...) (record ...) = record ...
>>
>> But then, naturally, you need proof search for some fragment of FOL, e.g.
>> Horn Clauses, to find the instance
>>
>>  ... : Eq (Prod Nat Bool)
>>
>> given you have instances for Eq Nat and Eq Bool.
>
> If supporting type classes requires proof search, then no, I do not
> want to support type classes. Let's keep things simple! The
> underscore-based mechanism currently allows the user to omit some
> parameters. My default-based mechanism allows the user to omit
> strictly more parameters, at the cost of naming variables in a
> slightly-different but actually quite-similar way to the current
> naming convention. 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.

I think what we could do is, when the user mentions (instance Eq (Pair
Int Int)) as a term (not as a parameter name), then we look in the
context not only for an instance of (Eq (Pair Int Int)), but also of
functions whose implicit parameters can be instantiated to give Eq
(Pair Int Int). I.e., in Andreas' example, A, Eq A, B, and Eq B would
need to be marked implicit:

instance ∀ {A B} -> {Eq A} -> {Eq B} -> Eq (Prod A B) = record {
   ...
   }

Er, well, that *would* be a handful to write even though some
complication is saved because we don't have to write the parameters
(because they are implicit, and Eq a and Eq b are type-named, so they
are automatically available in the body of the instance).

Well, considering that we already have the (on the surface) similarish syntax

module SortNat = Sort Nat leqNat

perhaps it would not be too weird to allow abbreviating the above
instance declaration to

instance ∀ {A B} -> {Eq A} -> {Eq B} -> Eq (Prod A B) where
   _==_ = ...

which looks reasonably familiar, I think.

If we find more than one instance declaration in the current context
that unifies with the instance type we're looking for, we give an
error. If we find only one, we treat the instance term -- say,
(instance Eq (Pair Int Int)) -- as a call to this function we've found
in the context, with its implicit parameters. So we do the same thing
as usual: ordinary implicit parameters are handled through type
inference; type-named (instance) parameters are replaced by instance
terms of the same type:

If we have

  foo : ∀ {A B} -> {Eq A} -> {Eq B} -> Eq (Prod A B)
  foo = record { ... }

  bar : Eq Int
  bar = ...

  instance ∀ {A B} -> {Eq A} -> {Eq B} -> Eq (Prod A B) = foo
  instance Eq Int = bar

then

  instance Eq (Prod Int Int) ==
  foo ==
  foo {_} {_} {instance Eq A = instance Eq Int} {instance Eq B =
instance Eq Int} ==
  foo {Int} {Int} {instance Eq A = bar} {instance Eq B = bar}

[I suppose we need to write the parameter names in the form from the
original function declaration, i.e. "instance Eq A" instead of
"instance Eq Int", so that we can always tell apart different
parameters as in the example above. But this seems to mesh reasonably
well with how things are done for ordinary, named parameters, where
when we set an implicit parameter by name, we also give the name as it
is declared in the function's type signature.]

- Benja