5 ms·

I have heard multiple people claim that macros are incompatible with strong or static typing and I don't see why. If there were a lisp with optional static typ

I have heard multiple people claim that macros are incompatible with strong or static typing and I don't see why. If there were a lisp with optional static typing like typescript, it would seem to me to be completely possible to write macros that write types. In many cases it woudl do away with the need for generic types (and allow multiple competing syntaxes for dynamic types). Most interestingly it would allow you to write new generic forms instead of waiting for whatever the language designer gives you. It would also allow you access to types at runtime (which the typescript language designers took away). Maybe people were telling me that lisp style macros were incompatible with hindley millner typing, but I still don't see how. The macros would just emit a hindley milmner subset. What am I missing?

reikonomusha 1y ago
As far as your first question is concerned, macros in and of themselves are not incompatible with a typed language. Coalton uses Lisp macros, for example, and they work seamlessly and as expected. But a Coalton macro is typically written in Lisp, not Coalton. This isn't in and of itself a problem---it's very easy and straightforward thus to write Common Lisp-style macros in Coalton. The difficulties arise when the macro must itself be (1) written in a statically typed manner, which gets into having a complete typing on your metalanguage (or your AST), and (2) allowed to access the type environment of the surrounding context in which the expansion is happening. If (2) should be accomplished, then the type-checking machinery must collaborate with the macro-expansion machinery, and that in practice makes both tasks very difficult to specify semantics for and implement. The language Hackett [1] worked toward solving the problem of having true typed and type-aware macros (they call them "type-aware" and "type-directed" macros [2]). Development unfortunately ceased ~7 years ago. [1] https://github.com/lexi-lambda/hackett https://github.com/lexi-lambda/hackett [2] I think this video has a good discussion of Lisp, macros, and static types, from the perspective of implementing a Haskell in Racket. https://www.youtube.com/watch?v=5QQdI3P7MdY https://www.youtube.com/watch?v=5QQdI3P7MdY
- spooky_deep 1y ago
  Since the macros run at compile time, I am ok with them not being statically checked. Statically checked macros seems like an academic curiosity. What am I missing?
  - wk_end 1y ago
    One concern I’d have is that any type errors would be reported on the macro expanded code and thus be pretty much inscrutable outside of toy examples.
    - reikonomusha 1y ago
      I think you're right that debugging errors involving complicated macros can get difficult, but to at least make the situation more tolerable, when Coalton expands a macro, it remembers where the expansion came from, so an error will be reported in the right place with the right source code. For example, using the RPN macro from the sister comment, here's an intentional type error: COALTON-USER> (coalton (rpn "x" "y" +)) --> <macroexpansion>:1:9 | 1 | (COALTON (RPN "x" "y" +)) | ^^^^^^^^^^^^^^^ expression has type ∀. (NUM STRING) => STRING with unresolved constraint (NUM STRING) | ^^^^^^^^^^^^^^^ Add a type assertion with THE to resolve ambiguity [Condition of type COALTON-IMPL/TYPECHECKER/BASE:TC-ERROR]
  - reikonomusha 1y ago
    Then nothing. Macros work. Silly example: COALTON-USER> (defmacro rpn (x y op) `(,op ,x ,y)) RPN COALTON-USER> (coalton-toplevel (define (double x) (rpn 2 x *))) ;; DOUBLE :: ∀ A. NUM A ⇒ (A → A) COALTON-USER> (coalton (double 3.0)) 6.0
  - taeric 1y ago
    The big miss here is that "compile time" is typically understood to be "batch compilation" time for languages. For Common LISP, macros run at read time. Which is often doable during runtime.
deleted 1y ago
[deleted]
kscarlet 1y ago
It's easy to just stick them together, but to me (who writes too much Lisp for my own health) this is unsatisfactory. The dream: just like macro can be seen as a (staged) extension mechanism for Lisp evaluator, there should be an extension mechanism for the static type system, which allows me to define new types, define new syntax (like Haskell do-notation) which makes use of typing environment and expected type of current context (return-type polymorphism), etc. The reality: very few environments figure this out. In Coalton Lisp macros do work, but only at the level of untyped S-expr. A Lisp macro can't know about types of the variables in the lexical environment, or expected type of its own context. But it quite possibly works fine for the "typescript-like" use case you described. The problem I see: H-M type system isn't designed with extensibility in mind, and it's hopeless to make it extensible. More technical explanation of why it's hard to integrate with Lisp macro is that H-M relies on a unification-based inference stage which execution flow is very different from macro expansion. Possible solution: There's no fundamental reason why static type can't have something as powerful as Lisp macro. However first of all you would need an extensible type system, which seems to still be an open research problem. I think bidirectional type system is hopeful -- it's so different from H-M at a fundamental level though that I think it's hopeless to retrofit into Coalton.
- JonChesterfield 1y ago
  What's the objection to putting type annotations on the macro, and refusing to compile code where the arguments to the macro don't match the type?
  - reikonomusha 1y ago
    Since a macro is a definition of syntax, I think you'd essentially need something like typing judgments to show how the typed elements of the syntax relate to one another, so that the type checker (e.g., a typical Hindley-Milner unifier) can use those rules. These are usually written as the fraction-looking things that show up in PLT papers. This is, as GP says, essentially extending the type system, which is a task fraught with peril (people write entire papers about type system extensions and their soundness, confluence, etc.).
deterministic 1y ago
You are missing nothing. Haskell has two different macro systems: typed and untyped.

reikonomusha 1y ago

As far as your first question is concerned, macros in and of themselves are not incompatible with a typed language. Coalton uses Lisp macros, for example, and they work seamlessly and as expected. But a Coalton macro is typically written in Lisp, not Coalton. This isn't in and of itself a problem---it's very easy and straightforward thus to write Common Lisp-style macros in Coalton. The difficulties arise when the macro must itself be (1) written in a statically typed manner, which gets into having a complete typing on your metalanguage (or your AST), and (2) allowed to access the type environment of the surrounding context in which the expansion is happening. If (2) should be accomplished, then the type-checking machinery must collaborate with the macro-expansion machinery, and that in practice makes both tasks very difficult to specify semantics for and implement. The language Hackett [1] worked toward solving the problem of having true typed and type-aware macros (they call them "type-aware" and "type-directed" macros [2]). Development unfortunately ceased ~7 years ago. [1] https://github.com/lexi-lambda/hackett https://github.com/lexi-lambda/hackett [2] I think this video has a good discussion of Lisp, macros, and static types, from the perspective of implementing a Haskell in Racket. https://www.youtube.com/watch?v=5QQdI3P7MdY https://www.youtube.com/watch?v=5QQdI3P7MdY

spooky_deep 1y ago
Since the macros run at compile time, I am ok with them not being statically checked. Statically checked macros seems like an academic curiosity. What am I missing?
- wk_end 1y ago
  One concern I’d have is that any type errors would be reported on the macro expanded code and thus be pretty much inscrutable outside of toy examples.
  - reikonomusha 1y ago
    I think you're right that debugging errors involving complicated macros can get difficult, but to at least make the situation more tolerable, when Coalton expands a macro, it remembers where the expansion came from, so an error will be reported in the right place with the right source code. For example, using the RPN macro from the sister comment, here's an intentional type error: COALTON-USER> (coalton (rpn "x" "y" +)) --> <macroexpansion>:1:9 | 1 | (COALTON (RPN "x" "y" +)) | ^^^^^^^^^^^^^^^ expression has type ∀. (NUM STRING) => STRING with unresolved constraint (NUM STRING) | ^^^^^^^^^^^^^^^ Add a type assertion with THE to resolve ambiguity [Condition of type COALTON-IMPL/TYPECHECKER/BASE:TC-ERROR]
- reikonomusha 1y ago
  Then nothing. Macros work. Silly example: COALTON-USER> (defmacro rpn (x y op) `(,op ,x ,y)) RPN COALTON-USER> (coalton-toplevel (define (double x) (rpn 2 x *))) ;; DOUBLE :: ∀ A. NUM A ⇒ (A → A) COALTON-USER> (coalton (double 3.0)) 6.0
