Comparison with other meta programming approach?

[glyh]

This reminds me of dependent types as they can solve similar problems. And naturally people will compare this to template haskell/rackets' macro system. And also there's recently Zig's comptime.

The question is simple: How is stuck macros compared to other approaches listed above?

Thanks!

[gelisam]

Thanks for your question, we should definitely answer those in the readme! Until I find the time to write a more polished version, here is a quick-ish answer.

Let's start with dependent types.

Dependent types and type-aware macros both allow you to compute part of the program based on a part of the program which is inferred by the compiler. Since dependent types can be quite long, dependently-typed compilers are typically quite good at inferring omitted arguments. And of course, the main feature of dependent types is that you can compute the rest of the type signature from that inferred value.

So in the case of dependent types, it is the value of an argument which is inferred, and it is a type which is computed. Of course, the output value is also computed based on that input value. Importantly, the compiler checks at the definition site that no matter which input value will eventually be inferred at the call site, the type of the computed value is guaranteed to match the computed type.

In the case of type-aware macros, it is not the value of an argument which is inferred, but a type T. And it is not a type which is computed, but rather the source code for an expression which, when type checked, must have type T. Importantly, the compiler does not check at the definition site that no matter which T is inferred at the call site, the computed code with always have type T. This is a trade-off: some errors are caught later than they could be, but in exchange, the macro is allowed to produce code using techniques which are more complex that what the compiler is able to prove correct.

[gelisam]

One confusing aspect of this comparison is that in a language with dependent types, the distinction between types and values is blurred. So when I say that it is a type and not the value which is inferred, that feels like a distinction without a difference, because the value of an argument of type Set is a type. The more important difference is thus the second one, the trade-off between type-checking at the definition site vs type-checking at the call site.

In the type-checking-at-the-definition-site world, dependent types is a feature which allows the programmer to express a more complex relation between the input type and the output type.

In the type-checking-at-the-call-site world, type-aware macros is a feature which allows the programmer to use more information (the type T) to compute the generated code.

[gelisam]

I should probably mention that there are languages like Agda which have both dependent types and type-aware macros.

[gelisam]

Next, Template Haskell. There are two parts to this: Typed Template Haskell, and the regular, untyped Template Haskell.

Untyped Template Haskell lives in the type-checking-at-the-call-site world. reifyType allows the splice to lookup the type of an identifier. Type-aware macros can be seen as providing an extra reifyCurrentType :: Q Type command which allows the splice to lookup the type T of the splice's call site. I would very much like to add this extra command to GHC one day!

[gelisam]

Typed Template Haskell is a complicated case. If I understood our last meeting correctly, @david-christiansen would say that Typed Template Haskell is Haskell's mechanism for staged computation, that is, it is a way to improve performance by running part of the computation at compile-time, it is not a way to improve the expressiveness of the base language by using macros to define new language constructs. Thus, macros and Typed Template Haskell simply live in different worlds and are not comparable.

I would say that in practice, Typed Template Haskell can be used for much more than that. Its API is clearly designed for the type-checking-at-the-definition-site world, but since the a in TExp a is a phantom type, it is possible to "cheat" by using untyped Template Haskell techniques to generate an Exp whose type cannot be inferred by the compiler, and then wrap it in a TExp a newtype to tell the compiler which type you expect that Exp to have. If that claim is wrong, the splice will fail at the call site.

When "cheating" in this way, it is possible to use type classes in order to compute a different Exp based on the type T, and thus, I would say that cheating-typed-template-haskell is very close in power to type-aware macros. The biggest difference, in my opinion, is that with Typed Template Haskell, you have to use typeclasses and type families to calculate that Exp, while with type-aware macros, it is a lot more straightforward: you pattern-match on the type.

[glyh]

Thanks for the detailed write up. I still have some questions here:

1. Given that dependent type system and stuck macros are calculating different things, are they able to coexist in the same system?
2. How is stuck macro compared to racket's macro system and zig's comptime?

[gelisam]

Given that dependent type system and stuck macros are calculating different things, are they able to coexist in the same system?

