[Agda] instance arguments proposal and crash
Paolo Capriotti
p.capriotti at gmail.com
Mon Mar 4 20:26:56 CET 2013
Hi all,
I'm currently experimenting with ways to squeeze as much overloading as possible
out of Agda's instance arguments. My simplified use case looks something like
this:
record IsMonoid (M : Set) : Set where
field
unit : M
_*_ : M → M → M
record IsGroup (M : Set) : Set where
field
is-mon : IsMonoid M
inv : M → M
record Monoid : Set₁ where
field
carrier : Set
is-mon : IsMonoid carrier
record Group : Set₁ where
field
carrier : Set
is-grp : IsGroup carrier
Now, I want to be able to define a function like:
f : (M : Monoid)(G : Group)
→ Monoid.carrier M × Monoid.carrier G
by simply writing
f M G = unit , unit
without any qualification on unit. This is particularly important for infix
operators, because qualifying them is horrible, and always renaming them is
error prone, confusing and unmaintainable.
So, my idea is to define a record for "supertypes" of Monoid:
record MonoidLike : Set₂ where
field
Sort : Set₁
C : Sort → Set
struct : (X : Sort) → IsMonoid (C X)
and define an instance for every actual supertype:
mon-monlike = record
{ Sort = Monoid
; C = Monoid.carrier
; struct = Monoid.is-mon }
grp-monlike = record
{ Sort = Group
; C = Group.carrier
; struct = λ G → IsGroup.is-mon (Group.is-grp) }
Now, to enable overloading of unit and _*_ over any MonoidLike, I'd like to
write something like:
module MonoidInterface ⦃ ml : MonoidLike ⦄
⦃ X : MonoidLike.Sort ml ⦄ where
open IsMonoid (MonoidLike.struct ml X) public
Unfortunately, this doesn't quite work. I think the problem is that instance
arguments are resolved individually, and since there are two terms of type
MonoidLike in scope, ml is not resolved.
So what would be nice to have, here, is a way to instruct the instance
resolution mechanism to search for ml and X "at the same time". Basically, that
means that for every ml : MonoidLike in scope, all MonoidLike.Sort ml should be
searched, and if this search _globally_ returns a single value, then resolution
should succeed.
The best we can do with the way instance arguments currently work is to combine
ml and X above in a single Σ type, but then resolution will fail unless we
explicit bring the right pairs into scope, which can be cumbersome, as the
number of pairs is quadratic in the number of structures and instances.
Anyway, in one of my earlier attempts at tackling this problem, I stumbled upon
a crash. Here's the code triggering it:
module bug where
record IsMonoid (M : Set) : Set where
field
unit : M
_*_ : M → M → M
record Monoid : Set₁ where
field
carrier : Set
is-mon : IsMonoid carrier
record Structure (Struct : Set₁)
(HasStruct : Set → Set)
(carrier : Struct → Set) : Set₁ where
field
has-struct : (X : Struct) → HasStruct (carrier X)
mon-mon-struct : Structure Monoid IsMonoid Monoid.carrier
mon-mon-struct = record
{ has-struct = Monoid.is-mon }
mon-mon-struct' : Structure Monoid IsMonoid Monoid.carrier
mon-mon-struct' = record
{ has-struct = Monoid.is-mon }
unit : {Struct : Set₁}{C : Struct → Set}
→ ⦃ X : Struct ⦄
→ ⦃ struct : Structure Struct IsMonoid C ⦄
→ C X
unit {Struct}{C} ⦃ X ⦄ ⦃ struct ⦄ = IsMonoid.unit
(Structure.has-struct struct X)
f : (M : Monoid) → Monoid.carrier M
f M = unit
This gives: An internal error has occurred. Please report this as a bug.
Location of the error: src/full/Agda/TypeChecking/Eliminators.hs:45.
BR,
Paolo
More information about the Agda
mailing list