20 ms·

Show HN: A dependently-typed programming language with static memory management

456 points by u2zv1wx 6y ago

elongatedMusku 6y ago
This is amazing. Looks like lisp with types.
akavi 6y ago
This looks amazing, albeit waaay over my head. 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?
- zozbot234 6y ago
  Isn't CBPV more of a way of accounting for both strict (call-by-value) and lazy (call-by-name) evaluation in the same programming language? Not sure how that would help wrt. static memory management.
  - throwaway17_17 6y ago
    Call by Push Value does account for both CbV and CbN language semantics, but the reason it can do so is by basing the language in a rather particular categorical semantic. 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.
    - eointierney 6y ago
      You give excellent commentary
- vilhelm_s 6y ago
  I would guess the main problem is that this approach will be slow, since it keeps making copies of all data. If you have a garbage collector you can just pass pointers around.
  - mintplant 6y ago
    Which Neut gets around with its borrowing facilities, as described in the README.
- u2zv1wx 6y ago
  Thank you for your interest. I think this is not a possible-or-impossible problem, but a what-to-choose problem. Both Haskell and OCaml happen to choose GC today, but they could have chosen an alternative memory management system. Memory management of a lambda-calculus based language can be realized in a few ways, and my project can be thought of as a one that suggests an alternative way. 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..
rntksi 6y ago
Interesting license choice. I've found out through reading about it that my country is not party to the famous Berne Convention.
devit 6y ago
It's kind of hard to decode the explanation given that it spends a lot of text on useless formalism instead of substance, but it seems like this language has three fatal problems: 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.
- h-cobordism 6y ago
  I'm pretty sure you're right on all counts; I'm not even sure that shared immutable borrows would work under the very simple transform given in the README. 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.
  - ferzul 6y ago
    yes, i found the first example quite surprising. there doesn't seem to be any request to copy the string; it is simply unintuively copied/produced three times. i would prefer the language have some kind of `dup` or something, which gives you an additional reference to the object. 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.
- _bxg1 6y ago
  I don't think it aims to be "as powerful as Rust", and I think that's okay. It's decidedly a narrow, pure, opinionated language, while Rust has practicality as one of its main priorities. This language is more like Haskell, or even more Haskell than Haskell, in that while some people might want to do real projects in it, its main purpose (from what I can tell) is to explore a concept. Nothing wrong with that.
lukevp 6y ago
You are almost 3500 commits in to this project already, with no other contributors? The dedication to this is incredible. It sounds super compelling and I wish you luck! 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!
- parentheses 6y ago
  We've entered an era where new languages are almost never used. The Go and Rust story are exceptions. This is the long thin tail of new language adoption.
  - Jaxan 6y ago
    Sure. But rust was not possible without all the research and little prototype languages. I think it’s good that many people are trying many things (as long as they clearly report their findings).
  - The_Colonel 6y ago
    Languages like this are usually not meant for mainstream adoption. 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.
potiuper 6y ago
TLDR dependent lambda calculus using linear type system memory management with LLVM backend. Oddly, the source language a [dependent] lambda-calculus or a [dependent] Cartesian closed category would seem more restrictive than the linear types or closed monoidal category used to implement the compile time memory management system.
- EE84M3i 6y ago
  If you're not familiar with linear types, a fun paper to read is "Linear Types Can Change The World!"[1] although I might just be partial to it because of the wonderful name. [1]: http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.31.5002 http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.31.5... by Philip Wadler
  - bo1024 6y ago
    This is great, thanks!
  - throwaway17_17 6y ago
    For anyone interested in Wadler’s publications on Linear Logic, his homepage has a lot of pdf versions of his work in the area. [1]: https://homepages.inf.ed.ac.uk/wadler/topics/linear-logic.html https://homepages.inf.ed.ac.uk/wadler/topics/linear-logic.ht...
- throwaway17_17 6y ago
  As I mentioned in another comment, the particular category he is deriving the semantic in is dictated by the CBPV semantics. I certainly agree that a closed monoidal category is the appropriate ambient category for the standard linear type theory, the structure required to reach the full semantics of CBPV, as designed by Levy, require a narrower framing. Although, it should be noted that there is only a small amount of formalism to work through and the adjunction model of CBPV can be seen as right adjoint to the linear/non-linear systems Benton describes in his 94 paper with Wadler.
