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