Home
Reading
Searching
Subscribe
Sponsors
Statistics
Posting
Contact
Spam
Lists
Links
About
Hosting
Filtering
Features Download
Marketing
Archives
FAQ
Blog
 
Gmane
From: Nils Anders Danielsson <nils.anders.danielsson-Re5JQEeQqe8AvxtiuMwx3w <at> public.gmane.org>
Subject: Codata oddity
Newsgroups: gmane.comp.lang.agda
Date: Friday 6th June 2008 13:16:53 UTC (over 8 years ago)
Hi,

The current implementation of codata seems to be a bit problematic.
The following program was suggested by Nicolas Oury:

  data _≡_ {a : Set} (x : a) : a -> Set where
    refl : x ≡ x

  codata Stream : Set where
    cons : Stream -> Stream

  out : Stream -> Stream
  out (cons xs) = cons xs

  out-≡ : (xs : Stream) -> xs ≡ out xs
  out-≡ (cons xs) = refl

  ω : Stream
  ω ~ cons ω

  p : ω ≡ cons ω
  p = out-≡ ω

If we evaluate p we get refl, but if we replace the right-hand side of
p with refl we get a type error, so we do not have preservation of
types.

-- 
/NAD
 
CD: 2ms