[Agda] Pie in the sky

[Bas Spitters]

Thanks for the summary.
Is canon supposed to be similar to canonical structures in Coq?

Bas

On Thu, Sep 23, 2010 at 11:47 PM, Samuel Gélineau <gelisam at gmail.com> wrote:
> 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.
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>