doersino 6y ago
The introduction at the top of the Readme is great – it succinctly explains what the project does, how it relates to existing languages, and why the reader should care. Way too many projects on GitHub and the likes don't do this well (or at all).
scott_s 6y ago
Have you considered submitting this work to any computer science conferences? PLDI is the obvious first candidate.
- u2zv1wx 6y ago
  Possibly, but not sure. Currently my life is in a peculiar state (?) so I think firstly I need to stabilize it somehow.
  - Syzygies 6y ago
    This is the most interesting language introduction I've seen in years. Work like this gives life meaning. You have a larger purpose for stabilizing your life; our hopes are with you.
  - Y_Y 6y ago
    If everyone had to wait until their life settled down before publishing science would be behind by a hundred years.
runeks 6y ago
The concept of linearity is referenced 21 times in various sections, but not in the introduction. As a first-time reader, I would appreciate if the introduction were to mention the role of linearity in this language before I encounter it in a subsection.
- u2zv1wx 6y ago
  Thank you for your kind feedback. I'll try to come up with a concise way to mention it in the introduction.
shpongled 6y ago
Very cool, I'll dig into this later. I've been meaning to gain a better understanding of dependent typing. Been working on an SML clone with first class modules (ala 1ML/F-ing modules), and I understand that the module language is typically modeled with dependent types. It's been challenging to try to enable modules-as-existentials without too much compiler-side hackery going on.
NieDzejkob 6y ago
If I understand correctly (and I'm not sure I do), neut achieves its memory management by not sharing data between structures, and instead copying it. This works well when all data structures are immutable. 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.
- throwaway17_17 6y ago
  I haven’t done a deep dive into the implementation, but based on the theory employed, particularly the linear nature of CBPV’s computational types, the copying would most likely be elided in all cases except for when a programmer writes a function which explicitly copies data to a new term.
  - u2zv1wx 6y ago
    I can't believe my good fortune to have a wonderful reader like you, by the way.
- ferzul 6y ago
  > 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 the requirement is simply that you don't inspect the value of x until later (f makes something, y, to use later; when you use y, it inspects x). x and y now have references to each other.
  - dependenttypes 6y ago
    > in a lazy language, you can certainly say: Not in haskell. Which language do you specifically have in mind?
    - tome 6y ago
      Yes indeed in Haskell. You have enable RecursiveDo for that particular example to work. I'm not sure why ferzul chose a recursive monadic computation when let { x = 0:y; y = 0:x } in x seems to demonstrate the same thing.
aey 6y ago
Super cool! Any idea how big the runtime is? Is it easy to run a libc free version? I honestly feel like the embedded/firmware slice of the stack desperately needs a next gen language.
- u2zv1wx 6y ago
  What you need are the two functions `malloc` and `free` that have the following signatures: declare i8* @malloc(i64) declare void @free(i8*) So if you have implementations of them written in LLVM IR, I think that's enough. Disclaimer: I'm not very good at low-layer concepts. Correct me if I'm wrong here.
  - aey 6y ago
    Is there a big runtime that’s linked to support all the language features? Like what is the fully statically linked size of int main(void) { return 0; } If it’s just providing free/malloc symbols, that’s wonderful!
namelosw 6y ago
Wow, this is mind-blowing. Great respect to the author. May I ask which preliminary knowledge or directions I need to look at, in order to have a decent understanding of the codebase?
logicchains 6y ago
Since this seems to support inductive types, would it be correct to say that it's based on the calculus of inductive constructions (CIC), not the plain CoC? Basing a dependently-typed language on pure CoC (plus some other features weaker than inductive types; it's been proven impossible in CoC alone) is an open research problem (see e.g. Cedille and Formality).
- perthmad 6y ago
  What do you mean? CoC definitely supports impredicative encodings, and as far as expressivity goes, this allows to implement a lot of programs. Proving them correct is another matter, but that's not what you implied. Also, CIC is notably not Turing-complete.
  - logicchains 6y ago
    I was referring to https://link.springer.com/chapter/10.1007/3-540-45413-6_16; https://link.springer.com/chapter/10.1007/3-540-45413-6_16; induction is not derivable in pure CoC. I suppose yes technically you could base a dependently-typed language on it if you didn't mind not supporting induction, but I can't imagine many people wanting to use it, as it would be quite limited compared to one supporting inductive proofs. Or at least when people think of "dependently typed programming language", they're usually thinking of something at least as expressive as CIC.
rehemiau 6y ago
I didn't find an explaination of how it deals with variables (e.g. strings) allocated on the stack, does/how borrowing work for those?
- rehemiau 6y ago
  Ability to use the stack is a very important performance oriented feature. Similarily, ability to nest structs or other data structures without intermediate pointers. I hope this could be solvable!
