ImprobableTruth

Metaprogramming does not require dynamic types, but this post seems to equate them. As far as I can see all this could be done in e.g. Java (and probably is).

IME this kind of "magic" very quickly loses its appeal when you have to debug it. The author's idea of libraries wrapping this stuff up so users don't have to care about it just doesn't pan out at all in my experience.

Fat pointers are a purely value level construct. STLC alone covers that. Non-determinism isn't really related to the lambda cube, even CoC is deterministic.

I think it's down to having a lot of feedback data due to being a service, SD has its aesthetics ratings, but I assume it pales in comparison.

The "intimidate" meaning of buffalo is in a bunch of dictionaries, I just checked. Regional slang, I guess?

...C. I thought the context here made it obvious, the person I replied to was talking about programming in a procedural manner and eschewing abstractions.

I never even mentioned anything that even relates to runtime types, I don't know why you'd bring them up?

And saying that classes, inheritance and overriding are orthogonal is bizarre. They're intricately linked and at the heart of OOP. It doesn't even make sense to define overriding without inheritance.

>In the end OO and FP are anyway the same thing at the core. You can mechanically translate one into the other:

Coinductive types have destructors so they look a bit OO-ish, but that's it. The key part of OO isn't having fields, but inheritance.

IMO types are fundamentally about restriction. Limiting the shape of your data and what you can do with it, so that this information becomes explicit - making it easier to reason about the program, both for yourself and the compiler. I think this is illuminated very well by sum types. If you have a variable of X | Y, you know that it's either exactly X or Y. You can pattern match, to handle the case that it's an X and then you call a function on it and you know exactly which function it is.

Inheritance is so nightmarish to me because people tend to use it in such a way that I often don't have the slightest clue what I'm actually dealing with, buried under layers of indirection that seem to serve absolutely no purpose. If I have an object of class X, is that actually an X, or something that just looks like it and actually behaves differently because someone decided to override a method in a subclass?

Interfaces tend to be much less monstrous IME, so I don't think the issue is with abstractions themselves. Especially when people use interfaces to abstract over common behavior between data types, rather than trying to future proof for something that never occurs.

Linearity is exclusive to Idris 2, compile time only values/run-time erasure are supported by all major proof assistants. Coq and Lean have the Prop type (compile time only) while Agda allows annotation of variables as run-time irrelevant.

Imo the biggest difference is the "heritage", Lean is Coq inspired, Idris Agda inspired. This manifests in how people prove things. Idris has dependent pattern matching, so proofs are written as normal terms. Lean has tactics and proofs are small tactics scripts (which then generate the proof term behind the scene).

Other than that, the difference is mainly in infrastructure/libraries and community.

Are you saying that these systems are just copying? Do you think the avocado chair is a copy and that nothing learning-esque occurred?

>claiming that automobiles are really the same as bicycles, just faster. Except automobiles resulted in major shifts in both behavior and policy, and there’s a reason people don’t ride bicycles on the autobahn.

But speed (and weight) is the key difference. If cars were just really fast and heavy bikes, would anything change? I don't think so. It's purely quantitative, rather than qualitative.

