kmill

27 ms·

211.
by kmill 6y ago
I'm not an expert on the foundations of Lean, but I do know that funext in the source code follows only from the axioms of quotient types and the eliminator for equality. There are a number of axioms that are implicit in the type chec
212.
by kmill 6y ago
I think your comment illustrates a difference in cultures -- mathematicians generally don't care about whether it's bad style in the constructive POV. Sure, you can 'just' stick to the negative fragment, but that '
213.
by kmill 6y ago
That's true, but there's an amusingly odd theorem (downwards Lowenheim-Skolem) that implies that if set theory has a model, it has a countable model. So, in a sense, all sets are countable. I think this just leads you to the nex
214.
by kmill 6y ago
Sort of the official policy is that inside proofs (i.e., terms of types in Prop) constructibility doesn't matter, but inside definitions (i.e., terms of types in Type 0 and above) try to be constructive. For example, it is ok to defin
215.
by kmill 6y ago
I use the mapsto arrow frequently for higher-order functions, and it seems to work fine for me.
216.
by kmill 6y ago
I've been thinking about this since my original comment actually, but there are complexities from using the noncompact group R. The exponential functions are still the simultaneous eigenvectors of time shifts. The Laplace transform se
217.
by kmill 6y ago
It's "fine" for imperative programming if you never make a mistake: the problem is that it is extremely permissive and won't stop execution on errors. I usually add my own error checking and default cases to cause progr
218.
by kmill 6y ago
Sometimes the way I explain Mathematica to people is that, where Perl is the Perl of string rewriting, Mathematica is the Perl of tree rewriting. Some comments about the article: Mathematica has two types of rules, Rule and RuleDelayed, giv
219.
by kmill 6y ago
A pattern like _List matches lists, but the match isn't associated to a variable.
220.
by kmill 6y ago
The left-hand side of the arrow is a pattern expression [1] (though usually you'd use the :> arrow to delay evaluation of the right-hand side). The "full" notation is x_H for a pattern variable x that needs to have head H.
221.
by kmill 6y ago
I use notebooks primarily -- it would be nice if syntax highlighting didn't put x+y in scary red :-) Something I've wondered: would it be possible to support With[x = 2, x + x] when there's just a single variable? It's
222.
by kmill 6y ago
It's because the eigenvectors of the collection of all time shift operators are the exponential functions, and if you want to stick with real functions, then sin(ax) and cos(ax) together form a basis for the sum of the ai and -ai eigen
223.
by kmill 6y ago
I think it's that exponentials simultaneously diagonalize time shifts, derivatives, and integrals. Convolution follows from these -- though there's something to be said for putting convolution above derivatives and integrals in i
224.
by kmill 6y ago
I'm sure there are subtle bugs, but it seems to work in a simple case: SetAttributes[Have, HoldAll]; Have /: HoldPattern[CompoundExpression[x___, Have[s_Set], y__]] := CompoundExpression[x, With[{s}, CompoundExpression[y
225.
by kmill 6y ago
I'd never seen UpSetDelayed used before (I've always used the longer /: notation), that's interesting. A silly idea I was thinking about is supporting With[{x = 2}]; With[{y = 3}]; x + y for With[{x = 2},
226.
by kmill 6y ago
I'd thought math was the part of philosophy dealing with ideas that are precise enough to say things with certainty. (No matter how well-qualified and vanishingly relevant those ideas might be ;-) )
227.
by kmill 6y ago
I've never thought about adding upvalues to CompoundExpression -- what kinds of applications have you used this for?
228.
by kmill 6y ago
You might find the book "How Equal Temperament Ruined Harmony" interesting, which presents a reasonably strong case that pre-1900s western music treated enharmonics as distinct pitches ("enharmonic" in the old sense seem
229.
by kmill 6y ago
Something that works rather well is taking ratios a/b with, say, a and b in the range 2 through 10, and then changing a or b by a small amount and avoiding a=b. You get some nice harmonies if you have multiple of these running simulta
230.
by kmill 6y ago
Oh, that's a great visualization! (And that's a wonderfully low-tech way of animating it.) I appreciate the Johnston notation, too, which made it easy for me to follow. The Well-Tuned Piano [1] also has a really nice lattice, tho
231.
by kmill 6y ago
I have basically zero knowledge why the hyphen moves as well, but from having talked with someone a while back who was very excited about ZK-SNARKs, I think they're named to refer to the Lewis Carroll poem The Hunting of the Snark. (An
232.
by kmill 6y ago
Resumable exceptions are still used in Common Lisp, in the form of the condition system. There have been a few recent posts about it on HN, including one about a new book. I think the key is that the system lets you specify multiple resumpt
233.
by kmill 6y ago
I read through the MIDI 1.0 spec last night, and I was very surprised to see it said nothing about default note number to pitch mappings, other than that 60 is middle C. The only time frequencies seem to come up is for the (optionally imple
234.
by kmill 6y ago
That's close but not quite how I meant for the notation to be interpreted: f is an argument to an anonymous function. Maybe clearer is swap = f ↦ ((x, y) ↦ f(y, x)) The rule this satisfies is swap(f)(x, y) = f(y, x) and the type for s
235.
by kmill 6y ago
Pretty much the same idea, but in math contexts I tend to use the \mapsto arrow (↦), since mathematicians are more familiar with this than lambda calculus. (The fat arrow seems like an interesting alternative in programming contexts, but I
236.
by kmill 6y ago
I thought it was more of an accident? The story I know goes that Church used hats over variables, and then he switched over to lambda prefixes for ease of printing.
237.
by kmill 6y ago
I've mostly used Pure Data patches or a C program I wrote that interfaces with Jack. I like Johnston's notation for extended just intonation, and the C program lets you press buttons on your MIDI controller to alter notes by the
238.
by kmill 6y ago
I've had lots of fun experimenting with JI, but I think you're greatly understating the difficulty of using a scale like that for conventional music! Basic chords (like ii) are horribly out of tune due to the syntonic comma, and w
239.
by kmill 6y ago
> Eg Conway’s notation for knots I'm not sure how well-known this is, but Conway notation can be thought of as taking a Tait graph of the knot (i.e., a checkerboard graph) then reducing all the series-parallel networks until you get
240.
by kmill 6y ago
Kauffman has some papers with Buliga about graphical lambda calculus -- it seems like it's working with the string diagrams for a reflexive category, but with some extra goodies from an algebraic structure. I was about to say "oh,

More ›