[Agda] Abstract existential ?
Jacques Carette
carette at mcmaster.ca
Thu Feb 7 18:11:43 CET 2019
Very nice paper, thanks for drawing my attention to it. You are correct
that I am looking for is "a parametric existential quantifier, as exists
in System F, Fω, Haskell, ...".
Unfortunately, for my application, I am not sure I can work in Set 0. I
could work in Set 1. But that's likely not small enough... To be
precise, I want to be able to hide a small type, but I want to produce a
non-small type that depends on it parametrically.
Jacques
On 2019-02-07 5:28 a.m., 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/161549fc/attachment.html>
More information about the Agda
mailing list