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

[Darryl McAdams]

Doesn't this make it every so slightly possible to violate parametricity?
 
- darryl
 
- darryl


________________________________
 From: Andreas Abel <andreas.abel at ifi.lmu.de>
To: Arseniy Alekseyev <arseniy.alekseyev at gmail.com>; Agda mailing list <agda at lists.chalmers.se> 
Sent: Monday, February 18, 2013 6:13 PM
Subject: Re: [Agda] Can rigid variables be treated as constructors/postulates?
 
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/
_______________________________________________
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/20130218/2dc1401e/attachment.html