<d_bot>
<beheddard> oh I see mnxn just posted same above 😅
<flux67>
but how do i search it, it's so massive :D
olle has quit [Ping timeout: 256 seconds]
catern has joined #ocaml
olle has joined #ocaml
Tuplanolla has quit [Ping timeout: 260 seconds]
zebrag has quit [Quit: Konversation terminated!]
zebrag has joined #ocaml
<flux67>
what does this mean? Values do not match: val option_concatenate : string option/2 -> string option/2 -> string option/2 is not included in val option_concatenate : string option/1 -> string option/1 -> string option/1
<flux67>
i am trying to use map2: `let option_concatenate string1 string2 = Option.map2 string1 string2 ~f:( ^ )`
<flux67>
it seems to work in utop which is why i am confused
Yagotzirck has quit [Quit: Leaving]
j14159 has joined #ocaml
j14159_ has left #ocaml [#ocaml]
mxns has joined #ocaml
wingsorc has joined #ocaml
<d_bot>
<glennsl> flux67: looks like you've redefined the `option` type.
<d_bot>
<glennsl> in other words, `option/1` and `option/2` are different types with the same name, hence the `/n` to distinguish them
flux67 has quit [Remote host closed the connection]
Haudegen has quit [Ping timeout: 268 seconds]
iridescence has joined #ocaml
<iridescence>
i'm trying to have a for loop be an intermediate step in a computation, like let _ = (for blah do stuff done) in (another expr)
<iridescence>
this seems like an awkward let statement, is this idiomatic?
<d_bot>
<glennsl> iridescence: you can use the sequence operator (`;`) instead: `for ... done; <another expr>`
<iridescence>
thank you, exactly what i was looking for
<iridescence>
what are the semantics of the sequence operator in terms of types?
<d_bot>
<glennsl> it'll warn if the first expression isn't `unit` and return the result of the second
<iridescence>
why can't i do, for example, let a=6; let b=7
<iridescence>
just kidding that's a silly question
zebrag has quit [Quit: Konversation terminated!]
iridescence has quit [Remote host closed the connection]
zebrag has joined #ocaml
oni_on_ion is now known as oni-on-ion
sm2n_ has joined #ocaml
drewolson3 has joined #ocaml
t-j-r has joined #ocaml
dmbaturin_ has joined #ocaml
cross_ has joined #ocaml
ahf_ has joined #ocaml
indicato` has joined #ocaml
bacam_ has joined #ocaml
infinity0_ has joined #ocaml
infinity0 has quit [Killed (moon.freenode.net (Nickname regained by services))]
infinity0 has joined #ocaml
infinity0_ is now known as infinity0
sm2n has quit [*.net *.split]
emp has quit [*.net *.split]
indicator has quit [*.net *.split]
bacam has quit [*.net *.split]
Johann has quit [*.net *.split]
dmbaturin has quit [*.net *.split]
_tjr_ has quit [*.net *.split]
so has quit [*.net *.split]
notnotdan has quit [*.net *.split]
ahf has quit [*.net *.split]
Jesin has quit [*.net *.split]
drewolson has quit [*.net *.split]
emias has quit [*.net *.split]
kvik has quit [*.net *.split]
cross has quit [*.net *.split]
daimrod has quit [*.net *.split]
drewolson3 is now known as drewolson
notnotdan has joined #ocaml
emp has joined #ocaml
kvik has joined #ocaml
emias has joined #ocaml
Johann has joined #ocaml
daimrod has joined #ocaml
mfp has quit [Ping timeout: 272 seconds]
so has joined #ocaml
madroach_ has joined #ocaml
madroach has quit [Ping timeout: 256 seconds]
<d_bot>
<mnxn> > how do people usually search for functions like this?
<d_bot>
<mnxn> > is there some equivalent of hoogle in ocaml :)
<d_bot>
<mnxn> flux67: i just searched hoogle by haskell type signature so I could figure out what the function is (typically) called. Then I just CTRL+F in base/batteries/containers documentation
dborisog has joined #ocaml
Jeanne-Kamikaze has quit [Quit: Leaving]
zebrag has quit [Read error: Connection reset by peer]
zebrag has joined #ocaml
_whitelogger has joined #ocaml
sleepydog has quit [Remote host closed the connection]
<oni-on-ion>
=)
<d_bot>
<darrenldl> is there any effort in making a ocaml doc system similar to rust's? (namely built in search)
mxns has joined #ocaml
<companion_cube>
No idea, look at what odoc has maybe?
madroach has joined #ocaml
peterbb has joined #ocaml
peterbb has quit [Remote host closed the connection]
madroach_ has quit [Ping timeout: 256 seconds]
mxns has quit [Ping timeout: 246 seconds]
FreeBirdLjj has joined #ocaml
FreeBirdLjj has quit [Read error: Connection reset by peer]
dborisog has quit [Ping timeout: 264 seconds]
mxns has joined #ocaml
zebrag has quit [Quit: Konversation terminated!]
zebrag has joined #ocaml
Jesin has joined #ocaml
wingsorc has quit [Ping timeout: 260 seconds]
mxns has quit [Ping timeout: 260 seconds]
cantstanya has quit [Ping timeout: 240 seconds]
cantstanya has joined #ocaml
mxns has joined #ocaml
mxns has quit [Ping timeout: 268 seconds]
zebrag has quit [Quit: Konversation terminated!]
zebrag has joined #ocaml
zolk3ri has joined #ocaml
zebrag has quit [Ping timeout: 240 seconds]
sleepydog has joined #ocaml
waleee-cl has quit [Quit: Connection closed for inactivity]
<zozozo>
also, dolmen is a parser lib I wrote that has an implementation of first-order formulas with the necessary functions to handle substitution
<Anarchos>
zozozo thanks i will look. btw i did it but i find it annoying to deal with subst and i am not skilled enough in logic
<zozozo>
ok, both logtk and dolmen are implementations that have been tested quite well I think (and companion_cube and I have been working on automated deduction, so I guess it's reasonable to say we're skilled enough in that, ^^)
<Anarchos>
zozozo i am writing a soft to verify demonstrations in ZFC.
<Anarchos>
zozozo i never found one able to deal with axiom schema
<zozozo>
oh, that's cool ! I'm sure companion_cube will be interested by that (when he wakes up)
<Anarchos>
zozozo i already talk him about it
<Anarchos>
zozozo it is only a verifier
<Anarchos>
zozozo and the syntax is plain old latex :)
<zozozo>
haha no worries, I don't have enough free time anyway, XD
<Anarchos>
zozozo i would be glad to have some feedback
<zozozo>
and I already re-implemented a mini-coq-like proof checker during my phd anyway
<Anarchos>
zozozo documentation is not my high skill anyway...
<Anarchos>
zozozo the coq source code is such a mess i think.... already looked at it, and ran away!
<Anarchos>
zozozo it suffers its technical debt and lack of refactoring
<zozozo>
haha, yeah, I haven't looked at it yet, but people who have didn't have much good to say usually, :p
<Anarchos>
but it is a cool tool anyway !
<Anarchos>
zozozo i tried to do it better, but i suffer from some circularities in the module : parser needs formulas and formulas need parser...
olle_ has joined #ocaml
<zozozo>
Anarchos: do you plan to have a cli checker (the netcat thing seems a bit hard to use for someone not familiar with the syntax) ?
<olle_>
Some Danish guy made "combining garbage collection with stack allocation"
<olle_>
wait
<olle_>
no
<zozozo>
Anarchos: why do formulas need parser ?
<olle_>
Combining region inference and garbage collection
<olle_>
from 2002
<Anarchos>
zozozo to be read and printed from/to strings
<olle_>
Made for SML
<zozozo>
Anarchos: well personally I'd say to print you don't need the parser module, and to read formulas, you have the parser module and don't need to have the functions in the formuals module (since they'll likely only be aliases anyway)
noonien has quit [Ping timeout: 272 seconds]
<d_bot>
<darrenldl> zozozo: dolmen is not using locally nameless representation is it? (just checking if it'd be better to just swap to dolmen/logtk from my current binder code)
<zozozo>
darrenldl: I don't think so, basically, variables are identified using a unique increasing id (and carry a name for printing because else it's hard to read)
<zozozo>
additionally, because of the code, each variable a "unique", i.e. equality between variables can use physical equality (but that's an implementation detail)
<zozozo>
darrenldl : however, if I remember correctly, logtk uses DeBruijn indexes for the variables, allowing terms in logtk to be easily compared modulo alpha renaming
<d_bot>
<darrenldl> zozozo: aha thanks - i used De Bruijn (+ string for constants) for a pi calculus parser component, but may need to parse (a lot of) TPTP at some point, will take a closer look at both libs by then
<zozozo>
darrenldl : well dolmen is a parser lib for automated deduction, so it has a parser and typer for TPTP (as well as SMTLIB), so that might be of interest
* d_bot
<Drup> stares at De bruijn indices disaprovingly ಠ_ಠ
<qwr>
olle_: region inference with additional (for example refcounted) gc is interesting idea, might be good, but certainly pretty complex. afaik SMLkit region inference yielded quite slow compile times
<zozozo>
Drup: haha, tbh I'm not a fan of them either, ^^
<d_bot>
<Drup> first of, and although it's not really their author's fault, the pronunciation is bullshit.
<d_bot>
<darrenldl> what would you advise using?
<qwr>
olle_: fully static region infererence also pretty much excludes separate compilation, maybe something with dynamic region passing could allow it, but i'm not aware of such implementations
<Drup>
qwr: Affe does :)
<d_bot>
<Drup> @BigOof for implementing, unique names, for formal proofs ... 🤷♂️
<d_bot>
<Drup> I just now that I hate working with de bruijn indices.
noonien has joined #ocaml
<d_bot>
<darrenldl> i definitely haven't rolled enough binders to understand when unique names are better than de bruijn indices (i thought not having to do alpha conversion is pretty neat)
Anarchos has quit [Quit: Vision[0.10.3]: i've been blurred!]
<zozozo>
well, I'd say the big advantage of Debruijn idnexes is when you regularly have to compare modulo alpha-equivalence
<zozozo>
and absent that, well use unique names/ids
Haudegen has joined #ocaml
<zozozo>
an intermediate step is to hash-cons the formulas modulo alpha-renaming, so that the alpha-equivalence test is memoized in some way (that's what zenon does)
<companion_cube>
DB indices are indeed super cool if you need to hashcons your formulas
<Drup>
qwr: disclaimer, I'm the author :p
* qwr
really likes that you've commented the rules :)
Anarchos has joined #ocaml
<Anarchos>
hello
gareppa has joined #ocaml
gareppa has quit [Remote host closed the connection]
bacam_ is now known as bacam
shawnw has quit [Ping timeout: 264 seconds]
Anarchos has quit [Ping timeout: 260 seconds]
waleee-cl has joined #ocaml
tane has joined #ocaml
Anarchos has joined #ocaml
Anarchos has quit [Ping timeout: 256 seconds]
<olle_>
qwr: hi ho
<olle_>
yeah, separate compilation is a must in big systems.
* olle_
gotta google about cyclone, it seems
benschza has quit [Ping timeout: 260 seconds]
<d_bot>
<dinmammapåminstekpanna> Is it feasible to write a recursive descent parser using GADTs to model the abstract syntax tree? I have written a small toy language using ADTs and is interesting if I can use GADTs to make the evaluation of the ast prettier too eliminate some of all the extra clauses I now have.
Serpent7776 has joined #ocaml
Anarchos has joined #ocaml
<olle_>
I'm offended by that username
<olle_>
deeply offended
Haudegen has quit [Ping timeout: 240 seconds]
benschza has joined #ocaml
<Anarchos>
olle_ which one ?
<olle_>
dinmamma etc
zolk3ri has quit [Write error: Connection reset by peer]
andreas303 has quit [Write error: Connection reset by peer]
tryte has quit [Write error: Connection reset by peer]
nicoo has quit [Read error: Connection reset by peer]
cantstanya has quit [Write error: Connection reset by peer]
<d_bot>
<xvw> > (modules_without_implementation <modules>) specifies a list of modules that have only a .mli or .rei but no .ml or .re file. Such modules are usually referred as mli only modules. They are not officially supported by the OCaml compiler, however they are commonly used. Such modules must only define types. Since it is not reasonably possible for dune to check that this is the case, dune requires the user to explicitly list such modul
mxns has quit [Ping timeout: 264 seconds]
<Anarchos>
xvw ok if it is not officialy supported, i will rather write the .ml file...
<Armael>
it is officially supported
<Armael>
you just have to add a line in the dune file as xvw is saying