[akavi]

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?

[u2zv1wx]

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..

[zozbot234]

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]

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]

You give excellent commentary

[vilhelm_s]

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]

Which Neut gets around with its borrowing facilities, as described in the README.