[Agda] Sized types and coinduction

[Andreas Abel]

Hi Brandon,

unfortunately, coinduction with sized types is not yet supported in 
Agda.  What is missing most is contravariant subtyping

   i <= j
   --------------------
   Stream j <= Stream i

I have plans to add support for this (since long), but currently do not 
have the time to implement it.

Cheers,
Andreas

On 6/10/11 12:36 AM, Brandon Moore wrote:
> I'm not sure how well supported sized types are supposed to be,but I don't see how to use them with coinductive definitions.
>
> I'm trying to follow the slides from a 2008 AIM meeting.
>
> Is there supposed to be an ^ for sizes which is different from ↑?
>
>
> {-# OPTIONS --sized-types #-}
> module size where
> open import Size
> open import Coinduction renaming (∞ to ∞c)
> open import Data.Nat
>
> data Stream : (i : Size) → Set where
>    _∷_ : ∀{i} → ℕ → ∞c (Stream i) → Stream (↑ i)
>
> mapStream : ∀{i} → (f : ℕ → ℕ) → Stream i → Stream i
> mapStream f (y ∷ y') = f y ∷ ♯ mapStream f (♭ y')
>
> nats : Stream ∞
> nats = 0 ∷ ♯ mapStream {∞} suc nats
>
> nats' : ∀ {i} → Stream i
> nats' {i} = {!!}
> -- can't refine with _∷_, as that only produces values in Stream (↑ i)
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>

-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Theoretical Computer Science, University of Munich
Oettingenstr. 67, D-80538 Munich, GERMANY

andreas.abel at ifi.lmu.de
http://www2.tcs.ifi.lmu.de/~abel/