[Agda] Why no impredicative prop?

[Timothy Carstens]

For most of the work I've done I haven't needed an impredicative universe;
that is, the main reason I'd use Prop in Coq was that the OCaml extractor
would eliminate Prop terms, which was nice.

But then I tried to implement indirection theory in the style of Hobor,
Dockins, Appel [1]. One can carry out their construction just fine, but
(from what I can tell) using the construction in the manner shown in their
examples requires an impredicative sort.

Namely, in section 4.1 they wind up in a situation where they have

T some type, say Set i

type = memtype * value -> T

ref : type -> type

At this point, their usage of 'ref' seems to require (type -> type : T),
which only seems possible if T is impredicative.

I'm unsure whether or not their construction could be carried out in a
satisfactory way by (for example) trying to make a universe-polymoprhic
version of 'type'. Regardless, running into this obstacle got me to
wondering whether or not there was a theoretical obstruction to Agda having
an impredicative prop.

[1] http://vst.cs.princeton.edu/msl/indirection.pdf

-t


On Tue, Dec 29, 2015 at 2:11 PM, Thorsten Altenkirch <
Thorsten.Altenkirch at nottingham.ac.uk> wrote:

> Actually why do you need an impredicative universe?
>
> From a purely pragmatic point it is a bit strange if one universe behaves
> different from the other one. But having two impredicative universes is
> already unsound.
>
> More on the philosphical side: impredicativity is basically a classical
> idea which arises from the identification of Prop and Bool. I don’t know an
> intuitionistic justification of impredicativity.
>
> Thorsten
>
> From: <agda-bounces at lists.chalmers.se> on behalf of Timothy Carstens <
> intoverflow at gmail.com>
> Date: Tuesday, 29 December 2015 17:19
> To: "agda at lists.chalmers.se" <agda at lists.chalmers.se>
> Subject: [Agda] Why no impredicative prop?
>
> Hello,
>
> I'm a relatively new Agda user, coming from a background using Coq for the
> past few years. As is well known, Coq has an impredicative Prop sort, while
> Agda does not.
>
> Why not? Is it simply a matter of project goals, or is there something
> about Agda's underlying theory which is incompatible with having an
> impredicative sort at the bottom of the universe hierarchy?
>
> Forgive me if this is an old topic or has an obvious answer; I'm not a
> logician, but I use proof assistants at work.
> -t
>
>
>
> This message and any attachment are intended solely for the addressee
> and may contain confidential information. If you have received this
> message in error, please send it back to me, and immediately delete it.
>
> Please do not use, copy or disclose the information contained in this
> message or in any attachment.  Any views or opinions expressed by the
> author of this email do not necessarily reflect the views of the
> University of Nottingham.
>
> This message has been checked for viruses but the contents of an
> attachment may still contain software viruses which could damage your
> computer system, you are advised to perform your own checks. Email
> communications with the University of Nottingham may be monitored as
> permitted by UK legislation.
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20151229/bcde47c2/attachment-0001.html