[Agda] printing infinite structures

[Paulo Pizani]

Wouldn't a generalized "take" function be nice for these kind of
experiments?


As in:

> record DepthBounded (α : Set) where
>   field  boundedType : ℕ → Set
>          boundedTake : ∀ d → α → boundedType d
> 
> genTake : ∀ {α} ⦃ bd : DepthBounded α ⦄ (d : ℕ) → α → (bd .boundedType) d
> genTake ⦃ bd ⦄ d = (bd .boundedTake) d
> 
> 
> instance
>   StreamBounded : {β : Set} → DepthBounded (Stream β)
>   StreamBounded {β} = record { boundedType = Vec β;  boundedTake d = Codata.Stream.take d }
> 
>   ColistBounded : {β : Set} → DepthBounded (Colist β)
>   ColistBounded {β} = record { boundedType = BoundedVec β;  boundedTake d = Codata.Colist.take d }

combined with a suitable "show" method from a "Show" class, you could
then do:


> shownStream = (show ∘ genTake) 42 (Codata.Stream.repeat whatever)
> shownColist = (show ∘ genTake) 42 (Codata.Colist.replicate Codata.Conat.inifinity whatever)


The interesting question then becomes on whether/how deriving such
instances can be done with generic-programming-like techniques, maybe
with a little help from reflection...

But even without deriving, just the existence of the class itself (in
for ex. stdlib or prelude) would create a nice expectation on users of
agda coinductive types that they could rely on getting initial parts
from elements of such types.

-- 
Paulo Pizani
paulopizani at posteo.net

On 26-02-19 15:55, Thorsten Altenkirch wrote:
> Hi,
> 
>  
> 
> Would it be possible to have a plugin to print infinite structures like
> streams (as in Haskell)? I have been playing around with streams and
> conats for my course and it is a bit underwhelming when you can’t see
> them. Ok ok I can write functions which convert an initial part into a
> finite structure but this is a lot of extra work and not so much fin.
> 
>  
> 
> Cheers,
> 
> Thorsten
> 
> 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.
> 
> 
> 
> 
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
> 
-------------- next part --------------
A non-text attachment was scrubbed...
Name: paulopizani.vcf
Type: text/x-vcard
Size: 325 bytes
Desc: not available
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20190226/8d4ca62a/attachment.vcf>
-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 488 bytes
Desc: OpenPGP digital signature
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20190226/8d4ca62a/attachment.sig>