[Agda] Sized types and Inspect idiom problem

[Andrea Vezzosi]

Specifing the sizes makes it work as expected

workaround : {ι : Size} → ListN {ι} → ℕ
workaround []n = 0
workaround (_∷n_ {i} x xs) with sized {i} xs | inspect (sized {i}) xs
... | n | [ fx≡n ] = { fx≡n }0

It seems like in a sized function the sizes doesn't get resolved early
enough for with to see that the two occurrences of (sized {_} xs) in the
context are the same expression.


Cheers,
Andrea

I guess the



On Thu, Feb 27, 2014 at 12:12 PM, Ernesto Copello <ecopello at gmail.com>wrote:

> Hi, Agda community.
> I found the following problem with agda's extension with sized types.
>
> As I show in the error function below, it seems that the inspect idiom does not work inside a sized function, when used to remember the result of another sized function.
>
> The other possible sized/not sized combinations seem to work, as tested in good1, good2 and good3 examples.
>
> Thanks
> Ernesto
>
> ---------------------------------------------------------------------------------
>
> {-# OPTIONS --sized-types #-}
> module InspectSizedTypesProblem {A : Set} where
>
> open import Data.Nat
> open import Size
> open import Relation.Binary.PropositionalEquality as PropEq
>
> infixr 10 _∷n_
> data ListN : {ι : Size} → Set where
>
>   []n : {ι : Size} → ListN {↑ ι}
>   _∷n_ : {ι : Size} → A → ListN {ι} → ListN {↑ ι}
>
> sized : {ι : Size} → ListN {ι} → ℕ
> sized []n = 0
> sized (x ∷n xs) = 1
>
> notSized : ListN → ℕ
> notSized []n = 0
>
> notSized (x ∷n xs) = 1
>
> -- sized/sized
> error : {ι : Size} → ListN {ι} → ℕ
> error []n = 0
> error (x ∷n xs) with sized xs | inspect sized xs
> ... | n | [ fx≡n ] = {! fx≡n!}  -- fx≡n has type ¨sized xs ≡ sized xs¨, error ?
>
> -- sized/not sized
> good1 : {ι : Size} → ListN {ι} → ℕ
> good1 []n = 0
> good1 (x ∷n xs) with notSized xs | inspect notSized xs
> ... | n | [ fx≡n ] = {! fx≡n!}  -- fx≡n has type ¨notSized xs ≡ n¨, good
>
> -- not sized/ sized
>
> good2 : ListN → ℕ
> good2 []n = 0
> good2 (x ∷n xs) with sized xs | inspect sized xs
> ... | n | [ fx≡n ] = {! fx≡n!} -- fx≡n has type ¨sized xs ≡ n¨, good
>
> -- not sized/not sized
> good3 : ListN → ℕ
> good3 []n = 0
>
> good3 (x ∷n xs) with notSized xs | inspect notSized xs
> ... | n | [ fx≡n ] = {! fx≡n!} -- fx≡n has type ¨notsized xs ≡ n¨, good
>
>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20140227/943042d6/attachment.html