[Agda] Abstract existential ?

[Andreas Nuyts]

Correction: I think Krishnaswami & Dreyer only prove some corrolaries of 
the given theorem.

On 7/02/19 11:28, Andreas Nuyts wrote:
> Dear Jacques,
>
> You seem to suggest that the first component of your dependent pairs 
> is going to be a type. Thus, it seems to me that what you are looking 
> for is a parametric existential quantifier, as exists in System F, Fω, 
> Haskell, ...
>
> Parametric quantification is certainly not available in vanilla 
> MLTT/Agda, but is implemented in an experimental branch of agda, 
> called agda-parametric:
> * github branch: https://github.com/agda/agda/tree/parametric
> * example code: https://github.com/Saizan/parametric-demo
> * corresponding paper: "Parametric Quantifiers for Dependent Type 
> Theory", ICFP 2017, https://doi.org/10.1145/3110276
> I emphasize that - as far as I understand - the Agda implementation 
> (by Andrea Vezzosi) is purely for research and there are currently no 
> plans for continued support or integration in the master branch.
>
> If you want to use vanilla MLTT/Agda, then the following theorem may 
> come in handy:
>
>     Any function in MLTT with small codomain, is parametric.
>
>
> (Some papers claim that ANY function in MLTT is parametric; this is 
> true for a weaker definition of parametricity that is called 
> continuity in our ICFP paper cited above, and that seems insufficient 
> for your purposes.)
>
> What this boils down to is that any function of type
> (p : ∑[ X \in Set ] P X) -> ... -> T,
> where T : Set 0, will satisfy the property you are looking for: its 
> output does not depend on the first component of p.
>
> This is proven metatheoretically in:
> Atkey, Ghani, Johann, 2014, "A Relationally Parametric Model of 
> Dependent Type Theory."
> Krishnaswami & Dreyer, 2013, "Internalizing Relational Parametricity 
> in the Extensional Calculusof Constructions",
> Takeuti, 2001, "The Theory of Parametricity in Lambda Cube."
>
> The theorem breaks down if you add axioms such as (non-exhaustively):
> * choice / law of excluded middle: (X : Set) -> X + (X -> False)
> * resizing axioms
>
> Best regards,
> Andreas
>
> On 6/02/19 22:30, Jacques Carette wrote:
>> Is there a way to encode an existential in Agda where the "exists" 
>> part of the dependent pair is abstract/private?  ∃ from the standard 
>> library just says that the first part is implicit (i.e. can be 
>> uniquely inferred).
>>
>> I think I could use the same trick as in Haskell (i.e. use a wrapper 
>> where I don't export the constructor but do provide accessor 
>> functions that don't leak), but that somehow seems heavy.  Is there 
>> something simpler?
>>
>> I don't mean a fully non-constructive exists here: I mean 
>> (informally!) "a dependent pair where the first projection is 
>> abstract and cannot leak". So to build such a thing, a definite type 
>> must be used, but once it is created, the 'clients' as it were, 
>> cannot find out what that type is.
>>
>> Jacques
>>
>> _______________________________________________
>> 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/20190207/46a57904/attachment.html>