Arc Forumnew | comments | leaders | submitlogin
3 points by rocketnia 2963 days ago | link | parent

Yeah! There's a certain way that it's really clear that macros and statically typed code can work together; just run the macros before interpreting the static types. Thanks for demonstrating that. I do think this can do everything Arc can do, like you say.

There are a couple of ways I think that can get more complicated:

In languages that resolve overloaded names in a type-directed way, I think the reconciling of static types and macros gets quite a bit more challenging due to the underlying challenge of reconciling name resolution with macros.

For instance, I think Idris has different meanings for the name (,) depending on if it occurs as a value of type (Type -> Type -> Type) or a value of type (a -> b -> (a, b)). In one case it's a constructor of tuple types (a, b), and in another case it's a constructor of tuple values (a, b).

Idris's macro system actually seems to have some special support for invoking the typechecker explicitly from macro code, which I think helps resolve names like those. I haven't actually succeeded in writing macros in Idris yet, and it seems to be a complicated system, so I'm not sure about what I'm saying.

Secondly, one potential goal of a macro system is that all the language's existing primitive syntaxes can turn out to be macros. That way, future versions of the language don't have to inherit all the crufty syntaxes of the versions before; they can stuff those into an optional library. If the language has sophisticated compile-time systems for type inference, term elaboration, name resolution, syntax highlighting, autocompletion, etc., then hopefully the macro system is expressive enough that the built-in syntaxes are indistinguishable from well-written macros.

Arc already gives us things like (macex ...) that can distinguish macros from built-in special forms, so maybe seamlessness isn't a priority in Arc. But if it were, and Arc had static types, we would probably want Arc to have type inference as well, which could complicate the macro system.

A lot depends on what Paul Graham expects from "true macros."



3 points by Pauan 2963 days ago | link

I don't think name overloading is a problem, at least not in Nulan.

Macros deal with things at the syntax level, far earlier than any kind of type overloading.

As far as the macro is concerned, it simply sees the syntax

  (*list [ (*symbol ",") (*integer 1) (*integer 2) ])
It doesn't care what the type is, or the meaning, or anything like that. In some cases, the macro doesn't even know whether the symbol is bound or not!

Basically, I view type inference/checking/overloading occurring in a phase after macro expansion.

Is there any benefit to mixing the type overloading phase and the macro expansion phase?

----

It occurs to me that you might not be referring to a macro which expands to syntax, but instead using the syntax within the macro body itself.

In Nulan, that isn't a problem either. A macro is essentially a function from Code to Code, so the macro body is compiled/macro expanded/type checked just as if it were a function.

Thus any type overloading will happen inside the macro body, before the macro is ever run.

That does mean that the type checker must be able to overload based solely on the types found within the macro body. In other words, it cannot dynamically dispatch.

----

I don't think it's possible for the primitives to be macros, for the simple reason that the language needs axioms.

If you mean that the primitives should appear to be macros (even though they're implemented with compiler magic), then I agree with you.

-----

3 points by rocketnia 2962 days ago | link

"Macros deal with things at the syntax level, far earlier than any kind of type overloading."

If the macro itself is being referred to by an overloaded name, then the name needs to be resolved before we know which macro to call.

(I'm not sure if macros' names can be overloaded in Idris; I'm just guessing. Actually, I don't know if Idris lets users define overloaded names. I just know a few built-in names like (,) are overloaded.)

---

"If you mean that the primitives should appear to be macros (even though they're implemented with compiler magic), then I agree with you."

Yeah, that's what I mean. :)

-----

2 points by Pauan 2962 days ago | link

You're right, if you allow for users to overload multiple macros onto the same name based upon type, then it gets very messy.

But I think if your language allows for that, it's inconsistent with the way that macros work.

If you want powerful Arc-style macros, then the macro must be run before any types are known.

Any system which allows for that kind of type-based dispatch is different from a Lisp-style macro system, and is probably less powerful.

For example, you won't be able to create macros which create new variable bindings (like "let", "with", etc.) because the type of the variable is not known until after the macro is run.

I'm not sure what a system like that would look like, or if I would even call it a macro system.

I think it makes more sense to have two separate systems: a macro system that deals with syntax only, and an overloading system that deals with types. That's what Nulan does.

But perhaps there is room for a third system, somewhere in between the two: that third system could do type-directed syntax manipulation.

-----

2 points by Pauan 2959 days ago | link

I thought about this some more.

I have no experience with Idris or dependent types, so I may be completely wrong.

But from my understanding, a dependent type system allows for types to include values (which are evaluated at compile-time).

If so, then you might not even need macros at all to create the "," behavior.

Instead, you create a typeclass which will dispatch to the appropriate behavior:

  data Pair a b = pair a b

  interface Comma a b c where
    comma : a -> b -> c

  Comma Type Type Type where
    comma = Pair

  Comma a b (Pair a b) where
    comma = pair
Now whenever you use the "comma" function, it will dispatch depending on whether its arguments are Types or not:

  -- Type
  comma Integer Integer

  -- (Pair Integer Integer)
  comma 1 2
And since types may include arbitrary expressions, you can of course use the "comma" function inside of a type:

  foo : a -> b -> (comma a b)
Note: all of the above code is completely untested and probably wrong, but you get the idea.

Basically, your language needs first-class types, and the ability to run arbitrary expressions at compile-time (even within types), and then you can use an ordinary typeclass to get the desired type dispatch. No macros needed.

-----

2 points by rocketnia 2957 days ago | link

"If so, then you might not even need macros at all to create the "," behavior."

I never said the overloading of "," was accomplished with macros.

The example I gave was of a macro whose name was overloaded in a type-directed way, similarly to the way "," is overloaded in Idris. (Maybe the macro itself is named ",".) My point is that if the macro system is designed to support that kind of overloading, then sometimes a macro call will depend on intermediate results obtained by the typechecker, so we can't run the macroexpander in a phase of its own.

---

For the sake of remembering Idris more accurately, I checked out the Idris docs to look for the particular "macro system" I was dealing with.

It turns out what I mean by the "macro system" in Idris is its system of elaborator extensions (http://docs.idris-lang.org/en/latest/reference/elaborator-re...). The elaborator's purpose is to fill in holes in the program, like the holes that remain when someone calls a function without supplying its implicit arguments.[1]

It's pretty natural to handle name overloading in the same phase as implicit arguments, because it's effectively a special case. Thanks to dependent types and implicit arguments, instead of having two differently typed functions named (,), you could have one function that implicitly takes a boolean:

  (,) : {isType : Bool} ->
    if isType then (... -> Type) else (... -> (a, b))
  (,) = ...
The elaborator phase is complex enough that I don't understand how to use it yet, but I think almost all that complexity belongs to implicit arguments. Name overloading is probably seamless relative to that.

Another "macro system" I encountered in the docs was Idris's system of syntax extensions (http://docs.idris-lang.org/en/latest/tutorial/syntax.html). As far as I can tell, these apply before the elaborator and typechecker, but they might not be able to run arbitrary code or break hygiene. Maybe someday they'll gain those abilities and become a Nulan-like macro system.

[1] Implicit arguments effectively generalize type classes. Idris still has something like type class declarations, which it calls "interfaces," but I bet this is primarily so a programmer can define the interface type and the method lookup functions together in one fell swoop.

-----