While Rust made Cyclone's type system more manageable for mainstream computing, everyone else is trying to combine the benefits of linear/affine type systems, with the productivity of automated resource management.
Naturally it would be interesting to see if some of those attempts can equally ping back into Rust's ongoing designs.
* Carp: https://github.com/carp-lang/Carp
* Nim: https://nim-lang.org/
* Zig: https://ziglang.org/
However, in the grand scheme of things heap vs stack allocation is minuscule. Many other factors are much more important for performance.
That said, as a sibling already pointed out, it's standard to control stack allocation with a single counter. It's kind of standard to control heap allocation with an index and a lot of book-keeping.
But you are allowed to optimize the heap until there's no difference.
Also, heap allocation is unpredictable. It is more likely to cause unexpected page faults or thread congestion (multiple threads often share the same heap so they need to synchronize access to memory book-keeping structures). Especially when it comes to kernel drivers, a page fault can lead to a deadlock, infinite recursion, or timeouts.
I'm not saying heap is always bad, not even that it's bad most of the time. But if a language doesn't at least give you the _option_ of having objects live on the stack, I wouldn't consider it a serious systems programming language.
Yes, linear / affine types and uniqueness types can give you a lot of control over resources, while also allowing you to preserve functional semantics.
I would like to see a version of Haskell that doesn't just track IO, but also track totality. Ie unless your function is annotated with a special tag, it has to be guaranteed to return a value in finite time, ie it has to be total. If you tag it with eg 'Partial', you can rely on laziness.
That's very similar to how functions in Haskell can't do any IO, unless they are tagged with 'IO'.
(I know that Haskell doesn't see 'IO' as a tag or annotation. But it behaves like one in the sense I am using here.)
In languages for doing practical calculations, a progress dialog and a cancel button are more useful than a totality guarantee. It should be easier to make complex, long-running calculations safely cancellable.
(Still true with laziness, though it changes a bit. At some point you will ask for a value to be calculated.)
So a default constraint on functions to be total, would be sensible and helpful.
To be able to do the opposite, constrain a function or continuation to never terminate (outside of program termination), would be useful too. Albeit in much fewer contexts.
Any constraint that forces implementations to match respective design intentions is good.
It’s kind of pain when you’re not making a theoretical argument. You might still want to eliminate all divide by zero errors. Satisfying the compiler of this using a machine-checked proof might be more trouble than it’s worth, though. It might require you to use a language whose types support proofs.
That can take the form of something like `try_divide` that returns a `Maybe` that you need to pattern match on. Or it can take the form of trust-me-bro via the equivalant of UnsafePerformIO, where you know that something is safe and you want to let the compiler know, but you can't prove it to the compiler.
You can also deal with errors by returning an `Either`. That doesn't mess with any totality guarantees.
Reporting an error to a function's caller isn't really a thing in a proof. A function proves that if any input exists, its result exists. Returning an error means "an error might exist." We don't want to return that, we want to eliminate the error from our proof, so that it proves that the result exists for any input. Returning an 'Ether' type might be useful in a proof, but a 'Maybe' type seems dubious. We already assume that 'None' exists, so proving that 'None' might exist is useless.
We don't have the same concerns in proofs and practical programs.
In a practical program you want to know that you in finite time you either get one of the declared errors, or you get a positive result. Using an `Either` type allows even a relatively weak type system to be of use here.
There's no 'error' in your proof: your proof can't do anything about eg running out of disk space.
Now, using an `Either` type for things like division-by-zero is a bit of a cop-out, and a compromise foisted on us by a weak type system. And you are right that in something like Agda you would hopefully never have to stoop so low. (Though even there, you can't proof everything. Eg if your program enumerates differences between adjacent prime numbers, you can't prove that it will (or won't) run out of 2s.)
In previous post you quoted the Dhall documentation:
> The main benefit of evaluation being finite is not to eliminate long-running programs but to make them significantly less probable. In practice, you will discover that you will rarely author a configuration file that takes a long time to evaluate by accident.
This might be practical advice, but it's not theoretically sound. It's drawing a conclusion that wasn't proven. Isn't it kind of weird to write proofs without caring about the result of the proof?
You are technically right, but in practice, finite time does help a lot. To quote from the Dhall documentation at https://docs.dhall-lang.org/discussions/Safety-guarantees.ht...
> Note that a “finite amount of time” can still be very long. For example, there are some short pathological programs that take longer than the heat death of the universe to evaluate. The main benefit of evaluation being finite is not to eliminate long-running programs but to make them significantly less probable. In practice, you will discover that you will rarely author a configuration file that takes a long time to evaluate by accident.
> It should be easier to make complex, long-running calculations safely cancellable.
Just send kill 9 to your program, if you want to cancel it? That seems like an entirely separate topic? (Especially if your calculation is pure, it's always safe to cancel it.)
Go’s Context API handles cancellation and timeouts at the request level, but it has to be coded manually; a badly-behaved goroutine could still leak and consume resources long after it’s cancelled.
So it might be nice to have automatic support at the language level, to make guaranteed cancellation happen by default. This is the approach taken with structured concurrency. To preserve the invariant that a child task doesn’t outlive the parent, there needs to be a way to kill any unneeded child tasks when a function returns early.
Totality checks seem like a poor substitute when what you actually want is to prevent resource leaks.
I haven’t used Dhall, but it seems like a config language has different concerns?
I don't disagree, but...
Except for excutable sizes and maybe unpredictable performance (performance unpredictability on Haskell has the same shape of UB on C, in that it creeps in, but it's way easier to keep away), there's actually no feature missing.
You can argue for C-like speed (instead of Java-like), but the stuff on the article doesn't have it either.
People have written kernels and unikernels in Haskell. So in that sense it's definitely a systems programming language.
However that comes with performance drawbacks (or at least unpredictable/unreliable performance) which creates the need for languages like Rust. It's great to see the progress in those languages as well.
Well, in the sense that garbage collectors solve memory management. But pure functional programming in the Haskell sense doesn't really manage file handles for you, or database connections.
You could have more predictable performance in Haskell, if you didn't have to deal with mandatory laziness for some functions.
(Basically, in this hypothetical variant of Haskell, by default functions would be safe to be evaluated in any order, strict or lazy or whatever. If you want functions that need to be evaluated lazily, then you'd need to declare that; just like today you already need to declare that your function might have side effects.)
The compiler would then be free to re-order evaluation a lot more, and pick predictable, fast performance.
No, I was actually talking about the latter and not about memory management at all.
In Scala we even achieve this on the library level. (e.g. https://zio.dev/reference/resource/ which also compares the existing problematic try/catch with its own approach)
And despite Scala being strict, the GC still makes it unsuitable for many cases where you just need something like Haskell.
Not a sensible default.
You cannot ask a strict function to behave lazily. But you can ask a lazy function to behave strictly.
"The problem is the very idea of a lazy language, which imposes a ruinous semantics on types. An eager semantics supports the expected semantics of types (for example, the natural numbers are the natural numbers) and, moreover, admits definition of the lazy forms of these types using suspension types (Chapter 36). A value of a suspension type is either a value of the underlying type, or a computation of such a value that may diverge. There being no representation of the eager types in a lazy language, it follows that, eager languages are strictly more expressive than lazy languages." [1]
This paragraph is then followed by a link to Harper's "PCF by Value" supplement/errata to the above referenced PFPL, where such a statement is reinforced. [2]
[1] - https://www.cs.cmu.edu/~rwh/pfpl/supplements/commentary.pdf
You make a lazy function strict by asking for its output now rather than later.
> An eager semantics supports the expected semantics of types (for example, the natural numbers are the natural numbers).
What a (counter)example! In lazy semantics the natural numbers are the natural numbers. In eager semantics the natural numbers are stack overflow.
> moreover, admits definition of the lazy forms of these types using suspension types
This is the required modification that your library maintainer would need to make if he had produced a strict library that you wanted to use lazily. Hence "You cannot ask a strict function to behave lazily."
> There being no representation of the eager types in a lazy language
Because the lazy representation is the same as the eager representation in the source code. It's up to the caller to demand values now, or later, hence "But you can ask a lazy function to behave strictly."
That doesn't mean you can evaluate the function strictly. Have a look at this example:
f = head . map (2+)
x = f [5, undefined]
In any case, my suggestion is not to deal with arbitrary functions; but to restrict the set of untagged functions to those where any evaluation order works. 'Works' in the sense that any evaluation order takes a finite amount of time.
Huh? I suggest that when you don't annotate anything, you can only use constructs that can be evaluated in any order (including both lazy and strict or any other order). So the compiler has maximal freedom.
So your supposed impossibility doesn't come into play: we are not dealing with arbitrary functions.
If your function needs a specific evaluation order, you'd need to tag that.
To do the reverse would require uncomputation. You can't turn all the natural numbers back into the expression [1..].
That's what monads are for.
Haskell doesn't require that you use automatic management. But it does absolutely have a solution.
You might want to look into 'indexed monads', they can perhaps help with that. But they aren't a type monads (it's the other way round, vanilla monads can be seen as a trivial kind of 'indexed monads', I guess).