rgrinberg has quit [Quit: My Mac has gone to sleep. ZZZzzz…]
deadmarshal_ has joined #ocaml
<companion_cube>
You don't need lazy to be referentially transparent
<companion_cube>
And it gets in the way of IOs a bit
ygrek has joined #ocaml
malte has joined #ocaml
malte has quit [Remote host closed the connection]
germ- has quit [Read error: Connection reset by peer]
germ has joined #ocaml
alfiee has joined #ocaml
alfiee has quit [Ping timeout: 265 seconds]
Haudegen has quit [Quit: Bin weg.]
Mister_Magister has quit [Quit: bye]
malte has joined #ocaml
Mister_Magister has joined #ocaml
<discocaml>
<yawaramin> you kinda do need it. eg let `downloadFile :: IO ()` and `retry :: IO () -> IO ()`. then `retry downloadFile` works as expected if IO is lazy but not if it's eager
Everything has joined #ocaml
malte has quit [Remote host closed the connection]
malte has joined #ocaml
malte has quit [Ping timeout: 252 seconds]
alfiee has joined #ocaml
alfiee has quit [Ping timeout: 248 seconds]
<companion_cube>
Just add `() ->` in front, whatever
<companion_cube>
I mean it's actually even fine, the issue is when >>= is lazy afaik
<companion_cube>
Here it's a question of hot vs cold
<discocaml>
<yawaramin> `() ->` is laziness
<companion_cube>
Not in the Haskell sense but anyway
malte has joined #ocaml
<discocaml>
<yawaramin> yeah in the Haskell sense too. Haskell `IO a` is defined as basically `RealWorld -> (a, RealWorld)` ie a function that can be run ie laziness
<companion_cube>
but is it lazy like Haskell's IO is lazy?
<companion_cube>
I've sometimes been wondering what it'd be like to have a sort of IO monad instead of Lwt
<companion_cube>
but I'm not sure it's a good idea for OCaml
<dh`>
in connection with $work I have been wrangling a DSL that someone built with monads because they were haskell people
<dh`>
but they did not feel like implementing the whole nine yards, so you can't define your own monads, soe you can't actually do anything
<dh`>
so part of what I'm trying to figure out is whether to rip the monads out in favor of a tasteful implementation of ref cells, or fix it to be useful
gzar has quit [Quit: WeeChat 4.5.2]
Tuplanolla has quit [Quit: Leaving.]
<discocaml>
<diligentclerk> @companion cube - "You don't need lazy to be referentially transparent" Can you explain this? Say I have a function f : 'a -> IO 'b and I have a function g that calls f. I want to make it clear from the type signature of g that g has side effects. Laziness provides an easy way (intuitively) to track this, because you have to return the value to the main module in order to actually execute that effect, so it shows up in the type signature
<dh`>
state monads encoded as functions as described above are inherently lazy that way anyway
<dh`>
nothing runs until you feed them the starting state at the top level
<dh`>
they have state -> instead of () ->, but it ends up serving the same purpose
alfiee has joined #ocaml
<discocaml>
<diligentclerk> Okay. So if you have a strict IO monad it has a completely different implementation. How does the type system track effects in these languages?
<discocaml>
<diligentclerk> Could I implement a strict IO monad in OCaml the same way we are talking about implementing a lazy IO monad above? or would this be at the level of the language implementation
<companion_cube>
look, Lean and Coq are pure but not lazy
<companion_cube>
lazyness just allows you to write some stuff like `>>` and `&&` more easily, at the cost of bad perf by default and space leaks
<companion_cube>
`f : 'a -> IO 'b` isn't inherently lazy, what matters is that all side effects are thus encapsulated
<dh`>
laziness is meaningless in coq because it's _actually_ pure so it doesn't matter when anything's eval'd
<companion_cube>
no I mean even if you extract Coq to OCaml and add some IO framework
<companion_cube>
but for lean it's maybe more apparent since it has some native IOs?
<dh`>
fair enough
alfiee has quit [Ping timeout: 248 seconds]
<discocaml>
<._null._> Rocq is call-by-name, so closer to call-by-need than to call-by-value. But also, Rocq has no effects, so the difference is not noticeable (except through complexity I guess)
<discocaml>
<._null._> And at the same time, extraction to OCaml means this code is run in call-by-value, because for closed terms it doesn't matter
<dh`>
is it any of these things specifically? there are several different proof tactics for evaluating things
<dh`>
(including "cbn" and "cbv")
<discocaml>
<._null._> The kernel needs to run in cbn for it to work properly. These tactics are purely for efficiency purposes
<dh`>
hmm
<discocaml>
<._null._> Not entirely sure about that "needs to", but I can at least tell you that it definitely does
<dh`>
hmm
<dh`>
idk
<dh`>
I wouldn't think that it would matter (for the reasons already cited) but there are many subtleties
<discocaml>
<._null._> The question would become "what is a value in an open term ?" Is `x 0` a value ? Because it's in normal form
euphores has quit [Ping timeout: 252 seconds]
<dh`>
anyway you can make an IO monad where things happen at the time you call >>=, you just need to make certain operations () -> IO t instead of IO t so they don't happen prematurely
<discocaml>
<._null._> If it's not a value, then cbv can't work in the kernel; if it is, then I'm curious what definition of "value" you would take
<companion_cube>
like dh` says
<dh`>
ISTM that 'x 0' is a value if and only if it's reducible (which is, granted, a circular definition)
<companion_cube>
and even then I don't think you actually need `() -> …` that much
<dh`>
but therefore it not a value if x unfolds
<companion_cube>
>>= is enough
<discocaml>
<._null._> (x would be a variable, so not reducible)
<dh`>
no, it's fairly rare to have actions of the form IO t that don't take arguments of some kind
<companion_cube>
`type 'a io = Ret of 'a | Bind : ('a io * ('a -> 'b io)) -> 'b io | Read : string io`
<companion_cube>
this just needs a sort of toplevel recursive interpreter and voilà
<companion_cube>
(s/Read/Readline or whatever)
<dh`>
ah, and you have to substitute x to make progress? that makes sense, but I'm also not sure it constitutes CBV
<dh`>
yeah but the general read takes a filehandle :-)
<companion_cube>
yeah yeah you know what I mean
<dh`>
right, there certainly are cases
<dh`>
just relatively few
<companion_cube>
`Read : fd * bytes * int * int -> int io`
<companion_cube>
exact same for Write
<dh`>
there's getpid: pid_t io
euphores has joined #ocaml
<companion_cube>
for a real implementation we'd need an open type
<companion_cube>
this is just to illustrate
<companion_cube>
but the thing is, a `foo io` wouldn't do a thing until it comes into the interpreter
<companion_cube>
(again unlike lwt, where promises are hot from the moment they're created)
<dh`>
depends if you tried to implement it with a state
<dh`>
you can still have the 'a IO = mkIO of world -> (world * 'a) formulation and be eager, but then a loose `foo io` has a state
<dh`>
s/has/has to have/
ygrek has quit [Remote host closed the connection]
<dh`>
but there's no reason that's necessary either, you can make the world state magic
<companion_cube>
this is just a metaphor, I can't pass the world into a OCaml thread :p
<companion_cube>
I'd absolutely not do that, I'd do a GADT + a `main : unit io -> unit` that runs the interpreter, I think
<dh`>
anyway if you have threads you really kinda want something that reflects the thread state, which then isn't actually a monad any more
<companion_cube>
why not?
<companion_cube>
as long as it stays in IO
<companion_cube>
`gettid : int io`, blabla
<companion_cube>
`spawn : 'a io -> 'a thread io`, `join : 'a thread -> 'a io`, etc ?
<dh`>
well
<dh`>
haskell threads are like that
<dh`>
but you give up any ability to use the not-monad structure to reason about things
<dh`>
whereas operations like passing a value from one thread to another are actions of the form IO a * IO a -> IO a * IO a
<dh`>
(sorta)
<dh`>
and obviously this does not work with either the monad type or the monad notation
<dh`>
but you could imagine a thing where instead of the single linear state of a monad gets you, you have one state chain per thread, and points where they intersect are points where the threads need to synchronize with each other
<companion_cube>
I mean, this gets you a clear way to see IOs in types, not much else I think
<dh`>
this gives you a directed graph and if it's cyclic you have a problem, so this gives you a pretty strong static deadlock checker if you can figure out how to write it down
<companion_cube>
hmmmmmm
<companion_cube>
if you can detect deadlocks statically I think it means it's too restrictive
<dh`>
when I first saw the "from monads to arrows" paper I got all excited because I thought this was where they were going, but it's something else much less interesting
<dh`>
maybe, maybe not
<dh`>
acyclicity of that graph is probably equivalent to assigning every lock a static priority, which is necessary but not sufficient
<dh`>
well, that's imprecise, but there's a sense in which it's necessary and not sufficient
<companion_cube>
means you have a statically known number/topology of locks?
<dh`>
yeah, but you might have multiple instances of some that you can only disambiguate at runtime
<dh`>
vnode locks in a kernel being the classic example
<dh`>
anyway this is an idea I mess around with occasionally but I haven't thought about it much for a while
<dh`>
one of the complications is that if you want to write your thread code in anything like a normal way, that 'a IO * 'b IO -> 'b IO * 'a IO exchange operation is not one operation, it's two half-operations that go in different places in the code
<dh`>
how do you write down half operations and link them to each other in a type system? seems both like it should be possible and that it isn't going to be trivial
<companion_cube>
maybe structured concurrency?
<companion_cube>
but I don't think it's very realistic to hope for ML-level types to solve threading issues
<companion_cube>
even Rust solves data races, not deadlocks
<dh`>
no
<dh`>
data races aren't even a real problem
<dh`>
but that's a whole other rant
<companion_cube>
wat :D
<dh`>
what cpu has unpredictable/undefined behavior if two cores store to the same address at once? none, one of the cores goes first, and it has been thus since the very early days
<dh`>
that is, data races on machine words are not a thing
<companion_cube>
isn't that unpredictable though?
<companion_cube>
which one goes first
<companion_cube>
and of course, what if you write multiple words
ski has quit [Remote host closed the connection]
<companion_cube>
you might get invalid stuff
<dh`>
not in the cpu sense of UNPREDICTABLE (which is like undefined behavior)
<dh`>
if you do a _sequence_ of stores from one core and a _sequence_ of stores from another store
<dh`>
er, another core
<dh`>
then you might get a different ordering on each word and you get trahs out
<dh`>
trash
<dh`>
and that's a problem
<companion_cube>
and that's a data race
alfiee has joined #ocaml
<dh`>
it's a _race_
<companion_cube>
in terms of the language, you get impossible values
<companion_cube>
so that's just… really bad?
<dh`>
two simultaneous sequences of stores are only correct if they're mutually consistent
<dh`>
there are various ways you might define consistency but it's stronger than data-race freedom
Everything has quit [Ping timeout: 272 seconds]
<dh`>
the upshot of which is that data-race freedom isn't useful for talking about correctness
<dh`>
suppose you have an incorrect concurrent program
<companion_cube>
afaict it's useful to have reasonable guarantees to understand what's going on
Everything has joined #ocaml
<companion_cube>
it might not be the only way but it works really well for rust
<dh`>
and you try to fix it by adding a global lock, and taking and releasing that global lock around every read or write
<dh`>
poof! no more data races
<dh`>
but you haven't altered the semantics of the program and it's still wrong
<companion_cube>
sure
<companion_cube>
but at least your program has a semantic
<companion_cube>
otherwise it just wouldn't
<dh`>
does it? not really
<companion_cube>
sure
<dh`>
the behavior depends on the interleaving of the executions
<dh`>
(that's more or less the definition of race condition)
<companion_cube>
yes but it remains within the boundaries of the language
<dh`>
oh, yes, there's a sense in which it's safe
<companion_cube>
all the possible interleavings are within these bounds
alfiee has quit [Ping timeout: 276 seconds]
<companion_cube>
that's why we talk of data races and not race conditions
<companion_cube>
it's just like how memory safety is not full correctness
<companion_cube>
but is still a useful concept
<dh`>
we talk about data races because data races are easy to identify and talk about
<companion_cube>
sure
<companion_cube>
and it's very valuable to prevent them
<dh`>
it is very valuable to have correct concurrent programs
<dh`>
I have seen no reason to think that data-race freedom offers any leverage in this
<dh`>
(and keep in mind that I taught undergrads concurrency for like 15 years)
<dh`>
if anything it gives people a false sense of security
<companion_cube>
So we also don't need memory safety cause it's not everything?
<dh`>
pragmatically? no :-p
<companion_cube>
Anecdotically, writing threaded code in rust is great
<companion_cube>
And the same in ocaml5 has been footgunny for me
<companion_cube>
Forgot locks, etc
<dh`>
anyway what I'm arguing is not that languages should have unsafe concurrency, it's that data-race freedom isn't sufficient
<companion_cube>
Nobody said it's the panacea
<dh`>
the RESF would have you believe it is
<companion_cube>
But given that barely any language provides even that
<companion_cube>
No, they're careful to say it doesn't prevent all race conditions
<dh`>
also twenty years of academic papers give that impression to the naive
<dh`>
my conclusion is that you either want lightweight messages, transactions, or maybe both, and without these it's always going to be a shitshow
<dh`>
the RESF is never careful to say anything :-)
<dh`>
but the rust book is pretty disappointing on this point
<companion_cube>
You could still make multiple transactions and be wrong, no?
<dh`>
you can't make it impossible to write wrong code
<companion_cube>
Hu. I remember this specific distinction being underlined, weird
<dh`>
maybe it's been improved since I last looked at it
<dh`>
(around a year ago I think)
<dh`>
the version I saw didn't even mention the concept of condition variables
<dh`>
but anyway, my vague ideas about parallel not-monads are in the same category, things you might be able to use to get some leverage on the real problem
<thizanne>
data race freedom offers you some form of sequential consistency, and that's often a big deal to avoid writing incorrect concurrent programs already
<companion_cube>
Yeah, you won't forget the lock or atomic
<dh`>
sequential consistency is neither necessary nor sufficient
<thizanne>
depends
<companion_cube>
You might still split critical sections too much(?) but that's more rare an error
<thizanne>
in theory, one can write correct programs in weakly consistent models
<thizanne>
in practice, I've seen people try.
<thizanne>
hoping that the average programmer does it on the average program is absolutely delusional in 2025
<companion_cube>
What does that even look like?
<thizanne>
madness, mostly
<dh`>
normal code with locks
<thizanne>
well if you have locks then you have no data races
<companion_cube>
Normal code with locks, in rust, works just fine
<dh`>
it's only the lock implementation that needs to care about the memory model, unless you're doing exotic things with lock-free data structures
<companion_cube>
Oh yeah people do that for queues, too
<companion_cube>
At least people who write schedulers and the likes
<dh`>
if you are doing exotic things with lock-free data structures
<companion_cube>
Or channels
<dh`>
you probably care far too much about performance to want the system to provide you sequential consistency
<companion_cube>
But there's a good book on atomics in rust
<thizanne>
of course you don't want sequential consistency from the system, otherwise we'd just have it
<dh`>
yes
<thizanne>
but you also definitely want some form of it for the end programer
<companion_cube>
Good news is, code can be reused and libraries exist
<thizanne>
and most of the time, yes, that means using locks on everything that can have a data race, effectively "restoring" data race freedom
<dh`>
so basically in the case where you might need to think specifically about data races, whether data-race freedom buys you back sequential consistency is irrelevant
<companion_cube>
And Rust allows you to make sure that once you send a value in a channel, you can't access it anymore
<dh`>
and in ordinary lock-based code it's irrelevant
<dh`>
er, in ordinary lock-based code data-race freedom is irrelevant
<thizanne>
my point is, ordinary lock-based code is ordinary precisely because data races are too hard to reason about
<companion_cube>
No no no, in ordinary lock based code it's super important to help you *not forget the locks*
<dh`>
no, ordinary lock-based code is ordinary because non-lock-based code is too hard
<thizanne>
even if you have a correct semantics for those -- which last time I looked wasn't even the case in the C model
<dh`>
data races are not the core of that hardness
<thizanne>
it's too hard for several reasons, one of them being that data races are a mess
<dh`>
you can make a lock-free queue or whatever entirely out of machine integers where data races are moot
<dh`>
it's still hard
<companion_cube>
Concurrent access to mutable data is the core of that hardness
<thizanne>
even if you're only manipulating words, not having locks on a program running on a weak model means many things can happen that you won't have considered
<companion_cube>
And most programs work on larger values than just words
<dh`>
yes, and that's not about data races, it's about ordering considerations
<thizanne>
thread { char x = 1; register char r0 = y } ;; thread { char y = 1; register char r1 = x }
<thizanne>
that thing doesn't have lock and will sometimes end with r0 and r1 both being still equal to 0
<dh`>
yeah yeah, any code like that is intentionally borrowing toruble
<thizanne>
(assume x and y start at 0)
<thizanne>
and it's because you have a data race
<dh`>
nobody besides researchers in memory models writes code like that
<thizanne>
you'd be surprised
<dh`>
well
<dh`>
ok, people write ill-advised code all the time
<thizanne>
people everywhere believe that "if it fits in a word then it must be atomic"
<dh`>
maybe I should say nobody who has any idea what they're doing writes code like that
<dh`>
it _is_ atomic
<thizanne>
well, depends on your definition of atomic
<dh`>
atomic means the access is indivisble
<dh`>
or indivisible
<dh`>
which is still the case, however insane the cpu's ordering semantics are
<companion_cube>
Causality is useful to reason about programs, isn't it
<companion_cube>
thizanne: that's not even true on arm is it?
<thizanne>
what if your store operation to an "atomic" location is not seen at the same time by different cores
<thizanne>
is that still atomic?
<companion_cube>
I know x86 is stronger than it has to
<dh`>
yes
<dh`>
it's atomic, but not consistent
<companion_cube>
😂 But no worries that's not useful to program
<dh`>
or to be precise, the store and the reads that observe the store aren't mutually consistent
<dh`>
a _sequence_ of operations may not be atomic
<thizanne>
but then the store doesn't really happen once
<dh`>
sure it does, it doesn't come undone in any cpu I've ever heard of
<thizanne>
it doesn't come undone, but between the point where it's initiated and the point where it's completed, many things have happened
<dh`>
that's about ordering of multiple operations, the store itself is still atomic
<thizanne>
that's some definition of atomic, which isn't the only one
<dh`>
that's the standard one
<thizanne>
not really
<thizanne>
the standard historical one kind of assumes sequential consistency, which makes it equivalent
<dh`>
no? unless you're talking about atomicity of sequences of stores
<dh`>
and you have to bring in isolation as well to really have a well-defined concept
<dh`>
and we're back to transaction semantics
<thizanne>
the atomic operations defined on modern (ie weak) memory models, as far as I'm aware, all imply that the operation completes atomically, ie for everyone
<dh`>
I'm talking about atomicity as a concept
<dh`>
and while many cpus define a total global ordering on atomic instructions, I don't think all do
<dh`>
my recollection is that with riscv atomics you have to set the memory barrier bits to get that behavior
<dh`>
(but it's been a while since I looked at the riscv spec and I might be confusing this with something else)
<dh`>
and in any case you don't need that global ordering for correct execution of lock-based code
<thizanne>
I don't really know that model but that's not my understanding from a quick look, my understanding is that here again atomic implies multi-process synchronised operations (as it should, because why would you ever have atomic word-sized operations otherwise)
<dh`>
one reason to use same-cpu atomic operations is to synchronize with interrupt handling code
<thizanne>
no of course you don't, because locked code is forcefully data race free, meaning that there is no weak consistent behaviour happening
<dh`>
sure there is
<thizanne>
no there isn't
<dh`>
there are only barriers on entry and exit to critical sections
<thizanne>
every weakly consistent model says you're SC if you're data race free
<dh`>
within a critical section things can happen however
<thizanne>
on one thread only
<thizanne>
so there isn't even concurrent behaviours happening there
<thizanne>
companion_cube | thizanne: that's not even true on arm is it?
<thizanne>
you mean the word thing? I don't know
<dh`>
so nobody can observe that store 2 reaches global visibility before store 1; that doesn't mean it doesn't happen
<dh`>
anyway I think we're chopping logic rather than having a productive conversion :-(
<thizanne>
who cares what happens in the silicon, we're talking program semantics
<thizanne>
I guess a more pedantic way of saying this is, if your program is data race free then there is no valid trace that isn't SC-valid
<dh`>
and what I was saying before is that this isn't much help in assessing whether your traces are correct relative to your intended program behavior
<thizanne>
and my point is -- SC-valid traces are the only one that you can expect the average programmer to handle
<dh`>
no, the average programmer shouldn't be doing any of this at all
<thizanne>
meaning that even though your program only involves word-sized operations that you believe are atomic, then you usually need to lock them anyway
alfiee has joined #ocaml
<thizanne>
well truth to be told, I agree that the average programmer shouldn't be doing any of concurrent programming
<dh`>
yes, of course you do, because in general correctness demands consistency across multiple loads and stores
<thizanne>
but I'm not sure that's a very reasonable expectation
<thizanne>
(I don't think the average programmer should do programming, actually -- but well)
<dh`>
the average programmer might be able to handle threaded code with locks, maybe
terrorjack has joined #ocaml
<dh`>
but lock-free stuff? hell no
<thizanne>
dh` | yes, of course you do, because in general correctness demands consistency across multiple loads and stores
<thizanne>
yes, and the best way to achieve this is by enforcing data-race freedom, and that requires lock even if you think you don't have data races "because that's only words"
<dh`>
no, because data-race freedom doesn't make your code correct.
<thizanne>
it isn't sufficient
<dh`>
thinking about consistency and isolation and atomicity does
<dh`>
it's neither necessary nor sufficient
<thizanne>
that's like saying "type systems aren't useful because they don't make your code correct"
<thizanne>
it's not necessary theoretically, it is in practice because the alternative is unreasonable
<dh`>
no, it's like saying Standard Pascal's type system isn't useful because it doesn't have a good tradeoff between making the code correct and being usable
<thizanne>
you already said that reasoning about anything that isn't SC is out of reach of programmers
<dh`>
there was a bunch of work on atomic blocks some years back that never really went anywhere, which was a pity
<dh`>
yes, reasoning about SC is also out of reach
alfiee has quit [Ping timeout: 252 seconds]
<dh`>
reasoning about transactions, however, is a lot more doable
<thizanne>
reaching SC can then be done either by carefully inserting fences or the equivalent, which amounts to reasoning in your weak model (so unreasonable); or by locking everything to get data race freedom and thus SC
<dh`>
and then the code is still wrong because SC is still too hard
<thizanne>
that's another point
<dh`>
that's the whole point
<thizanne>
not really
<thizanne>
of course programming is hard
<thizanne>
and concurrent programming adds another difficulty
<thizanne>
but at some point you need to accept some of that difficulty or you're never doing anything beyond hello world (and even then)
<dh`>
data-race freedom is not a good tool for assessing whether your concurrent code is correct
<dh`>
is that a better way of putting it?
<thizanne>
...yes but that's not its role
<thizanne>
not having data-race freedom is a recipe for incorrect code
<dh`>
only in the general case
<thizanne>
by contraposition, data race freedom is a required tool to make correct code. As most of these tools are, it won't be enough
<dh`>
there are quite a few special cases where that's not true
<dh`>
and that's one of the problems with the whole thing
<thizanne>
yes I think we agreed on that
<dh`>
stuff like statistics counters, for example
<dh`>
you can do an unlocked increment and once in a while it'll bobble one and you probably don't care
<thizanne>
not having data-race freedom is a recipe for incorrect code unless you know how to code in weak memory models, which is probably < 100 people in the world
<companion_cube>
And there it's fine to use an atomic even in application code
<dh`>
but oh now it's UB in C11 because C11 is silly
<companion_cube>
But it's opt-in
<dh`>
that's _not_ an atomic, is the point
<companion_cube>
I'd use an atomic, why wouldn't I?
<companion_cube>
Just with a chill ordering
<dh`>
because the unlocked increment doesn't do cache synchronization and so it'll be noticeably faster when contended?
<dh`>
this stuff unfortunately matters in real highly concurrent code like kernels
<companion_cube>
Depends on the architecture no?
<dh`>
not much
<companion_cube>
I thought on x86 it'd be atomic anyway
<dh`>
only if you do LOCK INC or whatever it is
<companion_cube>
Although maybe not if there's multiple cups?
<thizanne>
your point kind of amounts to "programmers that don't need correctness don't need the tools to write correct programs"
<dh`>
you get a total store ordering, that doesn't prevent READ READ WRITE WRITE
<companion_cube>
CPUs*
<thizanne>
which is undubitably true I guess
<dh`>
sort of
<companion_cube>
I'll let the experts opt in into doing imprecise but fast things
<dh`>
sure
<companion_cube>
I personally would rather use an atomic and know there's a good semantic
<dh`>
they will appreciate it if you don't go gratuitously make their code undefined
<companion_cube>
They can always write a bit of asm ig?
<dh`>
sometimes
<dh`>
my feeling is that lock-free stuff should in fact be written in asm
<companion_cube>
Maybe not everyone is a kernel dev or a concurrency expert, anyway
<dh`>
no
<companion_cube>
I'd rather get help from the language to tell me I did an unprotected read or write on shared data
<dh`>
which gets back to my other point, which is that ordinary folks much prefer transaction semantics when they can get it (once they understand what it's all about anyway)
<companion_cube>
OCaml doesn't (yet)
<companion_cube>
Maybe, but isn't it harder to reason about perf? And your code needs to be able to rerun?
<companion_cube>
If we're talking STM
<thizanne>
lock free stuff can be written in any language where you have an actual semantics for data races
<dh`>
every STM I've seen is crap :-(
<thizanne>
C has (a broken and unsound) one, why not use it if that's your codebase language
<companion_cube>
But then is there an example of what you'd actually like?
<dh`>
they are all trying to magically infer the granularity of locking, and that fundamentally doesn't work and never will, so they have huge overheads
<thizanne>
I guess that's what static analysers are for companion_cube
<dh`>
we had a memory transaction system with 5-10% overhead back in the 90s
<companion_cube>
Cause from what I see there's either rust (shared memory but manageable) or erlang (share nothing)
<companion_cube>
And the rest is very error prone
<dh`>
the transaction stuff was open-coded in C because that was what we had
<dh`>
there is not, I rant these rants to try to get people to think broadly
<dh`>
in the hopes that someone will make something better sometime
<companion_cube>
I'm not a researcher in that so I'm mostly interested in the existing stuff
<companion_cube>
JST's fork of ocaml tries to catch up with rust and that's exciting, for example
<dh`>
lightweight channels with shared-nothing are the best model, I'm pretty sure
<dh`>
but erlang itself has a lot of issues
<dh`>
golang also has channels, but it unfortunately also has issues
<companion_cube>
Rust (+ tokio) also has channels :)
mange has quit [Remote host closed the connection]
<dh`>
rust has a different pile of issues :-)
<companion_cube>
(and issues I suppose. But async rust pushes towards channels for some reason)
<dh`>
however, it's definitely possible to have strong transaction semantics without it being ruinously expensive
<dh`>
even with redo/undo
<dh`>
the problem with this model is that actions you can't undo have to be deferrable to transaction commit time
<dh`>
which is mostly ok but sometimes problematic
<companion_cube>
I think Vesa has something like that? Lightweight transactions
<dh`>
I don't know, I haven't gone and caught up with the literature for a while
<dh`>
the system I referred to above got published in 1996, I did more work later but that ended up being a casualty of the 2008 funding environment
<dh`>
google scholar doesn't recognize that reference, alas
<dh`>
also there's an additional set of unanswered questions about transaction nesting and abstraction boundaries
<dh`>
I'm reasonably certain I understand how it _should_ work but there's a good solid year or two of work to write it all down coherently
<dh`>
which is probably never going to happen at this point :-|
<dh`>
maybe I should look at implementing this kind of transaction system in ocaml
<dh`>
last thing I need is another project that size :-(
<companion_cube>
Well look at Vesa's maybe, his gh account is polytypic
<companion_cube>
Iirc the project is kcas
<dh`>
oh, thought that was a project name :-/
<dh`>
found it
<dh`>
my initial guess based on reading the description is that it's probably still ruinously expensive, just not as bad as some of the early STM attempts
<dh`>
(many of which were things like "orders of magnitude slower")
<dh`>
but that's only a guess, will need to look more
<dh`>
and it's getting late so I need to disappear :-(
<dh`>
feel free to prod me about this more later if you want
alfiee has joined #ocaml
alfiee has quit [Ping timeout: 252 seconds]
<discocaml>
<diligentclerk> @companion cube I looked up IO in Lean and it says: "IO action transforms the whole world. IO actions are actually pure, because they receive a unique world as an argument and then return the changed world. This perspective is an interior one that matches how IO is represented inside of Lean. The world is represented in Lean as a token, and the IO monad is structured to make sure that each token is used exactly once."
<discocaml>
<diligentclerk> Another quote from the "Functional Programming in Lean" book is "Writing a line of text to standard output is a pure function, because the world that the function returns is different from the one that it began with. Programs do need to be careful to never re-use the world, nor to fail to return a new world—this would amount to time travel or the end of the world, after all. Careful abstraction boundaries can make this style of program
<discocaml>
<diligentclerk> It reads to me like Lean has a linear type system for tracking effects?
alfiee has joined #ocaml
<discocaml>
<diligentclerk> You asked "Even if you want an IO monad, why would you ever make it lazy?" so I am wondering if there is a practical way to implement an IO monad which is not lazy in OCaml. This paragraph makes it sound like Lean uses linear types to have a strict IO monad, and AFAIK there's no way to implement linear types in OCaml
alfiee has quit [Ping timeout: 268 seconds]
alfiee has joined #ocaml
alfiee has quit [Ping timeout: 260 seconds]
ski has joined #ocaml
alfiee has joined #ocaml
alfiee has quit [Ping timeout: 260 seconds]
alfiee has joined #ocaml
Serpent7776 has joined #ocaml
alfiee has quit [Ping timeout: 276 seconds]
bartholin has joined #ocaml
alexherbo2 has joined #ocaml
alfiee has joined #ocaml
alfiee has quit [Ping timeout: 252 seconds]
Serpent7776 has quit [Ping timeout: 244 seconds]
Haudegen has joined #ocaml
Serpent7776 has joined #ocaml
alfiee has joined #ocaml
alfiee has quit [Ping timeout: 246 seconds]
Everything has quit [Ping timeout: 276 seconds]
mange has joined #ocaml
alexherbo2 has quit [Remote host closed the connection]
bartholin has quit [Quit: Leaving]
alfiee has joined #ocaml
alfiee has quit [Ping timeout: 276 seconds]
alexherbo2 has joined #ocaml
alfiee has joined #ocaml
alexherbo2 has quit [Remote host closed the connection]
alfiee has quit [Ping timeout: 252 seconds]
szkl has joined #ocaml
alfiee has joined #ocaml
alfiee has quit [Ping timeout: 248 seconds]
alexherbo2 has joined #ocaml
<discocaml>
<uberpyro181> I'm fairly sure that as long as there's no way to escape an IO action, e.g. some function with a type like `'a io -> 'a`, then linearity (really uniqueness) is enforced on every reference to an io object
<discocaml>
<uberpyro181> e.g. the cps style enforces uniqueness on every reference
<discocaml>
<uberpyro181> so with the monad-like handling of io actions there's no need to have linear types on top of that, linear types allow you to safely unwrap the actions
<discocaml>
<uberpyro181> well, even with linear types I think you need to use a callback style, you need essentially unique types to get rid of that
<discocaml>
<uberpyro181> well, even with linear types I think you need to use a callback style, you need "essentially unique types" as in Clean to get rid of that
<discocaml>
<gooby_diatonic> Very profound philosophy from the Lean manual
alexherbo2 has quit [Remote host closed the connection]
alfiee has joined #ocaml
alfiee has quit [Ping timeout: 272 seconds]
<discocaml>
<_4ad> it just uses monads.
<discocaml>
<_4ad> there are no linear types in Lean.
<companion_cube>
@diligentclerk I find it a bit solipsistic tbh
<companion_cube>
and I sketched a way to do it in OCaml without lazyness
mange has quit [Quit: Zzz...]
alfiee has joined #ocaml
alfiee has quit [Ping timeout: 252 seconds]
Haudegen has quit [Quit: Bin weg.]
ygrek has joined #ocaml
Putonlalla has quit [Ping timeout: 252 seconds]
alfiee has joined #ocaml
alfiee has quit [Ping timeout: 246 seconds]
Putonlalla has joined #ocaml
kurfen has quit [Ping timeout: 246 seconds]
kurfen has joined #ocaml
nirvdrum74 has quit [Quit: Ping timeout (120 seconds)]
nirvdrum74 has joined #ocaml
ygrek has quit [Ping timeout: 264 seconds]
ygrek has joined #ocaml
semarie has quit [Ping timeout: 248 seconds]
alfiee has joined #ocaml
alfiee has quit [Ping timeout: 244 seconds]
Haudegen has joined #ocaml
gentauro has quit [Read error: Connection reset by peer]
gentauro has joined #ocaml
semarie has joined #ocaml
alfiee has joined #ocaml
alfiee has quit [Ping timeout: 272 seconds]
steenuil has quit [Remote host closed the connection]
steenuil has joined #ocaml
steenuil has quit [Remote host closed the connection]
steenuil has joined #ocaml
alfiee has joined #ocaml
alfiee has quit [Ping timeout: 265 seconds]
wickedshell has quit [Ping timeout: 248 seconds]
<discocaml>
<diligentclerk> I don't understand what this means, I truly don't understand what a strict IO monad looks like or how one might implement one. Let's say that I have a function `f` that takes a string, prints it as a message to the user, and gets an integer input in response, so it's of type `string -> int IO.t`. Now I define `g (s : string) = ignore (let %x = f s in x); 4`. The type of `g` should be `string -> int`. If the monad is lazy then since the m
<discocaml>
<_4ad> strictness has nothing to do with it, you can have monads in a strict language (like OCaml).
<discocaml>
<_4ad> monads just sequentialize computations, it doesn't matter whether the language is string or not.
<discocaml>
<diligentclerk> I think you're misunderstanding my question because that response doesn't make any sense
Haudegen has quit [Quit: Bin weg.]
<discocaml>
<diligentclerk> I understand and agree with everything you just said, but it doesn't answer my question
<discocaml>
<contificate> > monads just sequentialize computations
<discocaml>
<contificate> monads taking the credit for what CPS gives you
<discocaml>
<diligentclerk> I was looking into cool CPS applications last night after you brought it up and naturally Oleg Kiselyov has a page on it
<discocaml>
<contificate> yeah, Oleg is a CPS, shift/reset, etc. chad
<discocaml>
<contificate> the coolest application of CPS is probably in defunctionalising CPS to derive abstract interpreters, but trampolining, schedulers, being the basis of monadic style, faithful compiler lowering, relation to SSA, etc. is neat as well
<discocaml>
<_4ad> and btw, saying that Lean is strict is not quite right. for a total language (like Lean), call by name (need) vs. call by value makes no semantic difference whatsoever, they are exactly the same (it can make a difference in performance or whatever).
<discocaml>
<diligentclerk> Interesting. I would have thought there was a semantic difference when it comes to an expression like (lambda x : unit.4)(print_endline "Hello, world")
<discocaml>
<diligentclerk> I would describe the "call by name" semantics of this as having no side effect, and the "call by value" semantics as having a side effect
alfiee has joined #ocaml
<companion_cube>
afaik Lean compile to call by value, is what I meaan
<companion_cube>
mean*
<discocaml>
<eval.apply> it's not about lazy vs strict, the side effect wouldn't happen on it's own you, and you can't just "ignore" the monad wrapper, bind is `'a t -> ('b -> 'a t) -> 'a t` you would have a "runIO" that interprets the IO actions in the monad you built up
alfiee has quit [Ping timeout: 272 seconds]
<companion_cube>
exactly, if you ignore the IO value nothing happens
<discocaml>
<eval.apply> now if you want that interpreter to execute in-place as if you were shooting off rockets in a normal imperative way, you can do that if your compiler is smart enough
<discocaml>
<eval.apply> or if you have linear types enforce it and just make that how it works
<discocaml>
<eval.apply> but that's an optimization
<discocaml>
<eval.apply> now do i edit and face the wrath of the IRC users or do i wait until someone decapitates me for the typo in that bind type
<discocaml>
<contificate> they'll say nothing 🔫
<discocaml>
<barconstruction> I think what companion cube just said is helpful, because I might have been misunderstanding what lazy/strict means in this context.
<discocaml>
<barconstruction> By "strict IO monad" I meant that the side effect associated to an IO value is performed at the time that the IO value is defined.
<dh`>
that is what I'd been thinking as well
<discocaml>
<contificate> does such a thing even exist
<discocaml>
<contificate> isn't the IO monad always backed by some kind of opaque state transfromer
<discocaml>
<contificate> isn't the IO monad always backed by some kind of opaque state transformer
<dh`>
it doesn't have to be
<companion_cube>
@barconstruction it's not monadic then
<companion_cube>
for me an IO monad _must_ only do IOs when it goes through the runIO interpreter
<companion_cube>
otherwise it's just lwt-style hot promises
<companion_cube>
hmmmI guess this is terminology from observables
<dh`>
yeah, I was about to say there's a problem if a loose 't IO causes something to happen without being bound
<dh`>
violates the sequencing axioms
<companion_cube>
and also makse `repeat 5 some_io` not actually repeat the IO
<companion_cube>
which is … not great
<discocaml>
<barconstruction> That makes sense.
<dh`>
for the same reason you also can't just have bind execute the effects
<discocaml>
<barconstruction> Right.
<dh`>
banning the existence of values of type 'a IO might make it work, but that would also get real weird real fast
alfiee has joined #ocaml
<discocaml>
<barconstruction> so `'a Lazy.t` is a monad, right? I can define `return x = Lazy.from_thunk (fun ()->x)` and I can define `bind x f = Lazy.from_thunk (fun () -> let a = Lazy.force x in Lazy.force (f a)`
<discocaml>
<barconstruction> I would call this a call by value evaluation order. So is this a strict monad
alfiee has quit [Ping timeout: 244 seconds]
bartholin has joined #ocaml
Haudegen has joined #ocaml
euphores has quit [Quit: Leaving.]
euphores has joined #ocaml
alfiee has joined #ocaml
alfiee has quit [Ping timeout: 248 seconds]
dylanj_ has joined #ocaml
dylanj has quit [Ping timeout: 248 seconds]
dylanj_ is now known as dylanj
wickedshell has joined #ocaml
alfiee has joined #ocaml
dylanj has quit [Remote host closed the connection]
dylanj has joined #ocaml
alfiee has quit [Ping timeout: 248 seconds]
Haudegen has quit [Quit: No Ping reply in 180 seconds.]
Haudegen has joined #ocaml
alfiee has joined #ocaml
alfiee has quit [Ping timeout: 252 seconds]
alfiee has joined #ocaml
alfiee has quit [Ping timeout: 252 seconds]
Anarchos has joined #ocaml
YuGiOhJCJ has joined #ocaml
alfiee has joined #ocaml
cawfee has quit [Ping timeout: 244 seconds]
ski has quit [Ping timeout: 260 seconds]
cawfee has joined #ocaml
alfiee has quit [Ping timeout: 260 seconds]
alfiee has joined #ocaml
alfiee has quit [Ping timeout: 252 seconds]
mange has joined #ocaml
ygrek has quit [Remote host closed the connection]
Tuplanolla has joined #ocaml
Serpent7776 has quit [Ping timeout: 252 seconds]
bartholin has quit [Quit: Leaving]
rgrinberg has joined #ocaml
exfalsoquodlibet has joined #ocaml
alfiee has joined #ocaml
Anarchos has quit [Quit: Vision[]: i've been blurred!]
alfiee has quit [Ping timeout: 252 seconds]
alfiee has joined #ocaml
alfiee has quit [Ping timeout: 252 seconds]
rgrinberg has quit [Quit: My Mac has gone to sleep. ZZZzzz…]