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/
dhil has quit [Ping timeout: 272 seconds]
<qwr> programming a microcontroller would be some way limited? ;)
Haudegen has quit [Ping timeout: 272 seconds]
<brettgilio> Something else, would linear types / substructural typing be possible in OCaml? I noticed Haskell has it now.
rgrinberg has quit [Quit: My MacBook has gone to sleep. ZZZzzz…]
<qwr> brettgilio: https://www.researchgate.net/publication/343413649_Kindly_bent_to_free_us imho described ML with linear and affine types
<brettgilio> qwr thanks!
<brettgilio> Are there any pl theory channels on libera?
vicfred has joined #ocaml
waleee has quit [Ping timeout: 240 seconds]
<drakonis> brettgilio: doesnt coq do it?
bobo has joined #ocaml
<brettgilio> drakonis you mean linear types?
<drakonis> yeah
spip has quit [Ping timeout: 276 seconds]
<drakonis> it is irrelevant whether it does or does not have linear types
<companion_cube> I don't think so
<brettgilio> I don't think so either
<drakonis> since you want to use it while writing code
<drakonis> i wonder if why3 is useful
<drakonis> it seems to be ocaml's agda
rgrinberg has joined #ocaml
<brettgilio> I'm assuming the alt-ergo prover for why3 and its mention of "linear and non-linear algebra over integers" does not mean substructural typing
<brettgilio> but I could be wrong
<brettgilio> but, using a proof system like this could be possible to reason an implementation of linear types for OCaml
<companion_cube> not, it means linear arithmetic
<companion_cube> and non linear arithmetic
<companion_cube> (non linear arithmetic over integers is undecidable, btw)
<drakonis> i see
<drakonis> unfortunate then.
ccx has quit [Ping timeout: 240 seconds]
<brettgilio> I am not super experienced on the key differences between why3 and coq, either.
<brettgilio> I would guess the proof style and tactics that are used
<brettgilio> but otherwise, I am totally uninitiated to what sets them apart, and where they overlap
<brettgilio> one is automated, the other is interactive. But cant why3 also do interactive theorem proving?
<drakonis> it seems like why3 sits on top of coq?
<brettgilio> so an AST built on Coq?
<drakonis> one of many provers i'd say
<drakonis> i'm not good at this, honestly
<drakonis> looks like it is an optional thing to use other provers beyond why3
<drakonis> see this
<companion_cube> iirc you need Coq for proofs by induction
<companion_cube> (that was years ago, not sure if it's still true)
<d_bot> <NULL> Why3 proves programs with some annotations, deferring logical steps to automatic provers
<d_bot> <NULL> Coq lets you write proofs (of anything)
<brettgilio> Thank you for the simple explanation NULL
<d_bot> <NULL> You can use Coq as a prover for those steps of Why3, if you don't like automation (and are a bit masochistic from my small experience)
<brettgilio> one of those automatic provers being Alt-Ergo, Z3, etc. right?
<d_bot> <NULL> You can do a bit of induction from Why3 directly, which is handy because the automated provers can't for the most part (probably undecidable)
<d_bot> <NULL> Alt-Ergo, Z3, CVC yeah
<brettgilio> Makes sense
<brettgilio> I tried my hand at some of this stuff (Frama-C, Coq) a few years ago, but put them down after a bit.
<brettgilio> this explanation makes sense
<d_bot> <NULL> You need something on top of Coq to prove external programs though
<d_bot> <NULL> Correct programs from Coq are just written in its language and extracted
<d_bot> <NULL> Whereas in Why3, it's also their language but it's not the same
<d_bot> <NULL> What I meant is that Coq looks like a prover where you can write programs, whereas Why3 looks like a language to write programs where you put additional annotations and hope they are enough to deduce the specs you gave the program
<d_bot> <NULL> I hope I was clear in the end
<brettgilio> You are
<brettgilio> It was a very good explanation
ccx has joined #ocaml
<brettgilio> I would imagine that Why3 and OCaml can pretty easily interop. I am guessing Why3 also has an extraction backend.
<d_bot> <NULL> Why3's language is extremely close to OCaml, and indeed has an extraction mechanism
shawnw has joined #ocaml
<d_bot> <NULL> I don't know how much/well/easily you can use OCaml libraries directly in Why3, but since you won't get any associated proofs I doubt it would be that useful
<d_bot> <NULL> I guess you could manually axiomatise the library functions though. Basically I don't know
<drakonis> so i guess it is a lot like agda
<brettgilio> Seems to have an overlap in idea to Agda
<brettgilio> but not totally identical
<d_bot> <NULL> In which regard ? Agda is more like Coq in that general prover sense
<brettgilio> Is Idris closer to Why3 or to Agda/Coq
<drakonis> the overlap is that agda lets you write code very similar to haskell's
<d_bot> <NULL> Coq also lets you write code which is similar to OCaml
<d_bot> <NULL> or to ML, OCaml's particularities kinda disappear I feel
<brettgilio> Do Why3 programs run on the ocaml runtime?
<drakonis> agda is a haskell library
<d_bot> <NULL> I don't think Why3 programs are run unextracted
<d_bot> <NULL> Well Coq is in opam, you could say it's an OCaml library
<drakonis> but you don't execute coq like you would with agda, would you?
<drakonis> why3 seems to be executed in the same manner as ocaml's
<drakonis> its a library you load
<brettgilio> NULL, so the Why3 system has its own runtime system?
<d_bot> <NULL> I don't know about Idris. Looked about it but I can't answer you
<drakonis> it is rather interesting
<drakonis> not all of it overlaps anyways
<d_bot> <NULL> If you only consider the "creating verified real world programs", there are two things you want to do : run them and verify them
<drakonis> idris is more like agda/coq though
<d_bot> <NULL> I think for all 3 of Coq, Why3 and Agda (I am not certain for that last one), to run it you extract the program to OCaml/Haskell; to verify it you call coqc/why3 check/agda_smth
<brettgilio> NULL, WhyML has an interpreter
<brettgilio> or, at least according to this page https://why3.lri.fr/doc/exec.html
<drakonis> that's for whyml as opposed to why3 the library
<drakonis> which is fine
<d_bot> <NULL> Makes sense; Coq also has one. I don't think you'd run it with the interpreter for more than tests though, it's an *interpreter*
<brettgilio> right
<d_bot> <NULL> Why3 is more of a framework to prove WhyML programs
<d_bot> <NULL> Or more correctly to organise the delegation to the automated provers
<brettgilio> I guess I got confused on this phrasing: "An alternative to interpretation is to compile WhyML to OCaml..."
<brettgilio> It saying "alternative" led me to think that both options are possible, but one would prefer to have their programs interpreted by some WhyML interpreter.
<d_bot> <NULL> To me, an interpreter is for [tests and] simple programs, and you don't really use a prover for simple programs
<drakonis> so yeah, the docs point out that you can use it as a software library or standalone
<d_bot> <NULL> Another way to say it is that if you have the patience to prove a program, you should have the patience to have it compiled
<drakonis> then right away it explains the standalone usage with .why files
<drakonis> which reminds me, can i do this with coq too?
<brettgilio> I am going to investigate Why3 more. and Drakonis, to my memory, "yes"
<drakonis> cool
<brettgilio> But I don't think it was preferred
<d_bot> <NULL> Do what with Coq ?
<brettgilio> Use it as a library with OCaml generally
<d_bot> <NULL> Differently
<brettgilio> rather than just using coq tactics in a coq environment
<d_bot> <cod1r> hi
<drakonis> hi
<d_bot> <NULL> For one you don't really use Why3 as a library with OCaml since you prove WhyML code
<drakonis> and yet the option still exists
<d_bot> <NULL> So you can write that code in Coq's language (Gallina) and prove it in-file as Coq theorems
<d_bot> <NULL> You mean you can prove OCaml directly in Why3 ? I don't know of that possibility (but it may very well exist)
<brettgilio> The API makes it seem like it does exist
<brettgilio> But I agree with you NULL, it seems unnecessary (for most things)
<brettgilio> I am sure some edge case probably exists
<brettgilio> then there is this: https://github.com/JBakouny/scalafromwhy3
<d_bot> <NULL> WhyML can already be extracted to OCaml, Haskell and C IIRC, so that's just one more target language
<brettgilio> I am also curious about if dune could handle whyml extraction to ocaml, and then the subsequent linking
<d_bot> <NULL> Probably similar to a "preprocessing" tool like menhir for that
<drakonis> it'd be quite nice
<drakonis> also refinement types would also be pretty great in ocaml
<brettgilio> tell me about it ;-;
<d_bot> <NULL> Way to strong to be decidable though
<drakonis> i saw fstar
<d_bot> <NULL> too*
<drakonis> it looks pretty cool
<d_bot> <NULL> An undecidable type system doesn't sound like a good idea
<drakonis> what do you mean too strong?
<d_bot> <NULL> You can express strong properties with those
<drakonis> okay i'm starting to walk into a domain of knowledge i have no experience on
<d_bot> <NULL> The canonical example would be that you could express the type of all programs which halt
<brettgilio> Like me that one time I went to a homotopy type theory conference... drakonis
<d_bot> <NULL> And you get confronted with the halting problem's undecidableness
<drakonis> ha
<brettgilio> Arrived knowing nothing, left knowing nothing
<drakonis> must've been rough
<drakonis> impostor syndrome ringing in your head every moment of it
<brettgilio> I learned mathematicians use cool chalk
<drakonis> plus reinforcing that old adage
<drakonis> "the more i know, the less i know"
<d_bot> <NULL> I also know that feeling, don't hesitate to stop me
<brettgilio> Dude. I am a science and math teacher. I was like, "this will be a lot, but ill be ok". I was not okay, lol.
<drakonis> haha
<drakonis> wild
<drakonis> huh, i can install fstar through opam
<drakonis> i'm pleased at this development
<d_bot> <NULL> So what about fstar ?
<brettgilio> fstar was interestingly how I got into all of this
<brettgilio> Literally stumbled across it
<drakonis> i did that just now and i'm curious
<brettgilio> that got me to learn a bit of OCaml, which took me to *SML, which took me down a rabbit hole where I feel like I know nothing lol
<d_bot> <NULL> The only thing I know about it is that it's relatively easy to write a (verified) static analyser in it
<drakonis> heh, that is the worst feeling
<brettgilio> I remember learning about some low level thing that was written in it
<brettgilio> https://github.com/RedPRL/cooltt Another rabbit hole for you bot
<brettgilio> bot
<brettgilio> both
<brettgilio> what is typing, and can I do it?
<drakonis> impressiv
<drakonis> impressive, but what the blazes is cubical agda
<d_bot> <NULL> I've heard a bit about it
<d_bot> <NULL> But not enough to explain it well
<brettgilio> homotopy type theory but with a cubical extension
<drakonis> that means nothing to me
<brettgilio> that is the unhelpful definition I know
<brettgilio> it means nothing to me either, dont worry
<drakonis> but that syntax looks rad as fuck
<d_bot> <NULL> You derive equalities as functions from a type to your two terms as a "continuous" function
<companion_cube> afaiu (which means not much) you get a version of homotopy where paths are computable, or something like that
<brettgilio> I will drag this channel down into the hole of ncatlab.
<companion_cube> with a notation on the path from [0,1]
<brettgilio> "Introductory lecture notes" -- Their definition of Introductory and mine are very different
<drakonis> is there a place i can fetch all of those pages?
<drakonis> there's a lot of things to read here
<drakonis> i'm almost falling into a haskell rabbit hole
<brettgilio> We need a plt channel
<drakonis> don't we already have that in libera?
<brettgilio> im not seeing one on libera
<d_bot> <NULL> noo stay on the ocaml side of this
<brettgilio> lol
<drakonis> dont worry
<brettgilio> its been fun, night all
<drakonis> same
<drakonis> well, maybe #plt isnt taken?
<drakonis> it isnt
<d_bot> <NULL> What does it say about me if I go to sleep after Americans ?
<drakonis> feel free to join
<drakonis> you're waking too early?
<d_bot> <NULL> I'm European, so it's 04:43 here and I should have gone to sleep many hours ago
<d_bot> <cod1r> having a nocturnal schedule isn't bad unless you have obligations that prevent you to do so
<d_bot> <NULL> I kinda have those
<d_bot> <cod1r> lmao
<brettgilio> I do, my obligation is I have offspring
<d_bot> <cod1r> up to you dood
<d_bot> <cod1r> LMAO
<d_bot> <NULL> I only have an internship, much lighter obligation
<brettgilio> I can't teach communism and type theory to my toddler when I am tired.
<brettgilio> Lol, night all
<companion_cube> night
<companion_cube> night-niiiight! even
<d_bot> <cod1r> ye I have school and it is annoying when you are trying to code something but then hw is due at like 11:59
<d_bot> <cod1r> and you just woke up at like 9pm
<d_bot> <cod1r> just an example of why a nocturnal schedule won't work
<d_bot> <NULL> Waking up at 9pm is quite a few steps deeper than what I'm at
<d_bot> <cod1r> ye I have had it pretty bad
<d_bot> <cod1r> recently I have been going to bed at like 12am or 9pm at best
<d_bot> <NULL> That's pretty much what I am going to aim for. On that, let me try to shift to that goal, good night
<drakonis> gn
<drakonis> i also want to play with coq at some point
rgrinberg has quit [Quit: My MacBook has gone to sleep. ZZZzzz…]
mbuf has joined #ocaml
tetrislife has quit [Ping timeout: 240 seconds]
Serpent7776 has joined #ocaml
Haudegen has joined #ocaml
mro has joined #ocaml
Anarchos has joined #ocaml
azimut has quit [Ping timeout: 240 seconds]
azimut has joined #ocaml
<Anarchos> when will ocaml 5.0.0 be released ?
<sim642> When it's ready :P
<Anarchos> sim642 i hope so :)
DNH has joined #ocaml
waleee has joined #ocaml
Sankalp has quit [Ping timeout: 272 seconds]
DNH has quit [Client Quit]
Sankalp has joined #ocaml
gravicappa has joined #ocaml
mro has quit [Quit: Leaving...]
Anarchos has quit [Ping timeout: 272 seconds]
olle has joined #ocaml
Sankalp has quit [Ping timeout: 272 seconds]
Anarchos has joined #ocaml
chiastre has quit [Ping timeout: 248 seconds]
chiastre has joined #ocaml
ts3 has quit [Quit: WeeChat 3.0.1]
thizanne has quit [Ping timeout: 260 seconds]
thizanne has joined #ocaml
dextaa4 has quit [Remote host closed the connection]
dextaa4 has joined #ocaml
bartholin has joined #ocaml
chrisz has quit [Ping timeout: 240 seconds]
chrisz has joined #ocaml
dhil has joined #ocaml
ccx has quit [Ping timeout: 276 seconds]
<d_bot> <blobfish> hello
Haudegen has quit [Ping timeout: 272 seconds]
Haudegen has joined #ocaml
ccx has joined #ocaml
gareppa has joined #ocaml
gareppa has quit [Remote host closed the connection]
dhil has quit [Ping timeout: 272 seconds]
gravicappa has quit [Ping timeout: 256 seconds]
jtmcx is now known as jtm
bartholin has quit [Ping timeout: 272 seconds]
spip has joined #ocaml
bobo has quit [Ping timeout: 256 seconds]
DNH has joined #ocaml
DNH has quit [Ping timeout: 260 seconds]
gravicappa has joined #ocaml
bartholin has joined #ocaml
neitsch[m] has joined #ocaml
dextaa4 has quit [Remote host closed the connection]
spip has quit [Ping timeout: 256 seconds]
spip has joined #ocaml
<d_bot> <ansiwen> If I keep the connection open, I have a huge memory leak of about 100k every request. 😱 I couldn't locate it yet more, than that it is from the H2 request and it's completely gone, if I clode the H2 connection for every request.
<d_bot> <quernd> See if this helps: https://github.com/anmonteiro/ocaml-h2/pull/159
<d_bot> <ansiwen> Ohhh!!
<d_bot> <ansiwen> Awesome... I should have checked the issues before learning how to use Memtrace 😆
<d_bot> <ansiwen> but that will be useful anyway, I guess
<d_bot> <quernd> Learning Memtrace is definitely not a waste of time 😉
<d_bot> <ansiwen> so, he So, he didn't make a new release with this yet. 🤔
<d_bot> <quernd> No, unfortunately it's not released yet, but merged.
<d_bot> <ansiwen> Thanks a lot anyway! I will pin it to master for now...
dhil has joined #ocaml
<brettgilio> Hey all
hyphen has quit [Ping timeout: 272 seconds]
olle has quit [Ping timeout: 276 seconds]
bartholin has quit [Ping timeout: 276 seconds]
dextaa4 has joined #ocaml
hyphen has joined #ocaml
bobo has joined #ocaml
spip has quit [Ping timeout: 256 seconds]
bartholin has joined #ocaml
<d_bot> <ansiwen> grpc-lwt doesn't work with master anymore (Body module has changed), so I had to pin to an intermediate commit. But now: `Showing objects that are never collected. Filtered allocations: 0B` 🥳 Thank you so much for that hint!
mbuf has quit [Quit: Leaving]
gravicappa has quit [Ping timeout: 272 seconds]
vicfred has quit [Quit: Leaving]
olle has joined #ocaml
dhil has quit [Quit: Leaving]
<d_bot> <quernd> Thanks, that's good to know! I'll take a look at what changed in H2 so we're prepared for the next release
gravicappa has joined #ocaml
perrierjouet has quit [Ping timeout: 272 seconds]
vicfred has joined #ocaml
olle has quit [Ping timeout: 276 seconds]
<d_bot> <anmonteiro> Nice
<d_bot> <anmonteiro> I can make a release soon if y’all need it
<d_bot> <anmonteiro> I hate releasing software. I vendor all my packages in my private monorepo
<d_bot> <ansiwen> We are also locking everything, (not monorepo yet), else would have to fix something every week. (That’s what I like in the Go community, minor releases are guaranteed to have no breaking changes.) So, if there is no additional QA done, I don’t mind release or not. It helps to backport fixes without breaking changes though.
vicfred has quit [Quit: Leaving]
bartholin has quit [Ping timeout: 272 seconds]
<d_bot> <mbacarella> before you do that, could I sneak an async TLS PR in?
<d_bot> <anmonteiro> you have all the time in the world 🙂
<d_bot> <mbacarella> (this would add support for tls-async, right now it only supports async_ssl)
vicfred has joined #ocaml
<d_bot> <mbacarella> I always groan a bit now when I have to do a release because every time I try the opam repo maintainer let's me know I managed to get something wrong 😂
bartholin has joined #ocaml
perrierjouet has joined #ocaml
bartholin has quit [Ping timeout: 250 seconds]
perrierjouet has quit [Quit: WeeChat 3.5]
<d_bot> <anmonteiro> this would be in gluten, and then h2 also needs a small changr
perrierjouet has joined #ocaml
spip has joined #ocaml
bobo has quit [Ping timeout: 246 seconds]
olle has joined #ocaml
bartholin has joined #ocaml
dextaa4 has quit [Remote host closed the connection]
bartholin has quit [Ping timeout: 272 seconds]
gravicappa has quit [Ping timeout: 240 seconds]
rgrinberg has joined #ocaml
bartholin has joined #ocaml
Anarchos has quit [Quit: Vision[]: i've been blurred!]
kotrcka has joined #ocaml
olle has quit [Ping timeout: 272 seconds]
perrierjouet has quit [Quit: WeeChat 3.5]
perrierjouet has joined #ocaml
rgrinberg has quit [Quit: My MacBook has gone to sleep. ZZZzzz…]
bartholin has quit [Ping timeout: 272 seconds]
Tuplanolla has quit [Quit: Leaving.]
bartholin has joined #ocaml
Serpent7776 has quit [Quit: leaving]
Haudegen has quit [Ping timeout: 276 seconds]
<drakonis> is there a way to get refinement types on ocaml?
bartholin has quit [Quit: Leaving]
<brettgilio> drakonis to my knowledge no.
<drakonis> ah well.
<brettgilio> "I wonder if we can encode full System F(no inference) with enough GADT magic."
<brettgilio> At a glance, I think it is possible. But it would be tough.
<drakonis> it seems like its already there without needing GADT?
<brettgilio> drakonis yeah, somebody said the module system works similarly
<drakonis> there's certainly a lot of room for adding these things
<drakonis> but i highly suspect these are only going to happen after 5.0 lands
<brettgilio> I'd still like something similar to typeclasses in OCaml
<brettgilio> its not hard to emulate, but I wish it was more in-built