companion_cube changed the topic of #ocaml to: Discussion about the OCaml programming language | http://www.ocaml.org | OCaml 4.14.0 released: https://ocaml.org/releases/4.14.0.html | Try OCaml in your browser: https://try.ocamlpro.com | Public channel logs at https://libera.irclog.whitequark.org/ocaml/
Haudegen has quit [Remote host closed the connection]
Haudegen has joined #ocaml
Tuplanolla has quit [Quit: Leaving.]
jao has quit [Ping timeout: 252 seconds]
jao has joined #ocaml
Haudegen has quit [Ping timeout: 252 seconds]
Haudegen has joined #ocaml
oriba has quit [Quit: https://quassel-irc.org - Chat comfortably. Anywhere.]
Haudegen has quit [Ping timeout: 255 seconds]
bobo_ has joined #ocaml
spip has quit [Ping timeout: 248 seconds]
waleee has quit [Ping timeout: 255 seconds]
<dh`> global state (or typically, top-level module-local state) is often the best or only viable way to handle a lot of things in systems code
<dh`> especially if it's concurrent
<companion_cube> is it? if it's concurrent you have to use a lock, and all that, it's not trivial
spip has joined #ocaml
bobo_ has quit [Ping timeout: 252 seconds]
rgrinberg has quit [Quit: My MacBook has gone to sleep. ZZZzzz…]
chrisz has quit [Ping timeout: 246 seconds]
chrisz has joined #ocaml
tizoc has quit [Quit: Coyote finally caught me]
xd1le has joined #ocaml
tizoc has joined #ocaml
<dh`> and if it's concurrent and you _don't_ use a lock (or more elaborate things) you just end up with a mess :-)
<dh`> systems code is different from compiler code; in systems code you tend to have layers and layers of state abstraction and there's nothing similar in a normal compiler or interpreter
<dh`> if you try to pass the state around, at best you end up with the open sewer^W^W IO monad
zebrag has quit [Quit: Konversation terminated!]
chrisz has quit [Ping timeout: 252 seconds]
chrisz has joined #ocaml
mbuf has joined #ocaml
zebrag has joined #ocaml
bgs has joined #ocaml
zebrag has quit [Quit: Konversation terminated!]
fds has quit [Ping timeout: 240 seconds]
jao has quit [Ping timeout: 248 seconds]
fds has joined #ocaml
Johann has quit [Read error: Software caused connection abort]
Johann has joined #ocaml
Serpent7776 has joined #ocaml
bgs has quit [Remote host closed the connection]
mro has joined #ocaml
calvnce has joined #ocaml
Serpent7776 has quit [Ping timeout: 272 seconds]
calvnce has quit [Quit: Client closed]
Haudegen has joined #ocaml
mbuf has quit [Read error: Connection reset by peer]
calvnce has joined #ocaml
calvnce has quit [Quit: Client closed]
fds has quit [Ping timeout: 272 seconds]
Serpent7776 has joined #ocaml
azimut has quit [Ping timeout: 258 seconds]
mbuf has joined #ocaml
mbuf has quit [Remote host closed the connection]
mro has quit [Remote host closed the connection]
mro has joined #ocaml
fds has joined #ocaml
olle has joined #ocaml
bartholin has joined #ocaml
bartholin has quit [Client Quit]
taupiqueur has quit [Remote host closed the connection]
taupiqueur has joined #ocaml
reynir has joined #ocaml
taupiqueur has quit [*.net *.split]
adanwan has quit [*.net *.split]
rgrinberg has joined #ocaml
hrberg has quit [Ping timeout: 276 seconds]
troydm has quit [Ping timeout: 248 seconds]
Ekho has quit [Read error: Software caused connection abort]
mro has quit [Remote host closed the connection]
Serpent7776 has quit [Ping timeout: 252 seconds]
mro has joined #ocaml
Serpent7776 has joined #ocaml
Ekho has joined #ocaml
wingsorc has quit [Ping timeout: 246 seconds]
xd1le has quit [Remote host closed the connection]
xd1le has joined #ocaml
fds has quit [Ping timeout: 252 seconds]
fds has joined #ocaml
Haudegen has quit [Quit: Bin weg.]
hacking-haunt is now known as hackinghorn
mro has quit [Read error: Connection reset by peer]
mro_ has joined #ocaml
mro_ has quit [Remote host closed the connection]
rgrinberg has quit [Ping timeout: 252 seconds]
rgrinberg has joined #ocaml
Haudegen has joined #ocaml
Fardale has quit [Ping timeout: 268 seconds]
Fardale has joined #ocaml
rgrinberg has quit [Quit: My MacBook has gone to sleep. ZZZzzz…]
mro has joined #ocaml
Ekho has quit [Ping timeout: 252 seconds]
serpent has joined #ocaml
Ekho has joined #ocaml
gwizon has joined #ocaml
gwizon has quit [Client Quit]
spip has quit [Read error: Connection reset by peer]
spip has joined #ocaml
xd1le has quit [Ping timeout: 252 seconds]
<companion_cube> what do you call "system code" anyway?
rgrinberg has joined #ocaml
<olle> Hm, what's the question? Missing IRC history, sorry.
serpent has quit [Ping timeout: 248 seconds]
<sleepydog> the discussion was about "systems code" needing to have global state.
<sleepydog> the term has certainly become overloaded
<olle> Gotta love those "systems programming languages" xD
adanwan has joined #ocaml
<jedb> companion_cube: code that interfaces with hardware to provide services to other programs, often with significant constraints on available runtime library facilities, inability to use standard debuggers, and with constraints on resources and performance
<jedb> bare metal non-user-facing code, I guess?
<companion_cube> ah well, all OCaml code is unable to use standard debuggers :)
<companion_cube> for the rest, yeah, accessing hardware makes sense
<companion_cube> it's a more narrow definition, but of course the hardware itself is global state
<jedb> garbage collection is also rare to have in systems code, unless you're like that lunatic who wrote some sort of OS kernel in Haskell
<companion_cube> well there's mirage
<olle> Hey
<olle> Go
<companion_cube> some people say Go isn't really a systems language :)
<olle> Hehehe
<olle> I'd agree
<companion_cube> despite what Rob Pike claimed it was
<sleepydog> i partially blame Go for overloading the term systems language
jao has joined #ocaml
calvnce has joined #ocaml
<reynir> Rob Pike wanted to prove you *could* do functional programming in Go some years ago, so he implemented map, filter and fold, IIRC, except it was less general and rather unreadable
gwizon has joined #ocaml
azimut has joined #ocaml
mg has left #ocaml [WeeChat 3.2.1]
mro has quit [Remote host closed the connection]
rgrinberg has quit [Quit: My MacBook has gone to sleep. ZZZzzz…]
bgs has joined #ocaml
<olle> They have generics now to
<olle> tho*
<olle> It's all - working out!
<companion_cube> they just lack, hmm, any form of immutability
<companion_cube> or sum types, or tuples, really
<companion_cube> it's still a C-like language
<olle> Sure sure
azimut_ has joined #ocaml
azimut has quit [Ping timeout: 255 seconds]
mro has joined #ocaml
<Leonidas> I fail to see any reasonable definition that would make go a "systems language" that wouldn't make ocaml a "systems language" in the same way
<companion_cube> I'd honestly say neither is a systems language
<Leonidas> I'd agree
rgrinberg has joined #ocaml
zebrag has joined #ocaml
<olle> You'd have to be able to at least opt out of GC
<olle> And boxed values
<companion_cube> it's interesting to look at, say, Oberon
<companion_cube> designed to write its own OS in it, so you can do low level unsafe things, but it also has its own GC
taupiqueur has joined #ocaml
<olle> Meh
<olle> Low-level need to be safe
taupiqueur has quit [Remote host closed the connection]
<Leonidas> Oberon predates Rust by several decades
<companion_cube> olle: no?
<companion_cube> C is definitely low level
<companion_cube> I mean, it'd be nice, but I don't think all systems programming can be safe (unless you bring in the big guns like formal verification)
<olle> Right
<olle> companion_cube: Linear/affine types?
azimut_ has quit [Read error: Connection reset by peer]
azimut has joined #ocaml
x88x88x has quit [Read error: Software caused connection abort]
<companion_cube> that's not enough if you talk directly to hardware and stuff
<companion_cube> in rust you have to pull off "unsafe"
<olle> companion_cube: No? One use-case?
x88x88x has joined #ocaml
mro has quit [Quit: Leaving...]
<olle> Gotta go
Haudegen has quit [Quit: Bin weg.]
olle has quit [Remote host closed the connection]
Serpent7776 has quit [Quit: WeeChat 1.9.1]
Serpent7776 has joined #ocaml
calvnce has quit [Quit: Client closed]
troydm has joined #ocaml
hackinghorn has quit [Read error: Software caused connection abort]
hackinghorn has joined #ocaml
Serpent7776 has quit [Ping timeout: 252 seconds]
bgs has quit [Ping timeout: 252 seconds]
bgs has joined #ocaml
bartholin has joined #ocaml
rgrinberg has quit [Ping timeout: 252 seconds]
rgrinberg has joined #ocaml
Haudegen has joined #ocaml
Tuplanolla has joined #ocaml
olle has joined #ocaml
<olle> Test
<olle> Right
<olle> Use-case for when affine types is not enough for safe interaction with hardware?
<companion_cube> interacting with the hardware
<olle> A but unprecise
<olle> imprecise?
<olle> F* did some low-level stuff, but that is proving
<olle> Wonder if that linear types thing in Haskell is actually used...
<olle> Because I think it got merged
<dh`> Ultimately if you're going to write to a hardware register there's some form of let foo: ref T = address 12345 in foo := 6
<dh`> there's no way to make that safe according to the usual PL concepts of safety
<dh`> that is to some extent cheating, but it's also a real thing
bgs has quit [Ping timeout: 252 seconds]
<dh`> anyway, "systems code" is a fuzzy term but in the context I meant it definitely includes operating system kernels, database servers, and network protocol implementations
bgs has joined #ocaml
<companion_cube> yeah it's really a weird definition
<dh`> and in practice application code tends to share the same property (being dependent on state abstraction for organization)
<companion_cube> a kernel is much, much lower level than a http server
<dh`> it is really "most code that isn't compiler-like" where you want state abstraction
<companion_cube> idk, a network protocol should also abstract state
<dh`> it took me years to figure that out (that compilers are fundamentally different) when I was younger
<companion_cube> idk, I wish the OCaml compiler wasn't as full of global state as it is
<dh`> I haven't ever looked at it :-/
<companion_cube> well it's fundamentally design to analyze one file per process
<companion_cube> designed*
<dh`> but anyway at one point I remember counting the abstraction layers between calling write() (at the system call level, which is already several layers under most code) and iron oxide and it's on the order of 30
<dh`> and you couldn't have most of them if there weren't a lot of state hiding
<companion_cube> in the kernel, sure
<dh`> some of them are in the kernel, some of them are in the disk firmware
<dh`> the interface that lets you plug in disks is one of them more important ones :-)
<dh`> s/them/the/
<companion_cube> sure, no one is going to write kernels or firmware in OCaml though :)
<dh`> right
<dh`> well, you could, same as the guys who wrote a kernel in haskell
<dh`> but that would be to prove you can, not because it's a good idea
<companion_cube> you'd need some C in there anyway
<companion_cube> (even just for the runtime)
<dh`> if you're a purist you'd write it all in assembler
<companion_cube> real systems languages either have an optional runtime, or implement their own runtime
<dh`> but yeah, one of the critical things about C that people in the PL tend not to get is that it has almost no runtime
<companion_cube> thankfully, there's also rust now
<dh`> well, perhaps
<dh`> most of the stuff I've seen that explains why you should use rust is based on fundamental misunderstanding of what is and isn't wrong with C
<dh`> (and it has its own issues as well)
<companion_cube> I rather disagree :p
<companion_cube> rust also has no runtime (if you use #[no_std]), and it's simply a better language than C
<dh`> I remain unconvinced of that
<dh`> but I'll shut up before I attract the RESF
<companion_cube> 🤷
troydm has quit [Ping timeout: 248 seconds]
<companion_cube> care to take that elsewhere? :p
calvnce has joined #ocaml
bgs has quit [Remote host closed the connection]
<olle> Wait
<olle> ref t = address 12345
<olle> You're saying direct memory access can't be safe?
<olle> What is "usual PL concept of safety"?
<olle> dh`: ^
<companion_cube> of course not
<companion_cube> you can't access a random address and preserve memory safty
<companion_cube> safety
* ski . o O ( typed assembly )
<olle> companion_cube: well, how "random" is the address? :)
<olle> ski: Right, there is a dependently typed assembly, no?
<ski> possibly .. i don't recall
<companion_cube> olle: if you can provide it (as an integer value), it's random
<ski> (you can do various low-level things in ATS, too)
<companion_cube> nothing prevents you from `t := address 0`, and voilà, segfault
* ski notes locations zero and one on the C64 are magical I/O registers (memory mapped, but actually being inside the processor), controlling memory banking (and cassette tape)
<olle> companion_cube: Imagine a type-system where you can construct constraints around mem access?
<dh`> it's still not safe
<olle> More constraints -> more safe
<dh`> in the sense that you can (accidentally or on purpose) construct things so the addresses you use overlap other things in your program
<dh`> one reasonable working definition of safety is that the semantics of your program don't depend on details of its transformation into an executable form
<olle> dh`: I think dep types can control that, to prevent mem overlap
<dh`> maybe
<olle> Compile-time type state or sim
<dh`> I mean, you can do a lot of things with dependent types at the cost of effectively being working in a prover
<olle> You get a dummy version of it with phantom types
<olle> Wonder if it can be done with affine types too... :d
<olle> Kinda related to keep stack state in phantom type for a Forth eDSL
<olle> If you have phantom types you can discipline the phantom types properly, but it's doesn't scale well in terms of DX
<companion_cube> you're still going to get a magic integer value for the address, and the only reason it works is because it's where the memory map for this device starts
<olle> affine types*
<olle> companion_cube: why magic?
<olle> compiler can hide it? developer sees 0 etc
<olle> Well
<ski> ("DX" ?)
<olle> Developer experience
olle has quit [Ping timeout: 252 seconds]
olle has joined #ocaml
<ski> scale, in which sense ?
Stumpfenstiel has joined #ocaml
<olle> scale? was I out? o0
adanwan has quit [Remote host closed the connection]
Stumpfenstiel has quit [Ping timeout: 255 seconds]
Haudegen has quit [Ping timeout: 255 seconds]
Stumpfenstiel has joined #ocaml
<ski> "it's doesn't scale well in terms of DX"
Haudegen has joined #ocaml
_whitelogger has joined #ocaml
<olle> ski: Phantom types works ok for a list, but if you want to emulate more complicated states - like a collection of stacks - it gets hairy to write, I think
<olle> Something I might dig into since I've learned Forth has multiple stacks :)
<olle> But maybe an excessive use of type alias can help :d
<olle> So scales in terms of state complexity
wingsorc has joined #ocaml
<olle> jedb: safe because it doesn't have malloc? :D
<olle> Or maybe it does?
<olle> So how safe can it be then...
* jedb rolls his eyes
<jedb> it has the equivalent of malloc, but you don't need to use it in 99+% of code
* olle rolls his eyes back
<jedb> meanwhile it was also designed to detect as many errors as possible at compile time, and has a lot of support for that formal verification stuff that was mentioned
<olle> Can't kill brown people with memory bugs yo
<olle> I mean, developed by US DoD
<ski> Ada's not too bad
<jedb> I'd say the existence of RAII makes memory safety overblown except you extremely rarely need to even bother with that in Ada either due to the flexibility it allows with unconstrained types and the standard containers library...
<olle> RAII has its limits
<olle> Hm, can you do the A* algorithm within RAII?
<jedb> pretty sure I did the A* algorithm without any manual memory management at all
<olle> ?
<olle> How?
<olle> Unless you used a growing regions or something :d
<olle> region*
<jedb> sets and maps from the standard containers library, checking the code I wrote years and years ago
hrberg has joined #ocaml
<olle> Guess I can check it on rosetta code
<jedb> and indeed there is no equivalent of malloc anywhere written by me in that code
<olle> Nope, it's not there :(
<olle> jedb: set and map release when out of scope? How do you make sure not to leak?
<jedb> yes, set and map release when out of scope; they get placed on the stack
calvnce has quit [Quit: Client closed]
<jedb> internally they probably use RAII stuff for their own storage but that's not my concern
jao has quit [Remote host closed the connection]
hrberg has quit [Client Quit]
hrberg has joined #ocaml
<olle> Ya, but you can return any element from the set, or?
<olle> And leak that element?
hrberg has quit [Client Quit]
hrberg has joined #ocaml
<jedb> it sounds like you would be surprised at the flexibility of what can be placed on the stack and what can have a copy returned
hrberg has quit [Client Quit]
<jedb> I can assure you there is no leaking of anything going on and it all gets freed appropriately when it goes out of scope
hrberg has joined #ocaml
<olle> Not what I asked
hrberg has quit [Client Quit]
hrberg has joined #ocaml
hrberg has quit [Client Quit]
hrberg has joined #ocaml
hackinghorn has joined #ocaml
hackinghorn has quit [Changing host]
<jedb> it kind of is, since if you didn't manually heap allocate stuff you're putting into the set then there can't be any leaking of stuff you take out of the set and return...
<olle> the single element survives scope, the set does not
<jedb> yes, and? that single element also gets appropriately deallocated when it too goes out of its own scope
<jedb> everything is on the stack except for the internal mechanisms of the standard library
* jedb checks and notes this is code from circa 5 years ago which was a rewrite of Java code from probably about 7-8 years before that
<olle> Its own scope? But you copy it then? Or ref count?
<jedb> copied on the stack
<jedb> why would I need to ref count? it's on the stack, not the heap
<olle> Deep copy?
<jedb> yes, that's handled by the internals of the standard library
<olle> kk
<olle> Sure, that works. Just copy everything xD
<olle> How smart is the compiler to optimize such things?
<olle> Koka2 did ref count with some novel algo to remove lots of em
<jedb> you can go over to #ada and ask some adacore people about that if you really want to
<jedb> much as I'd like to, I haven't yet gotten around to writing my own compiler
waleee has joined #ocaml
motherfsck has quit [Quit: quit]
bartholin has quit [Quit: Leaving]
jao has joined #ocaml
jao has quit [Remote host closed the connection]
ocabot has quit [Read error: Software caused connection abort]
jao has joined #ocaml
Stumpfenstiel has quit [Ping timeout: 255 seconds]
ocabot has joined #ocaml
troydm has joined #ocaml
Haudegen has quit [Ping timeout: 252 seconds]
Haudegen has joined #ocaml
Tuplanolla has quit [Quit: Leaving.]
hrberg has quit [Ping timeout: 252 seconds]
hrberg has joined #ocaml