4 ms·

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 t

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.
  - BoingBoomTschak 1y ago
    No, macros run at compile time (cf https://www.lispworks.com/documentation/HyperSpec/Body/03_bbb.htm https://www.lispworks.com/documentation/HyperSpec/Body/03_bb...), you may be confusing macros and reader macros.
    - taeric 1y ago
      Fair that I was definitely mixing them in my thinking. My general point was supposed to be simply that "compile time" is probably not what people are thinking of when coming from other languages. I was clearly a bit too eager to try and say that, though. :(
- rscho 1y ago
  Statically checked macros are useful to introduce new syntax at no runtime cost.

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.
- BoingBoomTschak 1y ago
  No, macros run at compile time (cf https://www.lispworks.com/documentation/HyperSpec/Body/03_bbb.htm https://www.lispworks.com/documentation/HyperSpec/Body/03_bb...), you may be confusing macros and reader macros.
  - taeric 1y ago
    Fair that I was definitely mixing them in my thinking. My general point was supposed to be simply that "compile time" is probably not what people are thinking of when coming from other languages. I was clearly a bit too eager to try and say that, though. :(
rscho 1y ago
Statically checked macros are useful to introduce new syntax at no runtime cost.