Thanks for the clarification, I think I understand your proposal. And I see three problems:
1. I believe ‘traces/t’ is the evidence of the issue I brought up earlier: How do call sites know the form expects the extra argument? As your example demonstrates, call sites need to be explicit about the extra argument. This becomes a global transformation in the model, which is doable with macro wizardry, but isn’t convenient and doesn’t look like what you’d see on a paper. 2. The thing I’m calling ‘metaparameter’ (in your example, ‘ticks’) needs to be available for the definition of the reduction relation. Instead of ‘(--> a b)’, think ‘(--> a b (side-condition (> ticks 10)))’. In your first example ‘ticks’ is in scope, but it suffers from the caching problem from my original message. In your second example ‘ticks’ isn’t in scope, and introducing it would be unhygienic. 3. Most important of all: the ‘metaparameter’ needs to be available through several definitions. Maybe the reduction relation calls a metafunction, which calls a judgment form, which calls a relation defined with ‘define-relation’, and they all might or might not depend on the ‘metaparameter’. Bonus issue: typesetting this is probably hard. -- You received this message because you are subscribed to the Google Groups "Racket Users" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. For more options, visit https://groups.google.com/d/optout.
