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

[Benja Fallenstein]

Hi Andreas,

On Mon, Sep 20, 2010 at 10:31 PM, Andreas Abel <andreas.abel at ifi.lmu.de> wrote:
> the things you want could be realized with proof search or type classes.

I was trying to say that my proposal would be a nice way to implement
type classes and get some other use cases along with the bargain.
Sorry, I suppose I should have been more explicit about this, but I
really thought it would be obvious from the examples that looked like
type classes to you ;-)

So, unpacking the motivation a little: We already have records in
Agda, and it's no accident that the standard library uses records for
the equivalents of Haskell type classes. If we introduce type classes,
we will surely want to treat type class dictionaries as records. So
how about instead of introducing a separate namespace of type classes,
we simply introduce a way to pass around arbitrary records implicitly,
like type classes?

My proposal is that we can do this by simply having "anonymous"
variables that are named by their type (that is, the normal form of
their type, according to Agda's normalizer) and that are automatically
used for blanks whenever the ordinary type inferencer cannot determine
what to fill into the blank. For example,

    liftM :: forall m a b. Monad m => (a -> b) -> (m a -> m b)
    liftM f m = m >>= \x -> return (f x)

becomes

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

where the type-named parameter {Monad m} is used to fill the blanks
from the implicit {Monad M} parameters of _>>=_ and return:

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

(Though now that I write down that part explicitly, I realize that
we'd also need to have a way to open the Monad record module in such a
way as to make the {Monad M} parameters implicit :-))

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

So what I'm saying is that the above system for type classes could
also be naturally be used to name and pass around proofs in places
where you only care that you have a proof of a proposition, not what
the proof is (often because there is only one proof of the proposition
anyway). I'm not really advocating this for proof search, though;
perhaps my example with division was confusing: when I wrote

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

I didn't mean that the type checker should try hard to find a proof of
y /= 0, just that it should look for a type-named value of type (y /=
0) in the current environment, so that it can be passed around
implicitly:

    foo : (x y z : Rational) -> {z /= 0} -> Rational
    foo x y z = (x + y) / z

I haven't looked to closely at Coq type classes, and have only now had
a cursory look at canonical structures. If I understand right,

* Coq will try to fill in a type class by looking for anything in the
current environment that has the type of the type class -- that part
is similar-ish to my proposal -- but
* you're supposed to normally use the different "bracketed binder"
notation instead?

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

Hm, could you explain what the problems are? My proposal handles the
part where you cannot specify an alternative instance -- you can write

    liftM {MyMonad} {A} {B} {myMonadInstance}

or, with the (let _ : ...; _ = ... in ...) notation, you can write

    let _ : Monad MyMonad;  _ = myMonadInstance  in  liftM ...

or perhaps

    liftM {_ = myMonadInstance}

But I'm not sure that's what you have in mind?

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

Yep.

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

Actually, no; in first example, we're looking for a value of type (Ord
Int), in this one, we're looking for a value of type ((a b : Nat) -> a
+ b == b + a). The type checker tries to solve

(_ k l : k + l == l + k)   where   (k : Nat, l : Nat)

and infers that _ must have type ((a b : Nat) -> a + b == b + a) --
modulo alpha-conversion for bound variables, of course -- and finds _
: (m n : Nat) -> m + n == n + m in the context.

We *can* look for types with unbound variables, of course: in the
liftM example, we're looking for a value of type (Monad M), where M is
a variable. But in the 'addition is commutative' example, we're
looking for the closed function type.

Thanks for your answer!
- Benja