[Agda] Pie in the sky

[Samuel Gélineau]

On Tue, Sep 21, 2010 at 9:28 PM, Dan Licata <drl at cs.cmu.edu> wrote:
> What you're describing seems close to
> the mechanism for scoped instances in
>
>  Modular type classes
>  Derek Dreyer, Robert Harper, Manuel M. T. Chakravarty, Gabriele Keller
>  http://www.mpi-sws.org/~dreyer/papers/mtc/main-long.pdf

Let me summarize the relevant parts of the paper for the benefit of
those who want to join the discussion. I have attempted to convert the
paper's ML syntax into Agda wherever possible, please let me know if
something important was lost in the translation.

- Type classes are like record types, type class instances are like
record values (well, duh).

- An instance which requires another instance (for example, Eq (a * b)
which can only be implemented if (Eq a) and (Eq b) have instances) is
like a function from record value to record value. In other words,
they are high-order instances.

- Records are actually more expressive than type classes. Amazingly,
the extra expressiveness corresponds to many popular type class
extensions which have been proposed, such as multi-parameter type
classes and functional dependencies.

- In Haskell, instance declarations are global to the program, so it
is not possible to have more than one instance of a class for a given
type in one program (this is probably the scoping issues alluded to by
Andreas).

- To solve this problem, introduce the constructs "using" and "canon".
Using is a let-like construct which makes some instances available for
canon, which is used within using's body to lookup the instance for a
particular type. The lookup instantiates high-order instances as
required. Canon is implicitly used whenever Haskell would lookup an
instance from its global instance list.

Here is how the system would look like using Agda's syntax:

  -- class Eq a where
  --   (==) : a -> a -> bool
  record Eq (a : Set) : Set where
    _==_ : a -> a -> Bool

  -- instance Eq Int where
  --   (==) = primIntEq
  eqNat : Eq Nat
  eqNat = record { _==_ = primEqNat }

  -- instance (Eq a, Eq b) => Eq (a, b) where
  --   (x1, y1) == (x2, y2) = (x1 == x2) && (y1 == y2)
  eqProd : forall A B -> Eq A -> Eq B -> Eq (A * B)
  eqProd A B eqA eqB (x1 , y1) (x2 , y2) = record {
      _==_ = (x1 ==A x2) && (y1 ==B y2)
    } where
      open Eq eqA renaming (_==_ to _==A_)
      open Eq eqB renaming (_==_ to _==B_)

  using eqNat, eqProd in
     eqNN : Eq (Nat * Nat)
     eqNN = canon(Eq (Nat * Nat))

     -- Haskell-like type, because it's not clear how to translate this to Agda
     lookup : Eq a => a -> [(a, b)] -> b
     lookup = ...

     -- here canon(Eq (Nat * Nat)) is implicitly used to fill in
lookup's instance requirement
     lookZeroUp : [(Nat, Nat)] -> Nat
     lookZeroUp xs = lookup zero xs

---

The instance directives introduced by Andreas, however, make instances
available in the remainder of the file, not in a specific body. This
makes a difference because Andreas wonders how one should import and
export the instance declarations, and with the using notation it is
clear that only the named record instances are intended to be imported
and exported, with each module calling using on all of the instances
it needs.

Apart from that, I agree that using and canon are basically equivalent
to instance directives and default. They are not, however, equivalent
to the feature Benja and I finally agreed on, which is definitely
based on names.


Speaking of which, AAARGL! You have managed to find an obvious and
true reason why our name-based proposal can never work. I really like
the idea of using canonical names to identify canonical
implementations, but I am not willing to sacrifice alpha-equivalence
for it.

I still think this *ought* to be a good idea, somehow. Maybe if I
introduce dependent names, with their own variant of
alpha-equivalence? Maybe, but this sounds way to experimental for a
mature language like Agda. I hear that's what Mini-Agda is for, right?
I'll look it up.

thanks for putting up with our crazy ideas,
– Samuel, disappointed but persistent.