[Agda] a termination problem

[Ramana Kumar]

Thanks!

I think I got fairly close myself, but didn't succeed. The crucial
step I missed was saying _<_ was a Rel on Type {z} rather than just
Type (which probably means Type at the infinity size). (I tried
passing the {z} to the Type constructors in the definition of _<_, but
forgot to change the type declaration.)

Ideally, a lot of these implicit size arguments shouldn't have to appear, right?
I'm going to import Type into another module now, and I fear implicit
sizes are going to infiltrate everything there too... (e.g. if I have
a field of type Type in some new record, that record will have to be
size-indexed too probably)

Similarly it would be nice if the implicit argument to app<-cmp didn't
have to be given (so the definition of Application wouldn't have to be
made).

The latest version of my code is here
https://github.com/xrchz/typed-conv/tree/master/agda.
If you or anyone on the list have suggestions on the design or ways to
improve (possibly by making use of more cool new features like sized
types) please let me know :)

On Thu, Dec 1, 2011 at 8:09 PM, Andreas Abel <andreas.abel at ifi.lmu.de> wrote:
> Hi Ramana,
>
> I succeeded to pass your file through the termination checker.
>
> Cheers,
> Andreas
>
> On 30.11.11 3:19 PM, Ramana Kumar wrote:
>>
>> I put the Name module on hpaste too originally here
>> http://hpaste.org/54676
>>
>> if you would still prefer agda files let me know.... but I'm currently
>> in the middle of editing so I'd need to make them usable again first
>>
>> I'm experimenting with making Type sized and not just _<_ ... but I'm
>> not sure if you can compare/enforce sizes attached to different
>> types... but I think the termination argument for<-cmp would consider
>> sizes on Type and not on _<_.
>>
>> On Wed, Nov 30, 2011 at 2:16 PM, Andreas Abel<andreas.abel at ifi.lmu.de>
>>  wrote:
>>>
>>> Hi Ramana,
>>>
>>> would it be possible that you send me your agda file (including Name.agda
>>> which it relies on).  That would make my job easier than getting it from
>>> hpaste, fixing the problems due to absence of module Name, etc.
>>>
>>> Cheers,
>>> Andreas
>>>
>>> On 11/30/11 12:31 PM, Ramana Kumar wrote:
>>>>
>>>> I found your MiniAgda paper, and some slides... I had a skim, and
>>>> might read in more detail later...
>>>> It seems like sizes would have to appear on a lot of stuff in the
>>>> standard library for them to really be useful?
>>>>
>>>> I've put my next termination problem here http://hpaste.org/54700.
>>>> Can you see a way to use sized types to do this?
>>>> I will try myself, but I'm less sure about what's going on.
>>>>
>>>> I look forward to your reply :)
>>>>
>>>> On Wed, Nov 30, 2011 at 10:31 AM, Ramana Kumar<rk436 at cam.ac.uk>
>>>>  wrote:
>>>>>
>>>>> Wow, I would never have found that myself, thanks :)
>>>>> Is there any information or papers on sized types I could look at? (Or
>>>>> do you want to give a brief description here?)
>>>>>
>>>>> I have further similar termination problems later on in my
>>>>> development... I'll see if the same trick works! If not, maybe there
>>>>> is work on improving sized types support I could do?
>>>>>
>>>>> On Wed, Nov 30, 2011 at 12:18 AM, Andreas Abel<andreas.abel at ifi.lmu.de>
>>>>>  wrote:
>>>>>>
>>>>>> Hello Ramana,
>>>>>>
>>>>>> On 29.11.11 11:38 PM, Ramana Kumar wrote:
>>>>>>>
>>>>>>> Apart from the feeling that "there must be a better way", I also have
>>>>>>> a real problem to do with termination.
>>>>>>> In particular, I define a recursive function that passes itself to
>>>>>>> Relation.Binary.List.StrictLex.transitive.
>>>>>>> How can I convince Agda that transitive will only apply it to smaller
>>>>>>> arguments, or how can I avoid having to try?
>>>>>>
>>>>>> This is the typical situation where you would use sized types for
>>>>>> termination checking.  Unfortunately, the support for sized types is
>>>>>> rudimentary in Agda at the moment.
>>>>>>
>>>>>> However, your example works!  I attach a version of your agda code
>>>>>> with
>>>>>> a
>>>>>> sized definition of data type _<_.  [I removed Name since it was not
>>>>>> available to me, but this is inessential.]
>>>>>>
> --
> Andreas Abel  <><      Du bist der geliebte Mensch.
>
> Theoretical Computer Science, University of Munich
> Oettingenstr. 67, D-80538 Munich, GERMANY
>
> andreas.abel at ifi.lmu.de
> http://www2.tcs.ifi.lmu.de/~abel/
>