User loginNavigation |
Expressing the Type of a While LoopThe 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
|
Browse archives
Active forum topics |
Recent comments
17 weeks 4 days ago
17 weeks 4 days ago
17 weeks 4 days ago
39 weeks 5 days ago
44 weeks 16 hours ago
45 weeks 4 days ago
45 weeks 4 days ago
48 weeks 2 days ago
1 year 6 days ago
1 year 6 days ago