[Agda] Using instance arguments for pointed types

[Dmytro Starosud]

btw, I started working on the framework for defining complex instances
(type classes?).
It may be useful for you
(https://github.com/dima-starosud/Dynamic/blob/master/Instance.agda)

Best regards,
Dmytro

2013/10/1 Jesper Cockx <Jesper at sikanda.be>:
> A possible workaround is to define the [Pointed] instance of [Loop^ n A]
> only for n > 0, for example:
>
> module PointedType where
>
> open import Data.Nat
> open import Relation.Binary.PropositionalEquality
>
> record Pointed (A : Set) : Set where
>   field
>     point : A
>
> open Pointed {{...}}
>
> Loop : (A : Set) → {{_ : Pointed A}} → Set
> Loop A {{pointed-A}} = _≡_ {A = A} point point
>
> Loop^ : (n : ℕ) (A : Set) {{_ : Pointed A}} → Set
> pointed-Loop^ : (n : ℕ) (A : Set) {{_ : Pointed A}} → Pointed (Loop^ (suc n)
> A)
>
> Loop^ zero A {{pointed-A}} = A
> Loop^ (suc zero) A {{pointed-A}} = Loop A
> Loop^ (suc (suc n)) A {{pointed-A}} = Loop (Loop^ (suc n) A)
>   where
>     pointed-prev : Pointed (Loop^ (suc n) A)
>     pointed-prev = pointed-Loop^ n A
>
> pointed-Loop^ zero    A = record { point = refl }
> pointed-Loop^ (suc n) A = record { point = refl }
>
> (I hope my definition of Pointed looks more or less the same as yours)
> This is not completely satisfactory because you need an extra clause for
> Loop^, but it works.
>
> Jesper Cockx
>
>
> On Tue, Oct 1, 2013 at 3:45 PM, Guillaume Brunerie
> <guillaume.brunerie at gmail.com> wrote:
>>
>> Hi all,
>>
>> I’m trying to use instance arguments to implement various things
>> related to pointed types but I’m facing a problem that I can’t solve.
>>
>> A pointed type is a type [A] together with a point [a : A]. I want to
>> implement pointed types in such a way that by just writing [A], Agda
>> can guess what the base point is. This is easy to do, just define a
>> record [Pointed A] with a single field of type [A], and whenever you
>> need a pointed type [A], add an instance argument of type [Pointed A].
>> Then you can define terms of type [Pointed A] for various types [A]
>> and Agda will automatically find the base point when needed.
>>
>> Problems arise when I want to define the iterated loop space of a
>> pointed type [A].
>> The loop space of a pointed type [A] (called [Loop A]) is the type [a
>> == a] (propositional equality) where [a] is the base point of [A],
>> pointed by the reflexivity path.
>> Then the n-iterated loop space of a pointed type [A] is defined by:
>>
>>     Loop^ 0 A = A
>>     Loop^ (S n) A = Loop (Loop^ n A)
>>
>> It is clear that for all [n] and [A], [Loop^ n A] is pointed because
>> both [A] and [Loop _] are. But Agda does not guess it automatically,
>> so we need to prove it simultaneously (this is needed for [Loop (Loop^
>> n A)] to type check).
>>
>> But the problem is that given that [Loop^ 0 A = A], there are now two
>> different proofs that [A] is pointed, so Agda complains whenever you
>> want to do anything with [A].
>> And if [A] is itself a loop space, the problem is even worse.
>>
>> This is related to issue 899 (Instance search fails if there are
>> several definitionally equal values in scope) but also (I think) to
>> issue 751 (Non-unifiable terms defined by pattern matching are not
>> detected as such) because I think that Agda would not be able to solve
>> the metas in the constraint [Loop^ ? ? = A] (which make sense given
>> that if [A] is a loop space there are several solutions).
>>
>> Is it possible to workaround this problem?
>> Or do you think it would be possible to fix it? I’d be willing to try,
>> but I don’t know much work this could represent.
>>
>> Thanks,
>>
>> Guillaume Brunerie
>> _______________________________________________
>> Agda mailing list
>> Agda at lists.chalmers.se
>> https://lists.chalmers.se/mailman/listinfo/agda
>
>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>