As I mentioned above, Agda supports both dependent types and type-aware macros, does that count as coexisting in the same system?

[glyh]

Yeah that does, sorry that I missed a few lines there.

[gelisam]

Next, let's compare type-aware macros with Racket macros. @lexi-lambda gave a great talk explaining how macros and type-classes do different thing, and how type-aware macros give you the best of both worlds. She implemented Hackett, a programming language featuring type-aware macros. She implemented it in Racket. Hackett's type-aware macros look like this:

(define-syntax todo!
  (make-expected-type-transformer
    (syntax-parser
      ... (get-expected this-syntax) ...)))

https://github.com/lexi-lambda/hackett/blob/e90ace9e4a056ec0a2a267f220cb29b756cbefce/hackett-lib/hackett/todo.rkt#L14C1-L23

That is, Hackett's type-aware macros mostly look like ordinary Racket macros, except that the macro can call (get-expected this-syntax), which is Hackett's version of reifyCurrentType.

[gelisam]

The next topic would be zig's comptime, but I am not familiar with zig, sorry. It looks like it calculates values (rather than code) at compile time? That it can take a type as input, and that this type can be inferred, but only the type of an argument, not the type T of the code being generated?

[glyh]

Zig has first class type at compile type. At compile time everything is duck typed. So we may calculate type/values at compile time. I heard people comparing zig's comptime to dependent types, and the main difference is that with dependent type you prove the type is correct, while in zig every call site prove the instance is correct with that specific input. I guess racket's macro and stuck macros falls into the second category right?

[gelisam]

Yes: both kinds of macros produce a syntax object, which is just an arbitrary s-expression. So at the definition site, the compiler does not guarantee anything about the contents of that the s-expression: it could represent an ill-typed program, an ill-scoped program, or even something which doesn't look like a program at all, like a grocery list.

Then at the call site, the resulting s-expression is interpreted as a program, and depending on whether the language is dynamically-typed or statically-typed, it may or may not be type-checked and scope-checked.

[gelisam]

I think we have covered all the topics you listed, but there is one last comparison I want to make: the difference between type-aware macros and stuck-macros. They are only different in a language which uses unification variables to infer types. As @lexi-lambda and I explain in our respective talks (mine is linked from the readme), implementing type-aware macros requires interleaving macro-expansion and type-checking. If type-checking involves resolving unification variables, then the details of that interleaving affect which type variables have been resolved by the time the type-aware macro asks for the type.

Different implementations of type-aware macros handle this differently. Agda reveals which part of the type is still an unresolved unification variable, allows the macro to block until the unification variable is resolved, and then restarts the type-aware macro from the beginning. Klister does not reveal which part of the type of still unresolved, automatically blocks the macro if it tries to match on the type to which this unification variable will resolve, and then resumes the macro where it stopped. I call this particular approach "stuck macro", and I think it's a desirable feature because it prevents the author of the type-aware macro from accidentally depending on the details of the interleaving.

[gelisam]

Leaving this ticket open to remind me to add some of this to the readme

[david-christiansen]

Agda reveals which part of the type is still an unresolved unification variable, allows the macro to block until the unification variable is resolved, and then restarts the type-aware macro from the beginning.

Lean 4 does this too - see section 5 of the macro paper.

[david-christiansen]

I think it's a desirable feature because it prevents the author of the type-aware macro from accidentally depending on the details of the interleaving.

To be extra precise, this is true to the extent that macros have no other way of communicating with one another than solving unification variables (at least, I'm pretty sure it's true - no proof!). But if macros have access to arbitrary side effects, this goes away. Macro programming in Klister is really a kind of deterministic parallel programming issue - how can all these "threads" (macro expansions) be arbitrarily interleaved without that affecting the final answer, at least in cases where the program is type-correct? We're looking at techniques inspired by Lindsey Kuper's LVars.

[david-christiansen]

Agda supports both dependent types and type-aware macros

Idris and Lean both have this as well - I'm not sure about Coq, it wouldn't surprise me if there was something like that in there too.

[david-christiansen]

(Sorry for being nitpicky, hope it was useful)