[Agda] defining coinductive types

[Aaron Stump]

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
> 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>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
> https://lists.chalmers.se/mailman/listinfo/agda
>
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20131218/2c0c94a8/attachment.html