Zig’s comptime code generation is an example of this approach. From what I’ve seen it works pretty well in practice. It has one big property that I don’t like though: whether or not your code typechecks is tested when the macro/template is expanded, not when it is defined. This means that you can write a comptime function that generates invalid code in some cases, and you never find out about it as long as those cases never happen.

I think it’s important to note that when you do find a case that generates invalid code, it is a comptime error. So, you can guarantee all usages of your function are valid if the project compiles.

This can also be applied to platform-specific blocks:

if (on linux) {
 // linux specific stuff
} else if (on windows) {
  // windows specific stuff
} else {
  @compileError("unsupportedPlatform");
}

If you were to call this function on an unsupported platform, it would be a compile error. If you don’t, you can compile the project fine. I think this property of the language is really cool, and I think the Zig standard library uses it for a few different things like skipping tests on certain platforms (others compilers embed this as metadata in the file).

For small macros/templates this is perfectly fine because it’s easy to make sure all the code is tested. But when you start using it for large and complicated things that may have unused code paths lurking in unexpected places, it starts to worry me. Maybe it works fine in practice most of the time, but the idea leaves a bad taste in my mouth.

It did for me at first - why on earth wouldn’t you want all of your code checked?? - but I think I’m being converted. Partial evaluation like this just feels so powerful. I’ve even ended up emulating these ideas in Java for work.

