[Agda] Why does this pass the positivity checker?

[Thorsten Altenkirch]

Hi,

I think there should be an alternative to these ad hoc extensions of the type system (including the size mechanism). In general this corresponds to constructing an internal model of type theory.

Incidentally this is related to a grant proposal (on “Template Type Theory”) I am working on just now.

In this case a strictly positive type can be modelled as a container but the overhead of using containers explicitely makes this unfeasible. However, Tamara von Glehn and others have shown that containers form a model of type theory. Maybe this doesn’t yet give you everything you want but I think this can scaled up to enable us to provide the semantics for the judgement that a type or a family of types occurs strictly positively and hence that we can use it in an inductive (or coinductive) definition.

Hence what we are proposing is to turn the model constructions that justify extensions from paper code into agda code which can be used to implement these extensions safely. And using (and extending) type theory in type theory developed with Ambrus Kaposi we have a good handle to talk about type theory internally.

Having said this I am very much in favour of experimentation now but I think in the long run we have to think how to reign in the wild growth of extensions and modifications of type theory.

Thorsten


From: Agda <agda-bounces at lists.chalmers.se> on behalf of Jesper Cockx <Jesper at sikanda.be>
Date: Friday, 20 July 2018 at 13:37
To: Neel Krishnaswami <nk480 at cl.cam.ac.uk>
Cc: agda list <agda at lists.chalmers.se>
Subject: Re: [Agda] Why does this pass the positivity checker?

Currently there is no way to do that, (partly) because positivity information is not stored in the type of a function. There has been talk of integrating this into the type system, but it's not clear at the moment how to do this in a nice way.

One special case are the polarity pragma's that can be used to assign a given polarity to a postulate, see https://github.com/agda/agda/blob/master/test/Succeed/Polarity-pragma.agda.

-- Jesper

On Fri, Jul 20, 2018 at 2:24 PM, Neel Krishnaswami <nk480 at cl.cam.ac.uk<mailto:nk480 at cl.cam.ac.uk>> wrote:
Hello,

Is there any way to annotate the type signature with positivity information? It would be helpful for localizing errors, and for doing ML-style modular programming.

Thanks for your help!



On 20/07/18 13:06, Jesper Cockx wrote:
I think Agda checks for each function definition whether it is (strictly)
positive in each of its arguments. The 'depth' of this check is not limited
AFAICT, but it is determined at the definition site of the function, not at
the use site. I've seen this used quite often for universe constructions
such as in your example.

-- Jesper

On Thu, Jul 19, 2018 at 1:15 PM, Neel Krishnaswami <nk480 at cl.cam.ac.uk<mailto:nk480 at cl.cam.ac.uk>>
wrote:
Hello,

I wrote the following bit of code, to experiment with generic programming.
data _×_ (A B : Set) : Set where
    _,_ : A → B → A × B


data _+_ (A B : Set) : Set where
   inl : A → A + B
   inr : B → A + B


data Poly : Set₁ where
   K : Set → Poly
   _⊗_ : Poly → Poly → Poly
   _⊕_ : Poly → Poly → Poly
   Id : Poly

[_] : Poly → Set → Set
[ K X ] A = X
[ p ⊗ q ] A = [ p ] A × [ q ] A
[ p ⊕ q ] A = [ p ] A + [ q ] A
[ Id ] A = A

data μ (F : Poly) : Set where
   into : [ F ] (μ F) → μ F
and Agda accepted the declaration of μ. I was surprised by this -- did
Agda look at the body of the definition of [_] to decide that every
recursive occurrence was  positive? If so, how deeply does it look?

--
Neel Krishnaswami
nk480 at cl.cam.ac.uk<mailto:nk480 at cl.cam.ac.uk>

_______________________________________________
Agda mailing list
Agda at lists.chalmers.se<mailto:Agda at lists.chalmers.se>
https://lists.chalmers.se/mailman/listinfo/agda

--
Neel Krishnaswami
nk480 at cl.cam.ac.uk<mailto:nk480 at cl.cam.ac.uk>




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 contact the sender and delete the email and
attachment. 

Any views or opinions expressed by the author of this email do not
necessarily reflect the views of the University of Nottingham. Email
communications with the University of Nottingham may be monitored 
where permitted by law.




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