11:42 <olle> Hmmmm

11:42 <olle> https://dev.realworldocaml.org/concurrent-programming.html

11:42 <olle> Not updated to use let* notation?

17:28 <d_bot> <arctumn> So i was implementing some Natural Numbers arithmetic using Piano Axioms but with a catch i cannot use equal sign implemented in the stdlib

17:28 <d_bot> <arctumn> however I started to question myself if the pattern matching is not using itself the equal sign operator, because if it is i flawed myself and all

17:28 <d_bot> <arctumn> that i implemented is invalid by my own terms, did i really locked myself (because matching is using the equal operator behind)? Or is there an alternative so I don't contradict my own terms?

17:30 <Corbin> You are onto something quite interesting and deep, yes. Equality on natural numbers can be defined by primitive recursion.

17:33 <d_bot> <NULL> Do you consider as equally invalid equality on `nat` and equality of constructors of a sum type ?

17:33 <d_bot> <NULL> I'm not sure how you can discriminate between `O` and `S _` without some sort of equality

17:34 <Corbin> First, figure out how to test whether a nat is zero, and also how to take the predecessor of a nat. Both are primitive recursive. Then, you can build equality from primitive recursion on (WLOG) the left side; the base case is when the right side is zero, and the recursive case takes the predecessor of the right side.

17:39 <d_bot> <arctumn> I assumed that there are only two possible cases for number : type number = Zero | Successor of number.

17:39 <d_bot> <arctumn> my invalid equality would be straight using for example number = number to check if they're different or equal

17:43 <Corbin> How did you define primitive recursion?

17:43 <d_bot> <arctumn> For example to generate the next number ?

17:45 <d_bot> <arctumn> i matched if the number is Zero -> Successor Zero | Successor x -> Successor (Successor x)

17:47 <Corbin> Sure. That's the sucessor function. Here's what I've worked on recently: https://bpa.st/3XQA

17:48 <Corbin> You can think of `pr`, the primitive recursion axiom, as generalizing the match-expression. Instead of writing `match` yourself, you provide it with two functions which handle the Zero and Successor cases.

17:58 <d_bot> <arctumn> I see, so in the end there is no way around avoiding some equality... well thanks for the help 🙂

17:59 <Corbin> What do you mean? Peano's axioms explicitly include primitive recursion. From primitive recursion, we can build equality.

18:03 <companion_cube> or you can assume a logic with pre-existing equality :)

18:03 <d_bot> <arctumn> For the example you posted the match will always appear in a way or another to represent, unless I'm misunderstood the "match" in ocaml it will check if any of the cases is what its going to be matched, and my initial idea was to try to avoid that any representation of equality

18:06 <d_bot> <arctumn> I implement my own equality, but at some point its being based in already existing equality https://bpa.st/GRAA

18:18 <Corbin> Sure. The beauty of Peano is that we *only* need primitive recursion in order to talk about equality for natural numbers, and moreover that we get an algorithm for how to do it.

18:20 <Corbin> I would like to give you a glimpse of something not easy to read. https://bpa.st/KMTA is a compiler-generated program. You can ask OCaml to type-check it for you; it should have type `nat -> nat -> bool`. And there's only a single `match`, in the definition of `pr`.

18:22 <d_bot> <Deadrat> Is there any point in esy rn as opam 2.1 brought a lot qol changes in easy to use form?

19:38 <companion_cube> hmm, is [%error] valid in types/signatures?

20:13 <d_bot> <leviroth> As in ppx_optcomp?

20:14 <companion_cube> no, just an OCmal extension point

20:14 <companion_cube> turns out it is and my type error was somewhere else, though

21:13 <d_bot> <froyo> hey is loop invariants in auxillary recursive call's args faster or outside of it?