kmill

17 ms·

91.
by kmill 4y ago
You should see the speedrunning videos on YouTube!
92.
by kmill 4y ago
We also support HTTPS over at https://secure.endless.horse/
93.
by kmill 4y ago
Co-creator here; but endless.horse was entirely Colleen's idea. It's wonderful seeing this pop up occasionally. As boing boing once said, it's not called endless for nothing. We personally use https://secure.endles
94.
by kmill 4y ago
This reminds me of a very curious feature of GPT-3. Whenever you ask it for a joke, no matter the way you set up the prompt, and so long as it has free reign to tell the joke, it will almost always give the chicken crossing the road joke. B
95.
by kmill 4y ago
> Submarines do have their own sonar, but using it comes at a price – loss of stealthiness.
96.
by kmill 4y ago
Is the content of your comment that you are explaining ad hominem to me and that vanderZwan's question requires mutual trust? Yes, I fully understand this. The only thing I am trusting here is that vanderZwan is trying to accurately re
97.
by kmill 4y ago
Where are you getting that they'd want to "dismiss you?" Smart and well-informed people can come to different interpretations of reality that are accurate in their own ways. It's interesting to know what sorts of consequ
98.
by kmill 4y ago
Search for "5mm red led" to see what they're talking about
99.
by kmill 4y ago
This is another fun geometry game: https://sciencevsmagic.net/geo/ I liked how it incentivizes finding efficient constructions, which made it competitive with friends.
100.
by kmill 4y ago
This reminds me somewhat of Stanley's symmetric chromatic function, which I guess came about ten years later (1995). Actually, what you're describing seems to be something I rediscovered a couple years ago, where P_k is interprete
101.
by kmill 4y ago
Is the first part similar to the "W function" from Tutte's A ring in graph theory (1947)? If I remember correctly, it generalizes the chromatic/flow/Tutte polynomial to yield a linear combination of disjoint union
102.
by kmill 4y ago
I think one thing that this could help with is that, even if you are proficient in Lean, finding the way you are supposed to translate an informal statement into Lean/mathlib can be time-consuming if not a challenge -- it is a very lar
103.
by kmill 4y ago
If there's a point to any of this, I think it's monads let you package up some algebraic structure in the form of a function `m a -> a` that satisfies certain properties, and then you can pass such a function around without any
104.
by kmill 4y ago
Here's another way to say the general idea, by way of example. Secretly, list is "the" exemplary universal monoid. Given any `a`, then `list a` gives you the free monoid generated by `a`, with composition given by `++` and th
105.
by kmill 4y ago
I agree with you that there's no inherent magic to the monad concept, but there really is something neat about the monad generalization -- it's not just a senseless abstraction. That meme "a monad is just a monoid in the cate
106.
by kmill 4y ago
I thought kerning specifically referred to small adjustments in spacing between pairs of letters. This just seems to be a failure in honoring the spacing for the different TeX math mode symbol classes. The rel and op classes each have a ce
107.
by kmill 4y ago
You really can simulate laziness in a strict language at the small cost of wrapping things in lambdas yourself -- you don't have to figure out what operations you can do yourself so long as you make everything that should be deferred d
108.
by kmill 4y ago
In strict languages, you can delay computation by wrapping it in a zero-argument lambda -- i.e., a "thunk." For efficiency, you want to memoize thunks (that's what Haskell does[1]) so that they only ever evaluate once. Schem
109.
by kmill 4y ago
I think it's like how in sexual selection, many animals display traits that take additional energy to maintain. The theory is that this is selected for since if a potential mate is able to display these traits while still being alive a
110.
by kmill 4y ago
Here's a verbose Lean calc proof using single rewrites: import tactic example (R : Type*) [comm_ring R] (a b c d : R) : a + b + c + d = d + b + c + a := calc a + b + c + d = a + b + (c + d) : by rw add_assoc
111.
by kmill 4y ago
It's pretty easy in Lean/mathlib: import tactic example (R : Type*) [comm_ring R] (a b c d : R) : a + b + c + d = d + b + c + a := by ring It takes about 50ms to parse, process, and type check this example, with
112.
by kmill 5y ago
I've messed around with this same graphical language, though only on paper. As I understand it, the lambda/apply nodes are the two morphisms for reflexive objects[1], and these are something like string diagrams for them -- though
113.
by kmill 5y ago
(Sorry a1369209993, I got confused about HN threading -- somehow I thought you were responding to me.)
114.
by kmill 5y ago
Thanks for taking the time to explain your terminology. I've found a couple of things about partial equivalence relations (one neat one was on nlab about how the construction of the reals can either be a quotient of a subset of sequenc
115.
by kmill 5y ago
The definition is just saying that "<=" is reflexive. When it says it's "a homogeneous relation on a set P that is reflexive, antisymmetric, and transitive," the meaning of P being a set is that it's an obje
116.
by kmill 5y ago
I'm not sure what you're talking about by saying that this is the correct behavior for a partial order. In every definition of a partial order that I've ever seen, there is a pre-existing notion of equality (which is an equiv
117.
by kmill 5y ago
For what it's worth, the Python example isn't too relevant since it's hiding a number of intermediate variables (that said, swapping without intermediate variables tends to be more of a curiosity anyway -- and a motivated per
118.
by kmill 5y ago
Ah, for illustration purposes this is showing a "one-shot" button. Notice the "fire" state is a double circle -- this means that it's a terminal state for the state machine, meaning the state machine is "done&q
119.
by kmill 5y ago
Sometimes I think about what it were like if land rights were structured as limited-term exclusive-use licenses. The licences are offered in recognition of the fact that it takes time and money to develop the land, so the licensee, by takin
120.
by kmill 5y ago
They'd probably be delighted to hear that you're reading the book (and it wouldn't hurt to mention that you think it's good!) You could mention that, and ask about the causality problem, why it seems backwards compared t

More ›