LightMachine

Exactly. This is so infuriating. Whoever let little-endian win made a huge disfavor for humanity.

How do you find Discord servers for a specific interest?

Ethics aside, if we could simulate a whole brain, then we could simulate billions of brains and try all sorts of things, something we wouldn't be able to do with physical humans. At least not without being labelled as mass murderers and turning into a bird.

Just replied to let you know that you have an amazing take on the matter.

If 75% of the users want something, of course they can do that. They uninstall Bitcoin, implement a new software with the new rules, and install it. This becomes the new "Bitcoin". That is called a hard fork. You can't prevent that because it literally means people just chose to use something else. They may even keep the name and call the new thing Bitcoin, for what it is worth.

That isn't what polymorphism means, polymorphism would be more like Point<Float> and Point<Double> using the same Point definition.

I have a good answer to you. It is not unlikely the universe is made out of Interaction Combinators. That's purely because those are arguably the most elegant model of computation. Of course, elegance is on the eye of the beholder and it is hard to express why I believe that, but I do, so feel free to have a look and judge yourself. Even if I'm right, though, how useful is that? Not at all, I guess. As you said, anything equivalent to a Turing machine could be running the universe, so even if we figured out the specific model "used" by reality, this wouldn't be that useful.

I wonder if I should take those opportunities to talk about Formality (https://github.com/moonad/formality).

You have a point

Precisely. Food for thought: IOTA nowadays is not only fully centralized currency (in any meaningful technical sense), but it also has a much higher market cap than Bitcoin had a few months ago. So, is the market really valuing decentralization as much as we think?

Sure, if you wait for a sufficiently large weight on top of your transaction, then you solve the double spend problem. But you need at the bare minimum that every transaction that happened at roughly the same time as yours to be included as an indirect child of your tips. If you do not understand that sentence, please try to, as it is the very reason that IOTA doesn't scale (and isn't fundamentally different from usual blockchains in any sense other than a somewhat contrived construction).

You do not even need to use dependent types. You could just restrict yourself to polymorphic types if you wanted to. And you could use dependent types just for the things that don't require any "proving" work. Returning multiple types from a function, implementing type-safe `printf`, checking out-of-bound errors at compile time, things like that.

Dependent types allow you to express things such as `a == b` as a type, and proving that requires some work, but you don't need any of that at all. Idris is a superset of Haskell, you may say.

... why a question I asked 4 years ago is on the first page of Hacker News?

That's a scary thought.

There is no competition to Ethereum in terms of back-end decentralized computer, AFAIK. I picked Swarm because of familiarity and being closer to the devs. I don't know the IPFS devs. I do find both projects awesome.

It was designed to allow a client to run code submitted by other clients safely on the browser without isolated environments. It is an important building block for a decentralized-application browser I'm developing. In the soon future, you will be able to publish a decentralized application with an one-line command. It will be stored on Swarm (decentralized Store), will use Ethereum as the back-end, and anyone will be able to access it using a decentralized browser such as Mist.

So, in short, remember the Pirate Bay idea of putting drones around the world to host their sites, allowing it to stay up forever without censure? Moon does exactly that, without the drones of course.

Those wars are actually quite healthy and productive for the whole, because they make people defend their sides and thus develop their best arguments. They're a great source of information. You just have to be careful not to get emotional and/or degrade to name-calling.

Thanks for sharing your experience! EMACs is another masterpiece on its own merits and I'm all for diversity. Also, hijacking the top comment on my own post to say the obvious: people, this is just my opinion! I'm not saying you shouldn't use and love your IDEs because I like VIM! Love you all. Peace!

eli5?

I agree with everything you said.

On doing that in Idris (which is my dream language - the only reason I don't use it is its JS compiler is too slow), would it be possible to randomly generate elements of any data type, or would we have to write an `Arbitrary` instance for every type you want to test? I don't know/remember much about generics on Idris, would love to learn more.

(Seriously, though, why is the JS compiler still so slow? Again - I'm willing to put substantial money into funding a better one...)

Oh. Thank you very much for linking that. I wish I saw it 3 days ago, though. It is basically the same thing.

If it quacks like a type and it types like a type...

Just kidding! A type system, in essence, is not much different from that, though - Pi, for example, is basically a type-level lambda that is applied to the typed function (and it is sufficient to express basically any real-world type system). In any case, I hope I made it very clear on the that it is in no means an actual type system, but my dirty way to get invariants and some refined types on plain JS. If we had a mature Idris->JS compiler this hack wouldn't be necessary. ):

Which is a great thing for the whole

Not sure I understand how that is possible. How would you implement a boolean "and" with only "mov"? If you can only move stuff around, how do you read and compare things?

I wrote this after trying to find something to keep state in check for React applications and noticing a lot of over engineering and a lot of misunderstandings about FP even from libs that claimed to do it. I hope this isn't too stupid for this (site), but I really think we should write less code and think a little bit about the problems we are actually trying to solve.

Macros (not necessary at all, just use regular functions and enable laziness), ints/strings/bools/lists/etc and all their hardcoded features (you can encode all that neatly on the λ-calculus). Every single addition that Scheme makes on top of λ-calculus is harmful in some sense - algorithms on list, for example, don't fuse because of that, making Scheme less performant than the λ-calculus; multi-argument functions make the whole language segmented and are much less convenient than curried functions... etc., etc.

R5RS, the simplest used spec of Scheme, takes dozens of page to merely describe the language. The λ-calculus can be described and implemented in a paragraph. That makes it much easier to create new backends, for example.

Of course I can, much faster. Maybe you do not see how high level the λ-calculus is... take a look on the Caramel syntax. I can translate line-by-line any Haskell program to Caramel. The λ-calculus, when given a decent syntax, is just Haskell without the types (but still has algebraic data structures identically, just no annotations). And I can be much more productive in Haskell than in Scheme, I think that goes without saying.

About the performance of the program itself, yes, λcalculus is faster than Scheme, by an order of magnitude, sometimes. For one, algorithms on church-encoded lists fuse by reduction, which means that the code below, in Caramel:

    map f (filter cond (zipWith (+) (map f a) (map f b)))

fuses to a single tight loop - i.e., it iterates through the lists `a` and `b` only once, and returns the result after that, creating no intermediate structure. Scheme would create 4 intermediate structures on this case. Since it is already 2~3x slower than the λ-calculus (running on GHC), that'd make it an order of magnitude slower in that case.

Specifically because Lisp/Scheme, as simple as they are, still add a lot of complexity on top of the λ-calculus that isn't needed at all. In fact, I think the λ-calculus has a shield against this very issue on Lisp/Scheme, which is the fact is is much easier to quantify what is the "best" abstraction for a given problem.

Are dolphins on the top of the food chain? I thought they were predated by whales and sharks?

I think it doesn't make sense for it not to be. It seems like a very good way to transfer data with almost no drawback given a decent setup. I don't understand why that isn't used more often.