The Koka language uses a similar approach to track resource usage, except there they use ref counting and just remove unnecessary ref counting operations. Neat stuff.
> Here, we'll see how a type is translated into a function that discards/copies the terms of the type. To see the basic idea, let's take a simple ADT for example:
data item {
| New(int, int)
}
> The internal representation of New(10, 20) is something like the below:
> New(10, 20)
// ↓ (compile)
let v = malloc({2-words}) in
store(10, v[0]);
store(20, v[1]);
v
I suspected that it's not actually heap-allocating every single bit of memory in every program, and from looking around more in the docs, I _think_ the "Allocation Canceling" section here explains what I was missing (https://vekatze.github.io/neut/basis.html#allocation-canceli...):
> When a free is required, Neut looks for a malloc that is the same size and optimizes away such a pair if one exists.
This is a really interesting way of automating memory management at compile time. I imagine there's still a lot of room for different choices in this strategy (e.g. choosing to reuse part of a larger allocation rather than looking for one that's exactly the same size and then leaving behind the remainder to re-use for a future allocation), and I'm super curious about whether this would end up encouraging different patterns than existing memory management systems. Offhand, it almost seems like it could act as a built-in allocation buffer managed by the compiler, and I'm curious if the algorithm for reusing memory is smart enough to handle something like manually allocating the maximum amount of memory needed for the lifetime of the program up front and then re-using that for the duration of the program to avoid needing to allocate anything dynamically at all (although my worry would be that this would devolve into the knapsack problem and not be feasible in practice). If this did work though, my immediate idea would be for some sort of hook where you could specify the maximum amount of memory you'd be willing to use, which could then turn "using too much memory at runtime" into a compiler error. My assumption is that that I'm missing something that would make all of this not work the way I'm thinking though.
> I'm curious if the algorithm for reusing memory is smart enough to handle something like manually allocating the maximum amount of memory needed for the lifetime of the program up front and then re-using that for the duration of the program to avoid needing to allocate anything dynamically at all
I imagine this would be equivalent to solving the halting problem. So you’d need to restrict the language in some significant ways. I’d definitely still be interested.
There might even be some possibility for cross-pollination with ideas such as Counting Immutable Beans [0].
I’ve long wondered if there could be a functional programming language that made static memory management less verbose and easier to manage without monads and other explicit structures.
Could someone explain the “Necessity and noema” section [1] or share a reference? Looked like it might be significant but I couldn’t make much sense of it
TL/DR: All functions are pass-by-value. To avoid complete tanking of performance, they have "noema" (same as a reference in other language), which contains pointer to "hyle" (reference target in other languages). Since the language is GC-free, the references cannot escape out of the block they are defined in.
The language authors really like inventing the new programming terms.
It looks partly like OCaml, with the "let ... in" kind of syntax. Also the "unit" word. I think in OCaml it means a function that doesn't return any value, but why is the word unit used for that?
This comes up in languages where everything is an expression, nothing is a statement. Because everything is an expression that needs to be evaluated, everything has a return type. You can't have something that doesn't return literally nothing (void), you have to return an empty expression. Thus, unit.
Requiring all language constructs be expressions and eliminating statements means that you avoid a lot of duplicate effort in the language design.
For example, in C-like language you have if-else statements and ternary expressions. The ternary expression does "the same thing": as condition statements, but it also evaluates to a value. So in functional programming languages, you just have the one kind of conditional expression, and then maybe some syntactic sugar to morph it into more ergonomic forms.
It's more precise to think of unit as an empty tuple. A tuple is like an ad-hoc struct without names for the fields, so `(int, string)` is like `struct MyTuple { int a; string b; }`. An empty tuple would be `()` (which is the syntax for unit in many languages), meaning `struct MyTuple {}`. If you think about it, that's about the closest you can get to "nothing" without invoking type system handwavium (like void, which is basically "unit without the good parts but that can also mean anything").
You can do clever stuff with it, for example `HashMap<string, ()>` is practically identical to `HashSet<string>` (depending on how clever the compiler is, possibly actually identical).
I don't think it's particularly useful to think of unit as an empty tuple specifically, that is just an arbitrary but convenient definition for it.
Really a unit type is just one that contains only a single value. This is a unit in the same way that 1 is a unit for the integers. With some hand waving it is an identity for product types, for example (int, ()) is the "same" (xxxmorphic yada yada) as int
Mildly disagree with your first statement. Well, I mostly agree that it's not particularly helpful for newcomers.
As a 0-tuple, it becomes a specific case of a more general concept -- there is some beauty/usefulness in not having to have a "special" construct for "Unit", which is (in a sense) not just "any" unit type.
It also "justifies" the syntax of `()` and notes that it is a product type, all the while fitting into the idea of the "cardinality" of `(a1, a2, ..., an)` being the product of the cardinalities of each of its type params.
>you think about it, that's about the closest you can get to "nothing"
Some other options could be to use None (like Python does) or Nil or Nothing itself, or even ReturnsNothing to be more explicit, or even the Pascal-style procedure keyword, instead of the function keyword, for a sub routine that returns nothing.
It's a one type, not a zero type - the function does return and it always returns the same thing. It makes this kind of function more normal and regular - you can say that functions always return 1 value, and then it means you don't have to special-case void functions (which is a problem you have to work around in e.g. C++ templating), you can do things like put the return value of the function in a variable and then use it for something since it's just a normal value (which matters if you want to write e.g. a generic compose function that runs a bunch of functions in, IDK, a database transaction or something).
You've gotten some great answers but lemme add another thing: The zero type is useful for things that should not happen that you can prevent at compile time, while the unit type is nice for things that can only happen one way.
In Elm (a functional language for making web UIs), you might use the unit type for a lazy view function. If and only if some condition is true, call a view function to render some stuff into your DOM tree as in the function viewIfLazy [0]. There's only one way to call that view function, so let's call it with the unit type.
Now, what about using the Never type (a type with no members that can be instantiated at runtime [1]) to do accessibility? In Elm, your DOM elements have type `Html msg` where msg is a type _parameter_ for your actual message type that makes your app update itself. Usually you create that type like `type Message = UpdatedTheFooCounter Int | UpdatedTheNameInput String | ClickedTheBlahButton` something like that. Then the type on your inputs and buttons will be `Html Message` (read as "Html of Message" or even "Html parameterized by Message").
Well, it's bad a11y practice to have onclick events attached to divs and spans and things that aren't buttons, generally. So you can give your divs type `Html Never` and then if you try to attach an onclick event to them, you find that you can't at compile time, because the members of the type Message are not members of the type `Never`. tesk9/accessible-html is a package that enforces that [2] (I kind of simplified how it does that because I'm deep enough in the weeds already).
> But seriously, according to that link, it seems to me like the zero or empty type is more suitable.
That's a bit different. The empty type is only suitable for functions that never return (e.g. loop infinitely, crash the program). The type checker will prevent functions that have the empty type as a return type from returning.
To expand on this: the "unit" here represents the number of possible values that can be returned.
The confusion is probably because "empty" can mean two things:
- What's inside the returned value. That may be why the parent suggested empty for the unit type. But that's now what "unit" means in the common parlance.
- How many possible values can be returned. Never returning means the function has zero possible return values.
For "How Fast is This?" it links to a benchmarks page, which only shows that it's faster than Haskell. It would be more informative to instead compare against a language that is more popular and/or more performant than Haskell.
C is usually 1-4x faster than Haskell. This looks to be within 1-2x.
The key takeaway for me is that you're in the range where very slight variations in implementation of the same algorithm make the difference between which is faster.
I'm currently reading through the automatic memory management claims which look really cool (reminds me of linear types), but the highlighted punctuation (, : =) makes it very painful to read.
Obviously the personal preferences about code formatting vary a lot among programmers and it is impossible to reach unanimity.
For instance, I am among those who are annoyed when seeing lines of text wasted with the opening curly brace, reducing thus the number of useful text lines visible on the screen.
Probably it is best to use an automatic code formatter and format the code according to personal preferences while working with it and then reformat it according to project rules when committing the code to the repository.
> For instance, I am among those who are annoyed when seeing lines of text wasted with the opening curly brace,
Conversely, I'm one of the people who are annoyed when the tokens that represent a block of code don't form a vertical line, making it much harder to see "at a glance" where blocks begin and end.
> Probably it is best to use an automatic code formatter and format the code according to personal preferences while working with it and then reformat it according to project rules when committing the code to the repository.
At the end of the day, I'm convinced there is no "right" way to do this. Everybody has their preferences, and who's to say that one set of preferences is objectively more meaningful than another? You care about wasted vertical space, I don't. I care about tokens lining up, you (probably?) don't (at least not as much as I do). But neither of us is really "right" or "wrong".
And I am annoyed with the lack of indentation with a dedicated character (like tab maybe). With spaces, my editor has to guess how much to delete. If I want to tabulate a table. It might fight me. This really irks me.
I want it all. No lines wasted, uniform indentation, dedicated indentation character.
Python with tab for indentation feels right to me.
I also like to set a vertical highlight in my editor to vertically delinate indentation levels.
The best available evidence is that bug count correlates only with number of lines of code, and therefore an approach that reduces the number of lines of code is objectively better. Some people don't like Whitney-style code, but as far as I can see that's just intellectual cowardice.
If I had to guess, it's putting the opening curly bracket on the same line as the function definition, instead of the next line. And if I'm correct, then I also agree.
Big in 2020 as a Show HN (456 points, 80 comments) https://news.ycombinator.com/item?id=23283880
Thanks! Macroexpanded:
Show HN: A dependently-typed programming language with static memory management - https://news.ycombinator.com/item?id=23283880 - May 2020 (78 comments)
I'll see if I can email the author.
The Koka language uses a similar approach to track resource usage, except there they use ref counting and just remove unnecessary ref counting operations. Neat stuff.
Koka is one of those languages that I really wish continue developing and growing. So many cool design concepts.
From glancing through a few of the pages that piqued my interest, I was somewhat surprised to see this section in "How to Execute Types" (https://vekatze.github.io/neut/how-to-execute-types.html):
> Here, we'll see how a type is translated into a function that discards/copies the terms of the type. To see the basic idea, let's take a simple ADT for example:
> The internal representation of New(10, 20) is something like the below:> New(10, 20)
I suspected that it's not actually heap-allocating every single bit of memory in every program, and from looking around more in the docs, I _think_ the "Allocation Canceling" section here explains what I was missing (https://vekatze.github.io/neut/basis.html#allocation-canceli...):> When a free is required, Neut looks for a malloc that is the same size and optimizes away such a pair if one exists.
This is a really interesting way of automating memory management at compile time. I imagine there's still a lot of room for different choices in this strategy (e.g. choosing to reuse part of a larger allocation rather than looking for one that's exactly the same size and then leaving behind the remainder to re-use for a future allocation), and I'm super curious about whether this would end up encouraging different patterns than existing memory management systems. Offhand, it almost seems like it could act as a built-in allocation buffer managed by the compiler, and I'm curious if the algorithm for reusing memory is smart enough to handle something like manually allocating the maximum amount of memory needed for the lifetime of the program up front and then re-using that for the duration of the program to avoid needing to allocate anything dynamically at all (although my worry would be that this would devolve into the knapsack problem and not be feasible in practice). If this did work though, my immediate idea would be for some sort of hook where you could specify the maximum amount of memory you'd be willing to use, which could then turn "using too much memory at runtime" into a compiler error. My assumption is that that I'm missing something that would make all of this not work the way I'm thinking though.
> I'm curious if the algorithm for reusing memory is smart enough to handle something like manually allocating the maximum amount of memory needed for the lifetime of the program up front and then re-using that for the duration of the program to avoid needing to allocate anything dynamically at all
I imagine this would be equivalent to solving the halting problem. So you’d need to restrict the language in some significant ways. I’d definitely still be interested.
There might even be some possibility for cross-pollination with ideas such as Counting Immutable Beans [0].
I’ve long wondered if there could be a functional programming language that made static memory management less verbose and easier to manage without monads and other explicit structures.
[0] https://arxiv.org/abs/1908.05647
Could someone explain the “Necessity and noema” section [1] or share a reference? Looked like it might be significant but I couldn’t make much sense of it
[1] https://vekatze.github.io/neut/terms.html#necessity-and-noem...
https://vekatze.github.io/neut/static-memory-management.html is a good explanation.
TL/DR: All functions are pass-by-value. To avoid complete tanking of performance, they have "noema" (same as a reference in other language), which contains pointer to "hyle" (reference target in other languages). Since the language is GC-free, the references cannot escape out of the block they are defined in.
The language authors really like inventing the new programming terms.
Ah, thanks
DDG took me straight to https://en.wikipedia.org/wiki/Noema
Seeing nent reminds me of MoonBit. Has anyone heard of this new programming language? It's pretty good.
https://docs.moonbitlang.com/en/latest/tutorial/tour.html
3 times on HN: 4 days ago, 3 days ago, and this one 2 days ago.
Still no, thank you, doesn't seem to be as compelling as Rust to me.
It looks partly like OCaml, with the "let ... in" kind of syntax. Also the "unit" word. I think in OCaml it means a function that doesn't return any value, but why is the word unit used for that?
This comes up in languages where everything is an expression, nothing is a statement. Because everything is an expression that needs to be evaluated, everything has a return type. You can't have something that doesn't return literally nothing (void), you have to return an empty expression. Thus, unit.
Requiring all language constructs be expressions and eliminating statements means that you avoid a lot of duplicate effort in the language design.
For example, in C-like language you have if-else statements and ternary expressions. The ternary expression does "the same thing": as condition statements, but it also evaluates to a value. So in functional programming languages, you just have the one kind of conditional expression, and then maybe some syntactic sugar to morph it into more ergonomic forms.
It's more precise to think of unit as an empty tuple. A tuple is like an ad-hoc struct without names for the fields, so `(int, string)` is like `struct MyTuple { int a; string b; }`. An empty tuple would be `()` (which is the syntax for unit in many languages), meaning `struct MyTuple {}`. If you think about it, that's about the closest you can get to "nothing" without invoking type system handwavium (like void, which is basically "unit without the good parts but that can also mean anything").
You can do clever stuff with it, for example `HashMap<string, ()>` is practically identical to `HashSet<string>` (depending on how clever the compiler is, possibly actually identical).
I don't think it's particularly useful to think of unit as an empty tuple specifically, that is just an arbitrary but convenient definition for it.
Really a unit type is just one that contains only a single value. This is a unit in the same way that 1 is a unit for the integers. With some hand waving it is an identity for product types, for example (int, ()) is the "same" (xxxmorphic yada yada) as int
Mildly disagree with your first statement. Well, I mostly agree that it's not particularly helpful for newcomers.
As a 0-tuple, it becomes a specific case of a more general concept -- there is some beauty/usefulness in not having to have a "special" construct for "Unit", which is (in a sense) not just "any" unit type. It also "justifies" the syntax of `()` and notes that it is a product type, all the while fitting into the idea of the "cardinality" of `(a1, a2, ..., an)` being the product of the cardinalities of each of its type params.
>you think about it, that's about the closest you can get to "nothing"
Some other options could be to use None (like Python does) or Nil or Nothing itself, or even ReturnsNothing to be more explicit, or even the Pascal-style procedure keyword, instead of the function keyword, for a sub routine that returns nothing.
Then you have to double-up all your higher-order functions, like Java 8 futures with their thenApply vs thenAccept.
It's a standard practice in functional languages: https://en.wikipedia.org/wiki/Unit_type
That sounds like those corporate types who brush off any complaints by users, by saying "that is corporate policy" :) #sorrycouldntresist
But seriously, according to that link, it seems to me like the zero or empty type is more suitable.
But I am not a PL or type theory expert.
It's a one type, not a zero type - the function does return and it always returns the same thing. It makes this kind of function more normal and regular - you can say that functions always return 1 value, and then it means you don't have to special-case void functions (which is a problem you have to work around in e.g. C++ templating), you can do things like put the return value of the function in a variable and then use it for something since it's just a normal value (which matters if you want to write e.g. a generic compose function that runs a bunch of functions in, IDK, a database transaction or something).
You've gotten some great answers but lemme add another thing: The zero type is useful for things that should not happen that you can prevent at compile time, while the unit type is nice for things that can only happen one way.
In Elm (a functional language for making web UIs), you might use the unit type for a lazy view function. If and only if some condition is true, call a view function to render some stuff into your DOM tree as in the function viewIfLazy [0]. There's only one way to call that view function, so let's call it with the unit type.
Now, what about using the Never type (a type with no members that can be instantiated at runtime [1]) to do accessibility? In Elm, your DOM elements have type `Html msg` where msg is a type _parameter_ for your actual message type that makes your app update itself. Usually you create that type like `type Message = UpdatedTheFooCounter Int | UpdatedTheNameInput String | ClickedTheBlahButton` something like that. Then the type on your inputs and buttons will be `Html Message` (read as "Html of Message" or even "Html parameterized by Message").
Well, it's bad a11y practice to have onclick events attached to divs and spans and things that aren't buttons, generally. So you can give your divs type `Html Never` and then if you try to attach an onclick event to them, you find that you can't at compile time, because the members of the type Message are not members of the type `Never`. tesk9/accessible-html is a package that enforces that [2] (I kind of simplified how it does that because I'm deep enough in the weeds already).
[0] https://github.com/elm-community/html-extra/blob/0b8fc70752c...
[1] https://package.elm-lang.org/packages/elm/core/latest/Basics... also has a simpler example now that I think of it.
[2] https://github.com/tesk9/accessible-html/blob/master/src/Acc...
> But seriously, according to that link, it seems to me like the zero or empty type is more suitable.
That's a bit different. The empty type is only suitable for functions that never return (e.g. loop infinitely, crash the program). The type checker will prevent functions that have the empty type as a return type from returning.
To expand on this: the "unit" here represents the number of possible values that can be returned.
The confusion is probably because "empty" can mean two things:
- What's inside the returned value. That may be why the parent suggested empty for the unit type. But that's now what "unit" means in the common parlance.
- How many possible values can be returned. Never returning means the function has zero possible return values.
thanks, guys.
For "How Fast is This?" it links to a benchmarks page, which only shows that it's faster than Haskell. It would be more informative to instead compare against a language that is more popular and/or more performant than Haskell.
C is usually 1-4x faster than Haskell. This looks to be within 1-2x.
The key takeaway for me is that you're in the range where very slight variations in implementation of the same algorithm make the difference between which is faster.
I'm currently reading through the automatic memory management claims which look really cool (reminds me of linear types), but the highlighted punctuation (, : =) makes it very painful to read.
Syntax highlighting of the background color is weird. It makes everything look like surrounded by a halo.
As a matter of personal preference, hoisted curlies drive me insane.
Obviously the personal preferences about code formatting vary a lot among programmers and it is impossible to reach unanimity.
For instance, I am among those who are annoyed when seeing lines of text wasted with the opening curly brace, reducing thus the number of useful text lines visible on the screen.
Probably it is best to use an automatic code formatter and format the code according to personal preferences while working with it and then reformat it according to project rules when committing the code to the repository.
> For instance, I am among those who are annoyed when seeing lines of text wasted with the opening curly brace,
Conversely, I'm one of the people who are annoyed when the tokens that represent a block of code don't form a vertical line, making it much harder to see "at a glance" where blocks begin and end.
> Probably it is best to use an automatic code formatter and format the code according to personal preferences while working with it and then reformat it according to project rules when committing the code to the repository.
At the end of the day, I'm convinced there is no "right" way to do this. Everybody has their preferences, and who's to say that one set of preferences is objectively more meaningful than another? You care about wasted vertical space, I don't. I care about tokens lining up, you (probably?) don't (at least not as much as I do). But neither of us is really "right" or "wrong".
And I am annoyed with the lack of indentation with a dedicated character (like tab maybe). With spaces, my editor has to guess how much to delete. If I want to tabulate a table. It might fight me. This really irks me.
I want it all. No lines wasted, uniform indentation, dedicated indentation character.
Python with tab for indentation feels right to me.
I also like to set a vertical highlight in my editor to vertically delinate indentation levels.
The best available evidence is that bug count correlates only with number of lines of code, and therefore an approach that reduces the number of lines of code is objectively better. Some people don't like Whitney-style code, but as far as I can see that's just intellectual cowardice.
What are “hoisted curlies”?
If I had to guess, it's putting the opening curly bracket on the same line as the function definition, instead of the next line. And if I'm correct, then I also agree.
Allman style FTW!