Haskell has a RULES pragma that lets a user declare rewrites for the high-level optimizations that a compiler cannot deduce. They are most commonly used in the libraries. They are automatically applied by the compiler in the order of matching the AST from bottom-up.
```
{-# RULES
"map/map" forall f g xs. map f (map g xs) = map (f.g) xs
"map/append" forall f xs ys. map f (xs ++ ys) = map f xs ++ map f ys
#-}
```
Depending on the order of rules application, the quality of optimization can differ a lot. This fragility makes it harder to understand the impact of even a minor code change on the performance. It is also very hard to test that a particular optimization is applied, and to track down why if it's not.
Because of the nondeterminism we get from the metalanguage being a logic language, we don't have to worry about applying optimizers in a particular order. You can compose optimizers together, produce the possible results, and then select the best using a heuristic. Of course, the search space is potentially huge, so I'm looking into integrating constraints.
Reminds me of this paper on implementing compiler optimizations within the Julia language itself: https://arxiv.org/abs/2112.14714 -- "can symbolic mathematics do high-level compiler optimizations or vice-versa?"
Is it possible to write an optimizer for something like `sum (filter is_even (range 0 100))` into a for loop, as to avoid materializing 2 lists in memory?
Note that Rust doesn't need to do this because of the way `iter_into()` and mapping works. List fusion boils down to removing interior `.collect().iter_into()`.
There is something to be said for designing APIs so that you don't need such rewrite rules, though, of course, the need comes up eventually anyways, so rewrite rules end up being kinda necessary.
Unfortunately not! Embarrassingly, I haven't implemented pattern matching yet, which means functions like `sum` and `filter` can't be written. So far all my effort has gone towards the metaprogramming system. Bugfixing has me occupied at the moment, but after that I plan on doing pattern matching.
From what I can tell this is having a term rewrite system integrated into your language. Is this significantly different then Haskell manual rewrites. Which I admit are sometimes brittle.
The difference is that it’s much more general - the metalanguage is an actual logic language, not limited to simple rewrites. You can (read: will be able to, haha) prove properties about meta-level program transformations. For those interested, I’m basing my system off of Twelf and Abella.
You're right about term rewriting as a staged evaluation scheme. Similar to Haskell, I made this PL/compiler for Morgan Stanley where qualified type constraints (for e.g. type classes) are interpreted as stage-0 programs and rewritten into stage-1 programs that compile down to stage-2 programs (so a similar kind of stratification):
https://github.com/morganstanley/hobbes
It looks like this method is aimed at doing user pattern-matching on expressions in the first stage, kind of integrating Haskell-style rewrite rules in the main user language (rather than bolting them on the side in comments).
Major language crush... Everything from the type system to the compilation model to c++ compat just oozes good taste. Glorious structural record types, real union types (my running theory is that expression-based languages lacking these - looking at you, rust - are insufferable) AND variants. Pattern matching, slices, unboxed arrays/primitives, eager evaluation... Damn I love it.
Hobbes looks so totally frickin' awesome, I'm so going to play with this tonight.
Incredible work!
What would be really cool for this language is to hook into jupyterlab via xeus. It's not even that hard to do - I did it for my own (far inferior) toy language.
Not really. A detailed account of 2LTT can be found in this paper https://arxiv.org/abs/1705.03307 - 2LTT can be thought of as a general, type theoretic framework for metaprogramming.
Unfortunately there isn't, but I'll try my best here: In two level type theory, your language is actually two languages - a "meta language" (or meta level) and an "object language" (or object level). Additionally, we have a construct for relating object-level terms/types to meta-level terms/types. There are other, more type theory heavy qualifiers, but that's the basic idea.
It's quite a simple system, but it turns out to subsume quite a lot of others. Depending on how your conversion construct behaves, you can get vastly different metaprogramming systems.
The most important consideration when determining what you can do with 2LTT is how "similar" your two languages are, in a rough sense of the word. Remember that these really are two separate languages - they can have entirely different features and behave completely differently. Peridot is actually a good example, the object language is functional and dependently typed, while the meta language is more akin to λProlog or Twelf (it's a logic language).
If the two languages are identical, you can get something akin to partial evaluation for example. Peridot is on the other end of the spectrum, where the languages are completely dissimilar.
Note that 2LTT is actually even more broad than this. I'm talking specifically about 2LTT's applications to metaprogramming, but the authors of that paper used it to overcome some limitations of theorem proving in homotopy type theory.
TL;DR: In two-level type theory, your language is really two languages (levels) stuck together. You also have a construct to relate object-level terms/types to meta-level terms/types (notably, the reverse is not allowed). Depending on how this construct works, you can get all kinds of metaprogramming systems.
CL has many merits, but it does not and cannot ever have a type system like Peridot has. (If it did, it wouldn't be CL anymore.) It also does not have a logic-based metaprogramming language. Peridot's metaprogramming model is quite far from DEFINE-COMPILER-MACRO. You could build Peridot as a DSL in CL, using DEFINE-COMPILER-MACRO, even, but that's not the same thing as CL having "had this" at all, let alone "for decades".
Whether or not CL would still be CL if you embedded a Peridot-style type system is debatable. But the example given in TFA can be easily and straightforwardly rendered as a CL compiler macro. There might be useful things that Peridot can do easily that CL can't but these are not immediately evident, at least not to me.
Compiler macros are kind of a fluff feature that can easily be subsumed into regular macros.
You need two ingredients: (1) it must be possible to define a macro and function simultaneously for the same symbol. (2) the regular macro expander must detect fixed points in macro expansion and stop expanding. You want (2) anyway; if a macro returns the original form, so that its output is eq to its input, it make no sense to call it again.
This is the TXR Lisp interactive listener of TXR 275.
Quit with :quit or Ctrl-D on an empty line. Ctrl-X ? for cheatsheet.
TXR Lisp has no protected class members; C++ refugees may face discrimination.
1> (sqrt 5)
2.23606797749979
2> (fboundp 'sqrt)
t
3> (mboundp 'sqrt)
nil
4> (defmacro sqrt (n :form f)
(if (constantp n) (sqrt (eval n)) f))
** expr-4:1: warning: defmacro: defining sqrt, which is also a built-in defun
sqrt
5> (sqrt 5)
2.23606797749979
6> (macroexpand '(sqrt 5))
2.23606797749979
7> (macroexpand '(sqrt x))
(sqrt x)
8> (mboundp 'sqrt)
t
9> (mmakunbound 'sqrt)
sqrt
10> (mboundp 'sqrt)
nil
11> (macroexpand '(sqrt 5))
(sqrt 5)
Unlike a compiler macro, sqrt will always expand, guaranteed.
User-defined optimizations want to be tree rewrite patterns. We can impose that onto macros (or compiler macros).
In the TXR world, this can be done with a parameter macro, and one is provided for that, namely :match.
12> (defmacro sqrt (:match :form f)
(((@(constantp @exp)) (eval exp)))
(((* @exp @exp)) exp)
(((expt @exp 2)) exp)
((@else) f))
** expr-23:1: warning: defmacro: defining sqrt, which is also a built-in defun
sqrt
13> (macroexpand '(sqrt (* (+ x y) (+ x y))))
(+ x y)
14> (macroexpand '(sqrt (* (+ x y) (+ x z))))
(sqrt (* (+ x y) (+ x z)))
15> (macroexpand '(sqrt (* 5.5 5.5)))
5.5
16> (macroexpand '(sqrt (expt (sin x) 2)))
(sin x)
17> (macroexpand '(sqrt (expt (sin x) 3)))
(sqrt (expt (sin x) 3))
Parameter macros like :match are bound in the keyword namespace. When these bound keywords occur at the head of a parameter list, their macro gets invoked, receiving the parameter list and the function body, rewriting both of them together.
I made an interesting discovery yesterday. When you allow a symbol to have both a function and macro binding, it behooves you to implement the following expansion rule:
If a function call form (op ...) is the result of the expansion of a macro form (op ...) then after its argument forms are recursively expanded, if those recursive expansions make any difference, the resulting form should again be tried as a macro form.
This is because transformations on the arguments of the function call may turn the call into something that is interesting to the macro again.
With this, I can do the following now:
This is the TXR Lisp interactive listener of TXR 275.
Quit with :quit or Ctrl-D on an empty line. Ctrl-X ? for cheatsheet.
TXR contains many small parts, unsuitable for children under 12 months.
1> (defmacro sqrt (:match :form f)
(((* @exp @exp)) exp) ;; (sqrt (* x x)) -> x
(@else f))
** expr-1:1: warning: defmacro: defining sqrt, which is also a built-in defun
sqrt
2> (defmacro expt (:match :form f)
((@exp 2) ^(* ,exp ,exp)) ;; (expt x 2) -> (* x x)
(@else f))
** expr-2:1: warning: defmacro: defining expt, which is also a built-in defun
expt
3> (expand '(sqrt (expt x 2)))
x
See? (sqrt (expt x 2)) reduced down to x, even though the sqrt macro has no such optimization case.
First (sqrt (expt x 2)) is tried as a macro. That immediately hits a fixed point by returning the form. The expander makes a note that expansion took place (even if a no-op). Then the expander expands it as a function call, expanding the argument expression, turning the form into (sqrt (* x x)). That expansion having made a difference, together with the fact that the form came from a macro, now means that the expander tries the form again as a macro: (sqrt (* x x)) is expanded again, and now there is a "hit".
(For simplicity, these examples don't care about multiple evaluation; and it is a given that algebraic changes are risky in the face of floating-point. It's a good way to illustrate the technique.)
CL compiler macros could do something like this. I don't see the requirement in the HyperSpec. The requirement could be that when a compiler macro declines expansion, then after the resulting function form is recursively processed for more macros, the compiler macro should be tried again, and this process should repeat until both conditions are met: the macro declines, and the function form no longer contains any arguments that are macros.
Of course, a compiler macro can capture an &environment and do its own expanding via macroexpand. In this example, that would work. What I implemented is subtly different: a complete expansion is performed on the function. You would need macroexpand-all to simulate the feature in the macro itself. Not having to do that at all, having things Just Work, is pretty nice.
But I have an impression that Common Lisp doesn't have a type system, whereas this languages strives to have all "levels" of it's metaprogramming typed, so it's not like this language doesn't have any novelty.
Common Lisp has a very sophisticated type system. The only thing it doesn't have (among things that are currently fashionable) is compile-time typing by default.
Peridot is "novel" in that it introduces user-level compiler optimizations into a language that does have compile-time typing by default. But that's kind of like Chevrolet making a plug-in hybrid version of the C8 Corvette (which they recently announced they are going to do). Neither the C8 nor plug-in hybrids are new. A plug-in hybrid C8 will be new, and when it happens it will be a Big Deal to a niche market: the intersection of C8 fans and plug-in-hybrid fans. But it won't change the world.
(For the record, I happen to be a member of the niche market to which a plug-in hybrid C8 will appeal, so I am very excited about it. So I get that some people may be excited about Peridot. I just think it's important to keep things in perspective.)
Actually no, not in programming language theory. What researchers call 'type system' is much more precise than what programmers call 'type system'. In the PL field, the behavior of a term is traditionally split into static behavior (described by types) and dynamic behavior (described by reduction/evaluation). What programmers call 'dynamic type systems' is just a way to instrument the runtime with dynamic data-shape checks. Note that most dynamic languages do have a non-trivial type system, where functions are typed with their number of arguments (eg static scoping and other structure-related static checks). Languages like bash otoh do really have a trivial type system, whith every term merrily going into the evaluator without any static/typing well-formedness analyzis. You might also be interested in gradual typing, which is about deriving systematic dynamic checks from a type system and then augmenting a given type system with an 'any' type to go into untyped (ie dynamically checked) mode.
I'm assuming you why want me to explain what the difference between a static data-shape check and a type system is (since i'm already saying type systems are about static information).
For sure there is a non-empty intersection in some way, but the two are differently structured. For one 'data' is a runtime concept (some programs might be data, but some others are computations). So already a data-shape check isn't always doable statically like you would at runtime. And the other way around, some information might be statically available but not materialized in any kind of data shape, like type parameters for polymorphic functions, lifetimes in rust or in general irrelevant proof-terms in dependently-typed languages.
Perhaps you would be satisfied if i said that type-systems are a shape-check for terms and not for data.
It's not that I don't understand the concept you are trying to convey, or even that I disagree with it. What I object to is the co-opting of the word "type" to mean something other than it means in common usage. I understand that "type system" is a term of art within a certain research community, but this is not that community. HN is much broader than that, and within the context of that audience, "type system" already has an established meaning that encompasses things that happen both at compile time and at run time, and which applies to both terms and data [1].
> 'data' is a runtime concept (some programs might be data, but some others are computations)
And how do you distinguish between runtime and non-runtime? It's true that most languages have a distinction between compile-time and run-time but this is purely artificial, a design choice, not a reflection of any deep underlying mathematical truth. Common Lisp notably does not have a sharp distinction between the two. Compilation can trigger macro-expansion, which can in turn trigger arbitrary computations. This process can even loop back on itself: the computations triggered by a macro expansion can themselves invoke the compiler, and can even define new macros.
So when you say "Common Lisp does not have a type system" what you really mean is "the structure of Common Lisp is different from what is currently being studied by a group of researchers who have chosen to call the object of their study 'type theory'." The problem with phrasing it the way that you do is that it implies that Common Lisp is lacking something (a type system, according to your narrow definition of what a type system is). It isn't. Common Lisp isn't lacking anything, it is just structured differently. But this is a feature, not a bug, because if you want to avail yourself of the technology of what in academic circles is called "type systems" in Common Lisp you very easily can. But you don't have to.
In fact it is so-called "strongly typed" language that are lacking something, namely, the freedom to write code that does not conform to the constraints of the "type system".
... By "output", I mean "static output": a property of the syntax. A programming language in which we don't know what the output will be of every relevant node of the program's graph is "unoutputted". How anyone can tolerate unoutputted languages this day and age is beyond me; don't you want to know that the output is wrong before running the program? We have the tools and everything.
tldr of my long response: the misunderstanding between the "common usage" and "some research usage" stems from the belief that by strong/static we mean a restrictive definition (like the common usage of "strong typing"), our "static typing" is much flexible than "strong typing", to the extent that everyone is using some because it's useful.
:) i was waiting for you to come all lisp on me! (eh i just realized your pseudo) [sorry for the long msg, i like this topic!]
But this is just all staging! I would never say that lisp is not typed! Only perhaps streaming lisp interpreters (perhaps like lisp machines, don't know them very well) could be said truly untyped (actually: trivially statically typed). Dynamic vs static is more precisely seen as a sequentiality between stages, and you can have several stacked stages and even looping (as in lisp). But the distinction (in lisp still) between something that is quoted (a next-stage computation encapsulated into what is currently data) and current-stage computation is pretty clear. Some function bodies eval quoted stuff and some build quoted computations and you can statically see that: you can type it (using a quoted vs normal modality on top of any type system you already have). We could also talk about erlang.
In fact the trend is that for every convoluted language semantic that has traditionally been seen as dynamic/permissive/untyped, the research oriented world has come up with type systems explaining these languages. I talked about gradual typing earlier in the thread. There is static typing for memory state, complexity constraints, timing, validating interface checks, for well-typed macros and syntax reflection. Typing in some way is just structuring the mathematical semantic of your language. It can always be done, even after the fact, usually in tons of different ways.
I see where you come from, but still, actually i do believe there is a "deep underlying mathematical truth" in the sense that this sharp definition (typing is static) will help you to understand things because it's a deep concept. And as any deep concepts usually when you think you hit it's limit, you understand that you can generalize it into something that is more abstract but still has the core properties. The concept is still there, just said in more precise terms (more precise, because you're taking more parameters and leaving more irrelevant choices open in the concept, hence more abstract).
> In fact it is so-called "strongly typed" language that are lacking something, namely, the freedom to write code that does not conform to the constraints of the "type system".
This is wrong if by "strongly typed" you mean the term of art: you'd have to be willing to go out of your way to write a compiler for a language without any appearance stuff that could be qualified static typing. Static scoping and dependency analysis is a strong type system where types are the number/name of free variables. Compilation of call-conventions, memory layout and memory allocation interfaces can be done at scale with type systems (the llvm one is well-known, you'd be quite in the minority saying that llvm constrains you not to write your "untypable" self-mutating program). For most part, in practice, type systems are not a feature of the language but of the compiler, as for tons of cool systems, types can be infered (by a complete deciding procedure). Static type systems are just the fact that you will annotate programs with some local invariants, whatever they might be, to ease manipulating and reasoning on some form of term representation (AST, call-graph, ..).
> Actually no, not in programming language theory.
Which implies "having dynamic typing == no type system", which is just wrong, even in programming language theory. These two things are just completely orthogonal to each other. One is a compile-time thing and the other is a run-time thing. Any language can have either, or both, or neither. (And BTW, none of this has anything to do with my original objection, which was your abuse of the phrase "type system".)
> the distinction (in lisp still) between something that is quoted (a next-stage computation encapsulated into what is currently data) and current-stage computation is pretty clear
I'm sorry, but this is nonsense. Your understanding of Lisp seems to be about 50 years old. The only distinction between "something that is quoted" and something that is not quoted is that the former was produced by the reader (and in CL is stipulated to be immutable, but that is neither here nor there) while the latter may or may not have been. But even the Lisp reader can do arbitrary computations, at least in CL. So I have no idea what "current-stage computation" can possibly mean. You can run your entire program at read-time in Lisp if you want to.
> i do believe there is a "deep underlying mathematical truth" in the sense that this sharp definition (typing is static) will help you to understand things because it's a deep concept.
No, I disagree. Static typing is nothing more than a particular kind of partial evaluation under a set of constraints and assumptions that adhere to certain conventions. There is no magic in it. The study of type systems is nothing more than the study of the trade-offs that come from different sets of constraints and assumptions and conventions. At the end of the day, bits go in and bits come out, nothing more. Anything beyond that is just in the eye of the beholder.
This is not to say that the eye of the beholder doesn't matter, only that the value of any structure you impose on your bit streams, whether you choose to call it a "type system" or not, is necessarily ultimately a subjective assessment, not a mathematical one.
> Compilation of call-conventions, memory layout and memory allocation interfaces can be done at scale with type systems
Sure, but not because type systems represent a deep mathematical truth, but rather because they constrain the programmer to write code that is easier to compile because it is amenable to certain kinds of partial evaluation. It's kind of like how the existence of roads makes it easier to design certain kinds of cars, and these cars all share certain design features, and this leads to certain significant economic benefits. It does not follow that there is no value in designing vehicles that don't need roads.
``` {-# RULES
```Depending on the order of rules application, the quality of optimization can differ a lot. This fragility makes it harder to understand the impact of even a minor code change on the performance. It is also very hard to test that a particular optimization is applied, and to track down why if it's not.