It might be that the quantitative differences make generative systems harmful (though I'm not convinced), but that's not substantiated by claims about it not actually being learning.

I mean, duh? Why would anyone with half a brain sue Midjourney, when it's unknown what it's trained on, let alone OpenAI, who are additionally backed by Microsoft? It's pretty clear what case has the best chance.

If you have an immutable structure, you can't just modify the leaf of it. Unless you're arguing that deep, immutable structures are an issue in themselves?

Imagine you changed it from an array of approvals to a single one like in the original example - you'd need to make a change in every method of that type (replacing the map). That's code duplication, it's just not really obvious yet because there's only two layers to pass through. Per layer you need a constructor call (or map to copy & modify the array).

As a more obvious example, if you want to modify a.b.c.d.e (which isn't unrealistic), you'll need to call the constructors of A, B, C and D. If you don't use lenses, this is the code that will be duplicated. You can spread it between the classes or do all that in a method of A, but if you want to also modify a.b.c.d.f, you'll need to duplicate all that code (add another method to A, B, C, D that each calls the constructor).

With lenses, you define once how to access d from a and then any modification of d can happen through that. If the structure changes, you only need to do the changes once by modifying the lens.

Lenses are an abstraction of what you mentioned. For a single example it's of course overengineering. The benefit is that e.g. when you have a bunch of methods like that, you can avoid duplicating the code that is responsible for copying the inner layers. Otherwise if you e.g. add a layer, you have to touch all those methods.

Yeah, it's also originally from the FP side. There it started I believe because people were looking how to easily make immutable updates to deep structures, since the normal way is pretty boilerplate heavy in comparison to the mutation way of just chaining accessors for an update.

And you're close, it's about using immutability to make value equality cheap by making reference equality a proxy for it. If you don't use mutations, value equality implies reference equality and is thus equivalent (since reference equality already normally implies value equality). That means you can get away with just a single pointer comparison in comparison to completely traversing both structures. This is e.g. what React does to determine whether arguments of a component have changed.

(Well, at least I also struggle to think of a scenario where both types of equality are semantically important).

I don't think I understand. We're talking about how to implement this. That method will still have to use deep copying + mutation, lenses or something else internally.

The issue is that this potentially copies a lot of unnecessary information. Also, if you depend on object identities (reference equality), deep copying will recreate objects even if they aren't supposed to change. Furthermore, if you want to chain two update functions, you'll deep copy parts of the object twice times.

Lenses are "smart" in the sense that they only copy what's necessary.

If they also give you the means to just do it yourself?

Imo something like dall-e or midjourney is much worse.

How does this relate to not telling people which rule they violated?

They said a C-free build. For that you'd need to "just" rewrite the core kernel, which will be 150-200k lines, and the drivers + arch specific parts for one system. Still a tall order, but a decade isn't unrealistic if Rust proves itself.

Now, rewriting everything, including all the legacy drivers? Yeah, never happening even if Rust succeeds utterly.

What do you think hidden layers do?

Tarn has made an off hand comment about it before [1], but I'm not sure how serious it actually was.

[1] https://www.pcgamer.com/if-dwarf-fortress-sells-millions-on-...

The article links multiple papers on chain of thought reasoning. There are tasks that language models struggle with, but when you ask it to explain its reasoning, certain large language models do much better than the scaling for the normal prompt would suggest. Calling this an 'ascribed quality' is crazy, it's just an observation and says nothing about the internals. Hell, you could even test it yourself if you don't trust the papers.

Saying that it just looks like P(text|internet) is a tautology, it's a text predictor trained on the internet. This doesn't tell you anything about why phenomena like the above occur, or why it occurs only in large language models and only in some of them.

Now that money worries are (hopefully) not an issue anymore, I really hope they consider releasing the source code.

Due to being written in C++, mods are quite restricted in what they can do (especially in comparison to more recent games like Rimworld that are trivial to decompile due to using C#). Especially frustrating because performance really isn't up to par - a lot of the old generational forts from a decade+ ago are really only possible now if you tailor your gameplay to account for performance issues.

I'm very certain that this is an external filter (that is, separate to the core LLM itself) - just like e.g. if you ask it for opinions.

I think they just mean indie rather than open source.

What is Wittgenstein's thesis?

Provides a perverse incentive for people to breed rats/cobra effect [1]

[1] https://en.wikipedia.org/wiki/Perverse_incentive#The_origina...

I refuse to believe that anybody who compares LLMs to Eliza has interacted with the technology for more than 10 minutes.

(using a non-Coq notation and using a newer form of coinductive types)

Inductive types are built using constructors. An example, defining two lists:

l1 = nil

l2 = cons 1 l1

Induction/recursion principles (fixpoints + pattern matching) consume them to produce some other value.

Examples:

length nil = 0

length (cons x xs) = 1 + length xs

For coinductive types it's the inverse. Coinduction/corecursion principles (cofixpoints + copattern matching) produce them. Take streams with the destructors hd : Stream A -> A and tail : Stream A -> Stream A). By defining how it's destructors work on the stream, we define a stream blink : (Bool -> Stream Nat):

hd (blink True) = 0

hd (blink False) = 1

tail (blink True) = blink False

tail (blink False) = blink True

blink True is the infinite stream 0101010101010101... To consume the stream, you call the destructors on it (and receive the defined result).

Now, just like how records are inductive types defined via destructors, the same can be done allowing coinductive types to be defined via constructors. In Coq this is called positive coinductive types and they're the original form of coinductive types introduced to Coq (and the only one until ~2019), but they're also not exactly well behaved, which is why it's now recommended to use the negative form, though e.g. this paper still uses the positive form. If you want to know more about this, I'd recommend reading the Coq documentation :-)

>Also curious how they interact with the termination checker

While infinite, negative coinductive types don't pose any termination issue because they're lazy - blink only 'describes how to deconstruct it' and does not do any computation of its own. So if you apply a finite amount of destructors to it, you only get a finite computation.

(positive coinductive types are a bit more tricky - there's a special productivity condition for them.)

The US has a larger population than the entirety of western Europe and it's easily the largest western country. I'm not from the US and I'd still consider it the default by sheer size.