[Agda-dev] Treating variables as named types

[Andreas Abel]

I think variables could be added to be eligible for instance search.

Happy Hacking,
Andreas

On 29.01.2015 14:21, Nils Anders Danielsson wrote:
> Hi,
>
> Conor uses lots of instance arguments in "How to Keep Your Neighbours in
> Order". However, his code was written using the old variant of the
> instance arguments, and fails to check now. I managed to make the code
> work again using some small tweaks, and wonder if we could get away with
> even less:
>
> * I replaced
>
>      record One : Set where constructor it
>
>    with
>
>      record One : Set where
>        instance
>          constructor it.
>
>    This seems fine with me.
>
> * I replaced
>
>      _:-_ : forall {P T} -> <P P P> -> (P => T) -> T
>      ! :- t = t
>
>    with
>
>      _:-_ : forall {P T} -> <P P P> -> (P => T) -> T
>      ! {{prf = p}} :- t = t {{p = p}},
>
>    because "Instance search can only be used to find elements in a named
>    type". Similarly, in two cases I replaced a module parameter
>
>      (L : REL P)
>
>    with
>
>      (L' : REL P) (let L = Named L'),
>
>    where Named is a named type family:
>
>      data Named {P : Set} (A : REL P) : REL P where
>        named : forall {x} -> A x -> Named A x
>
>    Would it be possible to treat variables as named types/named type
>    families?
>
>    Introducing special treatment for variables can be problematic, as it
>    can lead to problems with subject reduction. However, in this case the
>    instance resolution should happen before the variables get
>    instantiated, so I don't think this will be a problem.
>
>    Are there any other problems, related to implementation complexity or
>    efficiency?
>

-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Department of Computer Science and Engineering
Chalmers and Gothenburg University, Sweden

andreas.abel at gu.se
http://www2.tcs.ifi.lmu.de/~abel/