- taeric 1y ago
  The big miss here is that "compile time" is typically understood to be "batch compilation" time for languages. For Common LISP, macros run at read time. Which is often doable during runtime.

deleted 1y ago

[deleted]

kscarlet 1y ago

It's easy to just stick them together, but to me (who writes too much Lisp for my own health) this is unsatisfactory. The dream: just like macro can be seen as a (staged) extension mechanism for Lisp evaluator, there should be an extension mechanism for the static type system, which allows me to define new types, define new syntax (like Haskell do-notation) which makes use of typing environment and expected type of current context (return-type polymorphism), etc. The reality: very few environments figure this out. In Coalton Lisp macros do work, but only at the level of untyped S-expr. A Lisp macro can't know about types of the variables in the lexical environment, or expected type of its own context. But it quite possibly works fine for the "typescript-like" use case you described. The problem I see: H-M type system isn't designed with extensibility in mind, and it's hopeless to make it extensible. More technical explanation of why it's hard to integrate with Lisp macro is that H-M relies on a unification-based inference stage which execution flow is very different from macro expansion. Possible solution: There's no fundamental reason why static type can't have something as powerful as Lisp macro. However first of all you would need an extensible type system, which seems to still be an open research problem. I think bidirectional type system is hopeful -- it's so different from H-M at a fundamental level though that I think it's hopeless to retrofit into Coalton.

JonChesterfield 1y ago
What's the objection to putting type annotations on the macro, and refusing to compile code where the arguments to the macro don't match the type?
- reikonomusha 1y ago
  Since a macro is a definition of syntax, I think you'd essentially need something like typing judgments to show how the typed elements of the syntax relate to one another, so that the type checker (e.g., a typical Hindley-Milner unifier) can use those rules. These are usually written as the fraction-looking things that show up in PLT papers. This is, as GP says, essentially extending the type system, which is a task fraught with peril (people write entire papers about type system extensions and their soundness, confluence, etc.).

deterministic 1y ago

You are missing nothing. Haskell has two different macro systems: typed and untyped.