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

[Andreas Abel]

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

And here is Nisses' reply.

Nils Anders Danielsson wrote:
> Could one omit ♭? above? I think I prefer the answer to that question to
> be "no".

It is certainly no, unless one adds full extensionality for enumeration
types (such as Rec).
(But then many things become definitionally equal which are not
obviously equal, like f(f(f(x))) = f(x) provided f : Bool -> Bool).

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

On 2009-01-15 18:06, Andreas Abel wrote:

> That leads us to a research project:  Find a static analysis which
> inserts all the delaying and forcing for you!

> Actually, that problem should be trivial, once you have coercive
> subtyping.

I have thought about whether this would be a good idea. It could perhaps
be a bit confusing, but it would make the code less cluttered.

How strong would the subtyping be? (I want the rules to be simple and
easy to understand.) Consider the following code:

data Rec : Set where
  μ : Rec
  ν : Rec

∞? : Rec → Set → Set
∞? μ = λ A → A
∞? ν = ∞

♭? : ∀ r {A} → ∞? r A → A
♭? μ = id
♭? ν = ♭

data D (r : Rec) : Set where
  d₀ : D r
  d₁ : ∞? r (D r) → D r

data _≈_ {r} : D r → D r → Set where
  d₀ : d₀ ≈ d₀
  d₁ : ∀ {x y} → ∞? r (♭? r x ≈ ♭? r y) → d₁ x ≈ d₁ y

Could one omit ♭? above? I think I prefer the answer to that question to
be "no". In that case I assume that ♭? could be implemented as follows:

♭? : ∀ r {A} → ∞? r A → A
♭? μ = id
♭? ν = id

- --
/NAD




This message has been checked for viruses but the contents of an attachment
may still contain software viruses, which could damage your computer system:
you are advised to perform your own checks. Email communications with the
University of Nottingham may be monitored as permitted by UK legislation.



- --
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

iD8DBQFJkAGGPMHaDxpUpLMRAhobAKDRuSjV5nIxdJSv5hufCipZPPfq8wCdGs5N
cyOItCnODOR98JVVLXr2Krg=
=g07+
-----END PGP SIGNATURE-----