00:00 <d_bot> <Shon F> I think a more relevant approach to your needs might be normalization by evaluation? https://en.wikipedia.org/wiki/Normalisation_by_evaluation

00:00 <d_bot> <Shon F> (But I don't have a great grasp on the tradeoffs here vs. HOAS tho.)

00:04 <companion_cube> (hi, what's ABT? :P)

00:15 <d_bot> <Shon F> Sorry, ABT is "Abstract Binding Tree": it's an AST but with the notion of variable binding baked in.

00:16 <d_bot> <Shon F> Neel Krishnaswami has a nice exposition here: https://semantic-domain.blogspot.com/2015/03/abstract-binding-trees.html

00:18 <companion_cube> hmmmmmmmm

00:19 <companion_cube> is the `join` operation used to merge variables from subterms in a generic way?

00:19 <d_bot> <Shon F> The idea is that you can reuse your ABT library or data structure to take care of all the variable binding logic for your different languages, rather than have to re implement your binding/substitution logic for each language.

00:19 <companion_cube> ah yes, set of free variables.

00:20 <companion_cube> sure, but then you may have different efficiency tradeoffs :)

00:21 <d_bot> <Shon F> Yes, I don't think ABTs address the efficiency concern of substitution at all. I only thought that was worth mentioning because of the mention of using pointers.

00:23 <companion_cube> ah, yes

00:24 <d_bot> <Shon F> I'm more hopeful about NbE's re: the efficiency angle.

00:25 <companion_cube> @Cyclomatic Complexity: I've long wondered about using https://github.com/c-cube/ocaml-containers/blob/master/src/data/CCRAL.mli for O(ln n) de Bruijn environments

00:25 <companion_cube> gives you a O(1) cons, and O(ln(n)) indexing, which I think is just what's needed

00:26 <d_bot> <Shon F> Do you know offhand what would be the cost for replacing a cell?

00:28 <d_bot> <Shon F> Would you just do a `mapi` for the substitution? (Or perhaps I misunderstand entirely 😐 ).

00:30 <companion_cube> ouch, yeah, that's harder

00:30 <companion_cube> with DB indices you typically don't need to _replace_ stuff, I think? you just prepend when entering a scope

00:33 <d_bot> <Shon F> Ah! I'd assumed you'd needed some sort of replacement when it comes time to substitute values for the variables. But tbh, it's been a long time since I implemented something using DB indices, and I didn't like it or internalize it at all at the time any how 🙂

01:20 <d_bot> <darrenldl> wasn't there a shift operation required? (im very rusty) granted it's simpler than alpha conversion

01:20 <d_bot> <darrenldl>

01:20 <d_bot> <darrenldl> though still proportional to size of expression

01:21 <companion_cube> you need to shift the substituted term

01:21 <companion_cube> if it's closed, no shifting required :)

01:22 <companion_cube> in CBV I think it's possible that all substituted terms are closed

01:22 <companion_cube> (values should be closed terms after all)

02:57 <d_bot> <darrenldl> ah right

08:05 <d_bot> <Cyclomatic Complexity> companion_cube: two problems with this approach given what i want to do:

08:09 <d_bot> <Cyclomatic Complexity> 1. i need semantics where i can do some substitutions in a term, without reducing it to a normal-form (tl;dr, no `val eval : expression -> value`), and then assemble it with some other AST on which some substitutions were done too. the problem with environments is that they usually assume a "top-level" environment because you never reduce under lambdas. (obviously, because I have a very limited idea of SOTA, there i

08:09 <d_bot> <Cyclomatic Complexity> 2. because i don't only have cbv semantics, I need shifts

08:10 <d_bot> <Cyclomatic Complexity> @Shon F This looks very relevant, and I am currently looking at it, thank you!

11:48 <companion_cube> right

11:49 <companion_cube> I think Coq uses DB indices and yet does strong normalization

13:08 <d_bot> <Drup> @Shon F mmmmh, this is interesting, maybe I should see if I can provide something like that in https://github.com/Drup/peahell

13:10 <d_bot> <Drup> It's definitely missing name handling utilities right now

13:10 <d_bot> <Drup> (and efficiency barely matters for what it's intended, i.e. prototypes)

13:12 <companion_cube> I'm curious indeed about the tradeoffs wrt HOAS

13:12 <companion_cube> like bindlib

14:49 <neiluj> Hello! Is there a way to write the last function in point free style? https://bpa.st/QMZA

14:49 <companion_cube> maybe, but that sounds like a bad idea

14:50 <neiluj> okay, thanks :)

14:51 <companion_cube> also this is going to be slow ;)

14:52 <neiluj> oh yeah this solution is pretty inefficient, in C you can xor on 64 bit integers (thus reducing to 2 xors in this case) for instance

14:53 <neiluj> couldn't find a way to do so with the Base api

14:54 <companion_cube> ahahah no I mean, the lists

14:54 <companion_cube> xors are incredibly cheap in comparison

14:54 <neiluj> oh yeah

14:55 <companion_cube> something like https://paste.isomorphis.me/MIV should be faster

14:55 <companion_cube> (once tweaked so it compiles)

14:55 <companion_cube> much, much faster

14:56 <neiluj> maybe using Bytes.set?

14:56 <companion_cube> iirc `a.[i] <- x` is just `Bytes.set a i x`

14:56 <companion_cube> but maybe it's `a.(i)`

14:57 <neiluj> oh many thanks!!

15:21 <d_bot> <darrenldl> if you really need fast xor, look into c ffi

15:24 <d_bot> <darrenldl> though using unsafe_get/set might already provide enough savings

15:25 <neiluj> thanks for the suggestion, it's fast enough as it is

15:26 <d_bot> <darrenldl> what is this for if you dont mind me asking?

15:27 <neiluj> a Kademlia DHT :)

