You might think that "incorrect code gets generated" would be a maximum-priority must-fix-before-the-next-release bug in a compiler, but apparently not.
Computed gotos are commonly used in main loops of bytecode interpreters to get a separate dispatch (indirect jump) at the end of handling each bytecode, so the CPU's branch target buffer has a better chance of predicting the indirect jump target for the next bytecode based on the previous bytecode. For instance, CPython's dispatch loop uses computed goto on supported platforms, and Erlang's BEAM VM (in non-JIT mode) uses computed branch labels to convert bytecodes into branch addresses at bytecode load time.
I suppose, for twice the latency, CPU designers could implement (a hash of) the previous branch address from the source instruction pointer as part of the BTB tag, similar to using the global branch history as part of the state in the branch predictor. Presumably, the global branch history could also be used in the BTB tag to give some hint as to which bytecode we've just finished executing.
Though, where it really counts, interpreter writers are already often using computed gotos, reducing the reward to cost ratio for implementing such specialized BTB improvements.
On the other hand,
while (1) {
switch (...) {
...
}
}
is probably rare enough (and almost certainly in a hot loop) that a very specific optimization flag might be better than a syntactic extension. Granted, an optimization flag doesn't work for Erlang's threaded code use case.
The code in question is related to setjmp/longjmp. As a general rule of thumb, this is something where the gut reaction to any bug report is going to be "you're doing it wrong"--the C standard actually provides a lot less guarantees here than most people believe it does. I haven't read the verbiage and the bug report in question in enough detail to ascertain if this is true or not, but it isn't in the least bit surprising that most people see setjmp/longjmp and immediately table the issue as being low-priority.
Not that surprising given that it seems specific to asan mode and only in the presence of setjmp/longjmp. I.e. this cant be that important unless the same bug shows also in non-asan Setjmp/longjmp case. Setjmp/longjmp are often a source of trouble for the register allocator or related optimization due to its unique properties. Often the optimizing compilers treat set/longjmp as "give up almost everything around those functions" but maybe llvm is trying hard to model it precisely and failing. But I haven't personally looked at the relevant code in llvm so this is mostly a speculation.
Then I agree that this is surprising. That means clang/llvm is not modeling set/longjmp correctly in general and that is not acceptable as a C compiler.
That's apparent from your ticket (which is marked as a duplicate) but on the one you linked to, all the offending compiler lines contain asan. Is there a chance this is impacting prioritization?
Regarding asan bugs, if you do not free all of your memory before exiting main it will complain about stuff and end up calling _exit I think which does not flush the buffers.
I have solved the halting problem. Every program you write compiles and executes as HALT; and therefore it's possible to determine if a program halts! It might not be correct but it sure is fast!
Many compiler writers are employed by hardware companies, and these companies are employing them to sell their hardware chips. For these companies, even a 1% boost in performance on $BENCHMARK can drive measurable impact on sales. Even if you're not worried about driving hardware sales, performance tends to be the major benchmark that gets mentioned in comparisons--note how the "Benchmarks Game" (what used to be called the Programming Language Shootout) compares languages solely on the basis of performance.
In other words, if you look at actual customer behavior, performance tends to be one of the most dominant factors in choosing one compiler over another (language compliance is probably more dominant, however). Surety of correctness is not a major factor at all.
Now, in order to actually report benchmarks correctly, you have to implement them correctly, so to some degree you have a basic guarantee that the compiler will usually work. But someone pointing out a soundness issue using a hypothetical example (as opposed to real code) is going to end up low priority because the evidence is that it doesn't matter in practice for the real, large applications that customers care about (as no one else has complained about it for the past several years).
In summary, practical performance will win out over theoretical correctness, but not practical correctness.
This is new to me (the Benchmarks Game has been around for well over a decade).
> 2) correctness is checked
This is par for the course of benchmarks. A benchmark that is incorrectly compiled provides no useful information whatsoever about performance. It's not really what people mean when they complain about correctness issues in the compiler (which is generally referred to as soundness in literature).
> 3) time "to complete and log all make actions" (build the program) is also logged
Performance in a compiler is usually taken to be a combination of runtime, code size, and compile time, although all three components are not weighted equally.
Or create OSes where applications are all written in managed languages, and the use of GCC and clang is gate keeped to the OS vendor and native libraries, just an idea.
Bit of a nitpick, but the real value is in safe languages, rather than managed languages, no? The distinction is a little blurry, admittedly, but as an example, I figure that verified SPARK counts as safe but unmanaged.
Still niche, Rust is not up to the stuff that app developers expect in terms of tooling and D still has quite a few @safe bugs to sort out, among its current adoption issues.
Unfortunely regardless of their own reports regarding CVEs, Microsoft, Apple and Google keep turning to C and C++ for their bottom layers + managed languages, instead of going full speed in some of those alternatives.
So it appears to be the long term solution to mitigate security issues, while keeping compatibility with existing code and tooling.
Frama-C is a specific compiler. It has not much to do with proving your own code. (And C ain't a good language for writing code you want to prove correct in.)
You are right that after having proven your code correct, you might want to use an implementation (compiler or interpreter), that is also proven correct. But those are still two different things.
I do; low level, OS and library code should be both. It's not an either or; you start with the correct code (and code to verify), then if needs be you optimize.
So you're saying maximum priority is correctness, and performance second place? Because if you don't have correctness you can't "start with correct code"
If you have a broken compiler, you can have broken generated code, and not even know it. This isn't about whether or not your C code is correct, this is about whether the assembly that's generated matches the behavior in your code.
Almost every commercially successful product I've worked on has been known to be wrong at every point in its useful life. I've worked on a lot of microservices that had no known bugs for most of their deployed life, but they were simple parts of more complex systems that did have known bugs. The computing world is built top to bottom mostly out of programs that are broken.
If this had not been possible, the industry would have gone the way Dijkstra advocated, with mathematical rigor applied to all programming.
Hmm, so no floating point math ever, only use arbitrary precision? As far as I know most 3D games do correct-enough math because it'll be replaced in a couple frames anyway.
Of course not. Correctness doesn't mean that everything has to be perfect. It means that things work as defined. A C program should operate as specified.
I sort-of disagree. Compilers that produce small and/or fast code and good error messages for complex languages are hard, but simple ones for simple languages aren’t.
Also, creating a toy one for a simple language is a fun educational exercise. We shouldn’t deter people from having a go at that by making them think “compilers are hard”.
For many simple languages (e.g. a language doesn’t need to have strings, multiple numeric types, operator precedence, or even have expressions containing multiple operators), writing a one pass compiler that always spills back operation results to memory isn’t too hard. Its assembly output can fairly easily be matched to the source, and it will provide a decent speed-up compared to a naive interpreter.
From there, the first few steps (peephole optimizations to remove store-load pairs, then a slightly more advanced register allocator) aren’t too difficult, either, and bring nice speed ups.
‘Real’ compilers are ‘just’ thousands more of such steps, each either extending the language or improving code generation, up from there. And yes, things do become very hairy somewhere along that route.
The thing that's nice about compilers is that they're hard for reasons that actually make sense, e.g. trying to apply an optimization for a particular case where you have to precisely prove that it results in the correct behavior. Or figuring out which instructions are most appropriate given various constraints.
This is a different kind of hard than, say, the makework that dominates other domains: "oh I haven't touched this project in a month and it now is somewhat broken because dependencies have subtly changed in ways that I have to spend hours debugging."
I'm convinced some devs love the pain imposed by the former, while others can better tolerate the pain of the latter without issue.
For added easiness, outputting high-level language code instead of machine code is a "cheat" that is often good enough, and you can typically borrow a lot of the high level features with relatively little effort. Say you want to run a domain specific language in your program? Include V8, and write a compiler that turns the DSL into JavaScript. You get much better performance than a simple interpreter, sandboxing, and somewhat useful error messages.
I agree with you. In fact I would say understanding compilers is really pretty easy. They are some of the most well researched and documented subjects (in CS) out there. Almost all compilers are going to follow a similar structure of lex -> parse -> pass0 -> passN -> generation.
The challenge these days seems to be in the passes which can become numerous and complex.
> They are some of the most well researched and documented subjects (in CS) out there.
Hmm this is the first time I've ever seen someone say this! I would say compilers are famously badly documented part of computer science, with many essential techniques basically not written down anywhere but buried in code, and passed through oral history from senior to intern over the years! It's a real problem.
I'd say both sides are true. The theoretical aspects of compilers are quite well-understood, and for pretty much every pass or analysis in the compiler, I could go and rustle up a citation of a paper or a talk or a book or what have you that explains the theory of the algorithm. On the other hand, actual code brings up issues that aren't easily handled in the theoretical framework, and the adjustments necessary to make it work well in practice generally are in the vein of the-code-is-the-documentation.
That's not quite the whole picture. Several industrial compilers for languages used by people for work are made by people who recognize that tooling is important. So the compiler is also a service or set of services with (depending on how you think about it) a database of information to query. It significantly increases the scope of the compiler and adds another dimension of performance and reliability to the system. For example, it may be a good idea to allocate a bunch of memory up front as a part of batch compilation to process some stuff. In a tooling scenario that can be a bad idea unless that large allocation routine is done in a way that the memory is pooled for the many, many requests it's going to get over its lifetime.
The hardest thing about compilers is that they are expected to be nearly perfect.
A typical user spends hours every day actively using the compiler and if they manage to observe even one bug every five years, that's probably considered a low quality compiler.
In that case clang, gcc and msvc would be considered low quality conpilers.
I get the sentiment: compiler bugs have a cascading effect, especially miscompiles (looking at you, clang). Crashed while compiling (looking at you, msvc) are also bad, but less serious.
In any case, you'd be surprised how many bugs a useful compiler may have.
For the record, I consider the three compilers I mentioned, having observed all sorts of bugs in then almost yearly, very high quality compilers.
We can mostly just work together to add to the mountain of regression tests that safeguard our open source compilers.
Maybe formal verification will some day produce bug-free toolchains, but we are not there yet for the production grade optimizing compiler.
Very nicely written article. Kudos to the Shipreq team for having close to 100% offline or local-first feature, is Shipreq utilizing automerge library to do that?
It's mentioned in the article that Go has a very fast compilation time and the same can be said of D language. The reason they are fast to compile because the languages' authors design the languages to be compiler friendly unlike C++. One of the main tricks to being fast to compile is by avoiding symbols look-up table.
For one of the feasible solutions, perhaps Petri net is better than graph. It is a generic state machine mechanism and here are a few examples of having a compiler design using Petri Net approach[1][2].
Third year PhD student in compilers here. Yes, compilers are hard but they are fun and addicting. No regrets switching from cryptography in masters to compilers in PhD. Lattice based cryptography is actually very hard and that's why I couldn't continue.
Compilers take input source and libraries and maybe some configuration parameters (in C you can pass preprocessor definitions, etc) and produce an output.
No network calls, no conditional file IO - the only side effects that are needed have to be done at the beginning, when you load source files and other libraries.
Why are so many compilers not utilizing more pure functional paradigms? Focusing on transformations of input to output instead of doing side effects. It seems like such a perfect fit.
Tons of toy compilers are written in functional languages. Standard ML or ocaml are probably the first thing that grad students would reach for when developing a compiler from scratch that isn't intended for production purposes.
However, in the real world everybody is using GCC/LLVM because they have rich open source communities and your work might actually get used by humans. LLVM in particular is nicely architected to be easily extensible so you can focus on just the compiler feature you want rather than bothering with all the other stuff needed around it. So then you are bound to the architectural decisions of these platforms. GCC in particular is a bit of a spaghetti mess and was designed long before pure functional design was trendy so you just sort of need to live with it.
Immutable IR is also a big challenge since the IR tends to actually be quite large. Making copies of it is sloooow.
Wasn't Rust bootstrapped with OCaml? I'm sure there are additional popular(ish) languages (i.e. Elm and PureScript) that are compiled with pure FP languages.
In academia many compilers are written in functional languages, particularly OCaml. Unfortunately, the programming community has come to this bone-headed idea that to be a serious language, its compiler must be implemented in itself. As a result, compiler implementation languages follow popular language trends. I’m sure a much faster TypeScript compiler could be written in OCaml or Rust, for instance.
> Unfortunately, the programming community has come to this bone-headed idea that to be a serious language, its compiler must be implemented in itself.
I wouldn't say so, I think 'serious' compiler developers seem to take a fairly level-headed view here.
Python and JavaScript for example aren't likely to ever be self-hosting, as it wouldn't make much sense. There's PyPy of course, but people only pay attention to PyPy when it does impressive things with performance, it doesn't get all that much 'credit' for being written in RPython. If that were all it brought to the table it would be viewed as a mere curiosity.
Java is moving to be more self-hosted (Graal), but this can bring real advantages (fewer undetected buffer overflows inside the JVM for instance), it's not being done just because it's cute.
Compilers can of course be written in all manner of different languages, I don't think it's a mistake that DMD is written in D, or that GNAT (the Ada frontend for GCC) is written in Ada, or that GHC is written in Haskell. It could serve as a useful example of a complex program written in that language, and it only requires that contributors know the language they're compiling.
> I’m sure a much faster TypeScript compiler could be written in OCaml or Rust, for instance.
In that specific instance I suspect you might be right, but this is just guesswork.
Hmmm my conclusion was drawn from the following languages having their main compiler written in that language: Haskell, Java, Scala, OCaml, Kotlin, C++, C#, F#, Rust, Go, Nim, Zig...
Not criticising any of these choices, but one has to wonder why. Most of these compilers were rewrites after a bootstrap implementation was created in an existing language.
> my conclusion was drawn from the following languages having their main compiler written in that language: Haskell, Java, Scala, OCaml, Kotlin, C++, C#, F#, Rust, Go, Nim, Zig...
I don't see a problem, all those languages seem well suited to implementing a compiler. For comparison, the Bash scripting language would be a nightmare.
> Most of these compilers were rewrites after a bootstrap implementation was created in an existing language.
at least two reasons come to mind: simplified bootstrapping and being a testcase and a source for feature requests for the language itself (especially important early on when there are few large codebases in that language).
Is it a good test case though? If the language is designed for writing compilers then sure, but I imagine most people using TypeScript (for example) just want to write full-stack web applications.
I agree that TypeScript isn't an obvious choice for writing a compiler, but self-hosting still has advantages. It tests out the language at scale, and there's the 'dogfooding' aspect that the compiler developers use the language they created (although as you say they're using it for an unusual purpose).
A lot of compilers for functional languages do exactly that. Each intermediate representation of the program is expressed as an algebraic datatype and each phase is a transformation from one (immutable) IR to another. A simple compiler might be 3 to 5 such IRs, but a more complex compiler might be dozens of passes.
The problem is that dozens of passes means dozens of copies. Compilation gets quite slow. It's not clear how to make a really fast compiler that has to do so much copying.
All of the compilers that I have worked on, except the toy compilers in grad school, used complex, mutable, and ultimately graph-based IRs. Controlling exactly the memory representation of the IR is important when a compiler does a lot of inlining and other optimizations, because a design mistake here can mean the IR for a compilation unit gets enormous and compilation time goes superlinear.
I designed the core of V8's optimizing JIT and these issues are really important for an industrial compiler.
It's definitely true, but compilers also need to change quickly and run fast which can put a lot of strain on the initial architecture.
Also, although the books tell you compilers are all cause and effect there's are parts that are pretty intertwined, be that parsing C++ or even the way that x86 is sufficiently complicated that performing instruction selection and scheduling requires some jiggling because of the complexity of the ISA and the breadth of microarchitectures available.
Anecdotally: because my compiler was surprisingly slow following a purely functional architecture. Though that was likely my own idiocy more than anything anyone else can draw a conclusion from :)
What language? When I write functional code (the compiler can enforce purity) in D I can usually get it running fairly quickly, but because of various things (memory locality, memory usage, etc.) I can see it being a problem in problem in the more traditional functional languages.
Ultimately for single-threaded applications avoiding state is usually just slower, however, it also buys correctness. Eliminating mutable state in composition can also massively improve the parallelism available to the programmer without making changes to the implementation.
Algebraic data types (tagged unions) are very useful for representing syntax trees and other things of the sort.
I'm not sold on the idea of going 100% purely functional (a-la haskell) though. Even a compiler written in a nonfunctional language is already going to be architected as a series of passes. The thing that makes it hard is not the presence of mutable global state. It's more the actual algorithms and optimizations.
I'm no academic, but functional languages have performance problems that simply cannot be handwaved away. For example, say you have a function that modifies an array. In a pure function, you cannot mutate in place, the function would need to return a "new" array. This necessitates at least a partial copy. I have seen proposed solutions for this where the array structure is some type of index table, where you can just mutate part of it and still maintain most of the original, thus avoiding having to potentially copy a huge amount of memory. However there is an unavoidable performance penalty, and also introduces issues like cache misses/pipeline stalls come in to play.
>Why are so many compilers not utilizing more pure functional paradigms? Focusing on transformations of input to output instead of doing side effects. It seems like such a perfect fit
The primary engineering and scientific challenge of compilers is optimization. That is all about finding a needle in a haystack, converting that to a slightly different needle, and putting it back in the same location in the haystack. This is something functional languages are fairly poor at.
I'm in my final year of my Bachelor's and I'm probably going to do a Masters after that. Do you have any advice for me on how to best get introduced to compilers? I feel like I don't have a good idea of what I want to focus on, it seems like compilers would be fun to explore and see if I like the topic.
> I recently saw a PR to Scala that’s a great demonstration of exactly this. The private and sealed keywords have been in Scala forever and someone only just recently came up with the realisation that private classes are effectively sealed. Scala’s been in existence for 16 years!
Slight correction: someone came up with the realisation 7+ years ago[1] but someone else came up with a fix only recently
Oh man, that's cool and everything, but IMHO the concept of "final" or "sealed" (popularized by Java I think and cargo-culted by C#) is an anti-pattern.
A simple proof of how this makes certain use cases impossible is: imagine you want to do reactive programming by watching for when a class variable changes and then running a function to handle that event. The simplest way to do this in something like C# is to create a child class and override the getter/setter for the variable. Then pass that child class to any method that accepts the base class. But if it's sealed you can't do that.
To make matters worse, many developers don't understand that if you want to use final/sealed, then you need to provide an interface for your class. That allows users to write their own classes that implement that interface, but still be drop-in replacements for the original classes. If your class is sealed, and you don't write an interface, then there is simply no way to do reactive programming with your class.
A workaround is to manually write an interface for the class (in situations that allow that). But even if you get that working, your code is no longer future-proof, because the burden of updating the interface falls on you instead of the original author.
A better solution would be to provide an automatically-generated interface for all classes at the language level (something like MyClass::interface). Then additional methods to extend that interface, if desired. Sadly/shockingly, I'm not aware of any language that does that.
Now this wouldn't seem to be all that important, but it hit me when I was trying to write a Unity library. I want to be notified when classes like GameObject and Mesh change, so that I can perform additional functionality (like updating metadata associated with the class instance). But since those classes are sealed, there is simply no way to do that:
When a language makes an opinionated decision blocking the user from implementing a common use case like this, it becomes a toy language. I lost weeks trying to find a workaround in Unity before being forced to give up. So I'm saddened to see Scala make the mistake of adopting a conceptual flaw in the name of an implementation detail like performance.
If someone has a workaround for the Unity example I gave, maybe using components or MeshFilter or something, I'd love to hear it. Please don't respond with explanations of inheritance vs composition, because I've already heard them.
(This might sound snarky and I apologize for that, I don't have time to write a big long thing here. I'm seriously FWIW.)
If writing the compiler is hard your language is too complicated; also, use Prolog.
I've been writing a compiler in Prolog for Joy (a concatinative language, and one that I suspect may be the simplest useful language) and (other than my own idiocy) it's been a breeze.
Last month I started in on Make-a-Lisp using Nim. I like both of those languages but now that I'm used to Joy and Prolog they both seem painfully over-designed and over-engineered. Not bad just woefully baroque. I couldn't go on. Perhaps this is just a personal problem, I acknowledge that, but I have a feeling that my experience generalizes, that we're working too hard, making things too complicated.
There's a few things I'll nitpick in this article.
> I mean more the type systems in languages like Scala and Haskell, think features like existential and dependent types. Type systems like Java’s and Typescript’s are great! They add value! But you can be an order of magnitude or two more safe with more advanced type systems and it’s profoundly beneficial when you learn how to make good use of them.
> Unfortunately, type-safety didn’t help me very much when developing my big feature....
I feel like the author is unintentionally reinforcing certain stereotypes around type systems. Typescript actually has an insanely powerful type system, in many ways much more advanced than Scala's type system and certainly more advanced than "vanilla" Haskell (i.e. something like Haskell2010). What often gives people the impression that a type system like Haskell is "strong" (or in the even more extreme case a type system like Elm, which has a reputation also for being "advanced" but is actually one of the simplest possible type systems with polymorphism) is that other features (mainly stuff around immutability) combine with the type system to enhance the guarantees that the type system can give. Very roughly speaking it is very hard to "go behind the type system's back" in these languages. However, the actual type system is not terribly advanced.
It's also weird to mention dependent types here because dependent types would have precisely solved the example the author brings up (this is leaving aside other issues that current dependently typed languages have).
For example in Idris you could write something like
Now you can't do this in Scala (although you can achieve something like dependently typed smart constructors with path-dependent types in Scala, but it's very fragile and I wouldn't recommend it) so I agree that this may not be the way you want to do things in Scala.
To go back up a level, the way that non-dependent types of the sort you'd find in Scala help you when writing a compiler is when you split your compiler into different passes. You can write a statically typed representation at the end of each pass to act as an "anchor" to cut down on certain classes of bugs both between two successive passes, but also to ensure that certain bugs can't span multiple passes.
I suspect the reason that the author wasn't getting a lot of mileage out of the Scala type system is due to a monolithic "compiler" design. If everything is a single giant pass then you get a lot less lift from the Scala type system (but this is true even if you substitute human understanding for a type system).
> This is provenance. It doesn’t sound that hard but in practice it was surprisingly challenging to implement.
Provenance is indeed very difficult, especially in the presence of things that change your representation, but not your semantics. It can really muck up your code to have to carry around a lot of baggage that's unrelated to your final result, but also has to be updated through the various stages of data transformation your result goes through as well.
> I recently saw a PR to Scala that’s a great demonstration of exactly this. The private and sealed keywords have been in Scala forever and someone only just recently came up with the realisation that private classes are effectively sealed. Scala’s been in existence for 16 years!
I feel like this kind of misrepresents the situation. The original bug was filed 9 years ago and only just now fixed because it was very low priority (which makes me think a lot of people have come to the same realization and just not really bothered about it). Regardless the original sentiment that different options intersect in a combinatorial explosion is something I can get behind.
> Would the code just do the exact same thing but with more boilerplate using IORefs or huge StateT stacks? Would Haskell be so efficient in its optimisation that a more straight-forward FP approach would be sufficiently fast?
When comparing Haskell and Scala the answer is generally yes, functional idioms tend to run a lot faster in GHC than with scalac. Not necessarily IORef (which can be actually surprisingly slow due to boxing issues), but StateT (and by extension State) is way faster in GHC than in scalac. Similarly IO in Haskell is faster than the attempts to emulate it with cats-effect or ZIO. You pay an overhead for FP in Scala that you don't always have to in Haskell.
That being said I still prefer to write performance sensitive FP code, that is still performance-tolerant enough to be conceivably written in something like Java or Go, in Scala if the only choices were Scala or Haskell. As the author mentions, mutability contained entirely within functions isn't really all that icky to me and my mental model for low-level unboxed array hacking in Scala or Java is more robust than my mental model for intricately weaving Haskell code to make sure all the requisite GHC optimizations fire in terms of being fairly confident what the overall optimization process would look like.
> Typescript actually has an insanely powerful type system
I think you are conflating expressivity with complexity here. You do not need a complex type system to get a very expressive language. For instance, the typing rules of dependent type theory are fairly simple compared to the amount of trickery needed to make TypeScript work.
At constant expressivity, a simple type system is always preferable to a complex one. So I am not amazed by the fact that TS needs advanced PLT debauchery to kind of work. It doesn't even give you strong guarantees. There is a reason why Hindley-Milner type systems are called the sweet spot of static typing.
I think Typescript has both a complex and expressive type system. When I say "advanced" I'm talking about expressiveness. It is more expressive than Scala and (absent a laundry list of GHC extensions) Haskell.
I agree that Typescript certainly seems like a tower of hacks next to Idris.
Yet somehow it's pulled off a reputational miracle: having a more expressive type system than Haskell but not being regarded as an "advanced" language. Unfortunately I think that's mainly due to the ways the type system can be undermined, but it's still a useful nugget I ponder from time to time.
> It doesn't even give you strong guarantees. There is a reason why Hindley-Milner type systems are called the sweet spot of static typing.
HM by itself doesn't give you strong guarantees (see e.g. the ML family of languages which have comparatively weak guarantees next to Haskell). That's really due to other language and standard library decisions acting in concert.
HM type systems are often the sweet spot for static typing not because of the guarantees they offer, but because of the global type inference it yields. More expressive extensions of HM often break global type inference in some way.
Can you explain how you view Typescript’s type system as ‘more advanced’ than Haskell’s type system? I am working on a language currently and wonder what gives you that impression as a user who seems knowledgeable and demes to have a preference for one style verses the other.
Typescript has all sorts of type-level computation goodies that Haskell doesn't have (unless you turn on insane amounts of GHC extensions).
Stuff like mapped types, keyOf, typeOf, ReturnType, literal types, conditional types etc. all combine to give you a certain amount of dependent types in Typescript but also a very rich way of doing type level computations (this is how e.g. in Typescript we can have type signatures that capture all sorts of very dynamic Javascript function signatures).
On top of this Typescript also has a strong structural type system augmented by union types and intersection types. You can fairly easily emulate a nominal type system like what Haskell has on top of this system, especially with Typescript's string literal types, but it's quite difficult to go the other way.
The only big thing I can think of that both Haskell and Scala have that Typescript doesn't is higher-kinded types.
I also want to strongly caution that I don't think a more advanced type system is necessarily a better type system! E.g. I'm not convinced that Typescript really needs HKTs.
Likewise I have previously programmed quite happily in Elm despite its paucity of type-level features in comparison to Typescript.
> Stuff [...] all combine to give you a certain amount of dependent types in Typescript but also a very rich way of doing type level computations [...].
I think this is a wrong use of the term "dependent types". For example, you can't write this in TypeScript (yet):
Sure, you can have a type-level object that corresponds to the numbers and use the type-level expression to compute the equivalent of alen + blen, but they are not dependent types. You have just shifted values to the type level. The type-level expression is awesome---but not because they are dependent types.
TypeScript is also not a typical type system you can compare with others. Most famously it is intentionally unsound [1], meaning that it can mostly but not entirely prevent a certain class of runtime errors, because it can't guarantee the behavior of external JS code anyway. Most static type systems are or at least try to be sound because that's what users expect them to be: preventing a wrong code beforehand. Dependent type systems are complex because they also want to be sound. TypeScript has an entirely different goal for a reason and you can't compare it with other type systems not sharing that goal.
Except for some issues regarding the stack size when resolving the types. (But I think there are more efficient implementations using more copy and paste, making this actually work)
No, you are creating a literal type which is not same to the corresponding literal. This is evident when you try to use alen and blen (respectively named n and m in your code) in the function code: they are strictly type-level constructs.
Also, probably I should have written my example as follows:
My original code did distinguish two sets of arguments because that's the TypeScript syntax closest to currying (and I was lazy to check its implication), but the point of dependent typing is that alen and blen are not necessarily known to the compiler. The compiler may have to deal with the following code then:
...where the first type `ArrayOfLength<alen + (blen + clen)>` should equal to the second type `ArrayOfLength<(alen + blen) + clen>` for the assignment to be valid. Since the compiler doesn't know alen, blen or clen, this means the compiler needs to somehow understand the associativity! This is hard, considering that (a+b)+c is not even generally same to a+(b+c) thanks to floating point.
For this reason many dependently typed languages also act as proof assistants or verifiers. If this point is removed, so-called "const generics" will be classified as dependently typed.
Well... would this satisfy you? (I removed the _add part for convenience. You could still argue that `_concat` is not a literal... if by literal you mean a primitive provided by the language itself. Note that i'm not claiming that this is a dependent type system. But you can emulate some features of such a type system.)
Uh, no? _concat is a type-level function and you can't generalize it to receive runtime arguments in any way. I do acknowledge the value of type-level evaluation, but there is a very deep gap between type-level evaluation and dependent typing.
> I think this is a wrong use of the term "dependent types".
The operative term here is "a certain amount." `typeof` in Typescript is definitely a dependent type operator (it takes a runtime value and extracts its type which can then be used as a type signature for other types).
You don't have full-spectrum dependent types a la Idris, but you do have some amount of dependent typing. See for example
type MyResult<T extends boolean> =
T extends true ? { tag: 'a' } : { tag: 'b' }
function outputTypeDependsOnInputValue(
value: boolean
): MyResult<typeof value> {
if (value) {
// replacing 'a' with 'b' is a type error
const result: MyResult<typeof value> = { tag: 'a' };
return result;
} else {
// replacing 'b' with 'a' is a type error
const result: MyResult<typeof value> = { tag: 'b' };
return result;
}
}
Now there's a good deal of limitations and hackiness here in how you call this function (in particular you need some weird overloadedness to preserve the types at call sites), but it is really some measure of dependent types! I'll include a full example at the end of this post.
> Dependent type systems are complex because they also want to be sound.
Dependent Haskell, if it lands, will not be sound (TypeInType). Idris 2.0 currently also is explicitly not sound. In the case of Idris that's mostly a matter of prioritization, but it's enough to demonstrate that soundness is, perhaps surprisingly, not a huge priority for even all full-spectrum dependently typed languages.
Full TS example:
type MyResult<T extends boolean> =
T extends true ? { tag: 'a' } : { tag: 'b' }
function outputTypeDependsOnInputValue<T extends boolean>(
value: boolean
): MyResult<T>
function outputTypeDependsOnInputValue(
value: boolean
): MyResult<typeof value> {
if (value) {
const result: MyResult<typeof value> = { tag: 'a' };
return result;
} else {
const result: MyResult<typeof value> = { tag: 'b' };
return result;
}
}
function worksWithA(a: 'a'): void {}
function worksWithB(b: 'b'): void {}
function useOurFunction(value: boolean): void {
if (value) {
const result = outputTypeDependsOnInputValue<typeof value>(value);
worksWithA(result.tag);
// worksWithB(result.tag) is a type error
} else {
const result = outputTypeDependsOnInputValue<typeof value>(value);
worksWithB(result.tag);
// worksWithA(result.tag) is a type error
}
}
There are numerous other well-known terms other than "dependent typing" that describe those features better, namely flow(-sensitive) typing. I believe the implementation of those type systems is considerably different from one of dependent type systems. I do have heard calling const generics as a "dependent fragment", which is fitting given that it might be the largest feasible fragment of dependent types without actually implementing the full-featured type system. I however object to any mention of dependent typing to describe something less capable than const generics since it's pretty misleading IMO.
You are absolutely correct that soundness is not the highest priority for dependently typed languages, as it had been true for other languages as well. Still I think most languages with a complex type system (subjective) do try to minimize the number of unsound corners as circumstances permit. I'm not an Idris user by myself but for example, the recent Idris 2 0.3.0 announcement [1] clearly considers unsoundness as something undesirable. As a result I have a general expectation for the type safety of those languages; I don't have that for TypeScript however (and I don't view that as a problem, just a difference).
I mean we're talking about definitions here so ultimately there isn't a definitive answer, but I think your definition of dependent types excludes a lot of things that are commonly referred to as "some dependent typing" or "lightweight dependent types" (this includes things like GADTs and singletons, Liquid Haskell, etc.).
It's important to note that what is going on in that TS example isn't just flow typing (otherwise something like Kotlin would count as a dependently typed language). The `typeof` operator is playing a crucial role here. That's what makes this really a case of a type depending on a runtime value.
If it was really just flow typing, then you could still replicate it in something like Scala by just introducing additional layers of types and folding over them (this is also why I would agree flow typing by itself is not dependent types). But that's insufficient to replicate the full TS example.
Idris doesn't want to make its soundness situation any worse than it already it is because the community does eventually want it to be completely sound. But like I said, that's not at the top of its priority list.
EDIT: Removed "Flow-sensitive typing isn't really all that different from dependent pattern matching (the main difference is on the other side of the coin, where you need some way of generating those dependent patterns and of cascading the flow "down" so to speak, so indeed by itself flow-sensitive typing isn't dependent typing). " as the first line because it didn't seem all that relevant in retrospect.
TypeScript supports ADTs (discriminated unions) and not-quite-pattern matching using a combination of features: union types, literal types and control-flow based type narrowing.
What you need to understand about TypeScript is that it ultimately is just JavaScript. After TS 2.0 a decision was made that TS will align with standard EcmaScript and will not implement any* run-time features not part of the ES standard or ES proposals.
Because of this decision TypeScript cannot have a proper dedicated pattern matching syntax until JavaScript gets one. TypeScript does support some pattern matching using ifs and switch statements and other control flow structures, but that's as good as it gets until JS improves as well.
and just as the complexity of HKTs might not add value to your team/project, other type tricks may also detract. These 'goodies' can seem 'insane' (or not) irrespective of which language they're realised in. After a while, I realised that I enjoyed Elm partly because of features it doesn't have ;)
HKTs are a lot less complex than most of Typescript; in a way they're not so much a feature as just the absence of a restriction (type parameters can have parameters just like any other type).
> Typescript actually has an insanely powerful type system, in many ways much more advanced than Scala's type system and certainly more advanced than "vanilla" Haskell (i.e. something like Haskell2010).
That's a strange claim. I mean, yeah, maybe you can say that it's more advanced than "vanilla" Haskell, but how many people use no extensions at all?
As for the comparison with Scala - maybe for Scala 2 that's true because of union- and intersection-types and Scala 2's lack of certain typelevel programming features.
But when compared to Scala 3 - is there anything major that you can do with typescript but not with Scala 3?
When I looked at typescript, my impression was that it has a lot of special rules and special syntax for certain typelevel programming features. Which is nice in many cases, but it doesn't compose and does not age very well. Still, I'm happy to see this development in a mainstream frontend language.
> That's a strange claim. I mean, yeah, maybe you can say that it's more advanced than "vanilla" Haskell, but how many people use no extensions at all?
Let me broaden that then. Typescript's type system is more expressive than even the proposed list of GHC2021 extensions. You really need to turn on "GHC and the kitchen sink" (basically your code is probably going to be using the singletons library and everything that entails) to get to the feature set of Typescript's type system. I think that's beyond what the vast majority of Haskellers use or are comfortable with.
> But when compared to Scala 3 - is there anything major that you can do with typescript but not with Scala 3?
Plenty. Part of it has to do with the fact that interfaces are truly structural types in Typescript whereas traits are still nominal in Scala 3. So for example, Typescript lets you have "complement types" (i.e. give me all the fields of A except those in B) which you cannot do in Scala 3.
Here's an example of a useful type-level thing I've found myself wanting all the time in Haskell and Scala that is very straightforward in Typescript.
Often we have a record
data MyRecord = MyRecord
{ field0 :: Int
, field1 :: Bool
, field2 :: Bool
}
that must undergo validation first before we can generate the record (e.g. parse out a bunch of strings for each field into Ints and Bools where those parse operations may fail).
It is tedious to write a whole new data type which duplicates all the fields, but just adds a Maybe in front of each type. Haskell has a design pattern known as "higher-kinded data types" that tries to mitigate that.
data MyRecord f =
{ field0 :: f Int
, field1 :: f Bool
, field2 :: f Bool
}
In its more sophisticated form we can use type families instead of normal higher-kinded types along with TypeApplications to make this fully seamless and get rid of a lot of Identity wrappers. Scala 3 allows something similar with match types (in fact you don't even need match types for getting rid of Identity wrappers due to Id in Scala being a type synonym and being able to do the equivalent of TypeApplications for higher-kinded type synonyms).
This approach, however, doesn't quite work if you have multiple validation steps that return multi-field fragments of MyRecord (e.g. one step returns a fully validated field0 and field1 and another returns a fully validated field2). You basically need to resort to writing a bunch of duplicated types again (type families can kind of save you if you happen to have all entirely distinctly types).
Typescript's mapped and conditional types handle this with aplomb, letting me generate any combination of fields wrapped in any combination of types from a single type definition.
Separately, in another comment in this same chain I give an example of (limited) dependent types in Typescript. I think you can replicate it with singletons in Haskell, but that's definitely getting into stuff that I would say "doesn't compose and does not age very well" in Haskell (ah should the blessed day that dependent Haskell lands arrive soon!). AFAIK you can't replicate that in Scala 3 because of a lack of value to type promotion mechanisms (I think even with match types it's not quite sufficient).
Actually, both your examples are possible to solve even in Scala 2. Check my repository from 4 years ago. The Readme has the examples that will be interesting for you: https://github.com/valenterry/bamboomigrate
I'm not saying it looks very elegant though - this is certainly improved a lot in Scala 3
Ah I think we're talking about subtly different things. You can definitely use generic goodness (`Generic` in Haskell and shapeless in Scala) to create generic conversions between different types, but the result of each conversion is not itself a user-friendly type.
In the case of shapeless the general pattern is to have a starting type, use something like LabelledGeneric, do a ton of HList transformations, and then transform back. But while you're living in HList land those are in fact HLists and not, say, case classes.
Indeed, you must always write out the final type yourself (e.g. create a new case class). Even if you're using only HLists and completely eschewing case classes (which is both ergonomically painful but also has a pretty large performance hit), shapeless's functions that generate new HLists (as opposed to extracting an element) almost always require you to annotate their use sites IIRC, which is effectively the same thing as needing to write out the whole case class.
To put it another way, with shapeless in Scala 2 you could prove that a certain type was the intersection of two other types and create the generic transformation to do so. But this isn't true intersection types because you still need to write your starting types and your final type. That is in Scala 3 you `T0 & T1` is a type in and of itself; you don't need to rewrite all the fields in common between T0 and T1 and assign it to a new type (and then e.g. use shapeless to prove the relationship between your types).
In the same way what you've demonstrated here aren't mapped types, conditional types, etc., but rather a way of using shapeless to prove that a certain type is the mapped type/conditional type etc. of another type. The former is what I meant when I said "letting me generate any combination of fields wrapped in any combination of types from a single type definition."
Shapeless doesn't get rid of the problem that "Higher-Kinded Datatypes" (HKD) is trying to solve, since you still have to write all the duplicate types by hand for any reusable function.
Moreover, apart from the tedium of rewriting all these types, the bigger issue is that TS's type system lets you stay entirely at the value level, whereas shapeless requires things to become type level computations, effectively bifurcating your code into "shapeless transformations" and "ordinary functions acting on e.g. case classes."
For example, the equivalent of your library in TS would have each step just be a normal function like any other rather than a special type level computation. It can be applied to a normal object directly and can be tested and reused just like any other function.
That match types page on Scala 3 I think undersells the differences. The real power of a lot of TS's type level computations is how they interact with each other and typeof (see my other example in this thread of lightweight dependent types).
All that being said, I really like the concept behind your library and would love to see it updated for Scala 3!
I am not okay with the kind of changes the article suggests in the code and test suite. At least IMHO it defeats the purpose of using richly typed language.
The Approach i would take is smartly dividing the code into namespace and libraries :
1. Spend more time in design process and isolating the low level concerns.
2. Seperate the business logic code into multiple namespace or perhaps libraries
3. extract the common utility classes, interfaces, enums in separate namespace, also the common layers like ORM, HTTP networking etc.
4. Test suite must be separate and can also adopt above 3 points mentioned internally
5. Provide enough configuration in build file so that the Independent or Semi-Independent modules or libraries can be compiled in both parallel through using multiple CPU cores and incremental manner through last compiler output cache.
Everything is hard until you know how to do it. Some things are hard after you know how to do it. But there's usually an easier way to do it, you just have to find and use it. If you find yourself going "boy this is hard" a lot, you probably just aren't doing it the easy way.
If a project management app is the hardest code you've ever written, this sounds like overengineering**2. Just use lists of lists like every other project management app.
You might think that "incorrect code gets generated" would be a maximum-priority must-fix-before-the-next-release bug in a compiler, but apparently not.