[Agda] Can rigid variables be treated as constructors/postulates?

[Andreas Abel]

That could be debated.  Opinions?

A consequence of this relaxation would be that injectivity is not 
stable under module instantiation, so it has to be recomputed when 
'test' is applied to concrete sets A and B.  However, other properties 
are also recomputed at that point, for instance, polarity 
(=monotonicity) and the compiled clauses.

Cheers,
Andreas

Am 18.02.2013 15:57, schrieb Arseniy Alekseyev:
> I have the following example, which does not work:
>
>     module test (A B : Set) where
>
>     data U : Set where
>       a b : U
>
>     [_] : U → Set
>     [_] a = A
>     [_] b = B
>
>     f : ∀ u → [ u ] → U
>     f u _ = u
>
>     postulate x : A
>
>     zzz = f _ x
>
> Here we have unresolved meta on the last line.
> When we change A and B to be constructors with a data keyword (or
> postulates), the meta gets resolved. It gets resolved because the
> function [_] becomes constructor-headed (A and B become different
> constructors).
>
> Does it make sense to treat rigid variables, such as A and B in the
> example the same way constructors are treated? Why not?
>
> A related, but separate issue:
> http://code.google.com/p/agda/issues/detail?id=796
>
> Cheers!
> Arseniy
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda

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

Theoretical Computer Science, University of Munich
http://www.tcs.informatik.uni-muenchen.de/~abel/