gugagore

that matches

> it's the speed at which the sample pointer consumes the looping sine that's set to correspond to some frequency

The rest of your message doesn't make sense to me. Both phase and frequency can be modulated, perhaps most clearly seen with FSK vs. PSK.

Simply-typed lambda calculus guarantees that the computation terminates. Sometimes you need non-termination. Fixed point operators is one thing that brings in all the stuff that you threw out.

Linear logic is good for the bits and pieces of concurrency where you don't need concurrency. Linear logic guarantees that there are no race conditions. Sometimes you need race conditions — how do you fit that in there? Sometimes, having race conditions is really important: I am selling tickets and there is going to be a race for who gets the last ticket. Is there a single thing you can add to linear logic that would give me race conditions? Not known. - Philip Wadler on Type Theory Forall #54 - The Goal of Science is to Communicate Ideas!

That's not entirely true. Locomotion is well addressed by RL in sim. It's true that there is still a PD layer, and the RL policy produces setpoints for it.

I understood you to be saying "bundling is encouraged", in the sense of

https://leanprover-community.github.io/glossary.html#bundled...

I'm not sure it's encouraged. I agree that it felt natural to define a type like NonNegativeInteger, or a wrapper type like `Sorted(T)` to indicate that that wrapped list is sorted. But I think this is an area of style and aesthetic that is still emerging, far from ossified.

The problem of "threading" new things within existing programs is an important one to address, and it has multiple solutions (context management, dynamic scoping (lol), implicit arguments, type classes). I am curious if the claim of "does not scale" is mitigated by one of those solutions...

To each their own!

Do you want to give two different types to complex numbers, depending on whether a given complex number represents a point versus a transformation (an amplitwist)?

The distinction is whether zero is meaningful independent of a choice of origin. Zero displacement is meaningful. Zero position is arbitrary.

Are you thinking of displacement as an operation? Because it is just as well a vector. I don't see the connection to section I highlighted from the article.

> Most of the time we think of complex numbers as vectors in R2 or as rotation+scaling operators, but rarely do we actually we want them in both roles at the same time. So it is not very natural to equate the two objects, as opposed to finding a correspondence between them.

> So GA ends up being very stuck because it equates “vectorial objects” and “operators that act on vectorial objects”. It would be better to express all the geometric objects you care about in their most natural forms, and then find isomorphisms between them when it’s necessary to do so. Otherwise all the meanings get blurred together and it’s very confusing. So that’s another problem with geometric algebra: eliding the distinction between vectors and operators is undesirable, confusing, and disingenuous.

Even if that's true, you definitely do not want to attempt merge two lock files, and using the .gitattributes file to set the merge strategy is a good idea!

A related technology with a name that already answers your question.

I'm guessing is what they're really talking about. Which is not about NAND gates.

I have a suspicion that Julia, owing to multiple dispatch, has a sort of regularity that makes that you said plausible.

Though there is just so much more Python to train on, any I bet they even do RL with validated rewards on Python, and probably not Julia.

I am not myself a woodworker, however I have understood that part of what makes it "crafty" is that the woodworker reads grain, adjusts cuts, and accepts that each board is different.

We can try to contrast that to whatever Ikea does with wood and mass production of furniture. I would bet that variation in materials is "noise" that the mass production process is made to "reject" (be insensitive to / be robust to).

But could we imagine an automated woodworking system that takes into account material variation, like wood grain, not in an aggregate sense (like I'm painting Ikea to do), but in an individual sense? That system would be making judgements that are woodworker-like.

The craft lives on. The system is informed by the judgement of the woodworker, and the craftperson enters an apprenticeship role for the automation... perhaps...

Until you can do RL on the outcome of the furniture. But you still need craft in designing the reward function.

Perhaps.

I know that there was OO hype, but 1981 seems kind of early. I also know that OO means many, many things. What does it mean here, if anything?

But only some groups have the ability to systematically encode language as writing.

Writing is a technological marvel.

    - simply typed lambda calculus
    - System F
    - dependent type theory (MLTT)
    - linear types
    - row types
    - and so on

This is true. As far as I understand it, there is not a type theory basis for Julia's design (type theory seems to have little to say about subtyping type lattices). Relatedly, another comment mentioned that Julia needs sum types.

I think it can be all of these things, which in my opinion partially undermines the GP's point.

Recommended related musings: https://wiki.c2.com/?ClosuresAndObjectsAreEquivalent