<d_bot>
<Competitive Complications> anyone got any links toward ocaml repos implementing CoC or CiC?
eltonpinto has quit [Quit: WeeChat 2.3]
<d_bot>
<Competitive Complications> I have found 1 or 2 repo in my past searches, but I can't even find them anymore, and I imagine there must be like half a dozen
<companion_cube>
I only know of Coq and matita :p
<d_bot>
<Competitive Complications> I meant more simple / barebones / toy
<companion_cube>
not sure it can be done simply :p
<companion_cube>
but Coq's kernel isn't that big, it should be a few thousands lines
<d_bot>
<Competitive Complications> (I'm painfully going through my browser history)
<d_bot>
<Competitive Complications> Going to sleep, but I'll check tomorrow if anyone has a link to the micro/nano agda (haven't found anything on Google)
zebrag has quit [Quit: Konversation terminated!]
berberman has quit [Ping timeout: 258 seconds]
berberman has joined #ocaml
average has joined #ocaml
zebrag has joined #ocaml
remexre has quit [Ping timeout: 250 seconds]
zebrag has quit [Quit: Konversation terminated!]
mbuf has joined #ocaml
gravicappa has joined #ocaml
favonia has quit [Ping timeout: 258 seconds]
nd__ has joined #ocaml
nd__ has quit [Ping timeout: 268 seconds]
<Armael>
I was going to link Andrej's stuff but you saw that already
Haudegen has joined #ocaml
nd__ has joined #ocaml
nd__ has quit [Ping timeout: 258 seconds]
nd__ has joined #ocaml
bartholin has joined #ocaml
nd__ has quit [Quit: leaving]
yoctocell has joined #ocaml
olle has joined #ocaml
neiluj has joined #ocaml
<neiluj>
Hi! If a function returns an optional value encapsulated in an error monad, is it better to just return the value and raise the error in case the value is not set?
<neiluj>
in this case, the function attempts to establish a connection and returns it
<Fardale>
Why not staying in the error monad?
<neiluj>
indeed, that's sounds reasonable, especially considering that the absence of connection is a 'real' error
<neiluj>
thanks Fardale !
<d_bot>
<sarna> hey, how can I see the code generated by a ppx? I'm using emacs if that matters
<d_bot>
<sarna> okay found it: pass the `dsource` flag :)
<d_bot>
<Ulugbek> Can `Obj.magic` result in some compiler (including flambda) optimizations being inapplicable? If yes, how does that happen?
<d_bot>
<Ulugbek> Some context:
<d_bot>
<Ulugbek> I'm implementing a doubly linked list with a sentinel node. The nodes in the list are represented as
<d_bot>
<Ulugbek> ```ocaml
<d_bot>
<Ulugbek> type 'a t =
<d_bot>
<Ulugbek> { data : 'a
<d_bot>
<Ulugbek> ; mutable prev : 'a t
<d_bot>
<Ulugbek> ; mutable next : 'a t
<d_bot>
<Ulugbek> }
<d_bot>
<Ulugbek> ```
<d_bot>
<Ulugbek> Since a sentinel node doesn't have `data`, I'm initializing the list as `let rec sentinel = { data = Obj.magic None; prev = sentinel; next = sentinel }`. The list supports appending, prepending, popping head/tail, and detaching a node by its handle that's provided when that node is first added to the list.
<d_bot>
<Ulugbek> Also, are cyclic references costly for GC? For example, I can mark a node removed from the list either by `node.prev = node` or make `data` mutable and do `data = None`. I wonder which is better. (more curiosity than real desire to optimize this)
<d_bot>
<dinosaure> You can use `Sys.opaque_identity` to prevent mis-optimization from `flambda`
<d_bot>
<dinosaure> Then, a good (for perf) and bad (for maintenance) example of the double linked list is the one used by `lwt`
<d_bot>
<Ulugbek> Are conversion functions in the code below safe because `prev` and `next` are 0th and 1st fields in both records?
<d_bot>
<Ulugbek>
<d_bot>
<Ulugbek> ```ocaml
<d_bot>
<Ulugbek> type 'a t = {
<d_bot>
<Ulugbek> mutable prev : 'a t;
<d_bot>
<Ulugbek> mutable next : 'a t;
<d_bot>
<Ulugbek> }
<d_bot>
<Ulugbek>
<d_bot>
<Ulugbek> type 'a node = {
<d_bot>
<Ulugbek> mutable node_prev : 'a t;
<d_bot>
<Ulugbek> mutable node_next : 'a t;
<d_bot>
<Ulugbek> mutable node_data : 'a;
<d_bot>
<Ulugbek> mutable node_active : bool;
<d_bot>
<Ulugbek> }
<d_bot>
<Ulugbek>
<d_bot>
<Ulugbek> external seq_of_node : 'a node -> 'a t = "%identity"
<d_bot>
<Ulugbek> external node_of_seq : 'a t -> 'a node = "%identity"
<d_bot>
<Ulugbek> ```
<olle>
:(
<olle>
Less code, more talking.
<d_bot>
<dinosaure> Yes, it trusts on the OCaml representation - and, in that case, `flambda` can miss-optimize the access if you don't use `Sys.opaque_identity`
<d_bot>
<dinosaure> `Sys.opaque_identity` is like: don't try anything here, I know what I'm doing, trust me
<d_bot>
<dinosaure> Of course, it's completely unsafe
<d_bot>
<Ulugbek> > don't try anything here, I know what I'm doing, trust me
<d_bot>
<Ulugbek> that sounds like missing out on some possible optimizations
<d_bot>
<dinosaure> Yes because you already did "an optimization" via the identity which does not have a cost :)
<d_bot>
<Ulugbek> of course! thanks!
kakadu has joined #ocaml
vb has joined #ocaml
favonia has joined #ocaml
<cemerick>
✨ petition to change {Set,Map}.fold's signature to typical fold_left param order ✨
<cemerick>
😉
<olle>
"Change"?
<olle>
Get out!
<neiluj>
I love how you can just override existing modules to better suit your preference
* cemerick
is (obviously, hopefully) joking
<cemerick>
neiluj: I already have many times, but it does get wearisome
waleee has quit [Ping timeout: 272 seconds]
<olle>
"Joking"?
<olle>
Get out!
<cemerick>
lol
<cemerick>
blame shows that that signature was set 27 years ago, whew
<olle>
Old and gold
<neiluj>
^
kor1 has joined #ocaml
<cemerick>
heh, very silly
<olle>
Wait until they tell you how old the Neumann architecture is...
<olle>
Mind.
<olle>
Blown.
Haudegen has quit [Quit: Bin weg.]
yoctocell has quit [Remote host closed the connection]
<neiluj>
in a .mli a module is re-exported like so: module Node_id = Node_id. How to restrict its signature as well (specify which val to expose)?
<neiluj>
hmm wait, I'll do so in the Node_id module itself
<neiluj>
nevermind
mbuf has quit [Quit: Leaving]
Haudegen has joined #ocaml
<companion_cube>
module Node_id : sig … end ?
<neiluj>
yeah, figured it out
<neiluj>
thanks
yoctocell has joined #ocaml
mattil has joined #ocaml
mattil has quit [Max SendQ exceeded]
waleee has joined #ocaml
yoctocell has quit [Remote host closed the connection]
yoctocell has joined #ocaml
Skyfire has quit [Quit: WeeChat 3.2]
Skyfire has joined #ocaml
<d_bot>
<Competitive Complications> confused question: let's say I dislike linear-time substitutions, and I go the HOAS route.
<d_bot>
<Competitive Complications> I want to type simple dependently typed lambdas, with the regular rule to type dependent lambdas, and use HOAS to represent prod types too.
<d_bot>
<Competitive Complications> Now, I'm in a pickle: if I do the standard implementation where I create a fresh variable, give it the type of the bound parameter, and type the new term with the bound parameter in the env, I will generally get a type that depends on the bound parameter.
<d_bot>
<Competitive Complications> To transform this back into a HOAS form (instead of binder + body), I will need to crawl through the body to replace each occurrence of the fresh variable.
<d_bot>
<Competitive Complications> If I have n imbricated lambdas, the cost is quadratic, which is sad. How should I avoid this?
olle has quit [Ping timeout: 248 seconds]
<cemerick>
olle: don't think there's much in common between a random fun sig and something like a computing architecture
neiluj has quit [Quit: Leaving]
Haudegen has quit [Quit: Bin weg.]
olle has joined #ocaml
vicfred has joined #ocaml
Haudegen has joined #ocaml
kakadu has quit [Quit: Konversation terminated!]
olle has quit [Ping timeout: 245 seconds]
Tuplanolla has joined #ocaml
jonasbits has joined #ocaml
Tuplanolla has quit [Quit: Leaving.]
favonia has quit [Ping timeout: 248 seconds]
Anarchos has joined #ocaml
favonia has joined #ocaml
gravicappa has quit [Ping timeout: 268 seconds]
Skyfire has quit [Ping timeout: 245 seconds]
Skyfire has joined #ocaml
Haudegen has quit [Quit: Bin weg.]
favonia has quit [Remote host closed the connection]
Anarchos has quit [Quit: Vision[0.10.3]: i've been blurred!]