[jimsimmons]

I’m constantly baffled by what functional programmers call “simple”. I’m sure this language does a lot with little but calling it simple is audacious to say the least. Why do so many things happen in a single line? Lack of imperative constructs in these languages forces one to nest a lot to be expressive and we get a symbol salad. It’s almost as if the code got passed through a minifier/function inliner.

Unless FP embraces more modular and structured ways of programming it’ll always remain a niche. OCaml’s ‘let’ and Haskell’s ‘where’ are steps in the right direction but we need to go a lot farther. To think that any human, with any amount of training, can parse such code in one pass is a fantasy. Since parsing is part of the coding loop, developer productivity is compromised massively.

Mathematics has a similar problem where single letter variable names with tiny letters on all 4 corners are ubiquitously used. There’s definitely a tendency in the community to play “symbol” golf. It’s high time we improve ergonomics of both math and FP because the rewards can be tremendous. Rust manages to do some of this to great success and programmers have embraced it so well.

[carlmr]

I agree with you that spacing up everything with well-named let-bindings is a great idea, but most ML-based languages do support that.

>To think that any human, with any amount of training, can parse such code in one pass is a fantasy.

This is exactly what I think about OOP object hierarchies, where one function is distributed over 15 files and you need to keep the state of the object in your mind when thinking about what this function could do.

In contrast when reading F# I often only need a single-pass, because with let bindings and the |> operator I can see how the data goes in, what is done to it one step at a time, and what comes out. It's as simple as it gets. Granted that single pass might be slow, but that's because it is dense and doesn't contain so much extraneous noise, like the boilerplate standard-OOP creates.

If you then work with a team that uses proper railway oriented programming. I.e. not only pure functions but that use the type system to express failure. I.e. a sqrt function that returns Some(sqrt(x)) for x >= 0 and None for x < 0. Then it becomes even more simple and explicit to understand what can go wrong and how that is dealt with. Instead of some sub-sub-sub-function throwing an exception that you never heard about until it happens at runtime.

You can almost never single-pass OOP code, especially if some architecture astronaut that memorized the GoF book had their way with it.

[tome]

> I’m constantly baffled by what functional programmers call “simple”.

This github repo is clearly not for "functional programmers" nor a generalist audience on HN. It's for experts in type theory, graduate students, academics etc.. The word "simple" is relative to that particular audience.

[jimsimmons]

Posting to HN with a title that says “you can” makes your point moot no?

[tome]

Hmmm yes perhaps. Imagine a submission titled "A linear filter for DSP you can solder up yourself in a day". 95% on HN couldn't. Would the response "I’m constantly baffled by what electrical engineers call “simple”." be warranted? Maybe.

[gpderetta]

As someone that has very little idea of what all of that is, I think the title is great and certainly made me consider looking into the implementation.

It might be wildly optimistic, but encouraging people to learn new things, especially by trying, is always a good thing.

[caotic123]

Thank you, it is exactly what I was expecting people to understand!

[Zababa]

I think that's the case for most DIY projects that we have on Hacker News. Most assume that you have lots of X in the first place. It can be lots of experience with programming languages, it can be a lot of space, it can be tools.

[TeMPOraL]

Let me play the devil's advocate. Since you mentioned math's dense notation - perhaps people should slow down when reading functional code too.

You say:

> To think that any human, with any amount of training, can parse such code in one pass is a fantasy.

But that's a big assumption: that you need, or want, to parse such code in one pass. This works when code is so trivial you have to speed-read it so your brain doesn't get bored when going through heaps of letters saying very little - a common problem in mainstream languages. Maybe dense functional code should be read like mathematics - you might need to spend a moment or three over that single line. If it takes 5x longer to parse it, but it's 10x more expressive than equivalent "normal" code, then that's still a 2x speedup.

There are also extra benefits of density/conciseness: brain's equivalent of cache locality. You might need to spend more time reading the thing the first time, but you won't be constantly re-reading it while working on it, the way you'd do with verbose, enterprise Java-style code. Dense notation persists in sciences partly because of that effect.

[kragen]

I've heard that a typical reading speed for math papers is a page per day. In extreme cases, you might organize a semester-long graduate seminar so the participants can help one another understand a 30-page paper that has a result they think is important.

Math notation isn't designed to be as fast as possible to read—not even as fast as possible to read a given idea, much less a given page. It's designed to be fast enough to write that you can write down several forms of the same formula as you go through a calculation or other proof, or that while arguing with someone about something you can write down a formula on a blackboard without losing their attention. Also, it's designed to be compact enough that subtle errors of logic have no place to hide (though often it achieves its compactness by being ambiguous, which provides them with a different place to hide: in what is not stated).