Lovely lovely lovely! I pretty much think the same (eg, https://matklad.github.io/2021/02/24/another-generic-dilemma.html). Generic programs are often useful, generic programmers are a bane of my existence (https://github.com/fsharp/fslang-suggestions/issues/243#issuecomment-916079347) :)

Just passing in the table with methods feels like it should be simpler, but it’s interesting that it can be more general. Eg, you can do things like storing indexes in a hashmap, and using the Hash from the thing the indexes refer to.

In my own sketch of the language, I was thinking about List.Eq(Point.Eq) style of constructing the table, and doing something akin to C++ ADL syntax for implicit syntax at the call site (ie, if T.Eq is a thing, use that) (so, you only pass tables explicitly if they are defined in a different module) (which I think should give you “implicit syntax is always coherent” property, by virtue only considering impls in the type itself) (and I am not sure strict coherence is useful, unless you have associated types: even with coherence, a Hash impl can change behavior depending on some thread local, so generic code can’t really rely on user-provided callbacks to behave “the same”).

We need something like Rust’s derive macros. I love Rust’s derive macros more than life itself.

Just in case our position here is as close as for generics, my thinking here is:

• interface for derives is String -> String. We don’t need hygiene for derives (we don’t have it even for Rust), and token trees are not that great of an abstraction.
• derive are strictly additive, the compilation model is as if the compiler just appends a bunch of stuff to the end of file. Compiler might actually want to materialize results of derives to disk, so that the IDE doesn’t have to ponder inconvenient questions when serving goto.
• derives don’t go through name resolution rule. When compiling a CU, the set of derive names is known up-front. In the source code, derives are called with dedicated syntax like @Serialize
  • this allows to expand derives in an embarrassingly parallel way during parsing on a per-file basis.
  • this also make it much simpler to answer “when to re-derive?” question, simplifying incremental compilation significantly.

This is a great writeup! I thought about going down the same path with my language, but it appears you got much further along 😀 I haven’t thought it through too much, but for the Ord case could you add an implicit Eq parameter to signify the dependency?

On another note, I also wanted to have something like derive for these modules but I’d like to avoid a whole other syntax for macros. I was thinking of something like comptime specifically for that but still have first class generics.

Language design is fun. I think the essential debate about typeclasses vs. modules is the same as implicit vs. explicit. With modules, you need to explicitly say one extra thing, which is how to instantiate the module, i.e.

const IntListEq = make_list_eq_thingy(IntEq)
const FloatListEq = make_list_eq_thingy(FloatEq)

I’ve written a lot of OCaml, which has the familiar ML-based module system, so have written a bunch of code with this pattern. It’s mostly fine, I can’t ever point to a scenario where it made my life too bad. I like the ease of typeclasses which is due to their implicitness, which means that you get certain code “for free.” I can’t point to a time where they complicated my life too much, but I also don’t use fancy features like HKT. Modules do feel simpler overall.

One last point about this remark / joke:

Math people, don’t bother correcting me.

You just wrote a detailed analysis about programming language theory. You are a math person, in my opinion. This frames math as some kind of in-group that does something other than what we’re doing here, which is analyze and reason about programs. Programmers are some of the most analytical and detail-oriented people in the universe, so I don’t understand the need to distance us from CS. I understand criticizing academia maybe, but not math itself.

Digression: Lua does something spiritually similar to this with its metatables. It’s pretty great! Basically each value has a “metatable” attached that has some magical methods on it that are called by operators, comparisons, etc. It also includes methods that are called on function application and on method lookup failure, so with these small primitives you can build just about anything.

It is almost a rite-of-passage for a beginning Lua programmer to read up on tables and metatables, and then create their own object-oriented system. You can find many implementations of varying scope and complexity.

How does this compare for the example to python magic methods (https://micropyramid.com/blog/python-special-class-methods-or-magic-methods/):

Operator           Method
+                  object.__add__(self, other)
-                  object.__sub__(self, other)
*                  object.__mul__(self, other)
...

Two, it turns out that coherence isn’t just for show. If you call make_list_eq_thingy(IntEq) twice, you get two different Eq(List(I32)) values which, by ML’s type rules at least, are not the same.

Could this be solved with memorization? So long as a functor is pure, you memoize the result and return a cached implementation on a second invocation.

(Apologies if this is covered later. I am half way through the article, but I need to get to work. 😬)

Even though it’s originally inspired by Scala, the concept behind modular implicits is very simple.

The absolute shade.

Great read. @icefox you might be interested to know that this is almost exactly how Coq implements typeclasses. For example, the definition of Eq from your example would look something like:

Class Eq (A : Type) := {
  equal : A -> A -> bool;
}.
Instance Int_Eq : Eq int := {
  equal := fun x y => (* ... definition of eq for ints *);
}.

The Class and Instance keywords in Coq are essentially the same as defining and instantiating a struct (you can pass around an Int_Eq just like any other ol’ struct). The only magic is that Instance updates a database of terms to be implicitly resolved, in the same way that you use the implicit keyword in your generic_sum example. Using the above definitions, one could then define:

Definition explicit_func (A : Type) (H : Eq A) : unit.
Definition implicit_func (A : Type) {H : Eq A} : unit.
                                 (* ^ curly braces *)

At which point calling (explicit_func int Int_Eq) and (implicit_func int) are equivalent.

I personally find Coq typeclasses a little clunky (typeclasses were added later, and sort of compete with the module system inherited from OCaml). Coq also primarily deals with mathematics, which has some steep hierarchies of inheritance (e.g. a total order :> partial order :> reflexive etc) which can be pretty cumbersome.

One takeaway from Coq that you might find useful is the notion of sections, which can be used to automatically append typeclasses to function arguments when used in a function body. For example, in some pseudo-garnet, this might look like:

section WithLen
  -- Any function in this section that uses `len_impl`
  -- will have `len_impl` appended to its arguments
  context len_impl: Len(@C)

  fn foo(container: @C): int = 
    let len = len_impl.len(container)
    ...
  end

  fn bar(container: @C): int= 
    return foo(container)
  end
end

-- foo is now foo(container: @C, len_impl: Len(@C))
-- bar is now bar(container: @C, len_impl: Len(@C))
--   ^ because it called foo, which requires len_impl

This is a rough example (you’d probably need some extra logic / syntax to unify all those @C’s), but hopefully this is some more food for thought. It might prove useful in say, a list library, where Cmp, Eq, and friends are pervasive.

I wonder whether algebraic laws would solve two seemingly-unrelated complaints that you’ve put forward. First, the question of whether a template is valid can be answered with a proof that some algebraic law holds on the template, before the template is ever applied. Second, the question of which derived interfaces are valid (e.g. when Eq and Ord are correctly defined relative to each other) can be answered with an algebraic law which relates interfaces to each other. In your example, we might prove that all instances of Eq which are derived from Ord are correct.