EDIT: I'm referring to layout of the blog post in the thread title, the https://coalton.app/ is ok
"JSON Parser" example also has errors
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?
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
[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
What am I missing?
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]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.0The 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.
If you want to write a macro where any call to it which typechecks creates code which itself typechecks, you have to deal with eval of sexpr which is roughly a recursive typecheck on partial information, which sounds tractable to me.
CraigJPerry•3h ago
I'm completely clueless about Coalton, (and almost completely an idiot when it comes to CL more generally - been playing for a couple of years at this point but even so, every day is still a school day...)
asplake•3h ago
wild_egg•3h ago
Coalton moves that to the compilation step so you get an error back the instant you send the form to the REPL.
tmtvl•3h ago
skulk•2h ago
Here are some examples under:
First example is a generic multiplication. x and y could be _any_ type at all. If we disassemble this function, we get the following: Note that it calls `GENERIC-*` which probably checks a lot of things and has a decent overhead.Now, if we tell it that x and y are bytes, it's going to give us much simpler code.
The resulting code uses the imul instruction.matheusmoreira•1h ago
reikonomusha•1h ago
tgbugs•1h ago
0. https://www.youtube.com/watch?v=of92m4XNgrM
reikonomusha•1h ago
1. Bringing abstractions that are only possible with static types, like ad hoc polymorphism via type classes. For example, type classes allow polymorphism on the return type rather than the argument types. Something like
The function `into` is not possible in a typical dynamically typed language, at least if we aim for the language to be efficient. It only takes one argument, but what it does depends on what it's expected to return. Here, it's expected to return a string, so it knows to convert the argument type to a string (should knowledge of how to do that be known by the compiler). Common Lisp's closest equivalents would be which, incidentally, won't actually do what we want.2. Making high performance more accessible. It's possible to get very high performance out of Common Lisp, but it usually leads to creating difficult or inextensible abstractions. A lot of very high performance Common Lisp code ends up effectively looking like monomorphic imperative code; it's the most practical way to coax the compiler into producing efficient assembly.
Coalton, though, has an optimizing compiler that does (some amount of) heuristic inlining, representation selection, stack allocation, constant folding, call-site optimization, code motion, etc. Common Lisp often can't do certain optimizations because the language must respect the standard, which allows things to be redefined at run-time, for example. Coalton's delineation of "development" and "release" modes gives the programmer the option to say "I'm done!" and let the compiler rip through the code and optimize it.
3. Type safety, of course, in the spirit of ML/Haskell/etc.
bitwize•1h ago
It's 2025, people. Dynamic languages for serious projects were a 90s fad, hopefully never to be repeated.