Agda-2.3.2.2: notes/classes

------------------------------------------------------------------------
Notes after class discussion 2007-08-17 (Ulf, NAD)

These are just some quick and dirty notes outlining the outcome of the
discussion. The use cases motivating the choices done are not
discussed.

Class declarations:

  record class C Γ : Δ where
    ...

  data class C Γ : Δ where
    ...

  No restrictions on parameters or indices.

Instance declarations:

  f : ...
  f = ...

  instance f

    or perhaps

  instance f : ...
  f = ...

  f and the instance declaration have to be in the same scope.

  The instance which f declares is not in scope (with respect to
  instance search, see below) in the type signature of f, but it is in
  scope in the body of f (perhaps).

  The type of f has to evaluate to the normal form Γ -> C Δ, where C
  is a class. Γ has to consist solely of:

  • variables which are "rigid" in Δ (arguments to type constructors),
    and/or

  • class type constructors applied to arbitrary arguments. Denote
    these by C' Δ'.

  The type of f gives rise to a rewrite rule:

    C Δ -> C' Δ'  (With an empty RHS if C' Δ' is empty.)

  The collection of all instance rewrite rules always has to be
  terminating. For every new instance added the termination checker is
  run on the rewrite rules (treating data/record type constructors in
  Δ/Δ' as constructors). One could also imagine a more local variant,
  in which the "recursive calls" in the RHS always have to be strictly
  structurally smaller than the LHS arguments.

  We may also allow higher-order types, in which case the RHSs become
  higher-order and the positive occurrences in C' Δ' should be
  inspected by the termination checker.

Superclass declarations:

  record class C₁ Γ : Δ -> Setⁿ where
    ...
    instance x : C₂ X
    ...

  C₂ has to be a class; C₂ X becomes a superclass of C₁ Γ Δ.

Searching for instances:

  If ? : C Γ, where C is a class, then ordinary unification is not
  used. Instead a special instance search is performed.

  The instance search is performed in several "levels". First a match
  for C Γ is searched for. If several matches are found, an error is
  emitted (ambiguous instances). If exactly one match is found, that
  match is bound to the meta variable. And if no matches are found,
  the search continues with the superclasses of C Γ, in a
  breadth-first manner. (First all immediate superclasses, all at the
  same time. Then the next level, and so on.)

  The search at a specific level is done in the following way:

  ⑴ All instances in scope are collected. Locally bound arguments
    whose types are of the form outlined for instances above also
    count as instances.

  ⑵ The rewrite rules generated by the instances are applied to the
    goals at hand (for instance C Γ), yielding new goals. This is
    repeated until no rules apply any more. Due to the termination
    checking done we know that this will terminate (right?).

  ⑶ All successful matches (search trees whose leaves all correspond
    to empty RHSs) are collected.

  From a successful match a dictionary can be built by applying the
  instance functions in a way corresponding to the resulting search
  tree; all arguments to these functions are either given by the goal
  at hand (the rigid variables) or by the children in the search tree.

------------------------------------------------------------------------

A class system
--------------

what can be a class?

- any datatype/record

what is an instance?

- an element of a class (possibly parameterised)
- parameterised by what?
  + other instances clearly
  + non-instances? yes, arguments to the classes

some examples:

class Eq (A : Set) : Set where
  eq : (_==_ : A -> A -> Bool) -> Eq A

instance
  eqList : {A : Set} -> Eq A -> Eq (List A)
  eqList eqA = ..

what are the restrictions on an instance declaration?
- should probably be
    instance i : Δ -> Cs -> C ts
  where
    Cs are classes
    Δ can be inferred from C ts
- instance search will proceed as follows:
  + given a goal C ss, unify with C ts to get ρ (deciding all of Δ)
  + the new goals are Cs ρ

multiparameter type classes?
- how difficult?
- necessary? clearly useful (at least with inductive families)

functional dependecies
- probably not needed (we have associated types for free)

zero parameter type classes are useful:

  class True : Set where
    instance tt : True

  A constructor can be declared an instance by writing instance before the
  name. The normal checks are applied to the type.

  _/_ : (n m : Nat) -> {m ≠ 0} -> Nat
  m / n = ..

  now x / 3 requires a proof of 3 ≠ 0 = True for which there is an instance
  (tt). This would work with an inductive definition of ≠ as well (but requires
  multiparameter classes):

  class _≠_ : Nat -> Nat -> Set where
    instance neqZS : {m : Nat} -> 0 ≠ suc m
    instance neqSZ : {n : Nat} -> suc n ≠ 0
    instance neqSS : {n m : Nat} -> n ≠ m -> suc n ≠ suc m

How to do super classes?

    class Ord (A : Set){eqA : Eq A} : Set where
      ord : (compare : A -> A -> Ordering) -> Ord A {eqA}

    instance ordNat : Ord Nat
	     ordNat = ord compareNat

  this doesn't really work...

    sort : {A : Set} -> {Ord A} -> List A -> List A

  there is no instance Eq A here. Ord A must contain Eq A

    class Ord (A : Set) : Set where
      ord : {Eq A} -> (compare : A -> A -> Ordering) -> Ord A

  how to get the Eq dictionary from the Ord dictionary (nothing recording the
  relationship here). One attempt:

    instance ordToEq : {A : Set} -> Ord A -> Eq A
	     ordToEq (ord eq _) = eq

  How does this work with other instances (clearly overlapping)? Maybe there is
  a good reason it's treated specially in Haskell... It would be nice not to
  have to introduce more syntax.

Finding instances
-----------------

Instances form a rewriting system (there is a paper about this stuff...)

  instance i : Δ -> Cs -> C ts

corresponds to a rule

  ∀ Δ. C ts --> Cs



 vim: sts=2 sw=2 tw=80