tel

47 ms·

451.
by tel 10y ago
Classes and functors are still a bit orthogonal. There are tons of things you can do with classes nowadays depending on what language you're working in, but essentially, fundamentally, functors are about types and classes are about val
452.
by tel 10y ago
To be honest there's a lot of old information out there about Haskell's packaging. Today, I just use stack and it's completely fire and forget. The default template will build you a little executable and a companion library a
453.
by tel 10y ago
> special syntax at the call site Definitely Haskell's game then
454.
by tel 10y ago
Even "just IO" in Haskell enjoys some very nice typing properties and is often easier to write and ensure proper operation than similar "just IO" programs in other languages. It's actually super pleasant!
455.
by tel 10y ago
I imagine that given linear arrows you could write something like Rust's Rc/Arc?
456.
by tel 10y ago
Laziness gives pure semantics to a certain form of mutation. Technically you don't represent cycles but instead the infinite unfolding of that cycling structure... but you do so in a way where the compiler just makes the cycle. In pure
457.
by tel 10y ago
There are lots of programming styles where the programmer must ensure the invariant that some piece of data (value, reference, pointer, whatever) gets used in exactly one sequence. Normal types can ensure that functions and arguments fit to
458.
by tel 10y ago
No, as it turns out in presence of recursion it's undecidable to know that in general. Inference in a linear logic system can answer when it's possible some of the time. Programmer-written annotations can assert it's the case
459.
by tel 10y ago
Basically, non-linear variables are those with infinite duplication and sinks (they're "comonoids").
460.
by tel 10y ago
Or SuperCollider or any demo of a standard synth plugin dropped into a free VST host (like dropping a demo version of Massive [0] into Reaper [1]... though Reaper technically not free). [0] https://www.native-instruments.com&#x2F
461.
by tel 10y ago
This is Stretch Tuning, right? https://en.wikipedia.org/wiki/Stretched_tuning
462.
by tel 10y ago
I think that's exactly what they do sometimes though: and disclaim directly that This Is Not Legal Advice and I Am Not Your Lawyer. At this point they can take it easy and recommend literally anything since the most painful ramificatio
463.
by tel 10y ago
I see what you're saying now and quite like that. Thanks for clarifying!
464.
by tel 10y ago
> be Bayesian on the inside Strongly disagree, tbh. Picking one side or the other in this debate is silly. Don't "be Frequentist" so as to avoid Bayesian model building techniques since you'll end up stuck all the tim
465.
by tel 10y ago
- Where did this difference come from? When did it develop? I'm not sure of the specifics but it (a) appears to be a fundamental dichotomy on ways to practice "finding a good model" given statistical mathematical foundations
466.
by tel 10y ago
I'd also like to point out that there's a huge policy impact of one method over the other. Since Frequentist and Bayesian methods disagree in how we should construct and evaluate models then almost of all scientific practice is
467.
by tel 10y ago
Statistics is about finding a model of the world that we can trust. A model in this circumstance must be one that makes predictions about the world and therefore we trust it when we expect that its predictions will be largely correct—or at
468.
by tel 10y ago
It's a little weird. lvalues and rvalues are different things so a biased symbol feels nice to me, <-, e.g.
469.
by tel 10y ago
This example along with all the similar ones drives home the basic idea that probability is tied to its model and its model is often best phrased as a generative story. If we agree on the generative story we'll agree on the model and t
470.
by tel 10y ago
Hardly. It'll imply that any language could get stuck or fail to terminate but UB is something different.
471.
by tel 10y ago
The real heart here is that program analyses have opened doors to optimizations that cannot be represented at the level of the language (LLVM IR). This is super convenient for compiler authors who want a flexible IR for optimization purpose
472.
by tel 10y ago
Definitely, it's super weak but at the same time constructive. The issue is that it essentially ends up becoming a search algorithm where contradiction is backtracking. If the search algorithm doesn't stumble upon the solution (at
473.
by tel 10y ago
For finite proofs, proof by contradiction can be interpreted as continuation passing and then results in an algorithm. On the other hand, this algorithm may be no better than exhaustive search.
474.
by tel 10y ago
Quite apart from the proof theoretic advantages others have mentioned, it's sort of a big leap of faith to believe LEM = (for all propositions P, P or not P). For instance, the continuum hypothesis: unproven and still controversial. We
475.
by tel 10y ago
Fwiw, this is called the BHK or Brouwer–Heyting–Kolmogorov interpretation. It's a way of providing a model of intuitionistic logic in the same way that "sets" provide a model of classical logic. Intuitionistic logic this shou
476.
by tel 10y ago
"Derive absurdity" comes from the fact that in these logics there is only one statement which is "Absurdity"—capitalized perhaps. It's a unique thing to talk about and "an absurd conclusion" is actually sh
477.
by tel 10y ago
"... in many practical branches of pure and applied mathematics" On the other hand, there have been many mathematical papers written there this distinction was key. It all depends upon your topic, really, and how many times you ha
478.
by tel 10y ago
They feel that there are some sorts of statements ϕ for which ¬¬ϕ = ϕ is invalid. Or, more interestingly, that if we force it to be such that all statements have that property then we lose the ability to talk about certain interesting thing
479.
by tel 10y ago
At a very broad philosophical level---which is something one must assume if you're going to talk foundations of mathematics---"formalistic" logic makes a really unbelievable assumption: All facts are either true or false. G
480.
by tel 10y ago
Intuitionistic logic is a subtype of constructive logic, though, so it's more specific. That said, a lot of people don't make the distinction!

More ›