motherfsck has quit [Remote host closed the connection]
glassofethanol has quit [Ping timeout: 264 seconds]
glassofethanol has joined #ocaml
glassofethanol has quit [Ping timeout: 264 seconds]
mro has joined #ocaml
favonia has joined #ocaml
gravicappa has quit [Ping timeout: 252 seconds]
mro has quit [Quit: Leaving...]
Haudegen has quit [Quit: Bin weg.]
Stumpfenstiel has joined #ocaml
glassofethanol has joined #ocaml
waleee has quit [Ping timeout: 246 seconds]
waleee has joined #ocaml
olle has quit [Ping timeout: 246 seconds]
glassofethanol has quit [Quit: leaving]
yoctocell has quit [Ping timeout: 246 seconds]
pmetzger has joined #ocaml
<d_bot>
<RegularSpatula> Has anyone done much work with pyml for wrapping python libraries? I was looking at ocaml sklearn bindings and apparently they are generated automatically with this ~4000 line python script: https://github.com/lehy/ocaml-sklearn/blob/master/lib/skdoc.py. For anyone who has made ocaml bindings to python (or any other language), is it common to autogenerate the ocaml code like that?
<d_bot>
<EduardoRFS> why does value restriction apply to the following function?
<d_bot>
<EduardoRFS>
<d_bot>
<EduardoRFS> ```ocaml
<d_bot>
<EduardoRFS> let false_: 'a -> 'b -> 'b = assert false
<d_bot>
<EduardoRFS> let v = false_ ()
<d_bot>
<EduardoRFS> ```
<d_bot>
<EduardoRFS>
<d_bot>
<EduardoRFS> There is any possible unsoundness on it? Or is it just an accident of OCaml value restriction implementation?
<d_bot>
<EduardoRFS> Also, will typed effects effectively "solve" the value restriction? As now we can track if a function is pure or not
motherfsck has joined #ocaml
<thizanne>
that's no "accident", more like the very point of value restriction: `false_ ()` is not a value (and it's not covariant either), so its type can't be generalised
<thizanne>
re. typed effects: typing algebraic effects won't solve this, as there's still an opportunity to introduce side effects without using algebraic effects at all
<d_bot>
<EduardoRFS> Like? I was looking on Leo's talk, and it seems like you can only put all mutability with an effect of `[io]` which on his talk is an implicit effect of the arrow
<d_bot>
<EduardoRFS> so a -> a actually means a -[io]> b, which seems to remove any opportunity for mutation
<d_bot>
<EduardoRFS> the point of value restriction is to avoid unsoundness through mutability, sure, but there is any unsoundness possible on the type described being partially applied?
<d_bot>
<EduardoRFS>
<d_bot>
<EduardoRFS> If not, my argument is that it is an accident of value restriction, just another case of value restriction being too restrict
<thizanne>
the name "value restriction" means "if you're syntactivally not a value, then you're not generalized"
<thizanne>
indeed the goal is to avoid unsoundness, and indeed you could on the principle avoid the same unsoundness with a more relaxed criterion
<thizanne>
(adding "covariant variables can still be generalised" is one of those relaxings)
pmetzger has quit []
<d_bot>
<EduardoRFS> oh that's exactly what I wanted to search, thank you
<thizanne>
and yes the type '_b -> '_b itself would be unsound to generalise a priori: `let f = let r = ref None in fun x -> (r := Some x; x)` has the same type, and applying it as `f (); f 42` would be unsound
<d_bot>
<EduardoRFS> oh you're right, that's exactly the case I was looking
<Leonidas>
It looks like `match ... with | exception Not_found -> Error ...` triggers a deprecation warning now :'(
sagax has quit [Ping timeout: 268 seconds]
<d_bot>
<EduardoRFS> hmmm if we could move the forall it would be safe right? Similar to how you can pack it on a record with universal quantification for that.
<d_bot>
<EduardoRFS>
<d_bot>
<EduardoRFS> ```ocaml
<d_bot>
<EduardoRFS> val false_: 'a. 'a -> 'b. 'b -> 'b = assert false
<d_bot>
<EduardoRFS> ```
<thizanne>
Leonidas: looks like you're using Core and it deprecates Not_found itself
<thizanne>
Eduardo: yes, it would work
<thizanne>
compare: `let f : 'a -> < x : 'b -> 'b > = assert false;; let x = f ()` with `let f : 'a -> < x : 'b. 'b -> 'b > = assert false;; let x = f ()`
<thizanne>
generalisation happens for free variables, if you quantify them they become bound and there's no need for generalisation anymor
<thizanne>
(another way to see it: "_weak. _weak -> _weak" would make no sense)
<d_bot>
<EduardoRFS> yeah that's what I thought, just trying to understand the advantages of moving the forall
<d_bot>
<EduardoRFS> oh didn't knew that you could do universal quantification with objects, most of the time I do it with records
<thizanne>
for trying stuff, objects are slightly less verbose
<thizanne>
(for this purpose specifically I mean)
<d_bot>
<EduardoRFS> yeah but sadly you cannot unbox them right?
<d_bot>
<EduardoRFS> yeah you cannot
cedric has quit [Quit: Konversation terminated!]
daachi has joined #ocaml
favonia has quit [Ping timeout: 268 seconds]
favonia has joined #ocaml
Stumpfenstiel has quit [Ping timeout: 252 seconds]