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

[Conor McBride]

On 13 Mar 2015, at 12:36, Andrea Vezzosi <sanzhiyan at gmail.com> wrote:

> The subtyping only works when Foo is recognized as having the right
> polarity, I don't know the details of the implementation but the Size<
> version seems to work out right:
> 
> data Foo (i : Size) : Set where
>  boo : {j : Size< i} -> Foo i
>  coo : {j : Size< i} -> Foo j -> Foo i
> 
> subtype? : {i : Size} -> Foo i -> Foo infty
> subtype? t = t

Now we’re cooking with gas. Here’s something a little close to what I’m after,
and it now works.

data Foo (i : Size) : Set where
  boo : Foo i
  coo doo : {j : Size< i} -> Foo j -> Foo i

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

bloat : {i : Size} -> Foo i -> Foo infty -> Foo infty
bloat boo blob = blob
bloat (coo x) blob = coo (bloat (keep x) blob)
bloat (doo x) blob = x

Many thanks

Conor

> 
> 
> On Fri, Mar 13, 2015 at 12:51 PM, Conor McBride
> <conor at strictlypositive.org> 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