— ⁂ —

My favorite example of the benefits of math notation is the derivation of the one-pass formula for population standard deviation.

Because the average is defined as the ratio of the sum of the data items to the number of data items, the canonical definition of the population standard deviation is the square root of the sum of the squares of the differences between the individual data items and the ratio of the sum of the data items to the number of data items. Now, aside from the fact that this definition is pretty confusing, computing it that way requires two passes over the data: once to compute the sum of the data items, and a second time to compute the differences. That means you need memory enough for all the data, which can be a problem, and it also means that incrementally updating the result for a new data item requires you to recalculate the deviations of all the previous data items.

The one-pass, online method is to calculate the square root of the reciprocal ratio between the number of data items and the difference between the sum of the squares of the data items and the ratio between the square of the sums of the data items and the number of data items. That's not just hard to derive, it's hard to even understand.

That is to say, √((Σᵢ(xᵢ²) - (Σᵢxᵢ)²/n)/n). If you're unfamiliar with math this will seem like Greek to you (partly because it is in fact part Greek), but it's actually not that much harder to understand than the plain English definition in the previous paragraph; in standard two-dimensional math notation it's a little easier. With a pencil or a piece of chalk it's also immensely easier to write than the English definition.

But the real advantage is that, in about four or five lines of fairly transparent formulas, you can derive it from the other definition, in such a way that mistakes are, if not trivial, at least reasonably feasible to spot. Doing this without a computer algebra system requires writing out the whole formula in different forms four or five times, which puts brevity at a real premium.

And that, pace Iverson, is the power of notation as a tool of thought.

[Zababa]

I think there is a big difference between functional programmers and people making proofs with programs.

> Lack of imperative constructs in these languages forces one to nest a lot to be expressive and we get a symbol salad

I don't think that's true. If you really have nothing in your language, you can emulate this with small functions. Most functional languages do have support for "let ... in" which allows you to basically program like in an imperative programming language. There's also another part: sometimes no name is the best name. In imperative programming you sometimes have to either nest a lot of function (like `toto(titi(tata(x)))` with a lot more parameters), or give temporary names that are sometiems not helping at all.

> Unless FP embraces more modular and structured ways of programming it’ll always remain a niche.

> To think that any human, with any amount of training, can parse such code in one pass is a fantasy.

I could say the same for the usual OO/design pattern soup. The difference is that in the last 30 years, lots of people made a lot of money with OO training and consulting, and the same didn't happen with FP. What I'm saying is that it's not an inherent problem of FP, so we shouldn't treat it like such. It's a training/cultural/popularity problem.

> It’s high time we improve ergonomics of both math and FP because the rewards can be tremendous. Rust manages to do some of this to great success and programmers have embraced it so well.

Rust is a good compromise I think. A strong base of FP and imperative, while still allowing the useful OO paterns. However, I think the best innovation of Rust is around tooling, and this is where FP is often lacking. Cargo is a pleasure to use for basic stuff (which is 95% of programming), the compiler is very nice and gives useful error messages (unlike old OCaml/C++ error messages). An interesting fact is that Rust's error messages come from Elm, which is also a functional programming language. You're right about the ergonomics of Haskell and such being a bit rough sometimes, but what I find really baffling is that it took so long to just care about error messages. Rust also has great IDE support, rust-analyzer is impressive. All of that to say that as much as Rust gets some things right by allowing some imperative programming, it also gets tooling right, and that matters at least as much to the ergonomics of a language.

[simion314]

>Mathematics has a similar problem

Really??? you want to do a search and replace all Math text Like replace(" = " , " is equal ") ???

I think that abstraction is a feature we intelligent animals have, it makes the text easy to read and understand, , and much faster, the only downsides is people like you that can't jump over the introduction and just go to the interesting chapter.

Though if I misunderstood you I wish to see how your suggested Math looks like, how you can just jump at random location and read and still understand stuff and how equations without one letter symbols look like.

[jimsimmons]

That’s not better notation. Programming uses equals and it’s fine. Symbol salad is the problem. One needs to control the number of symbols. Using a symbol for frequently used operations is better. For everything else being explicit is better even if it means repeating it a few times or being verbose.

And you’re wrong about abstraction. It only works if the abstractions are solid and non leaky. Most abstractions aren’t. If I gave you education at a high level of abstraction you wouldn’t know much. Human ability is to move between abstractions and create new ones. Not parsing things at an arbitrary level of abstraction. One needs to build abstractions. Not hand over high level ones.

[simion314]

