[Agda] How to enforce dependencies between generalised variables

[Matthew Daggitt]

Okay, well at least I know to stop looking! Cheers Gallais that's a neat
work around (although it'll get a little cumbersome for deeper
dependencies).

Thanks both for the quick reply!

On Tue, Mar 26, 2019 at 8:33 PM Guillaume Allais <
guillaume.allais at ens-lyon.org> wrote:

> Alternatively you can pass `A` explicitly to `Decidable` like we often
> do for `Decidable _≡_`. This way you tell Agda that P's domain and A
> should be the same. This gives us:
>
> ```
> open import Level
> open import Data.List.Base hiding (filter)
> open import Relation.Unary
> open import Relation.Nullary
>
> variable
>   a p : Level
>   A : Set a
>   P : Pred A p
>
> filter : Decidable {A = A} P → List A → List A
> filter P? [] = []
> filter P? (x ∷ xs) with P? x
> ... | no  _ = filter P? xs
> ... | yes _ = x ∷ filter P? xs
> ```
>
> Cheers,
> gallais
>
> On 26/03/2019 12:27, Ulf Norell wrote:
> > No, there is no way to enforce this dependency, so you have bind P
> > manually. Generalisable variables would be quite awkward to use if they
> > weren't generalised in type signatures for other variables.
> >
> > See this section of the user manual for more details:
> >
> >
> https://agda.readthedocs.io/en/latest/language/generalization-of-declared-variables.html#nested-generalization
> >
> > / Ulf
> >
> > On Tue, Mar 26, 2019 at 1:07 PM Matthew Daggitt <
> matthewdaggitt at gmail.com>
> > wrote:
> >
> >> Dear all,
> >>  I'm trying out the new `variable` feature and am having some trouble
> >> enforcing dependencies between generalised variables. I'm trying to
> >> generalise the implicit variables in the following function type:
> >> ```
> >> filter : ∀ {a} {A : Set a} {P : Pred A p} → Decidable P → List A → List
> A
> >> ```
> >> My attempt at doing so is as follows:
> >> ```
> >> variable
> >>   a p : Level
> >>   A : Set a
> >>   P : Pred A p
> >>
> >> filter : Decidable P → List A → List A
> >> filter P? [] = []
> >> filter P? (x ∷ xs) with P? x
> >> ... | no  _ = filter P? xs
> >> ... | yes _ = x ∷ filter P? xs
> >> ```
> >> The problem is that slightly confusingly the `A` used implicitly in `P :
> >> Pred A p` is generalised separately from the `A` used in `List A` and so
> >> you get the following error
> >> ```
> >> A !=< P.A of type (Set A.a) when checking that the expression x has type
> >> P.A
> >> ```
> >> at `with P? x` in the definition.
> >>
> >> Removing `A : Set a` from the `variable` declaration obviously doesn't
> >> work as then the `A` in the variable declaration for `P` isn't defined.
> >>
> >> Is there a way of doing this?
> >> Many thanks,
> >> Matthew
> >> _______________________________________________
> >> 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
> >
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20190326/2ebd1e75/attachment.html>