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 random

continuation of my own thread on mathstodon1

Moving to * causes CONS nodes to no longer be a special case. Explicit promise and force expressions become redundant. * is a common model in software FP

  • similarities blow-up of storage requirements is the bugbear of lazy evaluation in software systems.
  • Static-allocation will limit the language’s laziness, so there will be some trade-off## basic approach is to take an eager control/dataflow graph,make it lazy by enclosing data processing elements so that the values returned are promises, and all parameter promises are forced before being used. DUP nodes are replaced with promise replication nodes### dealing with
  • iteration promise stability constraint requires a promise that is passed in a f be passed unevaluated in any recursive call. In graph=> disallowing promises as parameters to iteration and multiplexer nodes, unless promises are not forced within loop. This gives us our practical limitation on laziness in hardware: all values may be evaluated lazily, except those that are passed into recursive calls. This is as might be expected, since it is the recursive calls that allow build-up of unbounded nested promises that can make lazy evaluation so memory-hungry.
  • streams may not contain promises. values must be forced before beingsent over streams. but, streams are leniently evaluated, so this forcing is done leniently too (byperforming the forcing within a CONS node) ,forcing may be cancelled by resetting outputstream,like leniently evaluated forcing of a promise may be cancelled when the promise value iskilled. other stream-related nodes can be simply treated as normal nodes, in terms of the insertionof forcings , promises
  • Synthesis insimplest transformation, ~ every node s encapsulated to force I , promise O.by case, ( new reset boxes ll be upon new promise nodes)

image/png
image/png
image/png

brokenix, to haskell

Scheme - SICP - Is Scheme functional?: compsci

You don't need side effects for I/O. Purely functional languages like #Miranda and #Haskell 1.0 got along just fine with dialogues for I/O, although whether they could be feased is another matter. But 'side effect' is short for 'side effect of evaluation'; i.e., the computer calculates the value of this expression and oh by the way it does this I/O while it's doing that (as a side effect). The side effects of a drug are everything the drug does that's not its intended purpose; the side effects of an expression are everything the code for that expression does that's not 'calculate the value'. So you don't need side effects to do I/O. Just make the I/O part of the value and have the computer calculate the value, then do the I/O it calculated.

brokenix, to nostupidquestions

@nostupidquestions test
!nostupidquestions
https://lemmy.world/c/nostupidquestions@lemmy.world

brokenix, to emacs

I must say, emacs.ch has surprised me in terms how I get engagement on nearly any topic, thread I engage to and I am not even high an mighty.
It funny when I was thinking about posting anything besides
If I am not being unreasonable in my request and admins could only enable , I ll be glad to move my account here as well
IDK who to tag here

brokenix, to random

With i can use every buildon my machine with my phone , without installing a single thing on phone but ssh utils
iirc it wasnt the same with plain ssh

image/png

brokenix, to random

https://emacs.ch/@louis/110926837305831528
Let's try the low hanging fruit first
cos(x^3)
<math>x^2</math>

brokenix, to random

A free fediverse search engine , when the majority has adopted it, as an alternative
Cc @DuckDuckGo

brokenix, to vim

Modern IDEs are magic. Why are so many coders still using Vim and Emacs? - Stack Overflow Blog

"Fourth, modal editing. or evil-mode is the only way you should be editing code. Being able to move around the screen without so much as ever touching a mouse frees up so much effort that it’s actually hard to describe until you learn it. The ability to pick a word, or a line, or 10 lines, and just kill whole regions, moving them around, undoing and redoing with a literate undo tree and without ever using your mouse is incredible. After learning modal editing, using a non-modal editor actually feels like you’ve lost use of your thumbs. Vim and Emacs naturally allow you to ignore your mouse almost completely, so are natural extensions of this practice"
https://stackoverflow.blog/2020/11/09/modern-ide-vs-vim-emacs/#:~:text=Fourth%2C%20modal%20editing,of%20this%20practice

brokenix, to emacs

so far I can breath
folks , what keeps you from switching to ?

brokenix, to random

Funny sometimes I don't get any notification for DM

Is this happening because of those random tiny downtimes?
cc @louis

brokenix, to rust

CS SYD - Ad-hoc polymorphism erodes type-safety

" code tends to use Traits even more than uses type-classes. I was surprised by this because I've been hearing so much about how Rust code's type safety is amazing."
https://cs-syd.eu/posts/2023-08-25-ad-hoc-polymorphism-erodes-type-safety#:~:text=Rust%20code%20tends%20to%20use%20Traits%20even%20more%20than%20Haskell%20uses%20type%2Dclasses.%20I%20was%20surprised%20by%20this%20because%20I%27ve%20been%20hearing%20so%20much%20about%20how%20Rust%20code%27s%20type%20safety%20is%20amazing.

