Re: Termination and type systems

2006-06-27 Thread Dirk Thierbach
David Hopwood [EMAIL PROTECTED] wrote: Dirk Thierbach wrote: That's interesting, but linear typing imposes some quite severe restrictions on programming style. From the example of 'h' on page 2, it's clear that the reason for the linearity restriction is just to ensure polynomial-time

Re: Termination and type systems

2006-06-26 Thread Dirk Thierbach
David Hopwood [EMAIL PROTECTED] wrote: Marshall wrote: David Hopwood wrote: A type system that required an annotation on all subprograms that do not provably terminate, OTOH, would not impact expressiveness at all, and would be very useful. Interesting. I have always imagined doing this by

Re: Termination and type systems

2006-06-26 Thread David Hopwood
Dirk Thierbach wrote: David Hopwood [EMAIL PROTECTED] wrote: Marshall wrote: David Hopwood wrote: A type system that required an annotation on all subprograms that do not provably terminate, OTOH, would not impact expressiveness at all, and would be very useful. Interesting. I have always

Re: Termination and type systems

2006-06-25 Thread Marshall
David Hopwood wrote: Marshall wrote: David Hopwood wrote: A type system that required an annotation on all subprograms that do not provably terminate, OTOH, would not impact expressiveness at all, and would be very useful. Interesting. I have always imagined doing this by allowing an

Termination and type systems

2006-06-24 Thread David Hopwood
Marshall wrote: David Hopwood wrote: A type system that required an annotation on all subprograms that do not provably terminate, OTOH, would not impact expressiveness at all, and would be very useful. Interesting. I have always imagined doing this by allowing an annotation on all