Show HN: A dependently-typed programming language with static memory management
github.com
github.com
I hope you get more recognition to encourage you to continue. These new languages are so important in pushing forward our tooling and our understanding of workable abstractions as an industry. I am only recently getting into functional programming and it has already fundamentally changed a lot of my perspective on OO, composition vs inheritance, immutability, pure functions, etc.
Have you considered trying to make this a little more accessible (a bit of a focus on the marketing side?) I would really like to digest the main benefits of your language more easily. One example is that when skimming your readme, the first thing my eye is drawn to is the bulleted section which talks about other limited memory management solutions. But if I didn’t read the small text before it that says “neut doesn’t use these” I do not understand the compelling feature of the language to dive in further.
Have you followed Zig Lang? Andrew Kelly is doing something similar (in so far as he’s building a new language focused on memory management) and even though I don’t use it, I see the value in this work and support him on Patreon.
I would be happy to help you with reviewing the copy on the readme from the perspective of someone who is technical but not super knowledgeable in this domain to help you summarize the key concepts and advantages up front. Reach out to me with the email in my profile if you would like to discuss!
It's more of a research language useful as a vehicle for exploring new concepts and approaches. Target audience is probably other programming language researchers.
> Programming languages researchers are like fashion designers and "research languages" like Haskell and Idris are like runway looks. Nobody expects people to go around snakes on their bodies. They're pushing the boundaries of art and science and showing what's possible.
And just like in fashion, the runway looks eventually change what people are wearing. Rust’s memory management would never exist in its current form if Cyclone hadn’t already shown it was possible.
Production-history without expansive libs is probably bespoke and half a complete library (eg rust/go, having half of what you want, and missing the other half) is boutique :-)
I disagree. The same was said when perl dominated before Ruby and Python came along. And Pascal, C and C++ before that. Nowadays Nim, Crystal, Rust, Go, F#, D, Zig, JavaScript, Haskell, and more are all viable options for application development.
We have more viable programming languages than ever.
From a quick glance over a few dozen pages of job ads, it's mostly Java & PHP, with a bit of JS, Python and C# here and there and some C/C++ in embedded. Saw 2 node.js ads, as well as a COBOL and a Kotlin too.
So, yes, maybe they are viable. But.. used ? they're blimps in the radar next to the big ones.
+ Node.js is plentiful
+ Golang is up and coming
+ Some elixir
+ Haskell is pretty rare but it shows up as a secondary language
+ Java and php are plentiful but these tend to be large, older corporate gigs
+ Rust is rare
+ No crystal/nim/f#/zig/D that I've seen
Obviously anecdotal and your case my differ.
As so often, Alan Perlis said it best: "In a 5 year period we get one superb programming language. Only we can't control when the 5 year period will begin."
> The (with identity.bind (...)) is the same as the do-notation in Haskell or other languages, specialized to the identity monad.
The next section is called "Types as Exponentializers". The section after that explains
> That is, a lambda-abstraction is translated into a tuple consists of (0) the type of its closed chain, (1) its closed chain, and (2) a pointer to an appropriately-arranged closed function
As a Haskell fan this sounds like perfectly normal Haskell-speak. Is there something about it that makes is more digestible to you than the average Haskell-speak?
"Neut is (...) memory management" - first para ok, incl. the bullet list - specifically what original commenter complained about, for me was no problemo
"Theoretically (...) terms of the type" - 100% Haskell-speak, no slightest idea what it means, skipped; but relatively short optically, and author still has some credit after first para, so I still take a look further
"Practically, this means (...)" - cool, I can understand again! I think that's where I got hooked: now I know the author sprinkles their Haskell-speak because of an unstoppable inner need to be precise and probably also so that the tribe doesn't expell them, but they also seem to have this amazing spark of humanity and empathy towards common programmer folk, so that if I skip over the mysterious ivory-tower spells, I will find more nuggets of commoner-speak for me. Knowing a bit more about writing, I believe they additionally probably consciously put a lot of effort to write in an approachable way. Which is a surprisingly tough skill. This is a mix I honestly bow to. I can try and list more paras that were cool for me if you'd specifically like me to.
P.S. Also, I only put that July 1 date as further personal reinforcement that I am going to meet my self imposed release deadline. Gotta keep the pressure on or I’m sure I’ll hold it as a private project forever.
Here, if you don't understand identity.bind, or even do-notation, you can read on without losing much. Not understanding the section title, is not an obstacle to understanding the section. And so on.
The intro has nice non-local clarity. The dialog structure; having summaries.
I'd not stereotype a "Haskell writing style", but I certainly encounter writing elsewhere which seems to reflect a mindset of "since you've reached this paragraph N, you obviously fully understand, remember, and appreciate the implications of, everything that has been said earlier, so we can happily take this next step without any distracting redundancy, context, motivation, or other annotation". Which... needs to be approached in a particular way to avoid degrading nongracefully.
I also appreciated the intro's "here's how I suggest approaching learning the language".
I know Zig language (I've seen it before in an article that compares the binary sizes of hello world of various languages IIRC), though I don't know it in detail. Sounds interesting, I'll take a look at it.
The introduction says it "is made possible by translating the source language into a dependent variant of Call-By-Push-Value.". What makes such a translation impossible in the existing languages you mention (Haskell/OCaml/etc)? Are there restrictions on expressivity not present in those languages/augmentations to their type system needed?
Based on the linked intro, it would seem that the language is leveraging the ‘computational’ types that are an intrinsic part of the CBPV semantics to force the ‘thunking’ of the dependent types. Effectively, all of the types become ‘functions’ from the CBPV lense and those functions are linear by construction (it is a categorical, as in category theory, feature of the underlying semantics). Although not cited, it seems like the underlying type theory takes notice and inspiration from Levy’s work on adjunction models for CBPV.
I tried to find a way to make this comment that wasn’t too acedemic sounding, but I think I missed the mark.
Having said that though, I don't think the approach in Neut can be directly applied to Haskell or OCaml. This is because mutable variables won't make sense in this memory management system since every use of a variable (theoretically) creates a distinct object.
I hope this answers your question..
Way too many projects on GitHub and the likes don't do this well (or at all).
However, I feel like it would be more performent to just use reference counting here. After all, incrementing a counter must be faster than a memcpy, no? Since immutable values can't create cycles, no memory will be leaked.
this is not generally true. in a lazy language, you can certainly say:
main = mdo
y <- f x
x <- g y
return y
Not in haskell. Which language do you specifically have in mind?
let { x = 0:y; y = 0:x } in x
May I ask which preliminary knowledge or directions I need to look at, in order to have a decent understanding of the codebase?
declare i8* @malloc(i64)
declare void @free(i8*)
Disclaimer: I'm not very good at low-layer concepts. Correct me if I'm wrong here.
int main(void) { return 0; }
If it’s just providing free/malloc symbols, that’s wonderful!
[1]: http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.31.5... by Philip Wadler
[1]: https://homepages.inf.ed.ac.uk/wadler/topics/linear-logic.ht...
I've found out through reading about it that my country is not party to the famous Berne Convention.
1. Borrowed pointers are not a first class concept, but just syntax sugar over returning a parameter from a function, i.e. &T or &mut T are not actual types in Rust parlance
2. There is no mention on how to achieve safe shared mutable data or even just shared read-only data, i.e. the equivalent of Rust's Arc<Mutex<T>> or Arc<T>, which probably means the language has no support
3. It seems there is no way for a struct/record/tuple to contain another non-primitive data type without the latter being allocated on the heap
So as far as I can tell aside from the dependent types this language is much less powerful than Rust and cannot fully utilize the CPU, and hence far from the goal of having a perfect Rust+dependent types language.
Edit: Also, the user-facing language doesn't seem to have linearity at all, i.e. all values may be cloned. But linearity is something that people use to guarantee certain invariants all the time in Rust (and ATS, I've heard), so this seems like a misstep. It also means that memory allocation is implicit, which makes things less predictable for users.
as it stands, it has transferred allocation from the runtime to the compiler. but the objective is to put it into the hands of the developer, since only then is it known when reading and writing code.
i begin to suspect that a typed joy may be more practical (or rather: match my desired improvements) than clarifying allocations in haskell.
But from a Haskell perspective, this language promises to completely eliminate the garbage collector, which is a big deal.
> Practically, this means that you can write your program in the ordinary lambda-calculus without any extra restrictions or annotations, and at the same time are allowed to control how resources are used in the program.
You can rewrite any Haskell program into the ordinary lambda-calculus, and this can be automated. The only possible problem might be that Haskell uses lazy evaluation, and I don't expect this to interfere with the control of resources but I could be wrong.
But as long as you're not storing closures in those shared data-structures, these structures will always be acyclic, and could be collected through simple reference counting. Perhaps that's an acceptable compromise.
let x = 1:x
At a glance, most of those look like bounds checking problems. tcc (Tiny C Compiler) allows you to compile in bounds-checking with all pointer dereferences.
C++ STL implementations generally have bounds checking all over the place - this requires compiling in debug mode IIRC, but it is evidence of the possibilities of safety without language or compiler support.
Lisp-style meta-programming can get you basically anything you want from a language without language or compiler support.
These vulnerabilities are typically in code implemented in C or C++.
I am suggesting that if you want to have a secure system, they have to be addressed by the language; if you are happy with systems that have exploitable memory management bugs, there are lots of existing UNIX variants to choose from.
> I doubt such a wide and diverse range of problems be addressed at such a low level.
May I suggest reading about some low-level languages that have been used in production and address these problems to varying degrees of success, for example ESPOL (from 1960s), Mesa/Cedar, Modula-2, Ada, or Rust.
https://en.wikipedia.org/wiki/Executive_Systems_Problem_Orie...
> tcc (Tiny C Compiler) allows you to compile in bounds-checking with all pointer dereferences.
This sounds impossible, there's not enough information in the C type system to know in the general case what the bounds are.
> C++ STL implementations generally have bounds checking all over the place
This wasn't true last I checked for libc++ (the most "modern" implementation), and isn't applicable for any non-STL container in a program anyway; nothing prevents using a plain C array.
> this requires compiling in debug mode IIRC
I'm not aware of anybody who enables this in production because the culture of C++ is all about performance.
> but it is evidence of the possibilities of safety without language or compiler support
Language or compiler support would reduce the performance overhead, because it makes it easier for the compiler to elide checks that can be statically proven to always succeed.
> Lisp-style meta-programming can get you basically anything you want from a language without language or compiler support.
Meta-programming cannot remove features from a language, which is typically the problem here.
> This sounds impossible, there's not enough information in
> the C type system to know in the general case what the
> bounds are.
Perhaps every pointer could be implemented not only as a raw pointer but one with a "valid" range attached, which indicated how many bytes prior and following the pointer that were part of the block original block the pointer was calculated as an offset from. Any dereference would check that it is within the range, and that is only O(1) for every `foo[bar]`.
> This wasn't true last I checked for libc++ (the most "modern" implementation)
> ...
> I'm not aware of anybody who enables this in production
> because the culture of C++ is all about performance.
> Meta-programming cannot remove features from a language, which is
> typically the problem here.
The main problem with this is that it's incompatible with every existing system C ABI.
There's also the problem of real-world C code converting pointers to integers and back again, but the compiler could define uintptr_t and intptr_t accordingly and code that uses other integer types is broken anyway.
> it is possible to create a new kind of "top-level context"
I'm not familiar with that, it sounds like quite some effort but I'll grant you that likely it can achieve what you claim.