pchiusano

> My reasoning was to just benchmark identical programs.

I would just report the results of a parallel Haskell program as well, and let people decide what programs they think are comparable. I don’t really think you come off well making the speed claims you do since many people who bother to dig in will conclude you are comparing apples to oranges.

> After all, it just returns the same result, faster.

That is not always true. There’s some overhead to introducing parallelization so it’s not always worth it unless you have a big enough chunk of work.

But the other reason fine grained parallelism isn’t often worth it even if it can provide a speedup for a single computation: you have other concurrent things going on, and plenty of potential parallelism from that. Think of a web server responding to many concurrent requests. In this situation, your program could easily have worse performance by injecting parallelism within each connection. Imagine we have k cores and k concurrent connections - we would likely be better off just giving each connection one core rather than having them all thrashing each other to use all the cores.

> Don't you find it compelling to write binary addition as "increment N times" and have it be as efficient as the add-with-carry operation?

It’s very cool in a “wow that’s neat” kind of way, but, well we already have machine ints that are even faster. :) I feel you need better examples to be compelling - people just don’t care very much about optimizing Peano arithmetic. If those speedups generalize to things people do care more about then you should show that and then people can be impressed! It sounds like you do have some ideas for examples, and I think your point about getting deforestation “for free” is cool… but, show us!

My other question - it seems like this approach requires giving up on separate compilation? Like you can’t compile a function in isolation, since it will do completely different things when composed with other functions? Or am I misunderstanding?

This is very cool research that I’ve been loosely following for a while but I feel the benchmarks you’ve presented are very misleading. They are comparing parallelized code to sequential code and then making a big deal that it’s faster. Of course, you could also write a parallel Haskell version of the same benchmarks in about the same amount of code, and I’d expect similar speedups.

Haskell doesn’t parallelize every independent expression because it’s a general purpose language and that’s unlikely to be the correct choice in all contexts.

I don’t have much of an intuition for whether the optimal evaluation stuff will be useful in practice for the kinds of programs people actually write. Like I get that it helps a lot if you’re doing multiplication with Church numerals… but can you give some more compelling examples?

So what we were going for with the core API is that it should be expressive enough for all kinds of distributed programming tasks, not just Spark-like or batch computing stuff.

We’re planning on doing several of these articles to show different applications. I think some distributed stream processing library would be super cool and there are lots of sources of inspiration for that like you mention. It would be a more interesting translation than the Spark-like stuff though. Likely using the channels ability for message passing.

> By the way, I really loved the FP in Scala book, it was my first step into FP -- thank you and Runar for writing it

That’s great to hear!

Recommend starting with part 1 of the article if you want more of an overview: https://www.unison-lang.org/articles/distributed-datasets/

One of the authors of the article here, happy to answer any questions about it!

https://rodneybrooks.com/a-better-lesson/ is an interesting retort to the Sutton post.

Cool. How does Twain compare to Scotty?

We just started on a project and Servant felt like overkill, but this is the first I’ve heard of Twain.

FYI you can do ‘ucm -codebase /someplace/else init’ to initialize a codebase in another directory.

And then ‘ucm -codebase /somewhere/else’ to launch ucm.

Also I’m not sure what Unison the file sync tool stashes in .unison or how it uses that directory but there might not be any conflict. UCM will just create a .unison/v2/unison.sqlite3 file.

Cool. Related question - how has been your experience working with firecracker VMs, and what led you to that decision? (I’ve been eyeing them for a while to get faster startup times for autoscaling).

GA-style search isn't actually taking multiple samples to decide on a new point to move to - it's taking multiple samples to decide on a smaller region to focus on. This can be more efficient than backprop, depending on how "easy" it is to tell via sampling which subregion has better performance.

Here's a post on this: http://pchiusano.github.io/2020-10-12/learning-without-a-gra...

Traditional GA has a practical problem for training large models - keeping a large population of model weights in memory is not feasible. Like if you had to keep 1000 variations of the GPT-3 model weights in memory for training that's no good. Though people have ideas for how to solve for that as well (again, see the post I linked).

You might be interested in "compact GA" which only requires keeping the % of 1s (or 0s) at each bit position.

I suspect that with some more engineering and attention from people doing ML stuff, GA-style algorithms can be made just as memory and space efficient as gradient methods, while giving better results and being more widely applicable.

Here's a post on this: http://pchiusano.github.io/2020-10-12/learning-without-a-gra...

Here’s a link that works I think: https://mobile.twitter.com/andrejbauer/status/12599019719910...

