[Agda] Problem with generalised variables

[Guillaume Brunerie]

Hi Thorsten,

I : A → A
I {A} = S K (K {B = A})

seems to work.

Best,
Guillaume

Den tors 23 juli 2020 kl 18:04 skrev Thorsten Altenkirch
<Thorsten.Altenkirch at nottingham.ac.uk>:
>
> Hi,
>
>
>
> I am writing some material about combinators and thought it is quite nice to use generalized variables for types:
>
>
>
> variable
>
>   A B C : Set
>
>
>
> K : A → B → A
>
> K x y = x
>
>
>
> S : (A → B → C) → (A → B) → (A → C)
>
> S f g x = f x (g x)
>
>
>
> However, when I try to define
>
>
>
> I : A → A
>
> I = S K K
>
>
>
> I run into the usual problem of an uninstantiated metavariable. Using explicit abstraction I was able to fix this by saying
>
>
>
> I : A → A
>
> I = S K (K {B = A})
>
>
>
> But when I try this in this setting I get quite a mouthy error message.
>
>
>
> Any advice? I don’t really want to introduce fake modules of possible because then I would to indent everything.
>
>
>
> Thorsten
>
>
>
>
>
> This message and any attachment are intended solely for the addressee
> and may contain confidential information. If you have received this
> message in error, please contact the sender and delete the email and
> attachment.
>
> Any views or opinions expressed by the author of this email do not
> necessarily reflect the views of the University of Nottingham. Email
> communications with the University of Nottingham may be monitored
> where permitted by law.
>
>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda