[Agda] Again, a question on records

[Benja Fallenstein]

Hi Dan & all,

On Mon, Sep 20, 2010 at 3:44 AM, Dan Doel <dan.doel at gmail.com> wrote:
>> _$_ : {t : T} -> T.carrier t -> T.carrier t -> T.carrier t
>> x $ y = T.op _ x y
>
> While it's obvious to you and us that you mean for t to be filled in there,
> it's not obvious to the type checker, and it isn't the only legal thing that
> could go in there.

Pie-in-the-sky idea: I've thought for a while that it might be nice
solution to a number of things if we could have implicit arguments
that are named by types, and that are used to fill in blanks of that
type when type inference fails:

    _$_ : {T} -> T.carrier t -> T.carrier t
    x $ y = T.op _ x y

    _/_ : (x y : Rational) -> {y /= 0} -> Rational

    insert : ∀ {X Y} -> {Ord X} -> X -> Y -> Map X Y -> Map X Y

I've noticed that I (and others) often name arguments, especially
proof parameters, by their types, something like

    foo : (k m n : Nat) -> m <= n -> k * m <= k * n
    foo k m n m<=n = ...

so having a way to name such things more directly by their types seems
like a nice idea.

One thing this is somewhat similar to is implicit parameters in GHC
(which aren't named by types, though):

http://www.haskell.org/ghc/docs/6.12.2/html/users_guide/other-type-extensions.html#implicit-parameters

If we allow them to be set through (let _ : MyType; _ = value in ...),
we could also write

    _ : Ord Int
    _ = record { ... }

on the top level, and use the same mechanism to name lemmas:

    _ : (m n : Nat) -> m + n == n + m

and if I'm guessing right, the type checker should then naturally be
able to find the right lemma if we write e.g. (_ k l) in a context
requiring a (k + l == l + k).

There's also the obvious potential for looking not only for the exact
type needed, but also for functions returning that type, so that we
can use

    _ : ∀ {X} -> Ord X -> Ord (List X)
    _ = ...

but I think even without getting into these even deeper waters,
something like these type-named parameters could be handy.

I'm curious what people think about this who have implemented more
advanced type checkers than I have... :-)

- Benja