codebje

6 ms·

181.
by codebje 1y ago
The system being demonstrated only has three effects: World, State, and Stop, and all the valid combinations of those are given at the very end of the document. As far as I can tell, these natural transformations are equivalent to the type
182.
by codebje 1y ago
The post I replied to was speculating on IPv4's life being extended by "simply making the numbers bigger" rather than having more bits per byte, but nevertheless... there still would've been a transition, delayed by at m
183.
by codebje 1y ago
If you "simply" added more bits to IPv4, you'd have a transition every bit (ahaha, ahem, sorry) as complex as the transition to IPv6 anyway, because IPv4+ would be a new protocol in exactly the same way as IPv6. A new DNS res
184.
by codebje 1y ago
Async is monad shaped. Not-async is monad-shaped, for a degenerate monad. Writing a function that works in both async and not-async contexts just means writing a function that works for any monad.
185.
by codebje 1y ago
If you want a function to be usable in both an async and a non-async environment, the monads in question are ones for async and identity, not IO. The choice between a true concurrent runtime and a single threaded cooperative coroutine runti
186.
by codebje 1y ago
8051s pretty much mean Keil - they used to do license dongles, but it's all online now. You really don't get much more established than the 8051. If you pick up any cheap electronic product and crack it open to find a low part cou
187.
by codebje 1y ago
Sadly, paid compilers still exist, and paid compilers requiring a licensing dongle still exist. The embedded development world is filled with staggering amounts of user hostility.
188.
by codebje 1y ago
Guaranteed employment is tricky to get right. How do you provide minimum wage jobs that are not soul-crushing, without destroying the private sector soul-crushing minimum wage jobs? How do you even find productive jobs people would want to
189.
by codebje 1y ago
Maybe very long term. I turn off code assistants when doing Lean proofs because the success rate for just suggestions is close to zero.
190.
by codebje 1y ago
None of this is as straightforward as it seems. A "for" loop in Python isn't particularly cheap. It compiles to some static overhead to set up the iterator, then each loop iteration compiles to the "FOR_ITER" opcode
191.
by codebje 1y ago
You did, but it might not be an effective strategy to mention asymptotic complexity to help forward your argument that one linear implementation is faster than another. Whether it's a win in Python to use one or two loops isn't so
192.
by codebje 1y ago
DOI has nothing to do with blockchain. There's no great looming issue with resolving the legitimate origin of published material. There's no provenance problem to solve. There's a registration problem, that has been solved, a
193.
by codebje 1y ago
I write a bit of literate Haskell, sometimes. It's one of the most well supported literate programming systems out there: the compiler supports it, the language server supports it, using VSCode as an "IDE" means full support
194.
by codebje 1y ago
Ah, my apologies, I wasn't particularly clear. The "best" I am referring to is only code generation into popularly used languages. I'm currently using Lean myself, but Agda's probably going to win out longer term fo
195.
by codebje 1y ago
The languages people already use are inconsistent (in a logic theory sense) and lack formal semantics. Efforts to try and prove anything useful about programs written in those languages don't get far, because the first fact requires yo
196.
by codebje 1y ago
On types, I think there's a philosophical argument about whether types can be values, and a related one on whether types should be values, but I think I disagree with the author about what a value is, because as far as I understand it
197.
by codebje 1y ago
On running code at compile time, what this reads as to me is evaluating constant expressions at compile time. We're thoroughly used to compilers optimising constant expressions away for us: "if 4 < 2 then a else b" will us
198.
by codebje 1y ago
It’s a confusing (and confused) article. The parts on type systems are expressing IMO a fair observation that dependent types are weird and hard, but without any sense of understanding what they are or what they can do that might justify th
199.
by codebje 1y ago
If someone cold calls me and asks me to verify myself, I refuse. If it’s an expected call or they give me a good reason to, I’ll call their listed contact number back. So far I have not missed out on anything of consequence by refusing to i
200.
by codebje 1y ago
They’re all double the last dimension plus two, without skipping any in that sequence - but that offers no insight into why it wouldn’t hold for 254.
201.
by codebje 1y ago
No, but they do (did?) have a vast ocean of Perl, and I did know a hacker or two who got hired to work there on it.
202.
by codebje 1y ago
I once updated a little shy of 1mloc of Perl 5.8 code to run on Perl 5.32 (ish). There were, overall, remarkably few issues that cropped up. One of these issues (that showed itself a few times) was more or less exactly this: the iteration o
203.
by codebje 1y ago
It's probably https://www.good-display.com/product/440.html which is also 1mil refresh cycles and a fast refresh time of 1.5sec - around 185 hours of screen updates, so ~3 months of 5hrs a day typing or a few year
204.
by codebje 1y ago
The main advantage of recursive descent parsing is readability. Forget the machinery of the parser, which is (a) trivial enough that AI will generate correctly it for you with next to no prompting, and (b) widely available in libraries anyw
205.
by codebje 1y ago
Here's one paper covering the derivation of a typed functional LALR(1) parser in which derivations are given explicitly in symbolic language, while proofs are just prose claims that an inductive proof is similar to the derivation:
206.
by codebje 1y ago
My experience in reading computer science papers is almost exactly the opposite of yours: theorems are almost always written in formal symbolic language. Proofs vary more, from brief prose sketching a simple proof to critical components of
207.
by codebje 1y ago
I love your Overcooked mod.
208.
by codebje 1y ago
Haskell has a type system that lets these things be directly useful in ways they cannot be in many other languages. You can't, in Java, declare anything like "class Foo<F<T> extends Functor<T>>", or use a si
209.
by codebje 1y ago
I am not yet sure whether it's a third mistake to think that it's particularly relevant to understand monads (and friends) outside of a language with (a) the higher-kinded types necessary to actually use them, and (b) a type syste
210.
by codebje 1y ago
One source for confusion around lists is that the list monad is often used to model non-determinism, rather than just "many things". If you're thinking about non-determinism, a list is akin to a container of one item when you

More ›