[Fwd: Re: [Agda] Tentative guidelines for working with coinductive types]

[Andreas Abel]

-----BEGIN PGP SIGNED MESSAGE-----
Hash: SHA1

Hi, there is a message which I accidentially only sent to Nisse.

- -------- Original Message --------
Subject: Re: [Agda] Tentative guidelines for working with coinductive types
Date: Thu, 15 Jan 2009 19:06:05 +0100
From: Andreas Abel <andreas.abel at ifi.lmu.de>
To: Nils Anders Danielsson <nad at Cs.Nott.AC.UK>
References: <496CB2B8.4080903 at cs.nott.ac.uk>


Just like to throw in the obvious observation that this style of
coinductive types is just what you do to simulate them in a strict
language. In SML, usually one chooses

  ∞ T = unit -> T

  ♯ x = fn () => x        delay
  ♭ y = y ()              force

so, all the forcing and delaying is explicit.

That leads us to a research project:  Find a static analysis which
inserts all the delaying and forcing for you!  (Then sharp and flat can
return to the music sheets.)

Actually, that problem should be trivial, once you have coercive
subtyping.  Just add the subtyping axioms:

  -------------------    ------------------
  T <:_sharp infty(T)    infty(T) <:_flat T

Mmh, maybe something for Agda 3?

Cheers,
Andreas


Nils Anders Danielsson wrote:
> Coinductive types
> -----------------
> 
> Let us now move on to coinductive types. Inspired by Anton's ideas
> about destructor-based approaches to coinductive types I suggest that
> there should only be a single "codata" type (plus variants for Set1,
> Set2 etc.):
> 
>   codata ∞ (T : Set) : Set where
>     ♯_ : T → ∞ T
> 
> This type comes with a destructor, which is the only function which is
> allowed to pattern match on ♯_:
> 
>   ♭ : ∀ {T} → ∞ T → T
>   ♭ (♯ x) = x
> 
> Coinductive types are then defined using /data/, but with ∞ annotating
> coinductive arguments (this was suggested by Thorsten Altenkirch):
> 
>   data Colist (A : Set) : Set where
>     []  : Colist A
>     _∷_ : A → ∞ (Colist A) → Colist A
> 
> This makes it easy to choose which arguments should be inductive and
> which should be coinductive, so we can for instance define stream
> processors in a nice way:
> 
>   data Stream (A : Set) : Set where
>     _∷_ : A → ∞ (Stream A) → Stream A
> 
>   data SP (A B : Set) : Set where
>     get : (A → SP A B) → SP A B
>     put : B → ∞ (SP A B) → SP A B
> 
> Note also that the use of data plus ∞ corresponds quite closely to
> Anton's explanation of codata in terms of mutual coalg and data. The
> data part is put on the outside, though, so the destructor ♭ is
> applied in the (co)recursive calls instead of before pattern matching
> can take place, which means that we can avoid Anton's use of with:
> 
>   map : ∀ {A B} → (A → B) → Colist A → Colist B
>   map f []       = []
>   map f (x ∷ xs) = f x ∷ rec
>     where rec ~ ♯ map f (♭ xs)
> 
>   eat : {A B : Set} → SP A B → Stream A → Stream B
>   eat (get f)    (a ∷ as) = eat (f a) (♭ as)
>   eat (put b sp) as       = b ∷ rec
>     where rec ~ ♯ eat (♭ sp) as
> 
> Note above that ~ is only used right before ♯_. This ensures that the
> delayed expression can always be forced using ♭. If ~ is never used
> anywhere else this also ensures that we do not get the subject
> reduction problem discussed above, because dependent pattern matching
> on ♯_ is not allowed.

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

Theoretical Computer Science, University of Munich
http://www.tcs.informatik.uni-muenchen.de/~abel/
-----BEGIN PGP SIGNATURE-----
Version: GnuPG v1.4.6 (GNU/Linux)
Comment: Using GnuPG with Mozilla - http://enigmail.mozdev.org

iD8DBQFJkAAaPMHaDxpUpLMRAro5AKDopJcy3p3iB+sWzcIsN/yGEtIfXACeNUAE
lYaigup/xv5T92WAOWgLBWo=
=CvHY
-----END PGP SIGNATURE-----