Home » forums » LtU Forum

Expressing the Type of a While Loop

The Cat language has a primitive called while. The while construct takes two functions as argument, an invariant and a variant. Both functions consume the same number of elements from the stack. The variant (loop body) produces the same number and type of elements that it consumes. The invariant produces the same types as the variant, plus it leaves a boolean value on top of the stack. The while loop terminates when the evaluation of the invariant leaves the value false on top of the stack. The while loop pops the value false, before exiting.

So the question is: how should one express this in the type system?

Here is my current proposal:

define while : 
( 
  a:A=any* 
  variant:(b:A)->(c:A) 
  invariant:(d:A)->(d:A continue:bool)
)
  -> 
(
  result:A
)

What is good or bad about this notation? What other possibilities should I consider?

By cdiggins at 2006-08-06 16:19 | LtU Forum | previous forum topic | next forum topic | other blogs | 6159 reads

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

have you looked at any of

have you looked at any of the literature on stack based typed assembly languages...? You might find it helpful. I think David Walker at princeton has a few papers on that matter?

By carter at Sun, 2006-08-06 16:39 | login or register to post comments

I haven't yet ...

I haven't yet, but it is a good idea. Thanks for the suggestion.

I just found a nice compendium of papers related to typed assembly languages at http://www.cs.cornell.edu/talc/papers.html.

By cdiggins at Sun, 2006-08-06 16:48 | login or register to post comments

Referential transparency

Type expressions should at least be referentially transparent. any* probably means a different amount of any each time it is used, so maybe you should use something like any*n. That way you can also have any*m and any*n in the same type expression.

By Sjoerd Visscher at Sun, 2006-08-06 16:54 | login or register to post comments

Thanks for bringing this up.

Thanks for bringing this up.

It was my intention that in the type expression that A=any* and B=any* can represent different types (or sets of types to be precise), but that all usages of a single variable, like A, in the type expression would represent the same type.

Do you think it is likely, or at least possible, that a programmer might come to the conclusion by which I intended?

It seems to me that expressing A=any*m and B=any*n would be adding an extra possibly superflous term. Of course I don't want to stray too far from what people are already familiar with.

Another way to look at it is that, any* represents a set of types: so perhaps we can reason that it is indeeed referentially transparent.

By cdiggins at Sun, 2006-08-06 17:11 | login or register to post comments

It is not referentially transparent

You cannot reason that this is referentially transparent. The following certainly means something else:

define while : 
( 
  a:any* 
  variant:(b:any*)->(c:any*) 
  invariant:(d:any*)->(d:any* continue:bool)
)
  -> 
(
  result:any*
)

So it is a choice between what users of your language will see as a superfluous term in most of the cases, or keeping referential transparency which imho will give you more possibilities with complex type expressions.

By Sjoerd Visscher at Sun, 2006-08-06 20:39 | login or register to post comments