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

[Conor McBride]

On 13 Mar 2015, at 13:04, Conor McBride <conor at strictlypositive.org> wrote:

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

And my next failure didn’t take long. This is a cut-down version of what I’m trying to do.

{- direction of type flow -}
data Dir : Set where chk syn : Dir

{- sized terms with type flow direction -}
data Tm {a : Size} : Dir -> Set where
  [_]   : {b : Size< a} ->   (e : Tm {b} syn) -> Tm chk
  Type  :                    Tm chk
  _::_  : {b c : Size< a} -> (t : Tm {b} chk)(T : Tm {c} chk) -> Tm syn
infixl 3 _::_

{- numbers will be used for fresh names, but no binding for now -}
data Nat : Set where
  ze : Nat
  su : Nat -> Nat

{-# BUILTIN NATURAL Nat #-}

{- reduction garbage-collects useless type annotations -}
data Red (y : Nat) : {d : Dir}(a b : Tm d) -> Set where
  {- b can be larger than a, if we add beta for lambda -}
  gamma : {t : Tm chk}{T : Tm chk} ->
          Red y [ t :: T ] t
  [_] : {e e' : Tm syn} -> Red y e e' -> Red y [ e ] [ e' ]
  tm  : {t t' T : Tm chk} -> Red y t t' -> Red y (t :: T) (t' :: T)
  ty  : {t T T' : Tm chk} -> Red y T T' -> Red y (t :: T) (t :: T’)

{- reflexive-transitive closure -}
data Reds (y : Nat){d : Dir}(a : Tm d) : Tm d -> Set where
  refl : Reds y a a
  _,_ : {b c : Tm d} -> Red y a b -> Reds y b c -> Reds y a c

{- develop a term by doing everything you can see -}
dev : {a : Size} -> Nat -> {d : Dir} -> Tm {a} d -> Tm d
dev y [ t :: T ] = dev y t
dev y Type = Type
dev y (t :: T) = dev y t :: dev y T
{- when I include lambdas, dev renames before and after recursive calls,
and sized types are just lovely! -}

{- show that you can compute a term to its development -}
devReds : {a : Size}(y : Nat){d : Dir}(t : Tm {a} d) -> Reds y t (dev y t)
devReds y [ t :: T ] = {!gamma!} , devReds y t
devReds y Type = refl
devReds y (t :: T) = {!!}

{- I can’t give gamma in that hole, due to size mismatch. Nor can I see how to
put sizes on the type of gamma to eliminate the mismatch. -}

So, the presence of sizes in types is just what I need to make the termination explanation
for dev, but the persistence of size information makes it harder to formulate and prove
properties of terms. I’m conscious that I’m just blundering about, but hopeful that there
might be some knack to learn.

I very much hope that, one day, the refinement of Tm with a suitable size discipline might
be localized to the definition of dev.

All the best

Conor



> 
> 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/
> 
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda