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

[Andreas Abel]

In the very latest development versions (maint-2.4.2 or master), 
irrelevant sizes work with Size<.  (However, there is no published paper 
assuring the soundness.)

{-# OPTIONS --experimental-irrelevance #-}

open import Size

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

{- sized terms with type flow direction -}
data Tm ..{a : Size} : Dir -> Set where
   Type  : Tm chk
   [_]   : .{b : Size< a} ->   (e : Tm {b} syn) -> 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

tm* : ∀{y}{t t' T : Tm chk} -> Reds y t t' -> Reds y (t :: T) (t' :: T)
tm* refl     = refl
tm* (r , rs) = tm r , tm* rs

ty* : ∀{y}{t T T' : Tm chk} -> Reds y T T' -> Reds y (t :: T) (t :: T')
ty* refl = refl
ty* (r , rs) = ty r , ty* rs

_++_ : ∀{y d}{a b c : Tm d} -> Reds y a b -> Reds y b c -> Reds y a c
refl     ++ ss = ss
(r , rs) ++ ss = r , (rs ++ ss)

{- 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) = tm* (devReds y t) ++ ty* (devReds y T)


On 13.03.2015 15:47, Andreas Abel wrote:
> The workaround is to actively replace all sizes by infinity.  Ideally,
> sizes in constructors would be irrelevant, but we are not there yet.
>
> er : ∀{a d} → Tm {a} d → Tm d
> er Type      = Type
> er [ t ]     = [ er t ]
> er (t :: t') = er t :: er t'
>
> {- show that you can compute a term to its development -}
> devReds : {a : Size}(y : Nat){d : Dir}(t : Tm {a} d)
>    -> Reds y (er t) (dev y (er t))
> devReds y [ t :: T ] = gamma , devReds y t
> devReds y Type = refl
> devReds y (t :: T) = {!!}
>
> Now you can give `gamma'.  Maybe the explicit erasure will get in your
> way somewhere else, but at least this lemma goes through...
>
> Cheers,
> Andreas
>
> On 13.03.2015 15:20, Conor McBride wrote:
>>
>> 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
>>
>> _______________________________________________
>> 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/
-------------- next part --------------
{-# OPTIONS --experimental-irrelevance #-}

open import Size

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

{- sized terms with type flow direction -}
data Tm ..{a : Size} : Dir -> Set where
  Type  : Tm chk
  [_]   : .{b : Size< a} ->   (e : Tm {b} syn) -> 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

tm* : ∀{y}{t t' T : Tm chk} -> Reds y t t' -> Reds y (t :: T) (t' :: T)
tm* refl     = refl
tm* (r , rs) = tm r , tm* rs

ty* : ∀{y}{t T T' : Tm chk} -> Reds y T T' -> Reds y (t :: T) (t :: T')
ty* refl = refl
ty* (r , rs) = ty r , ty* rs

_++_ : ∀{y d}{a b c : Tm d} -> Reds y a b -> Reds y b c -> Reds y a c
refl     ++ ss = ss
(r , rs) ++ ss = r , (rs ++ ss)

{- 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) = tm* (devReds y t) ++ ty* (devReds y T)