[Agda] Pie in the sky

[Benja Fallenstein]

Hi Samuel,

On Tue, Sep 21, 2010 at 7:02 AM, Samuel Gélineau <gelisam at gmail.com> wrote:
> On 2010-09-20 22:31, Andreas Abel wrote:
>> As I heard from Ulf, the main reason why it is not in Agda is that there is
>> not a good idea yet how to handle scoping.  Haskell's mistakes should not be
>> repeated.
>
> I'm not familiar with those mistakes, but it would be important to
> make sure that Benja's proposed feature doesn't have similar scoping
> issues, then.

Yeah.

> And as a matter of fact, I think the proposal does have
> issues, although those I have noticed are probably quite different
> from Haskell's.
>
> First, it seems that the proposal has a slightly inconsistent naming
> scheme. Sometimes the special implicit values are given the same name
> as their type, and sometimes their name is an underscore.

Um! I didn't mean to suggest that the parameter of type Ord Int should
be named by the string "Ord Int" -- what I tried to say was that it
should not have a formal name at all, and be accessed through its
type. I suppose calling them "type-named" parameters didn't help,
though that's how I think about them. Continuing to write _ for the
missing names, if I write

    sort : forall {A} -> {Ord A} -> List A -> List A
    sort xs = ...

then in the body of the sort, the context would be

.A : Set
_ : Ord .A
xs : List A

When type inference fails to infer a value of type FOO, it would look
in the context the innermost entry (_ : FOO), if any, and use that.

> Second, the usage examples clearly show that the implicit values are
> intended to be listed in the type, but not in the pattern-matching
> part of function definitions. According to the current agda scoping
> rules, the implicit value should therefore not be in scope inside the
> body, and the type checker would thus not be able to look in the
> current environment to find a value whose name is the same as the type
> of an implicit value it failed to solve.

True; my proposal would require the rule to change. My idea is that
whenever the type signature contains an unnamed parameter, like {Ord
Int}, and this parameter is not matched on in the pattern (left
implicit), then it's brought into scope as an unnamed parameter of
that type.

> And now, here is my attempt at fixing the flaws highlighted above. My
> version of the proposal is to introduce a new syntax for compound
> names, say '(Foo bar), where (Foo bar) is some expression which agda
> evaluates to its normal form. Now also introduce the syntax '{Foo
> bar}, as a shorthand for {'(Foo bar)}, and the keyword (default). 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.

Do you mean {Foo bar} should be a shorthand for {'(Foo bar) : Foo
bar}? Or are you saying that '(Foo bar) must always have type Foo bar?

(Note that {varname} is currently illegal syntax in type signatures,
i.e. you cannot write

foo : {myfoobar} -> Blah

but only

foo : {myfoobar : Foo bar} -> Blah

or

foo : forall {myfoobar} -> Blah.)

> hoping you like my version of the proposal,

It's closer to what I meant to propose than what you read me as saying
:-) But having the explicit names seems unnecessarily heavyweight to
me -- what do you think about my idea now that I've hopefully
explained it somewhat better?

Thanks,
- Benja