siraben

34 ms·

361.
by siraben 6y ago
> generalise the beautiful relationship between cut-elimination and beta-reduction in type theory, to cut-elimination and parallel composition + hiding How would you generalize the correspondence between cut-elimination and beta-reductio
362.
by siraben 6y ago
Hm yes. For instance the monoid of endofunctions on S would require one to prove that f . id = id . f = f. In vanilla dependent types this needs the extensionality axiom added, but in category theory it definitely is fine to speak of equali
363.
by siraben 6y ago
> For now we explore the language of a topos. There are multiple views, and often its full power is not used. Toposes support geometric logic, predicate logic, and moreover dependent type theory. We emphasize the latter: dependent types
364.
by siraben 6y ago
> Dependency is pervasive throughout mathematics. What is a monoid? It’s a set M, and then operations m,e on M, and then conditions on m,e. Most objects are constructed in layers, each of which depends on the ones before. Type theory is
365.
by siraben 6y ago
A good introduction to categorical logic is [0], introducing the simply-typed lambda calculus along with the categorical semantics for each construction (cartesian closed categories). The later sections include topics mentioned in this arti
366.
by siraben 6y ago
> In Rust, pattern matching breaks down as soon as your IR contains pointers to its children > Another way this manifests is that it’s often frustrating that patterns aren’t first-class; I can’t pass around a pattern, or build up a p
367.
by siraben 6y ago
> Is there anything like a linear state monad? Yes! Tweag has a blog post[0] on how there are two different kinds of Functor, linear and non-linear, and in turn, variants of Applicative and Monad. [0] https://www.tweag.io&#x2F
368.
by siraben 6y ago
This attack demonstrates one of the problems outlined in the Nix thesis[0], that is the problem of nominal dependencies. That is, dependencies of the dependencies, build flags and so on are not taking into account, and in particular, the so
369.
by siraben 6y ago
Correct. In a sibling comment I posted the actual script I used that scrapes and dedupes, and a "spoof only" mode to lessen the chance of a collision.
370.
by siraben 6y ago
Since I have no use for it anymore, here is the script[0]. I wrote most of it during a free period :D [0] https://gist.github.com/siraben/c3133b39e470d1aed16fd71f42b8...
371.
by siraben 6y ago
My high school provided MacBook Pros to students that would only connect to the network if the MAC address was whitelisted. Since I wanted to use my own newer Mac, I spoofed the address of my school provided one. Since it was an open networ
372.
by siraben 6y ago
More connections between FP and OOP: - Codata in action[0], FP emphasizes thinking about constructors, OOP emphasizes thinking about eliminators - Existential types[1], having higher-ranked types lets you express dynamic dispatch - Lenses[2
373.
by siraben 6y ago
How does GoboLinux distinguish between packages of the same version compiled under different environments, or compilers, flags etc.? In Nix such changes cause the resulting build to be prefixed in /nix/store with a different hash.
374.
by siraben 6y ago
This was fun to play around with, but I wish that there was also a mode to arrange the notes in the circle of fifths, since that places similar key centers next to each other. In the chromatic layout when you perform a chord progression (e.
375.
Google cutting off API access to Chromium-based browsers(twitter.com)
11 points by siraben 6y ago|1 comments
376.
by siraben 6y ago
Locking a stale issue seems a bit excessive to me. Nixpkgs, an extremely active repository (> 109K issues and PRs) has the stale bot configured to mark the issue or PR as stale[0] after 180 days. [0] Example: https://github.co
377.
Several tech vendors cutting ties with Parler(twitter.com)
3 points by siraben 6y ago|0 comments
378.
by siraben 6y ago
Lira[0] and its readable paper[1] is a good example of abstracting smart contracts into a statically typed, domain-specific language that describes the contract precisely at a high level. It's not Turing complete, which works for a la
379.
by siraben 6y ago
Reading the AWK Programming Language book, it's amazing how little has changed in decades, I can still run the code snippets in 2021 in the same way I would have in 1991.
380.
by siraben 6y ago
This reminds me of one of the closing remarks of Simon Peyton-Jones in his A History of Haskell talk[0]. "Haskell is great fun, it's rich enough to be useful but the thing that I think is really important about it is that it&#x27
381.
by siraben 6y ago
The reMarkable tablet, Supernote A5/A6 are some pretty hackable e-ink tablets.
382.
The Lasting Lessons of John Conway’s Game of Life(nytimes.com)
2 points by siraben 6y ago|0 comments
383.
by siraben 6y ago
สวัสดีปีใหม่! Can't wait to see what the community is up to in 2021!
384.
by siraben 6y ago
Given the context of OP I was genuinely initially fooled, though the audience reaction and visual effects gave it away. Truly chilling stuff.
385.
by siraben 6y ago
I used to do this for macOS and Linux but it was a fragile approach, since using Nix and NixOS I've had great success using home-manager[0] which takes care of what software is installed and any overrides or patches I desire. I also us
386.
by siraben 6y ago
Writing a Lisp transpiler is a great exercise, and becomes more involved but more also educational as the source and target language become more and more distant. Here's my Scheme to JS transpiler that supports higher order functions,
387.
by siraben 6y ago
This website recommends Brave, how does that compare to using something like ungoogled-chromium? IIRC Brave has extra activity regarding its use of cryptocurrency integrated with browsing.
388.
by siraben 6y ago
Right, so it's not that it's not possible but rather it's somewhat awkward to express non-compositional folds in the final approach. I'm not currently aware of a mechanical way to do the translation.
389.
by siraben 6y ago
Ah ha, but you see, you can perform transformations on tagless-final terms that are not strict catamorphisms. Oleg demonstrates this in (page 14)[0] with examples of reassociating binary expressions and double negation, so matching two leve
390.
by siraben 6y ago
I'm curious about the emphasis on fixpoints and lattices. These are two quite simple concepts often overlooked in CS and emphasized even less in programming languages. Lattices are natural to CS in that any time you have an order or ev

More ›