Sorry dude but you don't really know true Math. In Math all is precise, all abstraction is precise, there is no place for interpretation.

When you read a physics book you will see stuff like

F = m * a

this are defined somewhere , you can't just jump at the middle of the book and understand. Is the same with terms, you get teh concepts explained at the beginning where for example it will tell you that mass != weight and what it really represents , a physics paper does not need to get verbose because some random person wants to understand it but at the same time wants to skip the requierments.

Sure, there could be somewhere some bad book/article/paper that is confusing maybe for everyone but that is an exception>

I am still waiting for some proof or example on how this no symbols Math should like? Do we repat the terms definiont all the time , do I need to explain all the time what a natural and real number is ?,what a set and function is ? do I need to explain what PI and e is every-time I use it ? If not do I ask you what you level is and everything you personally don't understand is the thing that I must defined even if I don't target you?

But if you are a dev you should start cleaning up the software side too, like let's stop naming stuff functions what they are not functions, let's stop naming shit int if they are not the real Integers, let's stop using +, * and / because this are not the real thing(they do not respect all the laws in all conditions)

[jimsimmons]

Words are also symbols. When you say it’s defined somewhere means it’s defined in natural language somewhere. Things ultimately get defined in natural language and it’s unavoidable. You cannot take a kid and shower him with symbols and expect him to understand. One needs examples that elucidate the situation and pointers to understand the factors under analysis. You need to write down assumptions like “frictionless surface” or “isolated system”. Sure you can rigoursly try to define them too but eventually they’ll still be defined in terms of other words and sentences which are inherently ambiguous. Euclid’s theorems used an axiom that wasn’t known until 18th century. It’s not due to lack of rigour. It’s due to leaky abstractions.

I’m not arguing for no symbols. Surely the quantity of symbols used is less in Physics relative to math or geometry relative to algebra. Just like a well written physics textbook, there is a middle ground between verbose description and symbolic manipulation. They both have their place and neither can substitute one another.

You have a middle school interpretation of science. Things may seem rigours to you because it’s written in a language that’s a lot more precise than the day to day language we use. That doesn’t mean they are ultimately precise. Even mathematics hasn’t been automated or formalised in a computer. That’s not due to lack of trying. It’s insanely hard to precisely codify mathematical concepts. So imagine, when math and geometry are hard to formalise, how hard physics would be. All fields or models of reality are precise in answering the questions they consider. But they sweep hide swaths of ambiguity under the rug even before the proposing the first formal statement. That is what you need to realise.

[simion314]

I know what I am talking about, I graduated Math, I studied the Fundamentals of Math theory and all the fundamental branches.

You fail to understand that the symbols and terms are defined, the reason you don't understand an equation when you go to wikipedia is either the article is bad or you are not prepared to read that equation.

If we dumb down Math/science articles we will get a similar issue with biology, there are not many symbols in biology so any random dude (including some big ego HN-ers think they are now COVID experts just by reading wikipedia or worse some click farm article linked from social media).

Btw have you read a rigurous book on logic, sets and numbers? a university level one? Is there any ambiguity there so if you have 10 non retard readers you get 10 different Mathematics because some term or operation was not ambiguous?

Computers and software are limited, they are missing the creativity a human has, you can teach software to follow some steps but it will never create any original step so at best you might get computers to verify someone.

[jimsimmons]

You don’t know who I am yet you assume I’m unable to read math. I’ll ga have you know I’ve published original proofs and derived efficient algorithms from doing very delicate math. I’m employed to do this which is something most math graduates can’t say.

I’m not advocating for dumbing down —- rather the exact opposite. People have superficial understanding of things and think they know the subject deeply because they can write a bunch of symbols. But wannabe proofs written by such people lack predictive power or explanatory value. Logic, sets and numbers are precise about the things they address just like a board game can be precise about it’s rules and outcomes. This is not the case for mathematics at large. Doing exercises in the textbook will be unambiguous because the content of the textbook grounds the meaning of objects well enough using verbose natural language. The problems are also small in size. However there is a difference between reading a law textbook vs reading the constitution. Definitions and semantics at the frontiers of mathematics are under flux and consensus among mathematicians is slow. Proofs are large and contain a lot of holes. Without the kind of verbose grounding you have in textbooks, meaning can be quite ambiguous. What is a set by the way? Since it’s a fundamental construct, can you define it unambiguously? Again I’m not asking for the notation of a set. But rather the definition of it. If you were asked to present it to a tribal person with no formal education, do you think the definition you thought of would have the same explanatory value to them? If this constraint made you rethink your definition you see my point.

