Non-strictly-positive types [Re: [Agda] defining coinductive types]

[Andreas Abel]

My opinion on non-strictly positive types is the following:

If you have an impredicative universe, then adding non-strictly positive 
types in this universe is ok, if not conservative.  The reason has been 
given by Thierry:  You can use Knaster-Tarski to construct them, thus, 
they are just a special application of impredicativity.

However, I would be surprised if you could add non-strictly positive 
types to *Agda* as such, which would mean to add them to *every* 
universe.  At least I would have no clue how to construct a model for 
this theory.

Cheers,
Andreas



On 18.12.2013 19:57, Aaron Stump wrote:
> Thanks, Thierry, for the response about normalization with positive
> recursive types.
>
> One more update on the "sized observers" approach I am proposing: here
> is the Hamming stream example, written in the same compact style.  This
> was harder to do, because of the need to reason about the depth of
> observations.  (Note that I'm writing this with my own library, not the
> standard library.)  The code for merge is as expected, though the type
> is interesting.  But then the code for hamming is written in the desired
> style.
>
> merge : {n m : ℕ} → 𝕊 ℕ n → 𝕊 ℕ m → {k : ℕ} → k ≤ min n m ≡ tt → 𝕊 ℕ k
>
> hamming : {n : ℕ} → 𝕊 ℕ n
> hamming (ohead f) = f 1
> hamming {suc n} (otail o) =
>     merge (map𝕊 (_*_ 2) (hamming{n}))
>       (merge (map𝕊 (_*_ 3) (hamming{n}))
>          (map𝕊 (_*_ 5) (hamming{n}))
>             {min n n} (≤-refl (min n n))) lem o
>         where lem : n ≤ min n (min n n) ≡ tt
>                    lem rewrite min-same n | <-irrefl n | ≤-refl n = refl
>
> It seems to run fast, too.  If you want to see all the details, you can
> find dev/hamming-stream.agda and lib/ in my svn repo:
>
> https://svn.divms.uiowa.edu/repos/clc/class/111-spring14
>
> Use username "guest" and password "guest" if needed.
>
> Cheers,
> Aaron
>
>
>
> On Wed, Dec 18, 2013 at 11:31 AM, Thierry Coquand
> <Thierry.Coquand at cse.gu.se <mailto:Thierry.Coquand at cse.gu.se>> wrote:
>
>
>       At least in an impredicative metatheory, the usual normalization
>     argument should extend
>     to the addition of such positive recursive types in Agda (using
>     Tarski's fixed point theorem
>     to define the computability at these types).
>
>       Best regards,
>       Thierry
>
>     PS: This would be however incompatible with the addition of an
>     impredicative universe U,
>     since one can then form
>
>       R = mu X. (X-> U) -> U
>
>     and derive a contradiction from this following Reynolds' proof that
>     there is no set theoretical
>     model of system F.
>
>     On Dec 18, 2013, at 6:22 PM, Aaron Stump wrote:
>
>>     Dear Wojtek,
>>
>>     Yes, I know about this example for recursive types which contain
>>     negative occurrences of the recursively defined type.  But I am
>>     asking about positive but not strictly positive recursive types.
>>      An example is a type like the one Nils mentioned:
>>
>>     μA.∀R. (μX. (A → R) + X) → R
>>
>>     Here, the type variable A occurs to the left of an even number of
>>     arrows.  This makes it positive (the even number of negations
>>     cancel out), but not strictly positive.
>>
>>     Cheers,
>>     Aaron
>>
>>
>>
>>
>>     On Wed, Dec 18, 2013 at 11:14 AM, Wojciech Jedynak
>>     <wjedynak at gmail.com <mailto:wjedynak at gmail.com>> wrote:
>>
>>         Hello,
>>
>>         > Ok, I see.  Is it known that supporting non-strictly
>>         positive types would
>>         > have bad consequences in Agda?  Not that I am suggesting it
>>         -- I am just
>>         > curious about what might be possible.
>>
>>         Yes, it's possible to write a non-terminating expression using
>>         such a
>>         type. For instance, take a look here:
>>         <http://wiki.portal.chalmers.se/agda/pmwiki.php?n=ReferenceManual.BadInHaskell>
>>
>>         Best,
>>         Wojtek
>>
>>
>>     _______________________________________________
>>     Agda mailing list
>>     Agda at lists.chalmers.se <mailto: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
>