brokenix

@brokenix@emacs.ch

data Free f a = Pure a | Free (f (Free f a))
⊢ V : C ✓
classical logic corresponds to the mechanism of first-class continuation under the Curry-Howard isomorphism
all partial functions are computable
emacsclient --eval '(my-refresh-foo-bar)'

This profile is from a federated server and may be incomplete. Browse more on the original instance.

brokenix, to Lisp

This is a #lisp machine for network protocols. Initially in pursuit of a social forum focused on link sharing.
as #startups and free projects alike rush to implement some #IETF RFC adding only 'but on the web'. I aim to define a modular protocol server which can support an arbitrary number of network protocols as a network daemon. Our POC in this endeavour will be to build an #NNTP -like protocol daemon which gateways to #IPFS storage. The content held in this system can be consumed by arbitrary clients; a web application presenting #reddit -like services would be just one of many potential clients, although it is likely that Gnus for Emacs will be the first one.
https://codeberg.org/fade/callisto

brokenix, to haskell

quoting @prophet
mli files are mostly used to constrain the visibility of definitions whereas hs-boot files are about allowing mutual recursion between modules (which OCaml doesn't support, even with mli files!)
But the mechanism by which they achieve their goals is nearly identical even though the perception of it is so vastly different.

I guess the conclusion to draw from this is that both sides are wrong: IMO, mli files are not nearly as good as OCamlers think they are, but hs-boot files aren't as ugly as Haskellers think either.
-- prettySrcLoc and prettyCallStack are defined here to avoid hs-boot
-- files. See Note [Definition of CallStack]

Backpack's design is primarily driven by compatibility considerations (“how do we build upon GHC's existing foundation?”), rather than elegance. In particular, Backpack doesn't eliminate those ugly .hs-boot files, it just automates and hides their generation and processing.

For all their faults, Standard ML and OCaml have pretty good support for modular programming. And, as the Modular Type Classes paper you linked shows, type classes can be built elegantly on top of a good modular foundation.

https://cohost.org/prophet/post/3251638-it-s-really-interest
https://haskell.fi.muni.cz/doc/base/src/GHC-Exception.html
https://twitter.com/lexi_lambda/status/1172629363730333697
https://news.ycombinator.com/item?id=11371130

brokenix, to random

Endlessh is an tarpit that very slowly sends an endless, random SSH banner. It keeps SSH clients locked up for hours or even days at a time. The purpose is to put your real SSH server on another port and then let the script kiddies get stuck in this tarpit instead of bothering a real server.
https://github.com/skeeto/endlessh

brokenix, to random

> you mostly model data with sum types, which in my mind are the best way to model data

True its quite strict in Haskell though
https://blog.darklang.com/leaving-ocaml/

brokenix, to random