brokenix, to haskell
  • Meaning of the linear arrow: f :: s ⊸ t guarantees that if (f u) is consumed exactly once,then the argument u is consumed exactly once(Consume exactly once).to consume exactly once • (like Int or Ptr) - just evaluate it.• unction value -apply it to one argument, consume its resultexactly once.• pair - pattern-match on it, consume each component exactlyonce.• adt, pattern-match on it,, all its linear components a linear arrow specifies how f uses its argument. It does not restrict
    arguments to which function can be applied.a linear f cannot assume that itis given unique pointer to its argument. For example, if f :: s ⊸ t, then this is fine:g :: s → tg x = f xThe type of g makes no particular guarantees about the way in which it uses x; in particular, g canpass that argument to f.result of (unsafeFreeze ma) is a new immutable array, but toavoid an unnecessary copy, it is actually ma. The intention is, of course, that that unsafeFreezeshould be the last use of the mutable array; but nothing stops us continuing to mutate it further,with quite undefined semantics. The “unsafe” in the function name is a ghc convention meaning“ programmer has a proof obligation here that the compiler cannot check”.other unsatisfactory thing about the monadic approach to array construction is that it isoverly sequential. Suppose you had a pair of mutable arrays, with some updates to perform to each;these updates could be done in parallel, but the ST monad would serialise them

• Operations on files remain monadic, unlike the case with mutable arrays. I/O operations
affect world, hence must be sequenced. It is not enough to sequence operations on
files individually, as it was for arrays.
• generalise the IO monadst it expresses whether or not returned value is linear.
extra multiplicity type parameter p to the monad IOL, where p can be 1 or ω,
indicating a linear or unrestricted result, respectively. Now openFile returns IOL 1 File, the “1”
indicating that the returned File must be used linearly.
• As before, operations on linear values must consume their input and return a new one; here
readLine consumes the File and produces a new one.
• Unlike the File, the ByteString returned by readLine is unrestricted, and the type of readLine
indicates this.

  • Uniqueness (or ownership) types ensure that an argument of a function is not used elsewhere in an expression’s context even if the callee can work with the argument as it pleases. Linear types and uniqueness types have a ‘weak duality:’ ‘Seen as a system of constraints, uniqueness typing is a non-aliasing analysis, while linear typing provides a cardinality analysis.’1
    • API for pure mutable arrays, the original Linear paper [2] (Arxiv version) featured the function:newMArray :: Int -> (MArray a %1 -> Ur b) %1 -> Ur b
    • Taking a linear function as an argument, newMArray can make sure that the MArray is, in fact, not aliased. This is because linear types only restrict how a function can use an argument, it can’t restrict how the context uses an argument or a returned value. Contrast with uniqueness types (aka ownership types) in languages like Rust or Clean, which can demand that a value not be aliased. So, whenever we use linear types, in Haskell, to implement an API with a uniqueness requirement, we end up with such a newX function that takes a linear-function argument With newMArray and newMArrayBeside we have two functions to create new arrays. This isn’t satisfactory, but it gets worse. If I have another type with uniqueness constraints, say a ring buffer, then I’ll eventually need the ability to allow a ring buffer to piggyback on an array’s scope, and an array to piggyback on a ring buffer’s scope. with n types that can only be used linearly, I’ll need n^ 2 new functions. This is simply not sustainable. 3
    • of the many problems with Monads, one of them is that they are not composable, and Monad transformers are just a hack, you still have a stack of monads and how they interact when control flow gets involved can be hard to predict. Compare this with uniqueness typing (and syntax sugars for in/out arguments) and it's trivial to have multiple states used by the same function 4
brokenix, to random

here is nearly useless here with long posts with too many math expressions
brevity of [ ] for in is something worth adopting
cc @louis

brokenix, to random

Collins Dictionary has named "permacrisis" as its Word Of The Year. "Metacrisis" would be our contender...

" has its roots in contemporary systems theory, which claims that a crisis can become so complicated that we can’t predict its outcome"
https://www.thealternative.org.uk/dailyalternative/2022/11/7/permacrisis-metacrisis#:~:text=permacrisis%20has%20its%20roots%20in%20contemporary%20systems%20theory%2C%20which%20claims%20that%20a%20crisis%20can%20become%20so%20complicated%20that%20we%20can%E2%80%99t%20predict%20its%20outcome

brokenix, to random

I didn't read the full text search feature carefully
It doesn't matter , if I opt in or our out
Since many people have opted in , theirs posts ll appear in my search results , besides mine.
how about enabling a regular wordpress like search on the blog user.emacs.ch , st users can look up their exclusively their own posts, without having to rely on other apps/portals?
cc @louis

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 scheme

W.R.
A New for Writing Functional Operating Systems
https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-75.pdf

brokenix, to mastodon

A closer look at Nostr, the new decentralised Twitter alternative | Technology News - The Indian Express

unlike where user identities are attached to servers and servers have a degree of control over registered users, is a lot more open in that regard. There are two components at play on Nostr: clients and relays. Each user runs a client, while anyone can run a relay. Clients can publish data (i.e. create posts) on any number of relays and fetch data from other relays.

brokenix, to random

This like testing for fp

brokenix, (edited ) to random

This directory contains KR, a knowledge representation system. Unlike other systems, KR implements a small, carefully selected amount of functionality in order to keep performance within reasonable limits

https://github.com/rogersm/kr

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 random

is amazing
+
this is the best $TERM experience I ve had yet
hon mention -

image/jpeg

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 emacs

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

brokenix, to haskell

lenses are just functional references

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