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

[Andreas Abel]

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/