hither_shores

> misleading manner by labeling speculative ethical behavior as “EA” when it’s neither effective

I agree that they're ineffective, but I don't see any evidence that the MIRI types are lying - they're trying to help, they think they're helping ... and they're mostly wrong. It happens.

> But this kind of bootstrapping of classroom ethical dilemmas into actually diverting donated money away from human welfare efforts astounds me.

Are you sure that's what's actually going on? Donations and especially effort are not fungible. The techy libertarian futurist types in the MIRI orbit, for instance, are so far as I can tell simply not as bothered by poverty as Singer et al. A world in which they're not worried about AI risk is not a world in which they give just as much to other causes; it's a world in which they give less.

I don't know about "EA rationales", but rule utilitarianism is unpopular among philosophers largely because it's believed to collapse into act utilitarianism. The phil101 caricature is that rule utilitarianism says "no stealing, because 'no stealing' is a rule that increases utility" and act utilitarianism says "steal if you think it maximizes utility" - but on the one hand "no stealing, except for bread to feed your starving child" is an even better rule, and so on; and on the other hand not incorporating uncertainty into your decision procedure isn't being a good act utilitarian, it's just being an idiot. And so in practice they endorse the same decision procedures in pursuit of the same end.

> what precisely has the EA movement done to reduce, even marginally, the risk of a nuclear war?

Nothing that I'm aware of. In general I think that most of the current "longtermist" organizations are useless - but that doesn't mean they're incorrect.

When did I say it did?

> Consequently, we should divert money away from the welfare of people living today and towards efforts that maximize the likelihood of a galaxy filled with colonized planets. If that sounds ridiculous, it's because it is.

It sounds ridiculous to you because you framed it in an uncharitable way. Another way of saying "maximize the likelihood of a galaxy filled with colonized planets", so far as contemporary people are concerned, is "minimize the likelihood of civilizational collapse". Even a marginal reduction in the risk of nuclear war, for instance, would be a very good thing.

If by "EA the organization" you mean the Center for Effective Altruism, it came out of the Oxford philosophy department.

> Haskell is basically a category theory framework.

Haskell probably draws more from category theory than any other mainstream language, but in absolute terms that's still not very much. It's okayish for modelling cartesian closed categories, but if you want any more structure than that things get quite painful. Even something as simple as a category with finitely many objects requires stupid amounts of type-level boilerplate.

> You could rephrase Lisp as a Unityped system, but I seriously doubt it would be consistent.

It's not. (x -> x) is always inhabited, so if you have a fixed point combinator (x -> x) -> x then every theorem is true.

No, it isn't. A star-autonomous cartesian category is just a preorder. Chu(Set, n) is star-autonomous but not a preorder, and therefore not cartesian. Or more concretely: cartesian categories are models for type systems with copying and deleting, but the Chu construction builds a model for a linear type system.

There's not really a connection here, the category of vector spaces isn't cartesian closed.

> Was Tolkien right leaning himself, I would be surprised by that but I honestly don’t know.

Yes, but the small-c conservative Catholic sort of right-wing. He would have hated reactionary modernists like Thiel.

> But some sets of data and some operations on them that fulfill some formally stated requirements are just an abstract algebra, aren't they?

Not quite. A variety of algebras (which is usually what people have in mind when they talk about "algebraic structures" in general) is a collection of operations with equational laws, meaning that they're of the form "for all x_0, x_1, ... (however many variables you need), expression_1(x_0, x_1, ...) = expression_2(x_0, x_1, ...)", where the expressions are built up out of your operators.

Fields are the classic example of a structure studied by algebraists which is nonetheless not a variety of algebras: division isn't described by equational laws, because it's defined for everything except zero. This makes fields much harder to work with than e.g. groups or rings, in both math and programming.

> Addition is move and multiplication is also a move. a + b move from 0 a step then b steps. a * b is move a step b times.

By "move" do you mean adding 1? If so, then no. Consider, for instance, the complex numbers: multiplication by i isn't any sort of iterated addition.

> It's mentioned later, but the "math friendly" versions satisfy the axioms of a group and a field, which only works if the modulus is a prime.

The integers mod n >= 1 are always a group (under addition), only the field structure requires prime n.

> Imagine I want to test a function that operates on quite large application state but not all app state is necessary for that function

If not all app state is necessary for that function, it shouldn't require the whole app state in its arguments.

     type AppState = { databaseConnection: DatabaseConnection, env : "dev" | "prod", apiToken: string, userId: string, ... } & SomeOtherStuff

     const dropTables = (app: Pick<AppState, "databaseConnection"> & {env: "dev"} ) => app.databaseConnection.dropTables()

Conversely, if a function you don't control says it needs the whole app state, believe it.

> Whether or not a particular email address is verified or not isn't something that's generally known at compile time

Yes, obviously. What is knowable at compile time is the stuff that comes after: given that the input to this function has property X, does the output have property Y? Arguments, not premises.

> But... (1) you can do the very same thing without types