15:29 <d_bot> <darrenldl> interesting

15:32 <companion_cube> should be short strings then

15:32 <companion_cube> no need for C calls

15:33 <neiluj> yeah, 128 bit hashes

17:34 <hannes_> neiluj: in mirage-crypto we have on the ocaml side https://github.com/mirage/mirage-crypto/blob/main/src/uncommon.ml#L32-L35 and C side https://github.com/mirage/mirage-crypto/blob/main/src/native/misc_sse.c#L5-L25 (there's as well https://github.com/mirage/mirage-crypto/blob/main/src/native/misc.c#L3-L15 for cpus without ssse3 instruction set)

17:35 <hannes_> [where Cstruct.t is a record {length, offset, bigarray} backed by a bigarray https://ocaml.org/api/Bigarray.html -- should be similar if you use bytes/string

17:40 <neiluj> Nice! Thank you very much, this reduces to a one liner

17:56 <haesbaert> hannes_: anything missing to merge the dhcp changes ?

17:57 <neiluj> hannes_, it's 10% faster in average with your suggestion :)

17:57 <neiluj> huh, more like 15%

17:57 <hannes> neiluj: which suggestion?

17:58 <hannes> haesbaert: not sure, I have only been 1 hour in front of my computer since thursday

18:00 <haesbaert> ack

18:21 <neiluj> hannes, to use the xor from Mirage

18:28 <hannes> haesbaert: I pushed a commit to bump the lower bound of OCaml, now CI should be green, and that could be merged :) thanks for working on it!

18:32 <haesbaert> hooray, thanks for review

18:32 <haesbaert> and good times were had by all

19:05 <companion_cube> neiluj: but then you need Cstruct.t which is bigger and doesn't play as nicely with the GC :p

19:06 <companion_cube> if you allocate a lot of such small strings I'm not sure the benchmarks are accurate

19:10 <hannes> (please note the links above are for inspiration, you could very well use 99% the same code for bytes/string)

19:18 <neiluj> good to know

19:40 <copy> Aren't all of those instructions sse2 and could therefore be used on all x86_64 machines? (talking about xor_into)

19:42 <companion_cube> neiluj: if you implement a DHT, xoring might be a blip on the radar anyway

19:44 <neiluj> yeah, I've made some tests and there's not that much of a difference between the two ways

19:44 <neiluj> RAM and time-wise

19:44 <neiluj> and in unrealistic conditions: 200 nodes running locally :p