<html>
<head>
<meta http-equiv="Content-Type" content="text/html; charset=UTF-8">
</head>
<body>
<p>Hi Jesper,<br>
</p>
<p>Thanks for the information. On issue less is good news. However,
from what I understand from earlier exchanges on this list, the
more serious issue with sized types is the inequality ∞<∞. When
that is fixed I would be very interested to see the repercussions
on existing code such as the codata definitions in the standard
library and, much more modestly, on a development I did that uses
sized types. <br>
</p>
<p>Best regards,<br>
</p>
<p>- Vlad<br>
</p>
<div class="moz-cite-prefix">On 22/10/2020 13:36, Jesper Cockx
wrote:<br>
</div>
<blockquote type="cite"
cite="mid:CAEm=bozoOppn9q-02b=aqp7+7HRB6H1CTWkXMjdFxiaU9v2NeQ@mail.gmail.com">
<meta http-equiv="content-type" content="text/html; charset=UTF-8">
<div dir="ltr">
<div>Hi Vlad,</div>
<div><br>
</div>
<div>I just fixed issue #4995 this morning, this also means your
example is no longer accepted by the development version of
Agda:</div>
<div><br>
</div>
<blockquote class="gmail_quote" style="margin:0px 0px 0px
0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">
<div>Failed to solve the following constraints:<br>
Is empty: n ≡ suc (λ {_} → n) (blocked on _s_49)<br>
</div>
</blockquote>
<div><br>
</div>
<div>-- Jesper <br>
</div>
</div>
<br>
<div class="gmail_quote">
<div dir="ltr" class="gmail_attr">On Sat, Oct 17, 2020 at 11:39
PM Vlad Rusu <<a href="mailto:Vlad.Rusu@inria.fr"
moz-do-not-send="true">Vlad.Rusu@inria.fr</a>> wrote:<br>
</div>
<blockquote class="gmail_quote" style="margin:0px 0px 0px
0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">The
following code shows how a slightly wrong use of sized types
in a <br>
definition of natural numbers leads to a proof of ⊥.<br>
<br>
--------------{-# OPTIONS --sized --safe #-}<br>
open import Relation.Binary.PropositionalEquality as Eq<br>
open import Data.Empty using (⊥; ⊥-elim)<br>
open import Size<br>
<br>
<br>
-------------- auxiliary--------------<br>
→-elim : ∀ {A B : Set} → (A → B) → A → B<br>
→-elim L M = L M<br>
-- a trick found on the Web_<br>
data [Size<_] (i : Size) : Set where<br>
box : Size< i → [Size< i ]<br>
unbox : ∀ {i} → [Size< i ] → Size< i<br>
unbox (box j) = j<br>
<br>
--size eliminators<br>
size-elim : (P : Size → Set) → (∀ i → ((j : [Size< i ]) →
P (unbox j)) <br>
→ P i) → ∀ i → P i<br>
size-elim P Hind i = Hind _ λ { (box j) → size-elim P Hind j }<br>
size-elimproved : (P : Size → Set) → (∀ i → ((j : (Size<
i)) → P j ) → P <br>
i) → ∀ i → P i<br>
size-elimproved P Hind i = →-elim (λ {Hind' → size-elim P
Hind' i })<br>
λ {i' Hind' → Hind i' (λ { j' → Hind'
(box j') <br>
}) }<br>
------------ end auxiliary-----------<br>
<br>
-- one might think that the following is a definition natural
numbers <br>
using some Size arguments<br>
data ℕ {s : Size} : Set where<br>
zero : ℕ<br>
suc : ({s' : Size< s} → ℕ {s'}) → ℕ {s}<br>
<br>
-- the definition is slightly wrong ("suc" should not contain
<br>
()-parentheses) and leads to a proof of ⊥<br>
<br>
-- introducing foo, a certain natural number<br>
foo : ℕ<br>
foo = size-elimproved (λ s → ℕ{s}) (λ _ H → suc λ { {j} → H j
} ) _<br>
<br>
-- foo is a successor to itself<br>
bar : foo ≡ suc foo<br>
bar = refl<br>
<br>
-- which is forbidden<br>
baz : ∀ (n : ℕ) → (n ≡ suc λ { _ } → n ) → ⊥<br>
baz _ ()<br>
<br>
--hence...<br>
zut : ⊥<br>
zut = baz foo bar<br>
<br>
_______________________________________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se" target="_blank"
moz-do-not-send="true">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda"
rel="noreferrer" target="_blank" moz-do-not-send="true">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
</blockquote>
</div>
</blockquote>
</body>
</html>