Pie in the sky Re: [Agda] Again, a question on records

[Andreas Abel]

Hi Benja,

the things you want could be realized with proof search or type classes.

Proof search could be safely allowed in contexts which are irrelevant  
for computation, e.g., finding the lemma which proves commutativity.   
It does not matter which proof you get as long as you get one.  In non- 
irrelevant contexts, however, that could go badly wrong.

Systematic search according to rules can be done via a type class  
system. Coq already has two: classes and canonical structures.

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.

(some more comments below)

On Sep 20, 2010, at 4:34 AM, Benja Fallenstein wrote:
> 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 { ... }

This looks like type classes to me.  Basically you are saying that the  
canonical instance for Ord Int is the record given in the next line.

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

This could be subsumed under the type class paradigm, only that now we  
are not dealing with an identifier Ord but with a neutral term m + n  
== n+ m.

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

Andreas Abel  <><      Du bist der geliebte Mensch.

Theoretical Computer Science, University of Munich
Oettingenstr. 67, D-80538 Munich, GERMANY

andreas.abel at ifi.lmu.de
http://www2.tcs.ifi.lmu.de/~abel/