[Agda] Abstract existential ?

[Neel Krishnaswami]

Hi,

Yes, you should read Atkey, Ghani and Johann's paper. It's really nice, 
and they prove strictly more than
Derek and I did.

Best,
Neel

On 07/02/2019 10:33, Andreas Nuyts wrote:
> 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
>>>
>>
>
>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda

-- 
Neel Krishnaswami
nk480 at cl.cam.ac.uk

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20190207/bfd8a126/attachment.html>