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