UlfNorell
commented
10 years ago From andreas....@gmail.com on November 04, 2013 09:13:30
Btw. we could have saved the 'instance' keyword and used existing syntax instead, but this looks a bit awkward:
{{rawMonoidList}} : ... rawMonoidList = ...
Or does it?
From andreas....@gmail.com on November 04, 2013 17:57:50
2013-11-04 Andreas and Nisse
Currently instance search considers every name that in scope as a candidate. That would make recursive instance resolution forbiddingly slow. Here is a proposal how to change the instance mechanism to facilitate recursive instance resolution. I think it has been discussed before. Maybe it is time for action.
Add an 'instance' keyword in the style of 'private' and 'abstract' that classifies definitions as to be taken into account during instance resolution. Example:
{-# OPTIONS --copatterns #-}
record RawMonoid {a} (A : Set a) : Set a where field nil : A ++ : A -> A -> A open RawMonoid
instance rawMonoidList : forall {a}{A : Set a} -> RawMonoid (List A) rawMonoidList = record { nil = []; ++ = List.++ }
-- using copatterns to define this recursive instance:
rawMonoidMaybe : {A : Set}{{ m : RawMonoid A }} -> RawMonoid (Maybe A) nil (rawMonoidMaybe {{m = m}}) = nothing
++ (rawMonoidMaybe {{m = m}}) nothing mb = mb ++ (rawMonoidMaybe {{m = m}}) ma nothing = ma ++ (rawMonoidMaybe {{m = m}}) (just a) (just b) = just (++ m a b)
Each definition is thus tagged as 'instance' or 'not instance'.
When searching for an instance, take all local bindings into account plus the global 'instance' bindings. Also, search recursively. For instance, searching for
? : RawMonoid (Maybe (List A))
will consider the candidates {rawMonoidList, rawMonoidMaybe}, fail to unify the first one, succeeding with the second one
? = rawMonoidMaybe {A = List A} {{m = ?m}} : RawMonoid (Maybe (List A))
and continue with goal
?m : RawMonoid (List A)
This will then find
?m = rawMonoidList {a = lzero}{A = A}
and putting together we have the solution.
Uniqueness of instances should be up to definitional equality (see Issue 899 ).
Restrictions on the type of instances:
a) Each type of an instance must end in (something that reduces to) a record or data type.
This allows to build a simple index structure
that speeds up instance search.
b) [Termination check] recursive instances must be at structurally smaller types. This is the usual Haskell restriction. Something better might be How to exactly devise this termination check is not yet clear. rawMonoidMaybe is obviously ok, since in the recursive call RawMonoid A, A is smaller than (Maybe A).
Name space management.
No special management for now. If a definition is in scope, and it is an instance, it will be used during instance search.
If you want a name x from module M but not as an instance, you can do
open module _ using (x) where open module M renaming (x to y) x = y
Maybe some import directive like
using instances
that only imports the instances would be convenient, time will tell.
Original issue: http://code.google.com/p/agda/issues/detail?id=938