milkey_mouse 6y ago
This reminds me a lot of Carp: https://github.com/carp-lang/Carp https://github.com/carp-lang/Carp

456 points by u2zv1wx 6y ago

This is amazing. Looks like lisp with types.

This looks amazing, albeit waaay over my head. 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?

zozbot234 6y ago
Isn't CBPV more of a way of accounting for both strict (call-by-value) and lazy (call-by-name) evaluation in the same programming language? Not sure how that would help wrt. static memory management.
- throwaway17_17 6y ago
  Call by Push Value does account for both CbV and CbN language semantics, but the reason it can do so is by basing the language in a rather particular categorical semantic. 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.
  - eointierney 6y ago
    You give excellent commentary
vilhelm_s 6y ago
I would guess the main problem is that this approach will be slow, since it keeps making copies of all data. If you have a garbage collector you can just pass pointers around.
- mintplant 6y ago
  Which Neut gets around with its borrowing facilities, as described in the README.
u2zv1wx 6y ago
Thank you for your interest. I think this is not a possible-or-impossible problem, but a what-to-choose problem. Both Haskell and OCaml happen to choose GC today, but they could have chosen an alternative memory management system. Memory management of a lambda-calculus based language can be realized in a few ways, and my project can be thought of as a one that suggests an alternative way. 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..

rntksi 6y ago

Interesting license choice. I've found out through reading about it that my country is not party to the famous Berne Convention.

devit 6y ago

It's kind of hard to decode the explanation given that it spends a lot of text on useless formalism instead of substance, but it seems like this language has three fatal problems: 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.

h-cobordism 6y ago
I'm pretty sure you're right on all counts; I'm not even sure that shared immutable borrows would work under the very simple transform given in the README. 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.
- ferzul 6y ago
  yes, i found the first example quite surprising. there doesn't seem to be any request to copy the string; it is simply unintuively copied/produced three times. i would prefer the language have some kind of `dup` or something, which gives you an additional reference to the object. 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.
_bxg1 6y ago
I don't think it aims to be "as powerful as Rust", and I think that's okay. It's decidedly a narrow, pure, opinionated language, while Rust has practicality as one of its main priorities. This language is more like Haskell, or even more Haskell than Haskell, in that while some people might want to do real projects in it, its main purpose (from what I can tell) is to explore a concept. Nothing wrong with that.

lukevp 6y ago

You are almost 3500 commits in to this project already, with no other contributors? The dedication to this is incredible. It sounds super compelling and I wish you luck! 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!

parentheses 6y ago
We've entered an era where new languages are almost never used. The Go and Rust story are exceptions. This is the long thin tail of new language adoption.
- Jaxan 6y ago
  Sure. But rust was not possible without all the research and little prototype languages. I think it’s good that many people are trying many things (as long as they clearly report their findings).
- The_Colonel 6y ago
  Languages like this are usually not meant for mainstream adoption. 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.

potiuper 6y ago

TLDR dependent lambda calculus using linear type system memory management with LLVM backend. Oddly, the source language a [dependent] lambda-calculus or a [dependent] Cartesian closed category would seem more restrictive than the linear types or closed monoidal category used to implement the compile time memory management system.

EE84M3i 6y ago
If you're not familiar with linear types, a fun paper to read is "Linear Types Can Change The World!"[1] although I might just be partial to it because of the wonderful name. [1]: http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.31.5002 http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.31.5... by Philip Wadler
- bo1024 6y ago
  This is great, thanks!
- throwaway17_17 6y ago
  For anyone interested in Wadler’s publications on Linear Logic, his homepage has a lot of pdf versions of his work in the area. [1]: https://homepages.inf.ed.ac.uk/wadler/topics/linear-logic.html https://homepages.inf.ed.ac.uk/wadler/topics/linear-logic.ht...
throwaway17_17 6y ago
As I mentioned in another comment, the particular category he is deriving the semantic in is dictated by the CBPV semantics. I certainly agree that a closed monoidal category is the appropriate ambient category for the standard linear type theory, the structure required to reach the full semantics of CBPV, as designed by Levy, require a narrower framing. Although, it should be noted that there is only a small amount of formalism to work through and the adjunction model of CBPV can be seen as right adjoint to the linear/non-linear systems Benton describes in his 94 paper with Wadler.

doersino 6y ago

The introduction at the top of the Readme is great – it succinctly explains what the project does, how it relates to existing languages, and why the reader should care. Way too many projects on GitHub and the likes don't do this well (or at all).

scott_s 6y ago

Have you considered submitting this work to any computer science conferences? PLDI is the obvious first candidate.

