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

[Conor McBride]

On 13 Mar 2015, at 12:56, Andreas Abel <andreas.abel at ifi.lmu.de> wrote:

> Hi Conor,
> 
> sorry for the bad interface to sized types, it dates from 2008 when no big syntax invasions were wanted.  Thus, Agda silently accepts an "old-style" sized type (as you tried to implement with Foo) if it has the right format, otherwise it treats it as ordinary type.  [The new-style sized types Andrea explained are a bit less fragile.]
> 
> In particular, if you want an old-style sized type, every constructor has to target "Foo (up i)".  The following should work:
> 
> data Foo : Size -> Set where
>  boo : {i : Size} -> Foo (up i)
>  coo : {i : Size} -> Foo i -> Foo (up i)

OK, that explains a lot.

> 
> subtype? : {i : Size} -> Foo i -> Foo infty
> subtype? t = t

I’ll see if I can make progress with the new style.

Thanks

Conor

> 
> On 13.03.2015 12:51, Conor McBride wrote:
>> 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
>> 
> 
> 
> -- 
> 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/