tel

32 ms·

301.
by tel 7y ago
Algebraic effects are a popular subclass of effects, but not all effects of use in programming (or worthy of study!) are algebraic. The simplest example is the continuation effect. It's not immediately clear why this effect isn't
302.
by tel 7y ago
I'd argue this is incredibly common if you write a codebase without a specific, concrete effect stack. In Haskell, the mtl library offers constraints on types mandating that they support at least some effect. These compose together
303.
by tel 7y ago
Good point.
304.
by tel 7y ago
There’s nothing wrong with an infinite sum, in principle. You can’t usually define them unless you can use recursion. In the case of integers you can do data Int = Positive Nat | Negative Nat data Nat = Zero | Succ Nat
305.
by tel 7y ago
Yeah, I hesitated there. But at the same time, many JavaScript objects are just named tuples. That intuition is ok.
306.
by tel 7y ago
There are sums at the type and value level. If I define Color = Red | Blue | Green, that’s not a use of a type which sums types together, but instead just is a type composed of a sum of values. So a “sum type” can be any type which is the s
307.
by tel 7y ago
Summing is the act of gluing two components together with “or”. It’s possible to see all types as sums in this fashion (this is essentially “distributivity of addition over multiplication) but it’s also impossible to see char/int/
308.
by tel 7y ago
Don’t mind my nitpicking. A huge part of algebraic data types arises from products and sums just as discussed here. As is always the case, there is hairiness between metaphor and precision, but presenting these ideas in JavaScript like this
309.
by tel 7y ago
While I really like these blog posts for keeping things light and intuitive, they're also sprinkled with claims that go a bit too far. > Arrays, Objects, Maps, WeakMaps, and Sets are all algebraic data types This isn't
310.
by tel 7y ago
The question is phrased to mislead as this is a constraint satisfaction problem over the boolean space 2^6. There may be 0, 1, or many correct answers.
311.
by tel 7y ago
It might also be a side effect of how maps in the mountain west and mid west tend to visually overemphasize the impact of those regions. They have low population density and large area, so they can be more sensitive to smaller target popula
312.
by tel 7y ago
I've been really enjoying Picturing Quantum Processes by Coecke and Kissinger. It approaches QM by exploring Quantum Processes in terms of a sort of formalized flow diagram. Notions like entanglement and teleportation are pretty simple
313.
by tel 7y ago
A strong functor is one which supports the strength operation above. Haskell -> arrows being based on any lambda term are rich enough to make all Haskell functors strong. But not all functors are! And “non-string” was just a typo.
314.
by tel 7y ago
Ah, I misunderstood! And yes, absolutely. An even easier example data Nullity a This is a perfectly valid functor, too. Ignoring undefined, there are no values of it, but fmap cannot be used to create values of the mapped type, jus
315.
by tel 7y ago
> Hmm. if haskell types make up a small category that means 'a' and 'f a' are sets. I can't imagine a case where two sets cannot have a mapping between them. Can you give a specific example? This is incorrect in
316.
by tel 7y ago
What's hard about that? C and D are Hask. F_Q maps objects A to objects Const Q A, and fmap takes functions in Hom(a, b) to Hom(Const Q a, Const Q b). We identify that Const Q a is just a little subset of Hask, so Hom(Const Q a, Const
317.
by tel 7y ago
Sorry, you're right. I wasn't thinking with subtyping. Rockostrich demonstrated the other weakness of this approach, but I'll say it outright: if you return a supertype then you've lost information. It's very import
318.
by tel 7y ago
You don't. Of course. Honestly, you don't need much more than a really big chalk board to solve most problems one encounters when programming. Even that's probably strictly optional if you get enough people to double check th
319.
by tel 7y ago
Very much agree... but also want to be a little soft here. It's a very specific line of reasoning needed to discuss the difference between a "structured set", an algebra, a "theory" (algebraic or geometric or othe
320.
by tel 7y ago
Algebra is pretty overloaded. In the context of the study of "abstract algebra" the term takes on the more generic representation. You can also see it being defined in places like Lawvere Theories and F-Algebras. It's a conte
321.
by tel 7y ago
That gets closer to the problem, but the solution is further away. You don't want to return "Functor" (which is like a vtable, the interface itself) but instead the thing itself which is implementing the Functor interface. So
322.
by tel 7y ago
Calling these things algebraic structures might help you win some confidence, but the communities which talk about algebraic structures aren't going to be helpful for learning how to program with these things. Mathematicians love algeb
323.
by tel 7y ago
I agree that you can—I've done that in Coq, though I don't have any experience with Lean. The advantage of Agda is that everyone else does, too. This provides two things: one, there's a huge set of examples of how people have
324.
by tel 7y ago
Coq is definitely the best documented. Unfortunately, the tendency to use the tactics language—while incredibly practically useful—obscures how the structure of proofs relate to their theorems. This isn't really a problem per se, but i
325.
by tel 7y ago
The title is a bit misleading. The author doesn't really discuss whether computers can perform the act of proving. He's mostly focused on whether computer languages can represent proofs (yes) and whether computers can check them (
326.
by tel 7y ago
I’ve done Colemak and came back to Qwerty for two reasons that are really compelling, I feel. One, I program so I make lots of weird motions anyway. When writing long prose, Colemak felt nicer but for coding typing it wasn’t a big change. I
327.
by tel 7y ago
Point free can totally be abused. It's also, in my opinion, often very useful for clarity. It's my experience that, especially with FP code, often the important things to write down are the stages/steps in a transformation
328.
by tel 7y ago
It is pretty incomprehensible. It relates to the nature of words like "proof" and just, without and doubt, those are tricky concepts. There's also a lot of implied background. It sounds simple to say what's going on in
329.
by tel 7y ago
Probably, I didn't check it. I think the actual answer is messier: fromIntegral on a, b, and c.
330.
by tel 7y ago
The same sensibilities apply in Haskell. These sort of longer, more structured problems are exactly when do notation comes out do a <- [1 .. 29] b <- [a+1 .. 29] guard $ gcd a b == 1 c <- [b+1 .. 29]

More ›