My point is that if you read code using
Codeas a staged program, where aCode[T]is a “value of type T at the later stage”, thenCode[T]acts like a lazy type, because using it multiple times repeats the computation that creates the value.
I think this is misleading and wrong.
Code[T]` is a “value of type T at the later stage”
Code[T] is not a value at a later stage! Code[T] is an code expression of type T at a later stage.
then
Code[T]acts like a lazy type, because using it multiple times repeats the computation that creates the value
I’m not sure what a lazy type is. You said evaluation model before, I’ll stick with that. I think you mean call by name, not lazy. Lazy is memoized call by name.
This is also a categorical error: you’re mixing the evaluation model with the staged substitution model (escape in metaml, or splice in scheme, say) which are completely different things.
I also think you’re also wrong about the semantics of substitution in staged languages. Using metaml syntax x: int code = <5 + 7>, then <~x + ~x> evaluates to <(5 + 7) + (5 + 7)>. What else could it mean? metaml has explicit facilities for managing expressions vs values (bracket vs lift). There’s no free lunch.
(What else could it mean? <F[~x]> could mean <let t = ~x in F[t]> I suppose. I’m not sure if metaml is pure functional, in which case the distinction is at most efficiency, and if it is not, you couldn’t control the order of evaluation in staged code.
<F[x]> could mean <F[f()]> where f() is a thunk that implements lazy evaluation of x, and again you can’t control the order of evaluation.)
It seems backwards to me to use staged programming, and admitted obscure and underdeveloped area of language design, to model a classical, well-understood and concrete process like codegen, but hey, we should take our insights were we can get them.