The supposed selling point of HoTT wrt to formalizing mathematics is higher level proofs that are more general and are less work to express, due to having this richer notion of equivalence in the type theory.

I think the post you linked is pretty good... it makes me wonder - at this point, what is holding back more formalization? Is it a cultural thing? (None of the people who are doing “interesting” math care about formalizing It) Is it a technical thing? (Proof assistants and their type theories aren’t good enough?) Are we just missing a big enough “standard library” of mathematics so mathematicians can get to the interesting parts sooner? It’s probably all of the above.

What I think might happen is it reaches a tipping point where enough of the pieces are in place to where it rapidly becomes normal or expected to formalize mathematics and we have awesome tools and “standard libraries” to make it good.

People find it interesting and fun so IMO that’s the only bar that needs to be cleared to justify the attention it gets. If your pet areas of mathematics are more exciting to you, then share that with people and/or post here and maybe it will get more attention. Or not! I wouldn’t dissuade people from following their interests.

My background - I’m a programmer and like building programming languages. I’m interested in HoTT because I’m interested in type theory generally and also formalization of mathematics.

Most mathematicians don’t care much about these things, which is fine. Like most weird stuff, it’s good that some folks are doing it.

Lastly you might enjoy this thread about why formalization is interesting to another mathematician:

https://mobile.twitter.com/andrejbauer?prefetchtimestamp=160...

Switching speed is very fast with silicon, but we seem to be nowhere near the computing power of the brain, which incidentally runs on an absurdly low 20W. I think this power usage aspect is quite underappreciated.

You might like this article: https://blog.piekniewski.info/2018/08/28/fun-numbers-about-t...

I’d read through the link and see what you think, but TL;DR is that you can still propagate a change everywhere in Unison (and Unison tracks this for you), but even if you’ve partially propagated, you can run all the code that you’ve upgraded so far. So if a change has 500 transitive dependents and you upgrade 7 of them, you can run those 7 (and this might help you figure out that you want to do the change a bit differently) Whereas you’d typically need to upgrade “the whole codebase” before being able to run anything, including code unrelated to the change being made.

It’s true that with static typing, you are usually forced to propagate your changes to “your whole codebase” to get it compiling before you can run any of it. That stinks. However, it turns out you can lift this restriction in static languages, and this is what Unison does:

https://www.unisonweb.org/docs/refactoring

In Unison you can implement a change and propagate it just far enough to run one little experiment. There’s no need to upgrade all your code at once.

Also maybe of interest: “The advantages of static typing, simply stated” https://pchiusano.github.io/2016-09-15/static-vs-dynamic.htm...

I don’t know if you feel this way, but my complaint about the more hyped cloud services is that not only can they be expensive (fine) but the promised time-savings and simplicity of operating the system often doesn’t really materialize either, except in restricted circumstances that you don’t appreciate in advance and only find out later after you’ve already committed.

If it really did save time and were simpler, some companies would (quite reasonably) be willing to pay a premium for that - time is money and all that. In reality it seems like people often end up with the worst of both worlds - it’s expensive, complicated, still needs a huge staff to maintain, and doesn’t even work that well.

I think you are making a hidden assumption. Here is a good question to tease it out: why does it make sense to ask why a coin flip came up heads but not make sense to ask why we observe one QM outcome?

With the coin flip, it’s understood that the probability distribution is not reality. It’s just a way of approximating reality without having to model all the things that would explain our observations.

With QM we have equations that predict probability distributions, and there is debate about whether reality is literally a distribution of possible states, or if it’s more like the coin flip random variable.

The thing missing is an explanation for why we find ourselves in a particular branch. Insisting that this doesn’t require an explanation is never going to be satisfying for some people.

I’ll try to explain why, using your random variable sampling analogy, which is telling. In the case of say, sampling from a coin toss random variable, there is indeed a more primitive explanation for why the coin comes up heads or tails, it’s just that it would be a much more complicated explanation involving knowledge of huge amounts of detail about the exact force applied to the coin, maybe air currents in the area where coin is being flipped, etc. But in principle that is all explainable.

With quantum measurement, there is no such explanation available, even in principle. We are told only that we will find ourselves in one of the possibilities admitted by the distribution predicted by QM. We have no further explanation for which one it will be. The QM multiverse folks then expect us to be okay with this as the end of the explanation. But notice this is a choice to adopt something as axiomatic. We could have done that at other points in the history of physics but didn’t.

