<discocaml>
<softwaresirppi> Guys and also a quick question, is Ocaml theoretically sound like Haskell?
<discocaml>
<softwaresirppi>
<discocaml>
<softwaresirppi> Can I use it to demonstrate category theory and stuff?
germ has joined #ocaml
YuGiOhJCJ has joined #ocaml
<discocaml>
<yawaramin> it's not an 'afterthought', it's very much part of the language. i'm not sure but i think by 'extensions' they mean additions on top of the older Caml language
<euouae>
softwaresirppi: what do you mean by theoretically sound?
<discocaml>
<softwaresirppi> That's interesting
<discocaml>
<softwaresirppi> So e languages are more functional than other right
<discocaml>
<softwaresirppi> Some languages are more functional than other right
<discocaml>
<softwaresirppi> Okay let me rephrase.
<discocaml>
<softwaresirppi>
<discocaml>
<softwaresirppi> Will I be stuck if I learn functional programming theory or go through the SICPwith Ocaml?
<discocaml>
<softwaresirppi> Okay let me rephrase.
<discocaml>
<softwaresirppi>
<discocaml>
<softwaresirppi> Will I be stuck if I learn functional programming theory or go through the SICP with Ocaml?
<euouae>
You want me to answer what I think about you getting stuck?
<euouae>
OCaml is a great language and you will benefit greatly from studying it. Category theory is generally studied on its own. OCaml is close to Coq, and you can study Coq's type system for example.
<discocaml>
<octachron> The language extension part of the manual is mostly the staging part of the manual for new features (which the implication that they might be refined further in later OCaml versions)
<discocaml>
<octachron> Both OCaml and Haskell are Turing complete and thus cannot fully be used for proving any theorems.
<discocaml>
<octachron> In both language, you have to restrict yourself to a subset of a language to write proof.
<discocaml>
<octachron> For instance, `let compose: type a b c. (a -> b) * (b -> c) -> a -> c = fun (f,g) x = g (f x)` is a valid proof of `(A⇒B) && (B⇒C) ⇒ (A ⇒ C)`.
<discocaml>
<octachron> However, `let rec f: type a b. (a,b) Either.t -> a * b = fun e -> match e with Left x -> x, snd (f e) | Right x -> fst (f e), x` is (obviously) not a valid proof of `(A || B) ⇒ A && B`.
<euouae>
octachron, aren't you conflating too many things?
<octachron>
In which way?
<euouae>
Maybe you've just phrased it wrong but "Both OCaml and Haskell are Turing complete and thus cannot fully be used for proving any theorems." is strange. What does "fully" mean here as qualifier? (i.e. all theorems of a language?) Also *any* theorems should be all theorems?
<euouae>
You're also taking the stance that a proof must be a witness of its corresponding theorem as type, but there's no reason why /that/ particular encoding has to be taken.
<euouae>
e.g. Z3 prover is implemented in C++, it doesn't mean C++ uses its type system to prove things
<octachron>
In the sense that if you use the full feature set of the language, you cannot trust the proofs that you have written.
<octachron>
The code of the Z3 prover is not intended as a proof in itself?
<euouae>
You apply CT-Thesis judiciously, not just everywhere
<octachron>
You can use any language to write a prover, but then once you have a prover, the soundness of the host language is irrelevant.
<euouae>
I think that all these details might be lost on the person who asked the original question
<euouae>
If you want to prove things you can use Coq which looks like OCaml
<discocaml>
<._null._> (What is CT if not Church Thesis?)
<octachron>
Probably CH for Curry-Howard?
<euouae>
Yeah it was a typo for curry-horward correspondence
<octachron>
But yes, I agree that Coq is better vehicle to learn about proofs.
euouae has left #ocaml [#ocaml]
pi3ce has quit [Read error: Connection reset by peer]
pi3ce has quit [Read error: Connection reset by peer]
pi3ce has joined #ocaml
<discocaml>
<contextfreebeer> SICP is a fine book, some people don't like it but I am a big fan, but it is not a good resource for learning hardcore functional programming, it is more like a basic text on computer science and software engineering, it covers a lot of stuff and doesn't go too deep into anything but it will expose you to a lot of ideas and the exercises are excellent, I haven't found a book with better exercises personally, they are fun and challengin
<discocaml>
<contextfreebeer> but to really learn functional programming you need a strictly typed language IMO, like OCaml or Haskell, that's where functional programming really shines
<discocaml>
<softwaresirppi> Interesting. So is there anything else you recommend?
<discocaml>
<contextfreebeer> for FP?
<discocaml>
<softwaresirppi> Yep
<discocaml>
<softwaresirppi> I just wanna be able to write correct, provable and proper programs
<discocaml>
<contextfreebeer> oh then absolutely the above
<discocaml>
<contextfreebeer> you will love it
<discocaml>
<contextfreebeer> it is a great introduction to pure functional programming and theorem proving
<discocaml>
<softwaresirppi> SOUNDS VERY COOL
<discocaml>
<contextfreebeer> it is very cool
<discocaml>
<softwaresirppi> where can i learn fundamental math by the way?
<discocaml>
<contextfreebeer> I think this book is accessible enough without strong math skills even though it would definitely help, proofs are very difficult, you can't BS your way to a solution in these exercises for the most part
<discocaml>
<contextfreebeer> I think you would learn some mathematical thinking from going through this, otherwise just pick up some textbooks
<discocaml>
<softwaresirppi> my thought process is kinda fuzzy now which i wanna get better at. good reasonings, notations, algorithms (also the machine learning kinda algos).
<discocaml>
<softwaresirppi> if you have any cool resourse please link!
<discocaml>
<contextfreebeer> like Book of Proof
<discocaml>
<softwaresirppi> i see
<discocaml>
<contextfreebeer> there's a few books along these lines, also How to Prove It
semarie has joined #ocaml
<discocaml>
<contextfreebeer> you can shop around and choose what you like, most of them are free
<discocaml>
<contextfreebeer> They all discuss fundamental proof techniques and cover basic working knowledge in math at the same time
<discocaml>
<contextfreebeer> but watch out, all of them are classical mathematics, whereas Rocq is a system for doing constructive mathematics by default
<discocaml>
<contextfreebeer> which basically means you can't do proofs like: this is true because if it isn't true we get some result that doesn't make sense
<discocaml>
<contextfreebeer> which allows you to prove some statements without giving any evidence
<discocaml>
<contextfreebeer> but no need to think too deeply about that, it just means that the proof techniques are different
<discocaml>
<softwaresirppi> interesting... so you prove by constructing it of devising an algo to construct it
<discocaml>
<softwaresirppi> yeah ive heard about emm
<discocaml>
<softwaresirppi> coool
<discocaml>
<contextfreebeer> Yeah, essentially, any time you prove something exists you must show that thing
<discocaml>
<contextfreebeer> whereas in classical mathematics you can prove something exists by showing it can't not exist
<discocaml>
<contextfreebeer> but maybe there is no way to discover that thing
<discocaml>
<contextfreebeer> no known way
<discocaml>
<softwaresirppi> so were not assuming the fact `a thing can exist OR not exist.`
<discocaml>
<softwaresirppi> QUANTUM THINGGG
<discocaml>
<contextfreebeer> exactly
<discocaml>
<contextfreebeer> or to be more precise every statement is either true or not true
<discocaml>
<softwaresirppi> okay then what do you think about doing machine learning in ocaml?
<discocaml>
<contextfreebeer> in this case, "X doesn't not exist" is different from "X exists"
<discocaml>
<softwaresirppi> im interesting in the whole landscape of algorithms(let it be math, classical algorithms, ml, ...)
<discocaml>
<contextfreebeer> idk, I'm not familiar with ml at all
<discocaml>
<contextfreebeer> it's not a quantum uncertainty thing, it's just that there is a structural difference, in classical math you lose some information because those two things are regarded as the same, because you have this axiom that something is either true or not true, and a consequence of that is that not not P implies P
<discocaml>
<contextfreebeer> but that doesn't hold in constructive math
<discocaml>
<softwaresirppi> damn my whole boolean algebra went down the drain
<discocaml>
<contextfreebeer> you mean what do I do?
<discocaml>
<softwaresirppi> yeah like your expertise or summin man?
<discocaml>
<contextfreebeer> I'm doing a pure math degree at the moment
<discocaml>
<yawaramin> that's such a huge swath of possible techniques that it's difficult to know what to recommend. eg many of the OCaml people also work on verifiable systems software with C static analysis tooling like Frama-C, maybe you should use that if you write C code. or for Java you could use JML. Or Ada's Spark. functional programming is a small piece of the puzzle for software correctness. i recommend watching this talk by Prof. Leroy https://youtu.be
<discocaml>
<softwaresirppi> Thank you! The title captivats me!!!
<discocaml>
<softwaresirppi> Thank you! The title captivates me!!!
raskol has joined #ocaml
f[x] has quit [Remote host closed the connection]
semarie has quit [Quit: quit]
semarie has joined #ocaml
<discocaml>
<gooby_clown> How viable would it to create an OCaml version of numpy and matplotlib
<dmoerner>
i'm just trying to set up opam, but any operation after init gives an error that i've run out of space on /tmp. however, it seems like i've only used 75 mb / 1 gb in /tmp, so i don't understand why it's giving that error
semarie has joined #ocaml
<discocaml>
<otini_> Possibly it cleans up /tmp after the failure.
<companion_cube>
opam puts stuff in ~/.opam
neiluj has joined #ocaml
<dmoerner>
i can watch the directory, and it only uses a maximum of 75 mb in /tmp. and the error message is about /tmp: [ERROR] Could not update repository "default": /usr/bin/opam: "mkdir" failed on /tmp/opam-4801-070926: No space left on device
<neiluj>
Hi! regarding the problem I had earlier with the Lru cache in a mutable field and my application being blocked -- I suspect there is deadlock of sorts, which ocaml type/module would provide a lock for multiple readers and several readers? mutex?
<neiluj>
one writer
<octachron>
dmoerner, this could be a permission/sandboxing issue that makes it impossible for opam to create directories in /tmp
<discocaml>
<otini_> neiluj: you can ensure mutual exclusion of writers with the Mutex module
<neiluj>
thanks, I believe the fact that the readers access a mutable record field make them act as writers somehow
<discocaml>
<otini_> Not sure what you mean by that
<discocaml>
<otini_> there’s no special treatment of record field mutations, it’s compiled as a plain write
<discocaml>
<otini_> and reads are compiled as plain loads
<discocaml>
<otini_> (which can lead to data races, maybe that’s your problem idk)
<contificate>
There isn't really much in the way of MRSW, recursive, etc. mutexes in the standard library - but they're easy enough to implement. There's several variations of MRSW, but the simplest just causes a waiting writer to stop any reader from acquiring the lock in the meantime.
<discocaml>
<otini_> the simplest way of all being an Atomic.t 🤔
<discocaml>
<otini_> ah no, not if we’re talking about an actual data structure
<contificate>
If you want to avoid busy waiting, you need a signalling mechanism, so you end up with a Condition and Mutex as well.
<contificate>
Still, neiluj, you should narrow down where this is happening. Maybe get a backtrace or something. It's unusual to just have a deadlock out of nowhere with no locking (as they tend to arise out of lock ordering violations).
<neiluj>
thanks for the advice!
<neiluj>
basically I have one record with mutable field containing either Map/HMap/Lru cache, a worker to trigger a trim of the cache, and a worker to find elements in the cache, and a worker to pop elements from the cache (which does a cache trim as well after completion)
<neiluj>
using Lwt for asynchronous IO
<neiluj>
I notice that when I trim the cache at the same time as elements in the cache are accessed, the application does not stop, but not doing so the application stops
contificate has quit [Quit: Client closed]
<discocaml>
<softwaresirppi> do you use it!!
<discocaml>
<softwaresirppi> how is the experience!
<discocaml>
<softwaresirppi> this server is so activee
<discocaml>
<gabyfle> Haha I'm currently building a Sound Analysis library to allow computation of (phase|mag|PSD|complex|mel)-spectrograms and other kind of features from time series
<discocaml>
<gabyfle> And it's all based on Owl
<discocaml>
<softwaresirppi> !!! wow
<discocaml>
<gabyfle> It's super dope, I had a bit of trouble with the operators actually but when you're used to it it's insane
<discocaml>
<softwaresirppi> analysis in the sense how?
<discocaml>
<softwaresirppi> i wanna learn owl!!
<discocaml>
<softwaresirppi> plotting, data exploree, machine learning!!
<discocaml>
<softwaresirppi> but i dont know if it can do image processing
<discocaml>
<gabyfle> I bought the book from the Owl creators it's very well written and it have a lot of nice examples to learn the whole thing
<discocaml>
<softwaresirppi> wow
<discocaml>
<softwaresirppi> namee?
<discocaml>
<softwaresirppi> what can i do with owl?
<discocaml>
<gabyfle> I'm a bit ashamed that there isn't that many users of Owl because it's super super cool and you don't have to deal with Python hehe
<discocaml>
<gabyfle> Plus you have the benefits of OCaml's type system which is even more 🔥
<discocaml>
<gabyfle> You can do anything from linear algebra, differentiation and optimization to deep learning
<discocaml>
<gabyfle> You can even export models you built into ONNX format
<discocaml>
<gabyfle> But be aware that sometimes there are missing features from the usual libs like numpy
<discocaml>
<otini_> neijul: Lwt is not safe for use in parallel
<discocaml>
<gabyfle> (for example I had to reimplement the numpy.unwrap for this project but using owl)
<discocaml>
<softwaresirppi> python is not that bad.. i just dont dont like numpy, pandas, scikit-learn, matplotlib combo
<discocaml>
<softwaresirppi> it sounds too good to be true
<discocaml>
<softwaresirppi> in the docs, i can even find a NLP module
<discocaml>
<softwaresirppi> if the fundamentals are set, im ready to build stuff on
<discocaml>
<gabyfle> Yeah it's not that bad but you're not backed by ocaml's type system and the overall tooling around Python feels a bit odd to me when I have to compare to OCaml's
<discocaml>
<softwaresirppi> fair
<discocaml>
<gabyfle> Plus OCaml can be compiled to native so you can make super fast stuff
<discocaml>
<gabyfle> Go then haha ! I would be super happy to help if you have any issues while learning it
<discocaml>
<softwaresirppi> thank you! im just learning ocaml now
<discocaml>
<softwaresirppi> takes a bit of time
<discocaml>
<softwaresirppi> also i cant find many ocaml conference talks on youtube... which is kinda sad
<discocaml>
<gabyfle> Yes ! Exactly
<discocaml>
<softwaresirppi> im going through the ocaml correct + efficient + beautiful
<discocaml>
<softwaresirppi> i hope i pick it up soon!!!
<discocaml>
<gabyfle> I personally read a french book called "Apprendre à Programmer avec OCaml" which is super cool as it let you go through the implementation to all the common data structures you'll encounter while programming. I know that Real World Ocaml is said to be an excellent book but it's based on Janestreet's base library. And yeah the book you cited is excellent too
<discocaml>
<softwaresirppi> jane street core vs ocaml core?
<discocaml>
<softwaresirppi> i dont know french 😢
<discocaml>
<softwaresirppi> i was asking which one you prefer gabyfle
<discocaml>
<gabyfle> I don't have a personal preference because I don't have tried Janestreet's base yet
<discocaml>
<gabyfle> I didn't feel the need to
<discocaml>
<softwaresirppi> fair
<discocaml>
<softwaresirppi> bro i wanna become fluent in ocaml like you all!!!
<discocaml>
<gabyfle> But I'm pretty sure some guys here will have nice opinions on which one is nice to use for which kind of case
<discocaml>
<gabyfle> Hahaha I'm still a beginner there's lots of areas of the language that I need to explore
<discocaml>
<gabyfle> But you made a great choice, OCaml is dope. Trying it is adopting it
<discocaml>
<softwaresirppi> name some?
<discocaml>
<softwaresirppi> yeah the feature set is goated
<discocaml>
<softwaresirppi> but some syntax i gotta get used to
<discocaml>
<gabyfle> - how to use polymorphic variants efficiently and when to use them
<discocaml>
<gabyfle> - concurrency in OCaml
<discocaml>
<gabyfle> - working with classes
<discocaml>
<gabyfle> - going deeper with functors and when to use them wisely
<discocaml>
<gooby_clown> Sick logo
<discocaml>
<gabyfle> Hehe actually I'm not good enough in design to have made this on my own, it was done by dall-e (see the acknowledgement section of the readme)
<discocaml>
<softwaresirppi> interesting
euphores has quit [Quit: Leaving.]
<discocaml>
<softwaresirppi> isnt it flipped git logo
<discocaml>
<softwaresirppi> lol
<discocaml>
<softwaresirppi> anyways guys why is there `List.flatten` and `List.concat` both doing the same thing?
euphores has joined #ocaml
<discocaml>
<deepspacejohn> According to git history, concat was added as an alias for flatten 28 years ago. As for why, I don't know.
<discocaml>
<softwaresirppi> alright
<discocaml>
<softwaresirppi> coming from other languages i expected `concat` to behave like `List.append`
<discocaml>
<softwaresirppi> how did you look it up!! 👀
<discocaml>
<softwaresirppi> aww even the commit message is in french
<discocaml>
<softwaresirppi> i think i gotta learn french to do ocmal lol
<discocaml>
<softwaresirppi> i think i gotta learn french to do ocaml lol
<discocaml>
<deepspacejohn> only for older stuff, at this point. these days everything seems to be in English.
<discocaml>
<deepspacejohn> My _assumption_ is that they wanted an interface consistent with `String.concat`, `Array.concat` etc which concat lists of strings and arrays. since `List.flatten` already does that then it's easy to just add an alias for it.
<discocaml>
<softwaresirppi> i see
<discocaml>
<softwaresirppi> yo guys `List.init` this function funnily creates a mapped range lol
<discocaml>
<softwaresirppi> and the stdlib functions all raise exceptions... in version 4.05, functions with `name_opt` gets added
<discocaml>
<softwaresirppi> thats a history lesson for me
<discocaml>
<deepspacejohn> I think historically people preferred exceptions because they don't need to allocate an extra option for every successful action. but at some point people started preferring options and result types instead
<discocaml>
<deepspacejohn> the Jane Street stdlib replacements are the opposite, using options by default and `name_exn` as the exception versions.
<discocaml>
<softwaresirppi> what do you think about ocaml having exceptions and options?
<discocaml>
<deepspacejohn> they both have their use cases. I tend to use options/results most of the time when I can but sometimes its easier to use exceptions.
<discocaml>
<softwaresirppi> alright! exceptions easy? may i know where?
<discocaml>
<deepspacejohn> if everything that could possibly raise an error had to return a result type, then that changes every function's type and you have to use `Result.map` everywhere. With an exception you can just put a `try` expression at the beginning of your program.
spew has joined #ocaml
<discocaml>
<deepspacejohn> binding operators make it easier to deal with, but exceptions are still quicker and easier.
<discocaml>
<softwaresirppi> isnt that the whole point of option types 😅 carrying them in types
<discocaml>
<softwaresirppi> alright i get your point
<discocaml>
<contextfreebeer> there are cases where exceptions make more sense, especially OCaml exceptions. for example breaking out of folds, if you use Result you will need to thread it all the way through whereas with exceptions you can bail out early