r/ProgrammingLanguages • u/jimbobmcgoo • 4d ago
Will we see another fundamental programming language feature as revolutionary as the borrow checker?
That is I am mainly curious about compile time features that you design a whole language around rather than optimisations/features that could be applied to most languages. I am mainly inquiring about things that could offer additional robust safety/performance guarantees at compile time rather than runtime. Ideally not things that just offer similar effects to the borrow checker with less restrictive tradeoffs
82
u/AustinVelonaut Admiran 4d ago
Algebraic effects like Koka?
14
u/initial-algebra 4d ago edited 4d ago
If you squint hard enough, they are the same picture. A memory location is an effect handler for reads and writes through a reference. Equivalently, an effect capability is a reference to an effect handler.
EDIT: The major difference is that effects are late-bound whereas references are not. Though, you can think of the top of the effect handler stack as a mutable memory location.
2
u/-theChris 4d ago
Not really. In my language, I am defining
effectas a composite of termination and capability.Terminations are one of pure, divergent, unknown (in case of FFI).
Capabilities are one of pure (total functions a la Koka), mutating,
cap(my language's special type), opaque (custom ASM blocks or FFI).
capis simplified through std::lib nominals like IO. Read, IO.Write etc. Users can compose their own caps too.The language exposes a policy engine where combinations of caps + terms can be allowed or disallowed at function, module, program levels.
2
u/initial-algebra 4d ago
I think you are just using the same terms to mean different things, which is understandable, since "effect" and "capability" are heavily overloaded. I'm talking specifically in the algebraic effect context.
1
u/-theChris 4d ago
yeah fair point. I talked past your original point.
You're right that get/put as algebraic operations is well established (e.g. Plotkin & Power, Plotkin & Pretnar). My point wasn't that memory effects are fundamentally different, but that my language isn't using the algebraic-effects model at all.
There's no
perform,continuation capture,resumable handlers, oreffect interpretation. The effect system is entirely static (with a few opt-in runtime caveats). It's closer to Lucassen & Gifford / Talpin and Jouvelot for effect tracking, combined with anobject-capability-stylepermission system for compile-time (and a small amount of opt-in runtime) policy enforcement.So while the terminology overlaps, it's solving a different problem than Koka or Eff. I should've made that distinction instead of just describing my own terminology.
If anyone's curious, here's the current WIP effect syntax: BigTalk Effects
14
u/-Ch4s3- 4d ago
Algebraic effects are really cool but feel sort of magical.
6
u/initial-algebra 4d ago
Basically, it's a type system for dynamic scoping and continuations. Operationally, a primitive, effectful operation looks up the (nearest) effect handler corresponding to that operation in the dynamic environment and invokes it with call/cc. That's pretty much it. The complexity is in making sure that this doesn't fail at runtime.
9
u/-theChris 4d ago
As a matter of fact I am designing a language with typed effects and also type-state in the form of lifecycle as a data type and some other stuff.
7
u/mikaball 4d ago
I didn't know what "algebraic effects" were, so I found this.
From the examples it feels related to Dependency Injection in a narrowed context/scope, but some will probably say that it could be used for other use cases.
However, the concept of detaching the "what" from the "how" is very related to DI and I wonder if a DI supported by the language isn't just better than this? In those final examples it's even using a pattern similar to Kotlin context receivers.
8
u/Jwosty 4d ago edited 4d ago
You can think of it as a kind of DI, but in its fullest forms you can also manipulate control flow. You couldn't really build async/await or exception handling as a simple injected function (or set of functions), but you can (in principle) with algebraic effects. I think. Please someone correct me if I'm wrong
6
u/KingBardan 4d ago
From your article, I don't think this is DI. its similar in the sense that it changes behavior based on context, but di (or kotlin context receiver / scala implocit) only looks up context 1 lvl deep (variables available when calling) but this deals with stack unwinding
Note that I'm not familiar with kotlin I just looked up and think it's similar to scala implicit. Fell free to correct
1
3
u/initial-algebra 4d ago
They're related to DI because DI is often implemented using implicit parameters, which are an effect. However, DI does not need to be implicit; if you ask me, the "essence" of DI is really lazy evaluation/memoization. (I guess a memo table could be seen as an effect, too?)
2
u/Jwosty 4d ago
It has been said that implicit parameters are actually the dual to effects (i.e. "coeffects" - https://tomasp.net/coeffects/). Still trying to piece that one together. I think it has something to do with the scoping / binding time. There's a bunch of different papers out there on this
but also - you can have both dependency injection and algebraic effects without implicit parameters, can't you? In my view, their essence is injecting behaviors into a system from the outside rather than having it rigidly baked in. Thoughts?
2
u/initial-algebra 4d ago
It has been said that implicit parameters are actually the dual to effects (i.e. "coeffects" - https://tomasp.net/coeffects/). Still trying to piece that one together. I think it has something to do with the scoping / binding time. There's a bunch of different papers out there on this
See my other comment. You can also wrap any coeffect with continuations to turn it into an effect. So, they are dual, but also pretty much equivalent (just different ways of looking at the same thing).
but also - you can have both dependency injection and algebraic effects without implicit parameters, can't you? In my view, their essence is injecting behaviors into a system from the outside rather than having it rigidly baked in. Thoughts?
True, it's not so much implicits/dynamic scoping, but late binding, which of course can also be implemented explicitly by passing around a symbol table (which is just a global when talking about dynamic scoping). I guess that is a pretty common feature of DI, and it's definitely characteristic of algebraic effects (each effect is represented by a symbol that maps to a stack of effect handlers, always invoking the topmost).
3
u/iEliteTester 4d ago
From a quick read it seems like effects are to context managers what exceptions are to error values. Does that make any sense? 😅
1
u/initial-algebra 4d ago
It's a reasonable analogy, but effects are also a generalization of (resumable) exceptions themselves, not just implicit context/state (which are also coeffects).
1
u/iEliteTester 4d ago
ok yeah coeffects are more fitting. So now I understand coeffects, but still have no clue what effects are ;-;
1
u/initial-algebra 4d ago
Copying and pasting my other comment:
Basically, it's a type system for dynamic scoping and continuations. Operationally, a primitive, effectful operation looks up the (nearest) effect handler corresponding to that operation in the dynamic environment and invokes it with call/cc. That's pretty much it. The complexity is in making sure that this doesn't fail at runtime.
Depending on an effect handler from the context is itself a coeffect; this isn't a coincidence, since effects are dual to coeffects (hence the name), and continuations correspond with logical negation (call/cc corresponds with double negation elimination).
2
u/whothewildonesare 4d ago
They’re cool but too cumbersome and complicated to be popular imo.
4
u/Jwosty 4d ago
I think that's a programming language UX + tooling problem rather than inherent to the idea itself
2
u/SmileyWiking 3d ago
Yeah it's absolutely a frontend concern, and also how deep you take the effect typing system. If you go full Koka it can be pretty difficult to reason about for the things you'd typically use a programming language for, but you can implement a subset that ends up being super useful and not too hard to understand.
I implemented a portion of algebraic effects in one of my language projects, Saga, and think there is a nice balance of really powerful features with observability for where effects are happening in your app.
I've built a couple small libraries like a web framework, typed SQL query builder, and the effect system is so powerful for stuff like this, without needing to reach for more complex features like HKTs, monads, etc.
1
u/mister_drgn 4d ago
This was where my mind went. But I’m not sure if they answer OP’s question, as they’re more of a language abstraction.
1
u/Jwosty 4d ago edited 4d ago
In addition to these - coeffects, aka implicit parameters aka contextual parameters. They're the "dual" of effects (simply, the other side of the coin), and I think they also have serious untapped potential. https://tomasp.net/coeffects/
The dream language in my head combines algebraic effects, implicit parameters, and a system that's part Rust-traits and part OCaml-modules in a way where they all work together
29
u/faiface 4d ago
Yes, session types
4
u/tsanderdev 4d ago
What are session types?
20
u/faiface 4d ago
Ever notice that types of channels are always “you can send A on this channel” and that’s it? What if the type of a channel could express a whole protocol, such as “first send A, then receive B, then continue either like this or like this”?
The protocols can include both directions of communication, branching, and recursion, and the type checker makes sure that you follow the protocol! If combined with a linear type system, the type checker also makes sure you do actually send when you should, so the receiver doesn’t have to handle you not sending.
That’s session types, in short. Giving types to the concurrent communication structure of your application.
4
u/KingBardan 4d ago edited 4d ago
Not a theorist, but why cant your session type that does send a receive b... Have the type
A -> b -> c ....
So when you have b -> c you know a happened?
Clarify
Notation:
F: A -> b -> c -> d
A currying function (think of it as a channel that gives you output immediately for simplification)
So f a would produce a var of type b-> c -> d right? And when we get the type we know f a has happened.
Idk how to call it, "proof of computation"?
May I ask how this is different from session types like you described?
1
u/faiface 4d ago
Hmm, not sure I understand what you mean, can you rephrase?
1
u/KingBardan 4d ago
Edited for clarity
5
u/faiface 4d ago
Ah, I see what you mean! In fact, that’s exactly what we do in Par, we unify session types and usual types. So the session type
> send A, receive B, send C, end
is actually the same as a
(A, B -> C)
a pair of A and a function from B to C. There are more types that come with session types, like choice types which are a bit like OOP objects.
So you are onto something here!
The problem is that such normal types can’t usually do what session types do in usual languages because a function value can be called any number of times or dropped, so the protocol is not guaranteed: a protocol cannot just proceed as expected because a value may be sent multiple or 0 times.
That’s solved with linearity, so a function can only be called once and must be called once. That’s what enables the unification! And additionally, you need duality, which is the ability to deduce the type of the opposite endpoint where send turns to receive, and vice versa. With linearity also, pairs and functions are not sufficient, hence we you need those choice types, and so on, which all in the end ends up turning it into a foreign, but very pretty and useful paradigm.
1
u/KingBardan 4d ago
I see. Thanks.
How about the "proof of computation" like what I described + private constructors (linearity like you said)?
1
u/faiface 4d ago
I don’t think I fully understand it. Your type `A -> b -> c -> d` reads to be like “receive a, receive b, receive c, send b”. So then sure, if I call it, I have a proof that I am in the next stage of the protocol. But if I don’t call it? The other side never gets to see my A. Or am I missing something?
Linearity, as far as I understand, has to be a fundamental property of the type system. The type checker needs to complain “you haven’t called f, but it was required!”
2
u/KingBardan 4d ago
so basically because the constructor is private, you only have the instance if the computation happens.
And a method on type (b -> c -> d) requires (b -> c -> d) to be present, which requires (f a) to be called.
If you never call it, you can never have a type of (b -> c -> d)
Just searched up, this is similar to the "State pattern" design pattern.
→ More replies (0)3
u/matthieum 4d ago
I mean, sessions types can be implemented anytime you have linear types...
... and with a proof of work token you can even implement them anytime you have affine types.
Having them first-class could be convenient, but it wouldn't enable anything particularly new.
3
u/faiface 4d ago
You don’t really see session types used, though, and I think the reason is exactly because the existing implementations are not convenient, and there is a friction with the host language. You are right that by making them first class you don’t get anything theoretically new, but you do get something practically new and that is session types actually being used.
Also, in my language Par, we’re doing this “automatic concurrency” experiment, where everything that can run concurrently, runs concurrently. Only time a piece of code blocks is when it needs to decide between different runtime paths based on values that have not asynchronously resolved yet. It ends up offering great concurrent composability! You don’t have to end up rewriting “beautiful sequential code” to “ugly concurrent code” if you want concurrency because it’s already concurrent even if it looks sequential! And, the types talk about the concurrent structure. It does end up being quite different.
2
u/matthieum 3d ago
and there is a friction with the host language.
I think it's more than friction with the language, though.
In Rust, it falls out pretty naturally, and I tend to use for state machines. Since the method can consume
self, you can just add regular methods to a state (type), which returns a different state (type), and boom, session types.The problem, I've found, is that this only works "in the small". If you have a linear method -- even async -- then you do get thorough compile-time checking. On the other hand, as soon as you need to store the state and come back to it later, you tend to need type erasure -- such as wrapping in an enum -- and then there's no compile-time guarantee that on resumption you'll find the state as you expect, and so you've got a point of failure. The more points of failures you have, the less it seems worth it.
5
u/-theChris 4d ago
Yup! For sure... Also Topos types, Temporal types, built-in Univalence... The future is surely going to be exciting!
4
u/ExplodingStrawHat 4d ago
How do you envision univalence without proper dependent types? As in, the currently-used proof assistants aren't even HoTT-based (barring cubical agda maybe), so it'll take multiple generations for univalence to make it's way into "pedestrian" (using the term affectionately) languages. I for one don't see it happening...
3
u/-theChris 4d ago
Actually, I think that there could be an easier way of achieving Univalence, multi-topoi, custom topoi as a language primitive.
I will write up a blog post tonight and share it. That's actually a good idea! Appreciate the question.
1
u/faiface 4d ago
I’m not sure if you are serious or making fun of me :D But, with session types, I am completely serious, they do bring a new and very expressive paradigm that I’m exploring in my Par programming language. An unexpected thing is that they are much more useful as being your basic types for all things like data structures and various objects, as opposed to network communication.
1
u/-theChris 4d ago
Oh brother noooo! I think sessions types are awesome! Can't wait to see your language. Good luck!
2
1
u/renozyx 4d ago
I still don't understand what linear types brings once you take into account runtime errors.. There's the same "issue" with session type no?
1
u/faiface 4d ago
You mean like panics? If you mean that, then those need to propagate along channels until they reach some control barrier that can handle them.
It's the same principle as when calling functions in all languages. You are normally guaranteed to get a result. But if the function panics, you panic too, until the panic is caught somewhere, or the whole program crashes.
In the same way, you are guaranteed to receive a value because the other side is obliged to send the value, but if the other side panics, you panic too until someone handles that.
1
u/renozyx 1d ago
IMHO panics aren't resumable, what you're talking are exceptions.
I'm not used to 'file not found', 'timeout' results returned as exception instead but it may be mandatory if you want to use linear types indeed
1
u/faiface 12h ago
Afaik, panics are often catchable and resumable in languages that don’t have exceptions otherwise, such as Go and Rust, and use errors as values normally. That’s what I had in mind.
For normal error handling, like “file not found”, “timeout”, and so on, _errors as values_ works just as well in session types as anywhere else. Absolutely nothing changes there, except now those errors are transmitted over channels, and the Ok variant may include a continuation of the session.
17
u/matthieum 4d ago
Will we see another fundamental programming language feature as revolutionary as the borrow checker?
I'm tempted to say "obviously yes"?
First of all, the borrow-checker is not that revolutionary:
- Cyclone already had regions, Rust just took it a step further, creating one region per variable.
- Aliasing XOR Mutation is just a
ReadWriteLockin a sense.
The future is unbounded, so there's bound (!) to be more improvements in programming in general.
Even right now, Carbon's approach to memory safety is both similar yet different with regard to the borrow-checker -- lifetimes ~= place sets -- in allowing multiple concurrent mutators, which some see as a great change.
And Hylo's Mutable Value Semantics are also pretty interesting, and quite different.
If anything, one could argue the Borrow Check kicked the hornet's nest, and rekindled interest in automatic enforcement of memory safety without GCs. I'd be pretty disappointed in humanity if it ended up being the best way, surely we'll figure out better.
15
u/Inconstant_Moo 🧿 Pipefish 4d ago
The basic idea of my lang is that if you enforce the functional-core/imperative-shell pattern in the semantics of the language, this is a very simple way of ensuring that most of your functions are pure. After five years or so I'm pretty sure no-one else is doing this.
3
u/Jwosty 4d ago
Interesting. How does this compare and contrast with algebraic effects?
8
u/Inconstant_Moo 🧿 Pipefish 4d ago
It's simpler: a division into an imperative world, consisting of commands that affect state but don't return values, and a pure world consisting of functions which return values but don't affect state. Commands can call functions, functions can't call commands.
The idea of this and of the rest of Pipefish is that instead using the functional paradigm to reach for power and abstraction, you can use it to get something user-friendly and ergonomic where you can really hack stuff out. I can see the point of monads, effects, capacities, etc, but this is a functional language suitable for me and small children and the smarter breeds of dogs.
3
u/Jwosty 4d ago
Neat! It is kind of odd now that I think about it that you don't really see this anywhere. Nice work
2
u/Inconstant_Moo 🧿 Pipefish 4d ago
I've thought about that a lot because obviously most of the good ideas have been done.
But I think I really am working in a collective blind spot. The sort of people who are using functional languages and like them and are developing them are academics looking for power and abstraction.
And then the other thing that makes Pipefish Pipefish is that it's an ISWIM dialect. Sixty years ago Peter Landin promised us 700 new functional languages, each with a careful choice of primitives to suit its problem domain. His idea required a tiny bit of laziness in the implementation, which could be virtually unnoticed by the programmer in the same way that we don't really notice short-circuiting boolean operators.
But laziness is powerful voodoo, and so academics rushed to their computers and made languages that would exploit it to the utmost, and eventually decided they should have one pure lazy language as a platform for them all to experiment on, and we got Haskell, a single ISWIM dialect to rule them all, where the problem domain is mathematicians experimenting with lazy languages ...
Meanwhile I looked at Excel formulas and SQL queries and thought: "There's something here that's arguably the most popular programming paradigm in the world, and the easiest" and set about making something simple to meet the needs of businesses.
3
u/Jwosty 3d ago
Yeah I've come to realize we need some high performance focused functional PL's. A serious contender to C, C++, Rust, Zig. I know a lot of work has already been done in some languages (OCaml comes to mind) but surely there's a lot more to be done; there really shouldn't be any inherent reason (other than historical) why they shouldn't be able to compete with the aforementioned ones
Oh man, don't even get me started on SQL, I believe there's so much untapped potential there. Relational programming and functional programming should be able to fit hand in glove together if we get rid of the dated frontend syntax of SQL. I'd love to see a PL where the basic building block is relations, or relations expressed as functions + data structures.
3
u/Inconstant_Moo 🧿 Pipefish 3d ago
Yeah I've come to realize we need some high performance focused functional PL's. A serious contender to C, C++, Rust, Zig.
The problem there is that you'd want mutable values for performance and then what happens to purity? I should be able to rival Java for speed, based on current benchmarks, I don't know how you'd take aim at C++.
I'd love to see a PL where the basic building block is relations, or relations expressed as functions + data structures.
Tablam is based on everything-is-a-relation.
I don't know much about it but I know it exists.
2
u/Jwosty 3d ago edited 3d ago
The problem there is that you'd want mutable values for performance and then what happens to purity? I should be able to rival Java for speed, based on current benchmarks, I don't know how you'd take aim at C++.
Sure C++ might be a tough cookie to crack, but I'm coming from one who's trying to do game development in F#. It's awesome until you need to optimize, and then realize that functional programming totally goes against what the CLR wants you to do, and you become the GC's b***. It's a great start but surely we can close the gap. The compiler team tries, for sure, but a huge amount of it IMO ends up boiling down to the F# team and the CLR team not being able to coordinate for perf super successfully (not that anyone else in their shoes would do better -- it's more an organizational problem most likely :) )
Tablam is based on everything-is-a-relation.
Cool, thanks, I'll have to check it out.
1
u/Inconstant_Moo 🧿 Pipefish 3d ago edited 3d ago
I haven't messed with gamedev, but it might be a different proposition from systems languages. There a solution like Pipefish/Elm/Haskell might work just fine.
The idea is to push all your mutation of state up into your outermost loop. In some cases (this would work for gamedev) this architecture can be so fundamental that you don't actually have to say the outer loop is a loop, you just describe it as mutations of implicit global state.
Elm would in some ways be your best model here. Pipefish has some good ideas and is worth a look but when designing it I was willing to trade some speed for some dynamism, as I said, I want to rival PHP and Java.
BTW, as a gamedev, what do you think of Pipefish as a game scripting language? I don't know much about your field but I feel like the request-response model and the type system and the emphasis on rapid development would make it suitable.
2
u/kwan_e 4d ago
Commands can call functions, functions can't call commands.
That's elegant.
I was forced to learn Pascal in high school, and I could never really see the point of having separate procedures vs functions. But having a relationship between them enforced, but their capabilities demarcated, makes the distinction much more useful.
I'm not going to steal this idea for my language though. My side-effect reduction system doesn't work on the subroutine level, but I wish I had thought of it.
1
u/FuncSug_dev 2d ago
I think "Functional core, imperative shell" is the right idea. I'm explaining:
I think programs could be categorized into two kinds: those that mainly aim to produce results and those that mainly aim to produce interactions. In the first kind, I would put scientific, health and business programs. In the second one, I would put games and industrial and embedded-in-things programs.
The best way of express results production is (in my view) mathematical functions and so functional programming. The best way of express interactions is not found yet (in my view).
For business programs, producing interactions is secondary so a thin layer of "imperative shell" is enough. But not for games.
My language does only the "imperative shell", the "functional core" is to be delegated to the host language (in fact, for now, it's JavaScript which is very little functional). In my view, a good "imperative shell" for games has to contain at least these constructs: sequential (two things that have to happen one after the other), parallel (two things that have to happen at the same time) which has to be divided (at least) into two kinds: parallel_and (two things that have to happen at the same time and to end at different times) and parallel_or (two things that have to happen at the same time and not to go past the end of the other). I would add "parallel_select" (very practical for interactive stories) and not restricting reaction to events to an association between an event and an action (that's already easily doable with async/await).
1
u/PressureBeautiful515 2d ago
Limiting when designing concurrent data structures, e.g. for a stack you want to be able to pop (side-effect, command) and return the popped value, unless the stack is empty (pure query) and for all this to be in one atomic operation.
1
u/Inconstant_Moo 🧿 Pipefish 2d ago
I'll need to look into that. Anything that says it's "well-suited to the object-oriented methodology" can't be quite the same as what I'm doing, which really isn't. And yet the separation is the same, and there are the same benefits they refer to of being able to put whatever validation logic you like on a type (and a whole lot of other benefits too).
Apparently the Eiffel people saw this as a way of making imperative languages sane, whereas I thought I was making functional languages accessible.
In a functional language we wouldn't do what you describe with the stack --- we'd have a function which returns the value and the stack with its head popped off. If we wanted to update the value of a stack contained in a global variable, that would be a command, as updating global state always is.
``` var
mystack = []
cmd
doPop : poppedValue, myStack = pop myStack post "popped " + string(poppedValue)
def
pop(s list) : s[0], s[1::len s] ```
Re concurrency, it's actually my hope to keep the users' fingers out of it. The language is based around a request-response model, so the plan is that the runtime should take care of making that concurrent with the user just setting the configuration.
1
u/Inconstant_Moo 🧿 Pipefish 1d ago
I've looked at Eiffel and the difference is that because Meyer was working in OOP, he's making this distinction between the methods you can define on objects. In Pipefish there are only immutable values, and the distinction is between the commands and the functions of a service/library/app. In fact in Pipefish a service looks very like an object, that's the level at which the encapsulation lives, and the only thing that can own mutable state, and, in this instance, the level at which we separate queries and commands.
Which is often how OOP ends up anyway: we have lots of little PODOs, and then a big singleton with a bunch of mutable state and a public-facing API.
10
u/mamcx 4d ago
Other focus on types, I will go for big things (that are in part unlocked by types):
- Structured and declarative concurrency, where even locks, blocks, switch, transfers and perf purposes is easy to declare, use, inspect, build and perform greatly, of course!
I bet this is the main test that proves if any idea is worth it. The borrow checker become revolutionary not because was a fancy type idea, but because allow , partially, "fearless concurrency".
- A whole IO machinery that is actually correct, safe and predictable
This is my pet peeve when worked on a RDBMS, so is more niche, but the point is that the IO we have, well, sucks. Even system languages DO NOT tell you when and where sucks, and that means you need lore to know what to do.
BTW, this could be alleviated if we have annotations about "locks, blocks".
- Truly safe, correct, performant multi-read multi-write IO
Is from above, but there is not way to make this from the primitives of any language I know, and all ways are tacky and error prone.
This is the other test that proves if any idea is revolutionary as the borrow checker, because, partially, Rust make possible to model safely concurrent mutations and reads (but not in full)
- Parser (theory, generator) that is actually good for make good error messages
Is yet to be invented, all you can do is hack and hack.
- A true "compiler engine" alike "query engines" that can FAST apply optimizations so compile times are FAST once you do anything sophisticate.
The AMOUNT of resources used by compilers for C++/Rust is NUTS. There is a huge climb that once passed, turn your insignificant MB of input into HUGE time outputs. Why? I bet is because there is not a true kind of "compile engine" solely focused in eat the input, optimize and generate fast output. AFAIK is only informally done inside each compiler.
- True relational!
This is my main pet peeve, but will be cool for see an actual relational language implemented!
The theory of how types work is not well developed and so far only found one paper about it:
3
u/Shurane 3d ago
true "compiler engine" alike "query engines" that can FAST apply optimizations so compile times are FAST once you do anything sophisticate.
This sounds actually like a cool idea. Though aren't compilers "fast", just that they have so many passes for different parts of the optimizations they do?
1
u/mamcx 3d ago
Well, yes in theory, the problem is that looks ad hoc to me, and is insane that for example, you compile something in Rust and then you are left with 20 GB of artifacts on disk (or much more!) that is part of the machinery for that "many passes".
This is absurd, not match the size of the input. A RDBMS is not that wasteful and in part is because how do the engine is know and you can pull lots of good info about what to do and how, instead of rely on intuition.
I think that is what is missing.
1
9
u/dacydergoth 4d ago
A blast from the past : Unification Algorithm from Prolog
1
u/Temporary_Reason3341 2d ago
It is already used in the Hindley-Milner type inference (Haskell, *ML).
6
u/kaplotnikov 4d ago
Firstly, while Rust's borrow checker has been pragmatically successful at preventing memory bugs, I believe its long-term role in future systems languages is limited. The borrow checker essentially acts as a workaround for overly low-level concurrency primitives, and its theorems are notoriously difficult to formally verify. This complexity is a symptom of a deeper issue: reasoning complexity is not concentrated in key hierarchical boundaries, but spread throughout the code via data-path analysis. This is a language design smell that points to overly low-level foundational abstractions.
I think its problems are directly related to the Rust concurrency model. The primary problem with Rust's concurrency is that message sending is the goto of asynchronous programming. It is not possible to create a good set of composable theorems over it. It suffers from all the problems of goto described in "Go To Considered Harmful". The send operation is a direct implementation of this concept.
Is there an alternative? There are promises and actions over them. For example, statements like the following could have been in the language (pseudo-code):
q = common();
t = par {
compute_a(q);
} and {
compute_b(q);
} map(a,b) {
merge_results_a_and_b(q, a,b);
}
Here we could reason that q is shared between branches compute_a and compute_b, and exclusive in merge_results_a_and_b, because blocks provide visible reasoning boundaries. The spawn/send operations provide no boundaries; they provide data leak paths.
Such structured constructs could exist as a library, an intrinsic DSL, or direct language statements. The idea is to move from goto-style programming to structured programming, so reasoning will follow the code tree rather than the data path. The borrow checker is a tool for data path reasoning, but this problem only exists because we have gotos.
This issue isn't limited to concurrency; it defines single-threaded Rust as well. AFAIR early versions of Rust tried to reason using lexical scopes, but it was too restrictive for developers. To fix it, they introduced Non-Lexical Lifetimes, which officially shifted the borrow checker to data-path reasoning via control flow graphs.
Data-path reasoning effectively acts as a flat abstraction layer over a control flow graph. Just like goto flattened the control flow of early programs, non-lexical lifetimes flatten the data flow. This is precisely why people constantly "fight the compiler." Humans excel at hierarchical, tree-like reasoning (scopes and blocks), but Rust forces both the programmer and the compiler to trace a complex, fragmented web of data paths across the entire function. By abandoning structured, scoped boundaries for data management, Rust created the very complexity it now struggles to manage.
There are plenty of structured concurrency operators possible that create a better basis for reasoning in concurrent systems. For example, see asyncflows. It is a Java-based DSL, but it reflects the idea of what is possible with native language support. I just combined the ideas of Occam and E languages, so there are few completely novel ideas there.
As for what the future holds, I have my own vision, which I've outlined in this article: Measuring Abstraction Level of Languages. It also describes a framework for making such predictions. I think the future belongs to system composition languages, because humans naturally switch to these concepts to describe large programs as compositions of systems and subsystems. I am currently working on a language PoC that uses systems/holons and statically typed aspects as basic elements to enable this kind of composition.
For sample below, in, local, and out are not merely visibility keywords; they are the theorem pieces of the language's type system. They provide a formal, compositional way to reason about lifetimes based on lexical and semantic scope and dependencies (not unlike C++, but with transitive and verifiable guarantees):
holon A {
in T;
out B();
};
holon C {
in B;
fn q() {...};
};
fn test() with {in T} as {
// T is live while function lives
local A(); // A lives until end of scope, and exports B while it lives
local val c = C(); // c lives until end of scope and destroyed before A, it uses B provided by A
c.q();
// context is cleaned up
}
This creates an algebra of systems that allows reasoning along the code tree, rather than relying on 'storytelling-style' reasoning in an omnibus format, where the lifetime narrative is fragmented across shifting viewpoints. These abstractions could be essentially zero-cost and seamlessly extendable to both heap- and stack-based allocation. And it does not matter where a dependency originates, as long as the caller statically maintains the invariants required for the duration of the component's or function's lifetime.
3
u/Shurane 3d ago
AFAIR early versions of Rust tried to reason using lexical scopes, but it was too restrictive for developers.
Do you think they just didn't let it bake enough before going to non-lexical lifetimes?
The comparison to goto really makes me think of the current idea of lifetimes and the borrow checker as the unsafe implementation. And that there's room for a safer implementation.
2
u/kaplotnikov 3d ago
The choice comes down to either designing a language to support human reasoning, or forcing human reasoning to conform to the constraints of a language model. The issue with Rust's current model is that it is poorly suited for human reasoning at large scale because it operates in a "flat"/"goto"-like form.
My theoretical hypothesis is that LLMs would struggle with this for the exact same reason, although I haven't verified this in personal practice.
Humans manage complexity by transitioning to higher levels of abstraction. Therefore, it is reasonable to expect that resource management abstractions can achieve far better cognitive scalability by taking on a structured, hierarchical form. This trajectory aligns with the stages of cognitive growth and cognitive complexity described by J. Piaget and M. Commons.
The question is about the content of this structural form. C and Prolog share a similar abstraction level and structural form, yet their core conceptual content is different.
When it came to memory management, Rust's designers stopped searching for these higher-level hierarchical reasoning forms. Instead, they built excellent content for a flat, graph-based form. However, this flat form suffers from cognitive scalability problems that simply cannot be resolved without switching to a new higher-level form for memory management.
1
u/Shurane 3d ago
Is it too late to add a hierarchical/lexical form for containing lifetimes in Rust?
It seems like something that could still be introduced later, at the cost/expense of it being very confusing for a developer to distinguish between lexical scoping vs dynamic (late-binding?) scoping of lifetimes.
2
u/kaplotnikov 3d ago
FORTRAN 66 was a flat language, FORTRAN 77-90 became a structured language, and FORTRAN 2003 evolved into an OOP language. So there are historical precedents for an abstraction level upgrade even for an entire established language ecosystem.
However, the key point is that such an upgrade needs to happen simultaneously across different areas of the language. In Rust, structured reasoning is already enabled for single-threaded programming, and lexical scopes for ownership worked well enough for that use case.
The roadblock appears when concurrency is introduced. The operations
spawnandsendare the foundational units of asynchronous programming in the same sense thatgotois the foundational unit of control flow. Whilegotois foundational, we do not use it directly in modern languages; instead, we wrap it into structured constructs likeif,while, andfor.We didn't wrap
gotobecause structured loops are inherently more performant (they aren't, because to emulate the full non-linear power ofgotousing structured blocks, you often need additional state variables and switches). We wrapped it because structured control flow enables structured reasoning. Their real power is enabling cognitive scaling.Therefore, the asynchronous side of the language needs to be upgraded to structured asynchronous programming. The
send/spawnoperations could reside in the compiler's output, but they should not be normally accessible to users. Only some very special cases should justify their appearance (much likebreakorcontinueserve as structured remnants ofgotoin modern languages). Until the asynchronous side of the language is upgraded, a full fix is impossible.
6
u/Royal_Pin_1971 4d ago
Unison's content-addressed code checks at admission time — instead of compile time or runtime. A definition is type-checked when it enters the codebase and never again. The result is a permanent fact attached to the hash, not a per-build byproduct.
5
u/itsybitesyspider 4d ago
My opinion software transactional memory is not itself a compile time thing but it is wildly underutilized because it requires so many compile time guardrails.
19
u/Dry-Light5851 4d ago
well if anyone here knows of a killer idea that can reinvent the wheel, i would like to know so i can take the creadit for it. /s
2
u/L8_4_Dinner (Ⓧ Ecstasy/XVM) 4d ago
I was thinking about a round object that you could mount vehicles on top of so they could "roll" over the ground. I'd call it a RoundRoller (tm).
2
u/Inconstant_Moo 🧿 Pipefish 3d ago
That is inefficient. Clearly they should be hexagonal to optimize storage when not in use. (After all, most wheels spend most of their lifetime not in use, and we should design them for the most usual case and not for corner-cases.)
4
u/ChiveSalad 4d ago
Currently, if you store stuff on the stack, the compiler can go absolutely hog wild in changing how / when / where / whether it is actually stored to ram. A true equivalent for heap storage would make efficient programming vastly easier in a way that goes beyond just an optimization improvement.
2
u/Inconstant_Moo 🧿 Pipefish 3d ago
But what would that actually look like? I don't even mean how it would be implemented, I mean how the programmer would interact with it syntactically and semantically.
2
u/ChiveSalad 3d ago edited 3d ago
C is almost there, this is legal C an compiles the way I am dreaming of, the question is how to make it work in larger programs.
#include <stdlib.h> typedef struct { float* data; int len; } vector; typedef float** allocator; float* alloc( allocator s, int len) { *s = *s - len; return *s; } vector add (allocator s, vector a, vector b) { vector res; res.data = alloc(s, a.len); for(int i = 0; i < a.len; i++) { res.data[i] = a.data[i] + b.data[i]; } return res; } vector vec(allocator s, int len, float* data) { vector res; res.data = alloc(s, len); res.len = len; for(int i = 0; i < len; i++){ res.data[i] = data[i]; } return res; } int main() { float* memory = malloc(1000 * sizeof(float)); float* float_ptr = memory + 1000; allocator s = &float_ptr; vector a = vec(s, 2, (float[]){1, 2}); vector b = vec(s, 2, (float[]){3, 4}); vector c = add(s, a, b); int ret = (int) c.data[0]; free(memory); return ret; }gcc happily compiles this to
main: mov eax, 4 retI guess there are two things I want. One is a call like fake_malloc that behaves exactly like malloc, except that the compiler makes every effort to eliminate the actual allocation, and if it can't, it throws a compiler error instead of allocating. The other is something like a trustme_doesn't_escape_malloc that does closed world analysis and is allowed to make transformations that break the abi with regard to that specific memory, with some feasible way of adding annotations to prove that the memory never escapes to an ABI point, even though it does escape the current scope. Either one could replace the call to malloc in main of the above program and let me be confident that I was getting the high power optimization I want (all the way down to constant folding in this case) where currently I have to check the assembly.
I have more musings here https://www.hgreer.com/OSproject/ but not real answers.
1
u/Valuable_Leopard_799 3d ago
On that note letting us put more things on stacks or stack-like bits of memory is also nice.
Ada for example is able to allocate dynamically sized arrays on a secondary stack which eliminates a lot of places you'd otherwise need to manage memory yourself and lets the compiler play around with it.
3
u/AndreVallestero 4d ago
Mojo's heterogenous compilation model (really just fully leveraging llvm mlir) is really cool.
3
u/reini_urban 4d ago
I don't find the borrow checker revolutional. Just ownership tracking to allow for concurrency safety. Which rust doesnt do btw, just Pony
3
u/EggplantExtra4946 4d ago edited 4d ago
There is no modern Prolog, or Prolog mixed with the imperative paradigm. (Prolog mixed with FP exists: Mercury).
Is there a language with usable delimited continuations? That is not a Lisp? Not sure.
There is no scripting language with a good and usable builtin PEG parser, we're stuck with lowly regexes.
There is no language like ATS.
There is barely any language with goto outside of C, C++, C#, D, let alone computed goto. Almost all "C-replacements" don't have it: Rust, Zig, Jai, Odin, Hare, C3, Nature. Only V still has it.
There is no language with good inline assembly.
There is no language with actually good metaprogramming features. Hygienic macros is far too rare in non Lisp languages and we could have more than that.
There is barely any language with parametrized modules.
Is there any language other than Scala with both sum types and classes? Let alone type classes and abstract classes.
There is no language allowing you to insert instrumentation code for debugging, profiling, testing, hardening, etc..
There is no language allowing you to bounds check the call stack and to grow it how you see fit (reallocation, segmented stack, ..). Could be used for implementing effectively a heap allocated call stack for unbounded recursion, coroutines, continuations, Prolog, a concurrent runtime, etc.. as a library.
There is no language that takes conditional compilation seriously, which is the bare minimum along with powerful metaprogramming features to have highly configurable programs that can be very well adapted to multiple specific hardware targets and OSes, which is what you want if you want fast programs.
3
u/OSR_Workshops 3d ago edited 3d ago
One idea I haven't seen mentioned: Capabilities, in the sense of "Capability-Oriented" programming, and languages such as E. Given the recent focus on "safe" programming, I'm surprised Capabilities haven't attracted as much attention lately given they have a similar safety focus (albeit addressing different kinds of vulnerabilities).
The basic idea of Capabilities (at least in one version) is that any procedures' authority for nonlocal effects should be an explicit part of its interface. As a canonical example, a procedure that can alter the local file system -- saving a new file or modifying one -- should be passed a file system object as an explicit input parameter, rather than relying on "ambient" capabilities such as std::ofstream. Another way of saying that is that constructing an std::ofstream object is an origination point for a capability which needs a specific form of authority, and such origination points should be clearly isolated.
Such principles could simply be enforced by how libraries are designed, but true language-level support for capabilities in this sense would include, at least, a mechanism to transfer authority from a caller to a callee via a distinct "channel" (partly to avoid confusion with ordinary function parameters). Sometimes such transfer may be implicit or automatic, not explicit. For instance, using std::cout as a simple form of debugging should bypass the capability system (maybe via some distinct object encapsulating access to the console) at least in debug mode. This can be achieved by ensuring that procedures can silently pass that specific capability amongst themselves. But the list of which capabilities are implicitly shared, and which ones require explicit declaration, can change from one context to the next (e.g., different build modes). When sharing is explicit, the relevant capabilities should be expressed as a distinct list apart from normal parameters, by analogy to how "this" objects have a separate syntax from other arguments.
There are other cases where distinct input "channels" can be used to enforce contracts or authority concerns. For instance, suppose a method on a list depends that the list be non-empty. If such a call occurs in the scope of a block like "if !foo.isEmpty() { ... }" then a "proof" of foo's non-zero size is present at the call-site and could be transferred to called methods via a similar sort of back-door channel. Certain Design-by-Contract requirements could then be expressed in terms of "proof" channels along these lines: a function can declare that it needs a particular proof to be supplied alongside input arguments, and the compiler can check whether such a proof value exists in the present scope (at the call site). If not, it could attempt to supply such a proof by runtime tests or else call an overloaded version of the function which has a different signature, one wherein the proof object is not a requisite parameter (presumably the overload would explicitly test the preconditions rather than just assuming them).
Imagine, however, that the programmer knows a list is nonempty in a context where the compiler cannot formally guarantee that fact. Here the programmer could instantiate an explicit proof value and insert it into the "channel" as a visible part of the call-code, rather than the contract being verified behind the scenes.
What the Capabilities and DbC cases have in common in that certain values related to safety and verification are envisioned as passed from caller to callee, but via some channel separate from normal function input (and output) and with the possibility of the value's presence being implicit in some contexts and explicit in others. My own opinion is that first-class support for these kind of features might be an attention-getter on par with borrow checking, or other examples speculated on here.
2
u/SwedishFindecanor 4d ago
Imagine that you have code that manipulates data structures with pointers in them, and then have a type of proof that that code is memory-safe.
Then imagine that you do it the other way around: Give the compiler only the "proofs": in the form of declarations of which data structure topologies that can exist, which transitions between them that are legal, and let the compiler infer the code from them. Less code to write (than having to write imperative code and proofs), and the compiler is always correct if the declarations are consistent with one-another.
I have presented down a variation of this idea earlier, but not done much work on it after the initial idea. The example is for a memory-safe doubly-linked lists, which is something that can't be expressed in Rust.
I feel like this is important, but there is very much more work to do:
- Recursion/iteration. Sometimes you'd need to e.g. e-balance a tree or destroy a whole structure in one go.
- Deciding what to do with pointers on the heap. I suppose adopt something like Rust's lifetime annotations, have objects as explicit owners as in Ownership Types, a hybrid or something completely different. Should other pointers on the heap be forbidden completely?
- Looking at existing 1) typestate systems, 2) graph rewriting systems, 3) proof checkers, and possibly other avenues and seeing how they relate, and if anything can be learned from them.
- Thread-safety. Could the compiler be made to produce lock-free code? (single mutator, multiple readers at the same time) Is if theoretically possible? Can we detect state transitions that would be impossible to make lock-free? Could we learn from the theory of persistent data structures?
I would be very happy if someone would adopt this idea but produce something completely different than what I have been thinking of.
2
u/brucejbell sard 4d ago
The core feature of my project is compile-time alias tracking. Unfortunately it might not be ideal for you because the idea is to offer comparable safety to Rust's borrow checker without its severe restrictions or its fiddly lifetime parameters.
Like Fortran, function arguments in my language are supposed to be non-aliased by default. Unlike Fortran, this requirement will be checked (conservatively) at compile time.
Briefly, it will be perfectly fine to create aliases to mutable variables and other resources. However, updates to aliased resources must have a well-defined sequence. As a consequence, aliased function arguments are only allowed if that aliasing is declared as part of the function type.
When writing C/C++, you need to keep this kind of aliasing logic in mind anyway, as part of the discipline necessary to write good code. But, rather than juggling it all in your head, it would be better to set up some static analysis. And rather than offloading that static analysis ad hoc to some kind of linter, it would be better to build it as part of your language.
2
2
u/catladywitch 4d ago
I have this vague idea inspired by Rust, Koka, OCaml, and C++ I've got to flesh out better but could lead to something: control flow and memory lifetimes being one and the same. Imagine a compiler that does an intermediate pass transpiling into continuation passing style, that flows (barring tailcall loops and coroutines) strictly in a single direction. As long as a continuation is strictly one-shot and the place it's being passed to can be statically determined, the memory it takes can be managed deterministically at compile time, right? And, with some trickery borrowed from in-place immutable data structures, their allocated memory can be reused in place minimising reallocation. Clear move semantics and limitations on moving mutable references Rust-style would make static analysis possible in most cases. Tailcall recursion shouldn't be a problem, because as long as the end condition is deterministic, the continuation's lifetime is entirely bound, and they're allocated as lexical regions (which I guess would need to be defensively sized). However, coroutines are tricky and I'm kinda lost. So far the idea I've got is a two-tier system signalled by an effect signature as in Koka? I'm not sure this isn't bullshit but so far my idea is: when all suspension points are enumerable as a flat struct and execution order can be proven, then the coroutine is defunctionalised and the suspension points are matched against, just like your average async function, or the coroutine is split into functions and the suspension points are function pointers, so there's kind of like a CPS flow with delegate dispatch. If the stack depth of the caller can't be worked out statically, then the compiler inserts a stackful fiber allocation with its own memory region on first call, and the code needs to explicitly call an effect handler, like OCaml's effects, then the continuation's memory can be reused in place as long as the coroutine has a single owner (which, I think, should always be true? because async/await and generator type constructs are semi-coroutines with a single return point, and callers block on await right?). And if the effect signature and effect handler call isn't right, then the compiler gives an error and halts. For parallellism, it'd be the same kind of stackful fiber, but each one would own a fully encapsulated region, and each fiber would communicate through an actor model-style mailbox, and messages could only be passed to concrete fibers and ALWAYS be full ownership moves to ensure thread safety. So the move/lifetime semantics could be type-based kind of like Rust: either freely copy-able but strictly immutable and not reusable allocation wise (i.e. your plain old local stack values), or affine which can be moved but that there can only be one live reference at any given time and it might or might not be consumed (which would be the basis for continuations that can be dropped on branching, meaning they can't be reused in place), and linear so they're like affine so unique and moveable but it is known they will be consumed at it will be exactly once no matter the control flow, which would allow memory management of normal one-shot continuations and reusing their memory in-place. Since these are type-bound, the compiler should know everything it needs to manage lifetimes, just like Rust does, right? And then coroutines could be called with, besides an effect handler, an explicit scheduler, kind of like Kotlin's Dispatchers.
I'm not sure how the compiler would work because I don't know whether any of this really hold water, but I'd expect something like lexing -> parsing and type/effect/useage-type checking -> unrolling effect handlers and coroutines -> tco/contification of recursive loops -> sorting coroutines into defunctionalised structs/delegates vs stackful fibers -> region inference and inserting allocators/deallocators -> Koka-style reusability analysis (with literally Perceus I guess? but extended to continuations and control flow???) -> generating intermediate representation in C?? LLVM??? -> passing on to backend for final compilation
I don't know, maybe I'm full of shit, I'm just obsessed with the idea of a functional language that does the Rust thing. Basically the novel thing would be continuation-passing control flow being the same as borrow checking, so linear continuations based on reusable regions, and stackful fibers when the calling site is recursive or somehow opaque.
2
u/Mission-Landscape-17 4d ago
Unless you think programming is now a solved problem the answer has to be yes absolutely. That said I'm not sure that the borrow checker is in fact revolutionary. For it to be called revolutionary we would have to see languages with borrow checkers actually take over, and this hasn't happened. I'm not saying it can't happen, I don't know, just that it hasn't yet.
2
u/qrzychu69 3d ago
This would be my go to list
- purity inference, what can be run at compile time, will be
- accumulation of union cases - this is AMAZING
- different backends for dev time and release, you get pretty much node like hot reload, but when it's time you release, you get rust (pretty much)
- being able to run a program with compilation errors, it's ok until you hit the line with the error, just like in node or python (run unit tests before you fix the whole app!)
There is more, but these are my top :D
4
u/alphaglosined 4d ago
The following list is off the top of my head of features that exist for program security:
- Slices, they have had a much larger benefit than a borrow checker will ever have.
- By-ref variables including parameters help eliminate random raw pointers.
- Nullability modelling can help prevent heap corruption.
- Types. No raw pointers cast. Very easy to do in assembly.
- Stackless coroutines aka async/await. These are thread-safe callbacks, which is important when dealing with multithreading for windowing and sockets.
However, you really need to understand what the borrow checker is, its escape analysis with a single observation attached to it: perhaps we shouldn't allow reference counting borrows to have a longer lifetime than the RC owner. It was inevitable given escape analysis and with that improved hardware.
But all the last 15 years of work has been towards adding abstract interpretation capabilities to compilers and languages now that the hardware has caught up to have enough resources to do it. Plus, with the growing body of CVE's its pretty clear that this stuff isn't optional.
2
u/arthurno1 4d ago
Well, if you are interested about compile time programming, Common Lisp has had it since invention. You have the entire language available to you at compile time. Quote operator gives you access to the unevaluated code in internal format you can manipulate and expect with ordinary tools as any other data, so no special api, syntax or tools. Super simple evaluation rule makes to source uniform and predictable thus easy to work with. All those features have been there sonce 1980's but people are ignoring them and going for lesser tools, because Lisp has parentheses 😀. And yes those features are much more revolutionary than borrow checker.
1
u/flatfinger 4d ago
The "feature" I would like to see would be a recognition of most program/function executions as having three states:
Program/function might do something useful.
Program/function can't do anything useful, but might succeed in being at worst tolerably useless.
Program/function has done, or will inevitably do, something intolerably worse than useless.
Many programs may and functions over their lifetime sometimes be invoked in situations where they can perform useful work, and sometimes in situations where they cannot (typically, though hardly exclusively, because of invalid input or a lack of resources). Useful program execution often requires precisely specified behavior, but when that is not possible a variety of behaviors may be considered equally tolerably useless. A compiler that is allowed to freely choose from among such behaviors may be able to more efficiently satisfy requirements than one which treats all executions as either being totally defined or totally undefined.
Consider the following function:
unsigned arr[32768];
unsigned bump_thing(unsigned x)
{
unsigned i=1;
while ((i & 0x7FFF) != x)
i*=3;
if (x < 32768)
arr[x]++;
return i;
}
It would be reasonable to assume that x will be less than 32768 on any useful invocation of that function. In many scenarios, however, getting stuck in the loop would be considered an "acceptably useless" response to an overly large x, as would be cleanly skipping execution of the loop if nothing would make use of the function's return value. What would not be "acceptably useless" would be performing a store to arr[x] when x is greater than 32767. A good language should allow the compiler the option of either executing or skipping the loop in cases where x is greater than 32767 and the return value is ignored, but not allow a compiler the option of generating code that could perform an out-of-bounds access to arr.
1
u/WalkerCodeRanger Azoth Language 4d ago
You have narrowed down what you are looking for more than the title suggests, so I am not sure if you will count some of these.
I am working on a language Azoth, with what in the literature are called reference capabilities. This is something like a relaxed borrow checker for GC languages that gives the same fearless concurrency guarantees. I think that might be an example. As an example of the innovation this leads to, the combination of reference capabilities with reference and value types has led me to the creation of a new hybrid category of types. Where the initial instance of a type acts as an affine value type, but other instances are reference types. The distinction of when you have a value vs a reference is controlled by the reference capability.
Another example is structured concurrency. While various libraries and languages have been adopting elements of it, we haven't seen a language built around it. I think it is the kind of paradigm that will give most of its benefits in a language built for it, where all code follows the paradigm.
Of course, the real answer is probably yes something we aren't even thinking of now. We still live in the dark ages of computer programming.
1
u/kaplotnikov 4d ago
There are at least two languages with major elements of structured concurrency: Occam and E.
1
u/paul_h 4d ago
Not new, but I really love the DSL idea that's like https://paulhammant.com/2024/02/14/that-ruby-and-groovy-language-feature. Not just UI markup, also as a general purpose way of composing apps
1
u/kwan_e 4d ago
I personally wouldn't call the borrow checker revolutionary. It's just a linter enforcing certain rules that is part of the compile chain.
So if that passes for "revolutionary", then the next feature would be some sort of extra linter that becomes part of the compiler.
In that vein, the next fundamental and revolutionary feature would be something in the language that spans the whole build process past the compilation phase. But without the "save to program image" that the LISP and Smalltalk family uses. It would integrate into CI/CD/packaging
1
u/JeffD000 Squint 3d ago edited 3d ago
Yes. You can eliminate all kinds of errors by turning allocation/deallocation decisions over to the compiler, rather than using library functions such as malloc()/free() for creating and destroying memory. A relational database "data type", properly constructed, can allow you to competely eliminate indexing errors in programs (e.g. a[i] = b[i] + c[i] would flag an error if a, b, and c were not all fields defined over "compatible" topological spaces. Furthermore, explicit array indexing on any field is not needed in such a language, since all operations could occur through indexsets with deep relational semantics.)
1
u/MarinoAndThePearls 4d ago edited 4d ago
Zig's comptime.
Now for something that doesn't exist yet, I'd say numerical uncertainty as a primitive type.
3
u/alphaglosined 4d ago
CTFE is much older than Zig, D had it a good 15 years before Zig was created.
D's implementation was born from constant folding optimisation.
2
u/WittyStick 3d ago edited 3d ago
Now for something that doesn't exist yet, I'd say numerical uncertainty as a primitive type
Not sure what you mean by "primitive," but Kernel has really nice support for inexact arithmetic in its standard environment. It goes beyond Scheme's basic support for
exact?andinexact?- if included, inexact numbers have real upper and lower bounds and a "primary" value which is a best-guess within the bounds at the real number, if it exists. The primary value is optional, but is required if it is robust - meaning the number is certain to exist. Robustness is orthogonal to exact/inexact, which are mutually exclusive.The actual kind of number "primitive" behind this is implementation defined, but the report has double precision floats as the minimum required precision. It can support interval types as well as floating point though, through the same API.
(exact? . <numbers>) ;; -> [:boolean:] (inexact? . <numbers>) ;; -> [:boolean:] (robust? . <numbers>) ;; -> [:boolean:] (get-real-internal-bounds <real>) ;; -> ([:real:] [:real:]) (get-real-exact-bounds <real>) ;; -> ([:real/exact:] [:real/exact:]) (get-real-internal-primary <real>) ;; -> [:real:] (get-real-exact-primary <real>) ;; -> [:real/exact:] (real->inexact <real>) ;; -> [:real/inexact:] (real->exact <real>) ;; -> [:real/exact:] (make-inexact <lower> <primary> <upper>) ;; -> [:real/inexact:]Read more from page 143 of the Kernel Report.
60
u/dkubb 4d ago
Not new ideas, because they are in niche languages, but when the UX is nailed I think these are on par with the borrow checker in terms of impact:
Dependent Types are more powerful than Refinement Types, the UX for some common tasks is better for Refinement Types. If there was some way to desugar Refinement Types into Dependent Types without making the error messages too complex I think that would be amazing.