Conversation
Phantasm (alt)
phnt@pl.borked.technology
@newt
>Rust
>1990
It's funny, Rust is two decades old and only became usable few years ago when a bunch of memory safety autists decided that they will shill it to no end.
>Rust
>1990
It's funny, Rust is two decades old and only became usable few years ago when a bunch of memory safety autists decided that they will shill it to no end.
1
0
2
Zanzibart, forgive me...
newt@stereophonic.space
@phnt Rust is basically OCaml in disguise with some memory shenanigans bolted on top, so the point still stands.
0
0
0
Zanzibart, forgive me...
newt@stereophonic.space
@waltercool Rust is absolutely a 90s language that took a bit too long to figure out right.
1
0
0
Blurry Moon
sun@shitposter.world
@newt @waltercool Rust has really good incremental compiler and error and warning messages tho
1
0
0
Zanzibart, forgive me...
newt@stereophonic.space
@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.
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.
1
0
0
Zanzibart, forgive me...
newt@stereophonic.space
@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.
But I'd look at hardcore richly typed languages inspired by Rust and Haskell and their progeny. Lean looks promising, for one.
4
0
1
1
0
1
@newt @waltercool @sun It's not even about that.
A committee formed by Simon Peyton-Jones, Paul Hudak, Philip Wadler, Ashton Kutcher, and People for the Ethical Treatment of Animals creates Haskell, a pure, non-strict, functional language. Haskell gets some resistance due to the complexity of using monads to control side effects. Wadler tries to appease critics by explaining that "a monad is a monoid in the category of endofunctors, what's the problem?"
2
0
0
Zanzibart, forgive me...
newt@stereophonic.space
@phnt @waltercool @sun
>"a monad is a monoid in the category of endofunctors, what's the problem?"
Exactly! No problem here whatsoever.
>"a monad is a monoid in the category of endofunctors, what's the problem?"
Exactly! No problem here whatsoever.
0
0
0
Phantasm
phnt@fluffytail.org
@snacks @waltercool @sun @newt I think they are exactly what you think they are. Problem is, nobody agrees on what you think, so nobody knows what they are.
2
0
1
lolitechengineer@loli.church
lolitechengineer@loli.church
1
0
1
1
0
0
lolitechengineer@loli.church
lolitechengineer@loli.church
@sun@shitposter.world @newt@stereophonic.space @waltercool@pl.slash.cl actually I'd like to change my answer to ChatGPT Astra, it's extremely easy to use and transpiles to basically any other language you want.
1
0
1
0
0
0
@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.
P.S. this is a reply to your Koka comment.
1
0
1
Blurry Moon
sun@shitposter.world
@newt @waltercool gonna be awesome I'm a retard that probably maxes out conceptually at zig, I can barely do rust or ocaml, but I'm trying to get better.
1
0
1
Zanzibart, forgive me...
newt@stereophonic.space
@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.
0
0
2
@newt @waltercool @sun just go for provers directly. agda2 with special emacs mode to type in the math symbols.
2
0
1
@bonifartius @newt @waltercool every now and then I'm reminded that people here are way smarter than me
1
0
3
Zanzibart, forgive me...
newt@stereophonic.space
@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.
1
0
1
@sun @waltercool @newt i'm not smart, i only fiddled with agda2 once for uni (failed horribly at that ;). it was interesting, but more because of the emacs environment which was actually pretty neat.
1
0
1
Wiggenstein
Inginsub@clubcyberia.co
@phnt @snacks @waltercool @sun @newt the confusion about monads comes from both haskell people being very smug for no reason (there are languages that have all the same features and more, and most of those communities don't gatekeep) and imperative people being unwilling to understand anything fp-related. 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.
1
0
0
Zanzibart, forgive me...
newt@stereophonic.space
@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.
> 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.
1
0
0
Zanzibart, forgive me...
newt@stereophonic.space
@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.
1
0
1
Wiggenstein
Inginsub@clubcyberia.co
@newt @phnt @snacks @waltercool @sun I mean, I said it's a programming pattern, not that it's a language feature
1
0
0
Zanzibart, forgive me...
newt@stereophonic.space
@Inginsub @phnt @snacks @waltercool @sun true, I guess. Though, monads require some type system machinery. HKTs are a must, for one.
0
0
1
@sun @waltercool @newt iirc provers are good for some things, like designing robust network protocols.
for "real" programming you have to deal with the dirtiness of the physical world where things fail, so the interesting part is to find good ways to handle failure mode which work, in the real world.
1
0
1
@bonifartius @waltercool @newt looking at lean and koka. maybe it can be good for parts of an OS rammed through the C ABI
1
0
0
@sun @bonifartius @waltercool @newt
lean is option designed for infinity-brained pure maths people who don't like computers
lean is option designed for infinity-brained pure maths people who don't like computers
2
0
2
Zanzibart, forgive me...
newt@stereophonic.space
@ageha @bonifartius @waltercool @sun being a slave to the machine should be met with revulsion. Computers must be hated.
1
0
0
@newt @bonifartius @waltercool @sun
meant computer as in the mathematical descriptor for dynamical system that maps inputs to outputs, human being one of such
meant computer as in the mathematical descriptor for dynamical system that maps inputs to outputs, human being one of such
1
0
0
Zanzibart, forgive me...
newt@stereophonic.space
@ageha @bonifartius @waltercool @sun i'm sure you did.
Then again, human computers did exist.
https://en.wikipedia.org/wiki/Computer_(occupation)
Then again, human computers did exist.
https://en.wikipedia.org/wiki/Computer_(occupation)
0
0
0
@newt @waltercool @sun i was joking ;) it's an academical (almost always horrible software) prover (not really made for something else)
1
0
0
Zanzibart, forgive me...
newt@stereophonic.space
@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.
1
0
0
@newt @waltercool @sun haskell is an exercise in being a functional masochist.
1
0
0
Zanzibart, forgive me...
newt@stereophonic.space
@bonifartius @waltercool @sun nah it's fine. Much better than other FP languages for most applications.
0
0
0
@ageha @bonifartius @waltercool @sun @newt type theory opens up so many options for compilers or compiler-shaped things, that's why people are ecstatic about it actually
1
0
1
0
0
1