Post BAd4XZPVITGURiISwq by newt@stereophonic.space
(DIR) More posts by newt@stereophonic.space
(DIR) Post #BAcyBFqojqXVgh34Hw by newt@stereophonic.space
0 likes, 0 repeats
lol accurate
(DIR) Post #BAd3A0a2WoYRo9QTLs by newt@stereophonic.space
0 likes, 0 repeats
@phnt Rust is basically OCaml in disguise with some memory shenanigans bolted on top, so the point still stands.
(DIR) Post #BAd42dLyaQnjhLtZAG by waltercool@pl.slash.cl
0 likes, 0 repeats
@newt tf is rust doing at 90s lmao.Trannies are mad.
(DIR) Post #BAd42dbZeRHITjC1Tc by newt@stereophonic.space
0 likes, 0 repeats
@waltercool Rust is absolutely a 90s language that took a bit too long to figure out right.
(DIR) Post #BAd4XZPVITGURiISwq by newt@stereophonic.space
0 likes, 0 repeats
@sun @waltercool so do a lot of other languages. This is not new. The only new thing in Rust is the use of affine types, a feature that was invented and studied in the 90s.The thing is, popular programming languages lag behind the research by around 20 years. This is why, for one, OOP - aka a hip feature from the 70s - really took off in the 90s with Java.
(DIR) Post #BAd9a3wLG7DxTwfFuy by newt@stereophonic.space
0 likes, 0 repeats
@sun @waltercool ask me around 2046, if software engineering even survives as an occupation.But I'd look at hardcore richly typed languages inspired by Rust and Haskell and their progeny. Lean looks promising, for one.
(DIR) Post #BAdA7QOWnIXWgDkxxg by newt@stereophonic.space
0 likes, 0 repeats
@phnt @waltercool @sun dynamiccels mogged yet again by static chards superiority :chadhead:
(DIR) Post #BAdAcjUJr5TqsGOUy0 by snacks@netzsphaere.xyz
1 likes, 0 repeats
@phnt @waltercool @sun @newt monads are burritos actually
(DIR) Post #BAdAdFCLxQ7hDoEbPE by newt@stereophonic.space
0 likes, 0 repeats
@phnt @waltercool @sun >"a monad is a monoid in the category of endofunctors, what's the problem?"Exactly! No problem here whatsoever.
(DIR) Post #BAdBxqrXjQsbmVtJ56 by newt@stereophonic.space
0 likes, 0 repeats
@sun @waltercool effects have been thoroughly studied within Haskell, where they originate from. Check out Polysemy (https://hackage.haskell.org/package/polysemy), for one. Overall, it's a 2010s idea what doesn't seem to get much traction, mostly because it doesn't solve any problem in particular.P.S. this is a reply to your Koka comment.
(DIR) Post #BAdCCDnnEwISytzORE by newt@stereophonic.space
0 likes, 0 repeats
@phnt @snacks @waltercool @sun Monads are a rather low-level abstract thing that only becomes useful when you're used to it. It's best compared to pointers in C. C noobs are totally lost when they first encounter pointers, but then it turns out they are handy in all kinds of situations. Same goes with monads.
(DIR) Post #BAdCL9ek1YEWjG0zFA by bonifartius@noauthority.social
0 likes, 0 repeats
@newt @waltercool @sun just go for provers directly. agda2 with special emacs mode to type in the math symbols.
(DIR) Post #BAdCMrMf0EkmZsN2mG by newt@stereophonic.space
0 likes, 0 repeats
@bonifartius @waltercool @sun unlike Agda, Lean can generate C code that doesn't put your CPU to a halt. Writing anything even remotely useful with Agda is a huge pain due to horrendous performance.
(DIR) Post #BAdEV95vAOqfn7cUPQ by newt@stereophonic.space
0 likes, 0 repeats
@Inginsub @phnt @snacks @waltercool @sun > Monad in functional programming is simply a programming pattern that simulates state in languages that don't have it, enforces the evaluation order, and allows for early termination, by nesting anonymous functions and passing the state as an argument.Not really. Monads CAN and ARE used for all these things, but that's just due to them being handy. You could totally do those things without Monads. Haskell started without them, they were added to the standard library several years later.Coincidentally, literally every programming language that has async today provides a monadic interface to it.
(DIR) Post #BAdGtLia5H7bniN6HY by newt@stereophonic.space
0 likes, 0 repeats
@Inginsub @phnt @snacks @waltercool @sun there is more than one way to do anything (as Perl taught us), but you seem to have implied that monads are the way. I might be mistaken here.
(DIR) Post #BAdHOSSJ5HHXfqaqEC by newt@stereophonic.space
0 likes, 0 repeats
@Inginsub @phnt @snacks @waltercool @sun true, I guess. Though, monads require some type system machinery. HKTs are a must, for one.
(DIR) Post #BAdJfk31885j4A8L0C by newt@stereophonic.space
0 likes, 0 repeats
@ageha @bonifartius @waltercool @sun being a slave to the machine should be met with revulsion. Computers must be hated.
(DIR) Post #BAdKCvKWChK9c78rMe by newt@stereophonic.space
0 likes, 0 repeats
@ageha @bonifartius @waltercool @sun i'm sure you did.Then again, human computers did exist.https://en.wikipedia.org/wiki/Computer_(occupation)
(DIR) Post #BAdPymNrGg7fXSLJOi by bonifartius@noauthority.social
0 likes, 0 repeats
@newt @waltercool @sun i was joking ;) it's an academical (almost always horrible software) prover (not really made for something else)
(DIR) Post #BAdPymdoJMsoKvo3GK by newt@stereophonic.space
0 likes, 0 repeats
@bonifartius @waltercool @sun i wasn't. There are libraries for Adga to use it for application programming, making it Haskell on steroids. It's fun but ultimately very painful.
(DIR) Post #BAdSncJkeZmAznn5xw by bonifartius@noauthority.social
0 likes, 0 repeats
@newt @waltercool @sun haskell is an exercise in being a functional masochist.
(DIR) Post #BAdSncW9uRhVcHb0Iy by newt@stereophonic.space
0 likes, 0 repeats
@bonifartius @waltercool @sun nah it's fine. Much better than other FP languages for most applications.