Sure, and if someone makes an SMT-solver-oriented language (that isn't just using it to drive type inference) I'll be happy to try it out. But what most people who dislike types claim is that you can replace them with testing (true in principle, false in practice: no one actually remembers to test every last edge case every single time) or just programmer discipline (lol).

> sendToEmail sends to any kind of Email.

That's my point, you don't need a combinatorial explosion of behaviors for every possible most-specific-type, you can just reuse existing ones.

> And if the code wants to know if an Email is verified, it inspects the verified field.

That's exactly what you shouldn't do. Runtime "type" inspection is just bad overly distributed parsing. The point of typing is to move errors to compile-time.

    emailLaunchCodes = (email: VerifiedEmail): Promise<void>  => ...

This doesn't need to inspect anything, because the type signature guarantees that someone else has already handled that.

> Whether you centralize the verification code (or otherwise have a separation of concerns for it) or not is independent of whether you use the type system to express when an email is verified or some other mechanism.

Separating the verification code - which is table stakes, really - doesn't guarantee that you're not accidentally adding or losing "verification" elsewhere. Types can and should.

     newtype ArbitrarilyLabeled x = ArbitrarilyLabeled x
     
     forgetLabel :: ArbitrarilyLabeled x -> x
     forgetLabel (ArbitrarilyLabeled x) = x

What's the "global meaning" of `ArbitrarilyLabeled`? What control has `forgetLabel` lost?

Java and its consequences have been a disaster for the human race

> You'll need sendToUnverifiedEmail(email: UnverifiedEmail) and sendToVerifiedEmail(email: VerifiedEmail), and have code to get the right type to pass to the right function the in the right circumstance...

Only if you're using a language with an insufficiently strong type system (e.g. Java, C#)

in typescript:

    type UnverifiedEmail = { address: string, verified; false }
    type VerifiedEmail = { address: string, verified; true }
    ...
    type Email = UnverifiedEmail | VerifiedEmail | FooBarBazEmail

    const sendToEmail = (email: Email): Promise<void> = ...

in Haskell:

    class SendTo t where
         sendTo :: t -> IO ()

    newtype Email = Email string

    instance SendTo Email where
         sendTo (Email address) = ...

    newtype VerifiedEmail = VerifiedEmail Email deriving (SendTo)
    newtype FooBarBazEmail = FooBarBazEmail Email deriving (SendTo)

> I.e., due to a bug, a value of type VerifiedEmail could be created for an email address that is not really verified. Then, your static checks for VerifiedEmail don't help you at all.

Of course they do - they tell you that the bug is in the verification code, and not in any of the thousands of lines of business logic separating it from the place where the error was found.

Yes, but the mapping doesn't change the relationship between the units of measure, which is the actual meaning as far as the type system is concerned. It's just a change of names.

> this is a classic case of not needing more types but needing proper names.

Those are types.

> but I don't think e.g. Haskell98 can do it out of the box in an analogous way?

This is basically the runtime representation of `data Email = Verified { email :: string } | Unverified { email :: string }`, but promoting `Verified` and `Unverified` to type level requires an extension:

    data Email (verified :: bool) where
         Verified :: string -> Email true
         Unverified :: string -> Email false

> That you introduce more coupling is a tradeoff. That the program (sometimes) gets harder to change is a tradeoff.

You don't introduce more coupling, you document the coupling that already exists. If your program is hard to change with types, it would be hard to change without types - but easier to change incorrectly.

> That is becomes easier to write large, messy programs because programmers feel more safe in the future to refactor, is a tradeoff

Sure, I guess this is true in principle - but you could say the same about IDEs, or version control, or grep. The effect size is small.

> since the shared libs have generics and I'm always casting things.

This indicates to me that you're trying to write code that isn't correct (not doesn't work, but rather only works because of implicit couplings between components) and/or doing exotic lisp-style metaprogramming.

In the latter case, yeah, C#'s type system isn't powerful enough. Others are (to an extent: arbitrary code execution at compile time is never going to be completely safe).

In the former case ... that should be difficult. Forcing you to be explicit is half the point of a type system.

It was a leveraged buyout

It's about the meaning, not the raw bits. I might be able to duplicate your signature, but that doesn't mean I can sign documents for you.

"an X is just a Y" is a common turn of phrase in mathematical writing. It means that Xs and Ys are the same thing, whereas "an X is a Y" may, depending on context, mean only that every X is a Y. A human is a mammal, but a human is not just a mammal.

The original quote (from Categories for the Working Mathematician) is:

> All told, a monad in X is just a monoid in the category of endofunctors of X, with product × replaced by composition of endofunctors and unit set by the identity endofunctor.

Journalists don't decide the editorial stance of the publications they write for. In the short term, it's up to an editorial board or editor-in-chief. In the long term, it's up to the owners.

Yes, you (or rather, core library developers) need to pick a data structure appropriate to your access patterns: linked lists for iteration, search trees for concatenation, finger trees for random access, and so on. But you should be doing this anyway for clarity, even if you face no performance constraints.