u2zv1wx 6y ago
Possibly, but not sure. Currently my life is in a peculiar state (?) so I think firstly I need to stabilize it somehow.
- Syzygies 6y ago
  This is the most interesting language introduction I've seen in years. Work like this gives life meaning. You have a larger purpose for stabilizing your life; our hopes are with you.
- Y_Y 6y ago
  If everyone had to wait until their life settled down before publishing science would be behind by a hundred years.

runeks 6y ago

The concept of linearity is referenced 21 times in various sections, but not in the introduction. As a first-time reader, I would appreciate if the introduction were to mention the role of linearity in this language before I encounter it in a subsection.

u2zv1wx 6y ago
Thank you for your kind feedback. I'll try to come up with a concise way to mention it in the introduction.

shpongled 6y ago

Very cool, I'll dig into this later. I've been meaning to gain a better understanding of dependent typing. Been working on an SML clone with first class modules (ala 1ML/F-ing modules), and I understand that the module language is typically modeled with dependent types. It's been challenging to try to enable modules-as-existentials without too much compiler-side hackery going on.

NieDzejkob 6y ago

If I understand correctly (and I'm not sure I do), neut achieves its memory management by not sharing data between structures, and instead copying it. This works well when all data structures are immutable. 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.

throwaway17_17 6y ago
I haven’t done a deep dive into the implementation, but based on the theory employed, particularly the linear nature of CBPV’s computational types, the copying would most likely be elided in all cases except for when a programmer writes a function which explicitly copies data to a new term.
- u2zv1wx 6y ago
  I can't believe my good fortune to have a wonderful reader like you, by the way.
ferzul 6y ago
> 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 the requirement is simply that you don't inspect the value of x until later (f makes something, y, to use later; when you use y, it inspects x). x and y now have references to each other.
- dependenttypes 6y ago
  > in a lazy language, you can certainly say: Not in haskell. Which language do you specifically have in mind?
  - tome 6y ago
    Yes indeed in Haskell. You have enable RecursiveDo for that particular example to work. I'm not sure why ferzul chose a recursive monadic computation when let { x = 0:y; y = 0:x } in x seems to demonstrate the same thing.

aey 6y ago

Super cool! Any idea how big the runtime is? Is it easy to run a libc free version? I honestly feel like the embedded/firmware slice of the stack desperately needs a next gen language.

u2zv1wx 6y ago
What you need are the two functions `malloc` and `free` that have the following signatures: declare i8* @malloc(i64) declare void @free(i8*) So if you have implementations of them written in LLVM IR, I think that's enough. Disclaimer: I'm not very good at low-layer concepts. Correct me if I'm wrong here.
- aey 6y ago
  Is there a big runtime that’s linked to support all the language features? Like what is the fully statically linked size of int main(void) { return 0; } If it’s just providing free/malloc symbols, that’s wonderful!

namelosw 6y ago

Wow, this is mind-blowing. Great respect to the author. May I ask which preliminary knowledge or directions I need to look at, in order to have a decent understanding of the codebase?

logicchains 6y ago

Since this seems to support inductive types, would it be correct to say that it's based on the calculus of inductive constructions (CIC), not the plain CoC? Basing a dependently-typed language on pure CoC (plus some other features weaker than inductive types; it's been proven impossible in CoC alone) is an open research problem (see e.g. Cedille and Formality).

perthmad 6y ago
What do you mean? CoC definitely supports impredicative encodings, and as far as expressivity goes, this allows to implement a lot of programs. Proving them correct is another matter, but that's not what you implied. Also, CIC is notably not Turing-complete.
- logicchains 6y ago
  I was referring to https://link.springer.com/chapter/10.1007/3-540-45413-6_16; https://link.springer.com/chapter/10.1007/3-540-45413-6_16; induction is not derivable in pure CoC. I suppose yes technically you could base a dependently-typed language on it if you didn't mind not supporting induction, but I can't imagine many people wanting to use it, as it would be quite limited compared to one supporting inductive proofs. Or at least when people think of "dependently typed programming language", they're usually thinking of something at least as expressive as CIC.

rehemiau 6y ago

I didn't find an explaination of how it deals with variables (e.g. strings) allocated on the stack, does/how borrowing work for those?

rehemiau 6y ago
Ability to use the stack is a very important performance oriented feature. Similarily, ability to nest structs or other data structures without intermediate pointers. I hope this could be solvable!

milkey_mouse 6y ago

This reminds me a lot of Carp: https://github.com/carp-lang/Carp https://github.com/carp-lang/Carp