Reason Town: Elm to , Technical Debt, and Escape Hatches with Paul Biggar
Speaking of which , now that @codyroux has related diagonalisation to p = np ( which either idk or I don't recall reading ), I got to follow up the whole series
Episode webpage: https://podcasters.spotify.com/pod/show/reason-town/episodes/Elm-to-OCaml--Technical-Debt--and-Escape-Hatches-with-Paul-Biggar-e52keq

Media file: https://anchor.fm/s/79070e8/podcast/play/4329370/https%3A%2F%2Fd3ctxlq1ktw2nl.cloudfront.net%2Fstaging%2F2019-7-23%2F21544635-44100-2-c1b9431e68ec7.mp3

brokenix, to haskell

pseq combinator is used for sequencing; informally, it eval-
uates its first argument to weak-head normal form, and then eval-
uates its second argument, returning the value of its second argu-
ment. Consider this definition of parMap:
parMap f [] = []
parMap f (x:xs) = y ‘par‘ (ys ‘pseq‘ y:ys)
where y = f x
ys = parMap f xs
The intention here is to spark the evaluation of f x, and then
evaluate parMap f xs, before returning the new list y:ys. The
programmer is hoping to express an ordering of the evaluation: first
spark y, then evaluate ys.
The obvious question is this: why not use ’s built-in seq
operator instead of pseq? The only guarantee made by seq is that
it is strict in both arguments; that is, seq a ⊥ = ⊥ and seq ⊥
a = ⊥. But this semantic property makes no operational guaran-
tee about order of evaluation. An implementation could impose this
operational guarantee on seq, but that turns out to limit the optimi-
sations that can be applied when the programmer only cares about
the semantic behaviour. Instead, we provide both pseq and seq
(with and without an order-of-evaluation guarantee), to allow the
programmer to say what she wants while leaving the compiler with
as much scope for optimisation as possible.
https://simonmar.github.io/bib/papers/multicore-ghc.pdf

brokenix, to FunctionalProgramming

Implement web servers using lenses
dependent types
https://github.com/ska80/idris2-server?tab=readme-ov-file

brokenix, to haskell

fixpoint combinators like Y can't be well-typed in . Specifically, something of the form x x requires x to have two conflicting types simultaneously. In dynamic languages, this doesn't matter because you just don't care what the type is, only that you can use the value in some way. But a Haskell compiler does care. However there's no need for such combinators, because Haskell's solution fix f = let x = f x in x is more elegant anyway, and has no typing difficulties (but does require lazy evaluation).
is perhaps not the best launchpad to haskell , to their credit they make good fp presentations
https://stackoverflow.com/questions/68975627/translating-a-fixed-point-operator-to-haskell-language

brokenix, to random

A good strategy to go from a thesis to a typechecker
https://spire-lang.org/blog/2014/01/05/an-unremarkable-type-checker/

brokenix, to random

ZFC includes an infinite axiom schema

brokenix, to microsoft

Even if you’re one of the “good devs,” and even if Copilot suddenly makes you twice as productive, as (dubiously) claims, your day didn’t just suddenly get half as long. You just suddenly got twice as many responsibilities
https://joshcollinsworth.com/blog/copilot

brokenix, to haskell

when you reverse a list in 

aux_reverse [] out = out aux_reverse (x:xs) out = aux_reverse xs (x:out)<br></br>reverse l = aux_reverse l []<br></br>

does it keep the reference to the original list (using max space) ? ll do the same?

brokenix, to random

This like testing for fp

brokenix, to haskell

What is beta reduced ( evaluated ) form of

(\1 - &gt; ( x- &gt; 1)) 2

where x is f abstraction and 1, 2 are literals

brokenix, to guix

the “Nix store” is independent of the “Nix language” (which we’ll define below). In other words, you could replace the front-end Nix programming language with another language (e.g. scheme, as does). This is because the Nix derivation format (the .drv files) and the nix-store command-line interface are both agnostic of the Nix expression language.

In isolation, the Nix language is “just” a purely functional programming language with simple language constructs.
Nixpkgs support for overrides is essentially an embedded domain-specific language, meaning that you still express everything in the Nix language (layer 1), but the ways in which you express things is fundamentally different than if you were simply using low-level Nix language features.
OS is based on the NixOS module system, which is yet another embedded domain-specific language. In other words, you configure with Nix code, but the idioms of that Nix code depart even more wildly from straightforward “layer 1” Nix code
https://www.haskellforall.com/2022/08/stop-calling-everything-nix.html?m=1

brokenix, to haskell

lenses are just functional references

brokenix, to NixOS

I haven't caught up on even important changes in , has stopped using
but why ? Though?
alternative doesn't sound very cool either

image/png

brokenix, to random

vs for federating your self hosted code , of course if you know how secure it is and what are you doing

brokenix, to emacs

should become a compositor
https://emacsconf.org/2022/talks/wayland/

brokenix, to emacs

https://github.com/a-schaefers/systemE
replace with

brokenix, to guix

virtual machine shares its /gnu/store with the host, your new VM takes up far less space than you might expect! On my system, the disk image is just 2MiB! All the heavyweight stuff (qemu, the kernel, ) is shared among all my up-to-date VMs, and the state files all live elsewhere and can be managed directly from the host! You can also choose how much memory and how many cores your service is allowed to use

https://benwr.posthaven.com/magic-immutable-ish-virtual-machines-with-guix-and-tailscale

brokenix, to guix

, wraps every executable in a script, thereby always eating PS1
With that in place, guix shell can pretty much fill the same role as direnv and similar tools, with one difference though: speed. When all the packages are already in store, guix shell can take one to a few seconds to run, depending on the package set, on whether you’re using a solid state device (SSD) or a “spinning” hard disk, and so on. It’s acceptable but prohibitively slow for direnv-like use cases.

To address that, guix shell maintains a profile cache for the -D -f guix.scm and -m manifest.scm cases. On a hot cache, it runs in 0.1 second. All it has to do is fork a shell with the right environment variable definitions; it does not talk to guix-daemon, and it does not even read guix.scm or manifest.scm (it’s possible to forcefully update the cache with --rebuild-cache). (manual)
2c

brokenix, to guix

Really miss the util on
where i could just manage all my dotfiles with it in $HOME and could just give the profile path in bash in init , I had nearly nothing in /root/.config* and never cared about whether to source .profile or .bash-profile based on how i append my list of pkgs in home.comfiguration ( fwiw source the former when you append with specification / (output?) in scm) .
Case in point after a couple of baffled days , i now realize that my config had no error ( how could it , it was working just fine elsewhere) , its just that it was fetching it config from * , while i had it in ~/.config/nyxt
Quick and dirty way was to just copy the latter to the former path of finding the config
similarly emacs-pkg were listed in config.scm, but they could only be found by $USER and not $ROOT
yes nix exprs need not eval below a minimum version , bit that s not my immediate concern

brokenix, to random

@abcdw
I followed the manual , but
for some some reason rde channel derivative won't build on my systems
I tried both $HOME & /root env (even though I s less sure about the latter)
update - regrets for distraction , it was a commit confilict, it builds now

image/png

brokenix, to guix

Flakes seems to provide more hermetic builds than channels. Guix still can access different values on host
Inconsistent cli
https://gist.github.com/abcdw/e54807b0a25e61fe2cf1bf8991410f83

  • All
  • Subscribed
  • Moderated
  • Favorites
  • •
  • JUstTest
  • kavyap
  • DreamBathrooms
  • thenastyranch
  • magazineikmin
  • tacticalgear
  • cubers
  • Youngstown
  • mdbf
  • slotface
  • rosin
  • osvaldo12
  • ngwrru68w68
  • GTA5RPClips
  • provamag3
  • InstantRegret
  • everett
  • Durango
  • cisconetworking
  • khanakhh
  • ethstaker
  • tester
  • anitta
  • Leos
  • normalnudes
  • modclub
  • megavids
  • lostlight
  • All magazines
    •