Non-strictly-positive types [Re: [Agda] defining coinductive types]
Andreas Abel
abela at chalmers.se
Wed Dec 18 21:29:27 CET 2013
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
>
More information about the Agda
mailing list