Sizes should be irrelevant in constructors [Re: [Agda] (no subject)]

[Andreas Abel]

On 25.06.2014 22:36, Ernesto Copello wrote:
> Thanks very much for your quick response !
>
> Ok I need to generalize R to the sized version of D. But don't you think
> the next version of R is more specific ?
>
> data R : D → D → Set where
>      r1 : ∀{i}(n : ℕ) → R (d1 {i} n) (d1 {i} n)
>      r2 : ∀{i}(d : D {i}) → R (op d) (op d) → R (d2 d) (d2 d)
>
> I already check that this version works too.
>
> I understand your version indirectly size the elements of D, sizing the
> elements of R. While in this version I only size D elements not the hole
> relation R. In this example only D must be sized, because of I am doing
> induction in the length of D, not R.
>
> In fact, I want to know why I have to give explicit information about
> the size of the elements of D in R ? I belive that when no information
> was given, then ∞ size was assumed, and ∞ unificates with any size. So I
> don't understand the error : ∞ != .ι that gives Agda's compiler with the
> original version of R.

With {-# OPTIONS --show-implicit #-} you can see what is going on.  For 
instance, looking at term "r1 x" in hole 0:

   Goal: R (d1 {.ι} x) (d1 {.ι} x)
   Have: R (d1 {∞} x) (d1 {∞} x)

The original typing of constructor "r1" only constructs a relation 
between "d1"-constructed elements with size argument \infty, but the 
goal is for size argument \iota.  Agda does not know here that size 
arguments in constructors are irrelevant, so you get an error.

Here, you hit the research frontier...

Cheers,
Andreas

> On Wed, Jun 25, 2014 at 4:24 PM, Andreas Abel <andreas.abel at ifi.lmu.de
> <mailto:andreas.abel at ifi.lmu.de>> wrote:
>
>     Hi Ernesto,
>
>     you can generalize R to speak about the sized version of D:
>
>        data R : ∀{i} → D {i} → D {i} → Set where
>          r1 : ∀{i}(n : ℕ) → R {↑ i} (d1 n) (d1 n)
>          r2 : ∀{i}(d : D) → R {i} (op d) (op d) → R {↑ i} (d2 d) (d2 d)
>
>     Then the following function termination-checks:
>
>        ρ-good :  {ι : Size} → Reflexive (R {ι})
>        ρ-good {x = d1 x} = r1 x
>        ρ-good {x = d2 x} = r2 x (ρ-good {x = op x})
>
>     Cheers,
>     Andreas
>
>     On 25.06.2014 15 <tel:25.06.2014%2015>:04, Ernesto Copello wrote:
>
>
>         {-# OPTIONS --sized-types #-}
>         module problem where
>
>         open import Size
>         open import Data.Nat
>
>         open import Relation.Binary
>         open import Relation.Binary.__PropositionalEquality
>
>         data D : {ι : Size} → Set where
>             d1 : {ι : Size} → ℕ → D {↑ ι}
>             d2 : {ι : Size} → D {ι} → D {↑ ι}
>
>         -- d1 n, d2 (.. d2 (d1 n))
>
>
>         postulate
>             op : {ι : Size} → D {ι} → D {ι}
>             pr : {x : D} → op x ≡ x
>
>         -- Some reflexive binary relation
>         data R : D → D → Set where
>             r1 : (n : ℕ) → R (d1 n) (d1 n)
>             r2 : (d : D) → R (op d) (op d) → R (d2 d) (d2 d)
>
>
>         -- r1 (d1 n) (d1 n), r2 (r1 (d1 n) (d1 n))
>
>         good : D → D
>         good x with op x | pr {x}
>         ... | .x | refl = x
>
>         -- We are not able to do the same as above with size information
>         annotations, the following commented code does not compile:
>
>         -- problem : {ι : Size} → D {ι} → D
>         -- problem x with op x | pr {x}
>         -- ... | .x | refl = {! !}
>
>         ρ-good : Reflexive R
>         ρ-good {x = d1 x} = r1 x
>         ρ-good {x = d2 x} = r2 x (ρ-good {x = op x})
>
>         -- To pass the termination checking algorithm, we add size
>         information to the type signature of the previous code, but
>         another problem arises, and now the proofs do not pass type
>         checking.
>
>         ρ-problem : {ι : Size} → Reflexive {A = D {ι}} R
>         ρ-problem {x = d1 x} = {! r1 x!}
>         ρ-problem {x = d2 x} = {! r2 x (ρ-problem {x = op x})!}
>
>
>
>     --
>     Andreas Abel  <><      Du bist der geliebte Mensch.
>
>     Department of Computer Science and Engineering
>     Chalmers and Gothenburg University, Sweden
>
>     andreas.abel at gu.se <mailto:andreas.abel at gu.se>
>     http://www2.tcs.ifi.lmu.de/~__abel/ <http://www2.tcs.ifi.lmu.de/~abel/>
>
>


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

Department of Computer Science and Engineering
Chalmers and Gothenburg University, Sweden

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