[Agda] Help, I'm failing at sized types.

[Conor McBride]

On 13 Mar 2015, at 12:12, Jan Stolarek <jan.stolarek at p.lodz.pl> wrote:

> data Foo : {i : Size} -> Set where
>  boo : {i : Size} -> Foo {i}
>  coo : {i : Size} -> Foo {i} -> Foo {up i}
> 
> subtype? : {i : Size} -> Foo {i} -> Foo {infty}
> subtype?  boo    = boo
> subtype? (coo t) = subtype? t
> 
> Does that work for you?

Yes. But that relies on solving (up i) = infty => i = infty, not on subtyping. Is

pred : {i : Size} -> Foo i -> Foo i
pred boo = boo
pred (coo x) = x

something which should work? How about

pred' : {i : Size} -> Foo i -> Foo infty
pred' boo = boo
pred' (coo x) = x

?

I’d prefer to avoid gratuitously recursive identity functions.

Thanks even for helping me confirm that something is happening.

All the best

Conor


> 
> Janek
> 
> 
> Dnia piątek, 13 marca 2015, Conor McBride napisał:
>> Hi
>> 
>> Sorry to be a nuisance.
>> 
>> I’m trying to do some stuff with sized types, but I think I’m failing at
>> basic stuff like finding the on-switch. Specifically…
>> 
>> ****************************************
>> {-# OPTIONS --sized-types #-}
>> 
>> module SizeFail where
>> 
>> open import Agda.Primitive
>> postulate
>>  Size : Set
>>  Size<_ : Size -> Set
>>  up : Size -> Size
>>  infty : Size
>> {-# BUILTIN SIZE Size #-}
>> {-# BUILTIN SIZELT Size<_ #-}
>> {-# BUILTIN SIZESUC up #-}
>> {-# BUILTIN SIZEINF infty #-}
>> 
>> data Foo : Size -> Set where
>>  boo : {i : Size} -> Foo i
>>  coo : {i : Size} -> Foo i -> Foo (up i)
>> 
>> subtype? : {i : Size} -> Foo i -> Foo infty
>> subtype? t = t
>> ****************************************
>> 
>> …results in the complaint...
>> 
>> .i != infty of type Size
>> when checking that the expression t has type Foo infty
>> 
>> …whether the pragmas are present or not.
>> 
>> Any light gratefully received.
>> 
>> (Longer term, I want to do some syntactic mangling in which renaming is
>> obviously size-preserving, so I can apply a renaming to a substructure
>> before I do a recursive call on it.)
>> 
>> Cheers
>> 
>> Conor_______________________________________________
>> Agda mailing list
>> Agda at lists.chalmers.se
>> https://lists.chalmers.se/mailman/listinfo/agda
> 
> 
> 
> ---
> Politechnika Łódzka
> Lodz University of Technology
> 
> Treść tej wiadomości zawiera informacje przeznaczone tylko dla adresata.
> Jeżeli nie jesteście Państwo jej adresatem, bądź otrzymaliście ją przez pomyłkę
> prosimy o powiadomienie o tym nadawcy oraz trwałe jej usunięcie.
> 
> This email contains information intended solely for the use of the individual to whom it is addressed.
> If you are not the intended recipient or if you have received this message in error,
> please notify the sender and delete it from your system.