I’m not talking about any creative aspect. I’m just talking about formalisation. Geometry is notoriously hard to formalise for computers. Take a look at the Lean theorem prover and how hard it has been to formulate large sections of math despite repeated attempts over decades. The creativity you suggest is actually rooted in the pattern processing machine that is the brain which fills in large blanks left out from formal representation and which many mathematicians take for granted without realising the extent of ambiguity it brings.

Your language and usage of R word suggests you’re in an Ivory tower just because you understood a few problems in your textbook at some point.

[caotic123]

You can always use let (in that our case def) to minimize the problem with inlining. I think functional programmers get used to big expressions because they do not inspect every symbol when they are reading, the context gives enough information! But you are correct, I couldn't make it better than its syntax/semantics because the implementation should be also very simple. And yes, PomPom is very simple compared to other proof assistants (we are not dealing only with functional programming but also dependent types).

[saithound]

I think you made good trade-offs regarding the syntax. Your language needs to be simple in the sense that it should not be complicated to parse unambiguously. But it also had to remain somewhat usable.

I think you made a good choice: it's easy to parse, and not all that difficult to read for the people who are likely to use it, after some minutes of deliberate practice.

Sure, it's quite symbol-heavy, and it's not as clean as, say, Agda or Idris. But (after a few minutes of practice) I find the difficulty entirely comparable to reading Coq.

Unsurprisingly, people who by their own admission never use functional, much less dependently typed, programming languages won't find it easy to read. But nothing you can do would make it easy to read for them, any more than you can make Jack Sprat easy to read for those who do not speak any English. To convey what it does, you'd have to write it in an entirely different language, and it would lose its very purpose in the process.

[caotic123]

Also, my current work/job is using Kind as a foundation, the purpose of this language is exactly what you have asked for, give a check on https://github.com/uwu-tech/Kind.

[jimsimmons]

Cool! No offence, I went on a rant hoping to start a discussion about FP. The fact that you have a dependently typed language in 1000 lines is an amazing feat. Don’t want to take anything away from that. I just wish the functional community took readability more seriously is all

[tluyben2]

Maybe it is because of when you are doing this all day, you really don't see this anymore? I can read j/k just fine, as well as Haskell, but I find many imperative languages noisy and basically ugly and unreadable. I like things terse and as much as I can on 1 screen so I don't have to scroll or remember things (when you get older, remembering wtf something was called again gets pretty annoying; very strict static typing and defining types precisely (aka a zipcode or telephone number are not strings!) together with terse functional constructs help a lot; the IDE will know everything so you can focus on implementation).

[devit]

Interesting!

Though it seems to share the problem of all current dependently typed languages of not supporting efficient implementation since everything has to be boxed and there are no linear types.

So you are forced to choose between something efficient but with no built-in dependent types like Rust or an horribly inefficient dynamically typed languages.

[erichocean]

> So you are forced to choose between something efficient but with no built-in dependent types like Rust or an horribly inefficient dynamically typed languages.

Or…use TLA+, which doesn't have types (but you instead define near-trivial type invariants that the model checker checks). This turns out to have a lot less ceremony, while producing extremely useful results quickly.

tl;dr TLA+ is a lot more practical if you care about bug-free software, and not even in the same universe in terms of difficulty as something like Coq. However, Coq can do fancy mathematics that TLA+ doesn't even try to do, so both should exist. (Neither are easy to learn, but TLA+ is much, much easier than Coq.)

