ppalka has quit [Remote host closed the connection]
mfp has quit [Ping timeout: 258 seconds]
ppalka has joined #ocaml
tormen has joined #ocaml
tormen_ has quit [Ping timeout: 258 seconds]
brettgilio has joined #ocaml
brettgilio has quit [Read error: Connection reset by peer]
brettgilio has joined #ocaml
gravicappa has joined #ocaml
mbuf has quit [Quit: Leaving]
wingsorc has quit [Ping timeout: 245 seconds]
narimiran has joined #ocaml
oni-on-ion has quit [Remote host closed the connection]
oni-on-ion has joined #ocaml
oni-on-ion has quit [Ping timeout: 268 seconds]
ggole has joined #ocaml
mbuf has joined #ocaml
vicfred has quit [Quit: Leaving]
Serpent7776 has joined #ocaml
pepesza has quit [Ping timeout: 265 seconds]
greenbagels has quit [Ping timeout: 258 seconds]
greenbagels has joined #ocaml
pepesza has joined #ocaml
Wojciech_K has joined #ocaml
dborisog_ has joined #ocaml
bartholin has quit [Quit: Leaving]
ollehar has joined #ocaml
<ollehar>
test
<simpson>
Yep.
mfp has joined #ocaml
<ollehar>
huzzah!
mbuf has quit [Quit: Leaving]
<ollehar>
no oni, eh? bah.
Serpent7776 has quit [Ping timeout: 265 seconds]
Serpent7776 has joined #ocaml
Haudegen has joined #ocaml
dhil has joined #ocaml
Serpent7776 has quit [Remote host closed the connection]
Serpent7776 has joined #ocaml
<dborisog_>
Ocsigen Eliom/server reports a warning about "unused variable cname" in the line "let ccodes = List.map ( fun (ccode, cname) -> ccode ) codes". Indeed, this variable is unused within the function. Is there a good way to get read of this warning?
<octachron_>
Why not rename the variable to `_cname`?
<dborisog_>
Do you mean "_cname" instead of "cname" or "_" instead of "cname"?
gravicappa has quit [Ping timeout: 265 seconds]
gravicappa has joined #ocaml
<dborisog_>
I do not know of any difference between variable names with and without underscore at the beginning of the name. For example, https://dev.realworldocaml.org/variables-and-functions.html states "Note that variable names must start with a lowercase letter or an underscore."
<dborisog_>
Anyways, "_" instead of "cname" removes the warning. Thank you for the hint!
<octachron_>
Variable whose names start with an underscore do not raise the unused variable warning.
<dborisog_>
Oh, thanks!
<octachron_>
So, if the variable is really unimportant, using `_` works fine. But if you want to remember what was the ignored variable, `_cname` may work better on the long term.
<dborisog_>
Got it!
dhil has quit [Ping timeout: 245 seconds]
jao has joined #ocaml
jao has quit [Changing host]
jao has joined #ocaml
dhil has joined #ocaml
<vsiles>
dborisog_: another solution could have been to use `fun c -> fst c`
<dborisog_>
vsiles: thank you.
<theblatte>
(or "List.map fst codes")
<dborisog_>
)
<dborisog_>
Thanks )
<vsiles>
theblatte++
<ggole>
I've always found it a touch strange that you could have a variable called _foo, which is supposed to indicate a variable that is not used, and then actually use it without a warning
<ggole>
Not much of a problem in practice, just odd.
<dborisog_>
ggole: it is likely related to the type-safe use of algeabraic data types. Synctactic sugar for the very case I faced earlier.
<flux1>
I guess in most such cases the code has been automatically generated. I mean, how do you use an underscore prefixed variable accidentally?
<flux1>
whereas it might simplify code generation a bit if it can just define the bindings it might or might not use up-front
<ggole>
For a code generator you would just use normal variable names
<flux1>
yes, but in that case it could cause a warning if it ends up not using the variable
<ggole>
Yeah, I guess. You could emit the annotation to turn that off, but that's a recent thing.
<theblatte>
could also be the result of a variable renaming
<theblatte>
a warning would be useful indeed
Wojciech_K has quit [Remote host closed the connection]
<dborisog_>
I currently watching lections on Category Theory, it was said that a tuple of types is a product of types (the result of "*"-alike operation of the algebra of types), and according to the theory, the absence of one types in the product means the unit type/empty/nothingness/void. Thus, if one wants to have no gaps in type inference and alike, all the types in the product must be mentioned.
<dborisog_>
It seems to the major source of such warnings is to inform programmes about variables he does not need, e.g. to keep the code clean as much as possible. But because of the algeabraic data types of OCaml and the commonality of partial use of products, elements-of-tuples, _name syntactic sugar is introduced.
<simpson>
dborisog_: There exist systems, broadly called *linear* logics or linear languages, where every name must be used.
<gahr>
(unless specified with a 0 quantifier :) )
<gahr>
(in which case the name must *not* be used)
<simpson>
(Right, names are ultimately an illusion.)
<dborisog_>
:D
FreeBirdLjj has joined #ocaml
<gahr>
"the absence of one types in the product means the unit" <-- well, except such a type is not inhabited
<gahr>
a pair is an existential proof of the first and second type, and you can't proof falsity (hence "absurd")
<simpson>
Yeah, we should distinguish between a type that has exactly one member, which in OCaml is called `unit`, and a type that has no members at all. (Or "inhabited", "uninhabited".)
<gahr>
I guess s/unit/Void/ in the above
<dborisog_>
Could by :) At the moment I'm trying to prevent my head from exploding ))
<dborisog_>
*could be
<Leonidas>
I agree, having a warning about using _'ed variables would be nice.
<companion_cube>
ugh, how do you write debug print statements then? :p
<Leonidas>
these are clearly used and should not be named _foo :p
<gahr>
does OCaml have any notion of the Void type?
<companion_cube>
Leonidas: I mean, sometimes in a match I have _x cause I don't use it except in a debug statement
<companion_cube>
gahr: no
<Leonidas>
I'd love if at some point I get to a stage where I don't do print debugging but use a debugger, like a normal human :)
<companion_cube>
Leonidas: some things are better debugged with print statements
<companion_cube>
(not all of them, but some)
<gahr>
companion_cube: good :)
<dborisog_>
Well, in the lectures Haskell (and a bit of C++) is used for programmatic examples, and if I understood correctly, there is association(or equality) between Void and (), and OCaml has (), unit.
<gahr>
I think you didn't understand correctly :)
<dborisog_>
:D could be
<gahr>
I'd see Void and unit as opposites, categorically speaking
<gahr>
one is the initial element, the other is the final element
<def`>
gahr: there is no predefined void type but you can get one with this:
<def`>
type t = |;;
<gahr>
dborisog_: to be precise: one is the "initial object", the other is the "terminal object"
<def`>
this defines an empty sum type, which is the zero you looking for.
<gahr>
def`: nice, that's smart
<simpson>
def`: Oh dang, that works? Nice!
<gahr>
I thought | required a type after it
<def`>
to eliminate a value of that type you can do let (x : t) = match x with _ -> .;;
<dborisog_>
Initial and Terminal objects of CT, then. In the lectures, Initial is the opposite of Terminal, and it should be easily transferable in algebraic data types systems.
<dborisog_>
:)
<def`>
"." represents an unreachable branch.
<Armael>
just don't do categories, kids
<def`>
let f (x : t) = ...
<simpson>
dborisog_: Yep. In general, a type theory's corresponding category has an initial object for the type with no values, being called "void" today, and a terminal object for the type with one value, called "unit". (If they exist at all.)
<def`>
(also: type t = { void : 'a. 'a })
<dborisog_>
(I'm kind want to understand lwt properly, and it is mentioned lwt is based on monads, and to understand monads... ) CT is a rather fascinating thing ))
<simpson>
dborisog_: Also, the stuff mentioned about *elements* can be generalized too. We could say that an element/value of a type is picked out by an arrow from the terminal object, just like in Set. In OCaml, `let f () = 42` is an arrow from the unit type to an int; that is, it chooses a value from the int type.
<sarna>
hi, I have a record with an option in it. can I write a function signature to unpack the option for me?
<gahr>
from the initial object
<sarna>
something like let foo { bar = Some(baz) } = ...
spew has joined #ocaml
<simpson>
gahr: Oh whoops, am I upside-down? Most common problem when working with categories, forgetting which way the arrows are pointed.
<Armael>
sarna: what if the option is None
<Armael>
you have to use pattern matching because you wouldn't handle all the cases otherwise
<sarna>
Armael: well, I want to fail then.. so I have to specify that. thanks :)
<Armael>
then you can do "let foo = function { bar = Some baz } -> ... | { bar = None } -> ..."
<gahr>
simpson: that was my impression, but I could be the one mistaken :)
<gahr>
I think it's () ->|const|-> everthing ->|absurd|-> Void
<dborisog_>
simplson: if I understand correctly, one of the main pragmatic uses of good CT knowledge in functional programming is to have strong designs of modules and polymorphic functions. I'm curious if any good book/tutorial/simple-intuitive-yet-enlightening-library exists for study.
<theblatte>
TIL "."
<theblatte>
OCaml syntax is always bigger than I think
<Leonidas>
gahr: type t = | is a relatively recent addition
<gahr>
it doesn't surprise me that people did fine without it for decades :)
<gahr>
dborisog_: the book produced from bartosz's series of blog posts is pretty good
<gahr>
dborisog_: "seven sketches in compositionality" is also very good book, in my opinion
<simpson>
dborisog_: To be frank, I don't think that modern "functional programming" has much to do with category theory. There are families of languages that are "closer to the category", like concatenative and APL, but also languages like OCaml that use a lot of category theory directly.
<dborisog_>
gahr: Oh! I have it on my reading list on the first position. It seems MIT has started uploading lectures, which are also associated with this book.
<gahr>
ah good to know!
<sarna>
Bartosz's video course is pretty nice as well :)
<gahr>
I love Bartosz... a few years ago at a c++ conference he gave a presentation about monads in c++
<gahr>
pretty nice
<dborisog_>
simpson: I think that CT is relevant to design of systems like agent-based models, where an agent takes a reduced information (in comparison to the structure and "amount" of inforation theoretically available to him). In here we have a structural change In and Out. And from his lectures on CT I understood functors would be rather useful in design of such systems, and that I would have to start my design from the simplest possible structure to the
<dborisog_>
richiest structure of the potentialy avilable information in the environment.
<simpson>
dborisog_: Sure. One of my favorite corners of category theory is using them for ontology; the objects of study are known as "ologs" https://arxiv.org/abs/1102.1889v2
<dborisog_>
simple because you cannot recover loses of structure
<dborisog_>
Oh! that's hugely relevant! I know of MIPT-associated group designing conceptual structures for decades, but they are using offsprings of mathemtic proposed by Bourbaki.
<dborisog_>
Thanks!
FreeBirdLjj has quit [Remote host closed the connection]
mahmudov has joined #ocaml
<companion_cube>
monads certainly don't need any understanding of CT to be used
Leonidas has quit [Quit: An ideal world is left as an exercise to the reader]
<gahr>
just like + and * don't need any understanding of the ring algebraic structure to be used :)
<gahr>
but it surely help if you understand where it comes from, especially when you want to abstract + and * to more general operations
<companion_cube>
🤷
<companion_cube>
guess that's why I'll never be a mathematician
<gahr>
ENOEMOJI :(
<companion_cube>
install noto fonts ;)
<dborisog_>
Well, the idea and visualisation of transition of objects from the source category to the Kleisli category is very clear. It is a short and understendable idea behind each implementation of monad. Personally, I struggle with multiple cases trying to make sense of them, while having the core idea makes life much less frustrating.
<companion_cube>
I never could understand CT, I prefer algebraic or logic stuff
<companion_cube>
monads are nice because they're just a small bunch of axioms :D
<dborisog_>
)
<simpson>
companion_cube: I think that you're one of us, but with a low tolerance for needless abstraction.
<companion_cube>
heh! maybe I just never got the point of CT indeed
<companion_cube>
it's like pointless^W pointfree haskell
* gahr
is not a mathematician either
dhil has quit [Ping timeout: 245 seconds]
* gahr
likes to understand the fundamental ideas behind things, though
<gahr>
which is probably why most of the books I start I never finish
Leonidas has joined #ocaml
<companion_cube>
yeah but these things (like monoids, etc.) are not intrinsically categorical, and a lot of algebra existed before CT
<dborisog_>
Lat year I attempted to implment a library for this very powerful logic https://www.springer.com/gp/book/9789027701930 After few weeks I understood I need much more solid foundation of programming for this task. It seems to me, functional programming is the answer, yet I'm not sure if one of types lambda theories or CT would be the most useful. I think a certain level familiarization with all of these systems of concepts would be beneficial for the
<dborisog_>
task.
Leonidas has quit [Client Quit]
smazga has joined #ocaml
<gahr>
companion_cube: agreed - I just think CT formalizes and generalizes many concepts that were "discovered" here and there
Algebr has joined #ocaml
<gahr>
it's a nice meeting place for different intuitions
<companion_cube>
maybe so, it's just so godamn abstract :D
<companion_cube>
I guess I need a proof assistant for CT to help me
<gahr>
:)
<gahr>
bartosz's courses are nice because they continuously link CT to functional programming
<gahr>
so you see how concepts are applied
<simpson>
companion_cube: For me it's too applicable; I can't look at logic without considering the categorical POV.
<companion_cube>
:(
<companion_cube>
for me logic is the foundation, so it's what I understand other things with!
<companion_cube>
(not FP, though, not interested in the connection)
<simpson>
Aha, interesting. I don't have a foundation; I'm constantly trying not to fall into the void. Maybe that's the difference.
<Drup>
for me CT *is* the void
<Drup>
it's the place where I stop having any kind of intuition about how anything works
cranix has joined #ocaml
<cranix>
hello
<gahr>
top/ic CT is the Void
<cranix>
is there something like ocaml-graph-editor but more advanced?
<dborisog_>
companion_cube, you might find the book I referenced rather inspirational. For example, Zinov'ev provides a formal yet intuitive approch of generating values for many-valued logic.
<cranix>
i need to handle cyclic graphs
<cranix>
also is ocamlgraph library able to handle cyclic nondirected graphs?
<companion_cube>
generating values?
<companion_cube>
oh wow, I agree with Drup :o
<Drup>
cranix: sure. ocamlgraph works on any graph
<Drup>
(I mean, there are algorithms to find cycles, it would be sad if it didn't work on cyclic graphs :D)
<cranix>
Drup: thanks
<cranix>
is there any good tutorial/entry point to this library? there is paper about implementation and a few examples
<cranix>
but maybe i missed something else
<dborisog_>
True, False is the starting point. For his purposes he created and used a system of four primary and seven complementary values. true, indeterminate, unverifiable, false; and non-true, determinate, verifiable, not-false, verifiable-not-true, verifiable-not-false, verifiable-determinate. According to him, and I see his point, these values are much more suitable for scientific reasoning than the standard binary pair
<companion_cube>
oh boy
<Drup>
that's textbook intelectual onanism.
<Drup>
I don't mind indulging, but I usually don't pretend it's useful :p
<companion_cube>
non standard logics are cool, but I'm not sure generalizing over them is that useful
Serpent7776 has quit [Quit: Leaving]
<companion_cube>
it's already hard enough to reason about a given logic
<dborisog_>
:D well, the other tools were lacking in power for his task, thus he invented his logic, designed scientific methodology, created science and finally studied society with all that tooling
<Drup>
sure, and that's fine
<Drup>
I mean, my mean issue is with (often Haskellers) pretending that CT is the universal language of the universe, you can't do any kind of reasoning without it, and you absolutely needed to be half competent programmer
<simpson>
There *is* a turn-the-crank construction, if the truth values form a nice algebraic structure (poset? lattice?) to build a topos.
<companion_cube>
lattice, typically
<companion_cube>
you do want to have a top and bottom for your truth values :D
<companion_cube>
Drup: maybe CT is the haskell of maths ;)
<Drup>
only use on sundays ? :D
<companion_cube>
😂
<companion_cube>
complicated abstractions for the sake of them
<companion_cube>
I'm more into, like, the C of maths (or the SML of maths?)
<gahr>
we all love to hate a bit what's in hype
<companion_cube>
yeah, to hate a bit what's HoTT
<companion_cube>
😏
<gahr>
good one :)
<dborisog_>
)
cranix has left #ocaml [#ocaml]
klntsky has quit [Ping timeout: 240 seconds]
klntsky has joined #ocaml
oni-on-ion has joined #ocaml
dhil has joined #ocaml
ollehar has quit [Ping timeout: 268 seconds]
Haudegen has quit [Quit: Bin weg.]
<dborisog_>
Drup: In my pet Ocsigen project I deal with countries and unions of countries. It is handy for me to have a URL from a union to the related countries, and from a country to the related unions. I have urls union->country, but the almost carbon copy of this code country->union produces an error message of Unbound module with some compilarion specific stating something Circular dependency drop. I could have missed somthing, but I was able to narrow down
<dborisog_>
to this circular dependency only. Do you think my assumption is correct, and is this a familiar problem with a very simple solution?
<Drup>
is the carbon copy in the same module ?
<Drup>
I guess you placed the union -> country in the module Union, and the country -> union in the module Country ? :)
<dborisog_>
Well, I have Union_union module with union_service, and Country_country with country_service. The Union_union.union_service returns a list of countries forming this union, and the URLs work fine. However, when I am trying to refernce unions a country belongs to in Country_country.country_service, it throws an error of Unbound module Union_union
<oni-on-ion>
=|
<Drup>
Well, yes, you have a cycle.
<dborisog_>
(sad panda)
<dborisog_>
))
<dborisog_>
Is there a way to overcome this inconvenience? If services fail, may be plain HTML generation?
<Drup>
it has nothing to do with ocsigen. It's an ocaml thing. You can't have cyclic dependencies in your ocaml files.
<dborisog_>
As it is rather important limitation, to have a tree-alike structure of pages in a web project
<dborisog_>
I see. Thank you
<Drup>
That's completely unreleated
<Drup>
you can have all the dependencies you like in your pages. you just must organize your *code* differently
<dborisog_>
True. Thanks!
klntsky has quit [Remote host closed the connection]