[Agda] Abstract existential ?

[Andreas Nuyts]

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/9bd3e8dc/attachment.html>