I'm familiar with Coq, and reach for TLA+ and Alloy for practical programming. Coq is super-interesting, but ultimately not very practical for programming today. It's very nice for doing weird math stuff though. (You can't do any weird math stuff in TLA+.)

In the end, it kind of depends where you think you'll get the most bang for the buck with formal verification: can you confidently write correct code, if you get the design right? Or are you afraid that even with a flawless design/spec, you'll still screw up the code?

If it's the latter, Coq (and relatives) are what you want, though almost no-one uses the generated (read: provably correct) code. Expect to spend years on anything useful and produce at least one PhD, probably multiple, in the process. It's an absolutely enormous amount of work.

OTOH, if you're concerned that your proposed design might have issues, then TLA+ is many, many orders of magnitude more useful in practice, because it can help you produce a correct design with very little effort (days to weeks). TLA+ helps you find specification errors extremely easily, and the specs (once you get used to it) are easy to write.

Once the design/spec has been tested to work correctly in TLA+ (using a model checker), you still have to implement it (e.g. in Rust), but honestly, that's straightforward once the spec is correct and your mental model of the problem is solid. Highly recommended.

[amw-zero]

Have to jump in on a TLA+ comment, especially one about how it handles “types.” I say this all over the Internet - the way that TLA+ handles types is the absolute ideal from the programmer’s perspective - there is nothing special about them! No special syntax, semantics, nothing. It’s all the same language and logic, unlike most type systems which have a completely separate type language with subtly different semantics.

The problem is, that programmer simplicity pushes the complexity to the type checking. You can’t statically check TLA+ types, you have to model check them which is much more intensive.

Maybe there’s a happy medium.

[erichocean]

> You can’t statically check TLA+ types

I wish I could someday meet a programmer who's main problem, daily, is that their code won't type check. Otherwise, everything's great!

I like type checking, but not because the static type checker helps me write correct code. (When it does, the "bugs" it finds are trivial, at the same level as the syntax checker.)

I like type checking because it makes documentation easier, it makes writing code easier (code completion), because it means I can write fewer comments, etc. Not because of "correctness", and since that's the goal of something like TLA+, I haven't (yet) found myself wishing for it.

Especially with my experience using Coq, the way TLA+ handles types is a breath of fresh air. Simply lovely.

[zozbot234]

> tl;dr TLA+ is a lot more practical if you care about bug-free software

TLA+ is not generally used for end-to-end checking of actual program code, unlike Coq. Usually you build a simplified "toy" model in TLA+ of some architecture of interest, then use model checking to try and refute some claimed properties of that model. If the model checker finds a refutation of some property, then yes, that's a verified bug in your toy model. If it fails to find one, that's not a proof of correctness other than in very special cases where a property can be checked finitely.

So yes, model checking is helpful in some cases, but it's not a generally useful tool. And there are ways to do the same things in general proof assistants, e.g. by interfacing them with external SMT tools. The TLA language in itself is also unproblematic, it simply adds modalities for time, state and non-determinism to ordinary logic, and there are well-known ways to convert ("embed") those features to a form that a proof assistant can work with.

[erichocean]

> TLA+ is not generally used for end-to-end checking of actual program code, unlike Coq.

To my knowledge, TLA+ is never used for checking program code. At least, I've never heard of anyone doing it.

> model checking is helpful in some cases, but it's not a generally useful tool

I strongly disagree. Spending time trying to "prove" in Coq an incorrect, flawed specification is an insane waste of time. A model checker can show you the problems in (literally) seconds.

Consider Raft, for instance, which was formally verified in Coq. You know what they did first? Write a TLA+ model, and then model check that until they got the design right. Trying to start in Coq (with an incorrect design) would not have been smart.

Model checkers are extremely useful tools.

----

Going further, the TLA+ spec of Raft is less that 500 lines.

The Coq proof of TLA+ is ~50,000 lines. It resulted in a verified implementation that to the best of my knowledge, no one uses in production.

It's a nice achievement, but in terms of usefulness? TLA+ has Coq beat by a country mile.

[nextos]

What do you think about Ada Spark?

[erichocean]

I don't have any direct experience with it.

[zozbot234]

AIUI, the integration of linear types (or substructural types in general) with dependent typing is still a matter of research. Even "simple" type system extensions like higher-kinded types come with a lot of added complexity.

There is also what's arguably a deeper obstacle to "efficient" implementation of dependent types because dependent typing does away with the phase separation between compile-time and run-time. We do have "program extraction" features in many DT languages to mitigate this, but they're still ad-hoc additions, there isn't yet a principled approach to the issue.

[AnthonBerg]

Idris 2 has quantitative dependent types. As far as I know quantitative types contain linear types. Are a superset. Idris typechecks 0 and 1 uses of types (and many).

It’s a great language.

https://idris2.readthedocs.io/en/latest/updates/updates.html...

The locus of the research that Idris’ linear types are based on might be Conor McBride’s paper I Got Plenty O’ Nuttin: https://personal.cis.strath.ac.uk/conor.mcbride/PlentyO-CR.p...

It’s a beautiful paper.

There are other papers in between McBride’s paper and the implementation. They’re great papers too.

I find it telling that the Idris 2 source code for quantitative types in the Idris 2 compiler is beautifully readable and understandable. This is what tends to happen in Idris code. Clarity.

[mbrodersen]

Simple doesn’t mean easy. Making things simple can be hard. Understanding simple things can be hard. Easy means “familiar”. Hard means “very far from what I already understand”. The Lambda Calculus is super simple. But super hard to understand in all its ramifications.

[amw-zero]

You learned one way of programming, and that’s how you think. Nothing wrong with that.

But, many people are used to the functional paradigm. That that’s baffling to you is strange. People have different perspectives.