germ has quit [Read error: Connection reset by peer]
germ has joined #ocaml
Tuplanolla has quit [Quit: Leaving.]
alfiee has joined #ocaml
alfiee has quit [Ping timeout: 252 seconds]
Mister_Magister has quit [Quit: bye]
Mister_Magister has joined #ocaml
Haudegen has quit [Quit: Bin weg.]
alfiee has joined #ocaml
alfiee has quit [Ping timeout: 252 seconds]
<discocaml>
<dubious245> Took all weekend and I had to completely rewrite how I store images but I have implemented canny edge detection.
<discocaml>
<dubious245> I am quite proud.
alfiee has joined #ocaml
alfiee has quit [Ping timeout: 252 seconds]
<discocaml>
<diligentclerk> nice. I spent like multiple hours on a Coq proof and made essentially no progress
<discocaml>
<dubious245> What exactly is coq?
<discocaml>
<Kali> coq is proof assistant, with proofs written in a dependently-typed language and manipulated in a meta-language, with tools to view the state of the proof interactively
<discocaml>
<dubious245> Ah.
<discocaml>
<dubious245> I see.
<discocaml>
<dubious245> I never liked doing proofs in class.
<discocaml>
<Kali> it is based on the "curry-howard correspondance" which asserts an equality between proofs : propositions and terms : types
<discocaml>
<Kali> the inhabitance of a type being the proof of the proposition
<discocaml>
<gooby_diatonic> Why not?
<discocaml>
<dubious245> I struggled to understand them and resorted to rote memorization to get through those parts.
<discocaml>
<gooby_diatonic> Studying proofs in your own time can be rewarding if you find the right context for doing them
<discocaml>
<gooby_diatonic> For you maybe in the context of image processing
<discocaml>
<gooby_diatonic> You can take your time to properly understand and that
<discocaml>
<gooby_diatonic> It becomes almost like piecing a puzzle
<discocaml>
<dubious245> Where would you even start with something like that?
<discocaml>
<shawnfrostx> for general proofs I recommend How to Prove It by daniel velleman. for coq theres the software foundations book.
<discocaml>
<Kali> Proofs by Jay Cummings is very good
<discocaml>
<Kali> though it's more focused on mathematical proofs rather than computational proofs, it's still a very illustrative book
<discocaml>
<Kali> and funny, too
<discocaml>
<Kali> i second the software foundations book
<discocaml>
<Kali> there's also a bunch of interactive games about learning how to prove thing with Leanv4 on https://adam.math.hhu.de/
<discocaml>
<shawnfrostx> probably the easiest thing to do is learn the basics of proofs and pick a subject you're interested in and start proving things there.
<discocaml>
<shawnfrostx> for ocaml, you can try the types and programming languages book once u have a decent grasp on structural induction. the first like 14 chapters is pretty elucidating.
alfiee has joined #ocaml
alfiee has quit [Ping timeout: 260 seconds]
myrkraverk has joined #ocaml
myrkraverk_ has quit [Ping timeout: 268 seconds]
myrkraverk_ has joined #ocaml
alfiee has joined #ocaml
myrkraverk has quit [Ping timeout: 260 seconds]
alfiee has quit [Ping timeout: 252 seconds]
<dh`>
the curry-howard isomorphism also means that writing proofs is a lot like writing code
<dh`>
like, you have a thing you want to do and you need to write code for it
<dh`>
what code do you write? that's a matter of breaking the problem up into chunks and steps and so on
<dh`>
proofs turn out to basically be exactly the same skill
<dh`>
this is less obvious with paper proofs than it is in a proof assistant, and it's not how math folks think about it, but it's nonetheless true
alfiee has joined #ocaml
alfiee has quit [Ping timeout: 252 seconds]
YuGiOhJCJ has quit [Read error: Connection reset by peer]
YuGiOhJCJ has joined #ocaml
alfiee has joined #ocaml
alfiee has quit [Ping timeout: 252 seconds]
alfiee has joined #ocaml
alfiee has quit [Ping timeout: 260 seconds]
YuGiOhJCJ has quit [Quit: YuGiOhJCJ]
alfiee has joined #ocaml
alfiee has quit [Ping timeout: 252 seconds]
Serpent7776 has joined #ocaml
alfiee has joined #ocaml
alfiee has quit [Ping timeout: 260 seconds]
bartholin has joined #ocaml
bartholin has quit [Quit: Leaving]
alfiee has joined #ocaml
alfiee has quit [Ping timeout: 260 seconds]
Haudegen has joined #ocaml
alfiee has joined #ocaml
alfiee has quit [Ping timeout: 252 seconds]
dhil has joined #ocaml
patrick_ is now known as patrick
alfiee has joined #ocaml
alfiee has quit [Ping timeout: 252 seconds]
patrick has quit [Changing host]
patrick_ has joined #ocaml
infohazards has quit [Remote host closed the connection]
alfiee has joined #ocaml
mange has quit [Quit: Zzz...]
alfiee has quit [Ping timeout: 252 seconds]
wbooze has joined #ocaml
alfiee has joined #ocaml
alfiee has quit [Ping timeout: 252 seconds]
myrkraverk has joined #ocaml
myrkraverk_ has quit [Ping timeout: 252 seconds]
alfiee has joined #ocaml
alfiee has quit [Ping timeout: 252 seconds]
ridcully has quit [Quit: WeeChat 4.5.2]
<discocaml>
<barconstruction> How to prove it by Velleman is a common textbook recommendation. I've heard good things about it. I also think that you can probably learn it by reading rigorous math books and solving exercises (e.g. Linear Algebra Done Right or Calculus by Apostol), but you probably want some external authority to check your work and point out flaws in your arguments.
<discocaml>
<barconstruction> I've heard of using Coq to teach proofs but since Coq forces you to check every little detail it can cause you to miss the forest for the trees (i.e. students don't develop higher level reasoning skills).
<discocaml>
<barconstruction> When I first started Coq I often got sucked into the trap of focusing on making line by line incremental progress and then ending up at a dead end because I wasn't thinking at a higher level of reasoning. I still do that today when I get tired.
<discocaml>
<barconstruction> The Software foundations book is a lot of fun
gahr_ is now known as gahr
alfiee has joined #ocaml
alfiee has quit [Ping timeout: 252 seconds]
<discocaml>
<darrenldl> personally felt that software foundations vol 1 was inspiring and made proofs click for me
<discocaml>
<_4ad> or am I holding it wrong, and I should do this sort of thing completely differently?
<discocaml>
<_4ad> basically it's a composition of lattices, where bottoms are being joined, but individual tops are kept separate (and there's an overarching top).
<discocaml>
<_4ad> it's just bothering me how similar and yet how different it is to both map and bind, and that makes me thing there could be some sort of useful generalization or something.
<discocaml>
<_4ad> and yes, I tried to make two types, one with Top, and the other with Bottom, but it just gets too indirect/too confusing. not better.
<companion_cube>
what do you use this stuff for?
ridcully has joined #ocaml
alfiee has joined #ocaml
<discocaml>
<_4ad> it's for the implementation of a programming language (CUE), where the main data structure is a lattice (actually a Heyting algebra).
alfiee has quit [Ping timeout: 260 seconds]
<discocaml>
<_4ad> basically the rules are simple:
<discocaml>
<_4ad> 1. it's a commutative monoid. we call the identity element "top" and the binary operation "meet".
<discocaml>
<_4ad> 2. it has an absorption element "bottom" such that `bottom * a = bottom` for all a.
<discocaml>
<_4ad> 3. there are implementations for scalars, where non-equal meets return bottom.
<discocaml>
<_4ad> 4. there are heterogeneous implementations, combining multiple types, where meet of disjoint scalar types return bottom, and meets of the same type are the scalar meets with lifted bottoms. note, however, that a top is not lifted, the individual, scalar tops are distinguishable. and also there can be multiple non-scalar types, and meet of disjoint non-scalar types is not necessarily bottom.
<discocaml>
<_4ad> 5. things should be ergonomic and modular in the sense that adding more type can be done incrementally, and there shouldn't be a combinatorial explosion of pattern matches.
<discocaml>
<_4ad> (there's also a join operation, but don't worry about that).
Haudegen has joined #ocaml
<discocaml>
<eval.apply> i think needing to pass the `f` in that a subset of `t` is a hint that you should break up `t`
<discocaml>
<eval.apply> bottom is obviously distinct in a join semilattice so it should be as well in the encoding
<discocaml>
<eval.apply> wouldn't `type 'a t = 'a option option` be a faithful encoding and make it obvious that it is actually bind
alfiee has joined #ocaml
alfiee has quit [Ping timeout: 252 seconds]
<discocaml>
<eval.apply> also i said join semilattice there which is triply confusing because it's top that's special there, join semilattices are what people usually use in computer science stuff and i was trying to meet you at the middle
<discocaml>
<eval.apply> there's other reasons you'd want it to be broken up like efficiency, e.g. with intervals (-inf, +inf) is "top" (in your perspective) but doesn't need a layer of boxing to distinguish it from a filled out interval like (1, 5)
cr1901 has quit [Read error: Connection reset by peer]
cr1901 has joined #ocaml
<discocaml>
<eval.apply> in types for example: `Any | Int` instead of `Bottom` and `Value Int`
alfiee has joined #ocaml
alfiee has quit [Ping timeout: 252 seconds]
Haudegen has quit [Quit: Bin weg.]
wbooze has quit [Remote host closed the connection]
wickedshell has quit [Remote host closed the connection]
bartholin has joined #ocaml
alfiee has joined #ocaml
Anarchos has joined #ocaml
chiselfuse has joined #ocaml
alfiee has quit [Ping timeout: 260 seconds]
myrkraverk_ has joined #ocaml
myrkraverk has quit [Ping timeout: 252 seconds]
alfiee has joined #ocaml
Anarchos has quit [Quit: Vision[]: i've been blurred!]
alfiee has quit [Ping timeout: 252 seconds]
<discocaml>
<_4ad> good point, yes.
<discocaml>
<_4ad> yes.
<discocaml>
<_4ad> I don't understand the rest of the argument tough, wouldn't a type like `'a option option` be less efficient because of *more* boxing? I don't understand how it can result in less boxing. (not that boxing really matters in my case).
<discocaml>
<_4ad> it's somewhat unfortunate that most values would turn out as `Some (Some x)`.
Haudegen has joined #ocaml
<discocaml>
<eval.apply> the 2nd part would be about ditching the inner option for more direct representations
<discocaml>
<gabyfle> Hi ! I'm willing to implement a generic functionality into an OCaml project and I'm wondering what design choice would best suit it. This generic functionality is meant to be used to build more specific ones (in fact, I'm building an IIR filter, that'll then be used to create low, band and high pass filters).
<discocaml>
<gabyfle>
<discocaml>
<gabyfle> My number 1 goal is to have the simplest API as possible so that even programmers/scientists with very little to zero knowledge in OCaml can use it seemlessly.
<discocaml>
<gabyfle>
<discocaml>
<gabyfle> I've thought about two ways of doing so:
<discocaml>
<gabyfle>
<discocaml>
<gabyfle> - First one that came to my mind is using functors, with a generic IIR functor that could be used to then create more specific filters. Regarding OCaml, I really feel like it's the more idiomatic way of doing this, and this is how I'd write this functionality in a "normal" project.
<discocaml>
<gabyfle> - Second one is using a class to create such a generic IIR filter and then instantiate it in the specific functions
<discocaml>
<gabyfle>
<discocaml>
<gabyfle> Note that actually, the project doesn't contains any functors. If you guys have any opinion about this, feel free to share 🙂
alfiee has joined #ocaml
alfiee has quit [Ping timeout: 245 seconds]
myrkraverk has joined #ocaml
myrkraverk_ has quit [Ping timeout: 252 seconds]
alfiee has joined #ocaml
alfiee has quit [Ping timeout: 244 seconds]
polykernel has quit [Remote host closed the connection]
polykernel has joined #ocaml
alfiee has joined #ocaml
Haudegen has quit [Quit: Bin weg.]
Haudegen has joined #ocaml
alfiee has quit [Ping timeout: 246 seconds]
Tuplanolla has joined #ocaml
bibi_ has quit [Quit: Konversation terminated!]
alfiee has joined #ocaml
bibi_ has joined #ocaml
alfiee has quit [Ping timeout: 244 seconds]
myrkraverk_ has joined #ocaml
myrkraverk has quit [Ping timeout: 260 seconds]
infohazards has joined #ocaml
alfiee has joined #ocaml
alfiee has quit [Ping timeout: 244 seconds]
myrkraverk has joined #ocaml
myrkraverk_ has quit [Ping timeout: 248 seconds]
bartholin has quit [Ping timeout: 276 seconds]
bartholin has joined #ocaml
myrkraverk_ has joined #ocaml
myrkraverk has quit [Ping timeout: 272 seconds]
alfiee has joined #ocaml
alfiee has quit [Ping timeout: 252 seconds]
qu1j0t3 has joined #ocaml
bartholin has quit [Quit: Leaving]
Serpent7776 has quit [Ping timeout: 252 seconds]
dhil has quit [Ping timeout: 276 seconds]
alfiee has joined #ocaml
alfiee has quit [Ping timeout: 248 seconds]
szkl has joined #ocaml
myrkraverk has joined #ocaml
myrkraverk_ has quit [Ping timeout: 265 seconds]
<discocaml>
<mbacarella> anyone planning to go to DEFCON this year M
<discocaml>
<mbacarella> anyone planning to go to DEFCON this year?