It’s not much different. That doesn’t mean DM is wrong, though! Logically, there’s two possibilities: laws of gravitation are 100% correct at all scales and the discrepancies we see at level of galaxy rotations, etc, are due to matter we can’t yet observe in other ways (hypothesized dark matter). Other option is gravity dynamics are in need of further refinement, much like GR refined Newtonian gravity. Or some combination... maybe GR isn’t the full story but dark matter is also a real thing.

Earlier discussion: https://news.ycombinator.com/item?id=19605065

I think there’s often sloppiness in how things are stated - dark matter is inferred based on observation of X (edges of galaxy rotate too fast) and an assumption that GR is 100% correct. X is then said to be “evidence for DM”, but there’s that unstated premise.

Wow, I had the exact same experience. Would never bother with it again.

Ok, so epistemologically we can’t know what reality “really” is, only what we observe, and we can come up with models that fit our observations. Your (I’d say vacuous) point is that my model of reality that includes a chair is epistemologically on the same level as a model of the cosmos that includes dark matter... though it’s also on the same level as a model that gravity is caused by invisible purple dinosaurs. :) So this perspective doesn’t really get us anywhere in judging models of reality.

I’d say models are useful when they are simple and predictive. Dark matter isn’t really predictive, it’s what is hypothesized to compensate for the prediction error of our current model of gravity. (Doesn’t mean it’s wrong but am just pointing this out)

So I don’t think dark matter is inherently problematic, just that it’s not predictive and it’s worth considering whether the model of gravity we have needs tweaking instead (much like GR refined Newtonian gravity).

I think your response makes sense (neutrinos are another example where the theory predicted an as yet undetected particle and it was eventually found).

But the other reply to your comment is good too - at what point, after failing to detect any OTHER signs of these invisible elephants, do you wonder if there’s other explanations? What it would take to falsify dark matter, given that you can invent it in whatever distribution you like to fit the data?

There’s nothing that logically compels us to assume the existing model of gravity is correct, and its discrepancy with observation is explained by assuming the inputs aren’t what we can observe. It is also logical to consider that the existing model of gravity isn’t quite right. Of course any tweaks to gravity have to be compatible with a lot of other observations but it would be wrong to rule out the possibility of an alternate model.

You might be interested in quantized inertia http://physicsfromtheedge.blogspot.com/ which is a model that does away with the need for dark matter and that has been gaining some interest. For instance, author claims it replicates the success of MOND but also predicts where MOND and GR both fail (see wide binaries posts on the blog).

I 100% agree that when the model doesn’t fit the data, making up some hitherto undetected kind of matter, distributed in just the right way to explain the discrepancies, is kinda odd... the QI author is constantly complaining about this.

Could you link to your source?

I recall seeing some research on this topic but I got the impression (perhaps wrongly) it has to make so many simplifying assumptions to get a result that it’s not clear how much carries over to real systems where not all those assumptions hold.

Cool. :) Not sure how well this came across in the post but I was trying to be careful to say that even though there is a tendency for intelligence to arise (it is really more that evolution tends to accelerate its own rate of adaptation over time, for the reasons I gave in the post, and intelligence is the eventual result), whether that tendency plays out for a particular run of the tape may depend on many things. As an analogy, think of the long term trends of evolution like the force of a river, and the biosphere’s evolution like a pebble in that river. Maybe the pebble will be carried a great distance in the direction of flow, or maybe it will get stuck someplace at the bottom of the river for a million years. In that sense, pointing to the historical record of evolution is misleading and too much detail — IMO you have to distill evolution to some computational essence in order to reason about whether it has any long term trends.

Something that I don’t think is well known is how likely it is that evolution will get stuck or reach equilibrium (how often will the pebble get stuck), but I think it’s wrong to say there is no long term tendency.

Also see this other post which talks more about this, see the Getting Stuck section - https://pchiusano.github.io/2018-04-14/intelligence.html

Related, this post has a simple argument for why intelligence IS a long-term trend in any evolutionary process:

https://pchiusano.github.io/2018-04-21/evolutionary-methods....

So intelligence isn’t a fluke adaptive trait, it’s something that evolution tends toward. While I think it’s possible for evolution to get stuck (and perhaps this is very common on other planets or even on earth if we could replay the tape), it does have an arrow pointing in the direction of intelligence.

Random question, but did y’all purchase a different license from Zero Tier the company or is the GPL on ZT somehow not relevant for you given how it was deployed or used? (And if so can you elaborate?)

Random thought: I'd be curious if results hold up after drinking sparking water regularly and the novelty of it wears off. Like is any of the effect due to an associations in your brain triggered by the carbonation.