reynir has quit [Remote host closed the connection]
reynir has joined #ocaml
mxns has joined #ocaml
mxns has quit [Ping timeout: 264 seconds]
borne has joined #ocaml
borne has quit [Ping timeout: 264 seconds]
motherfsck has joined #ocaml
mxns has joined #ocaml
mxns has quit [Ping timeout: 256 seconds]
amiloradovsky has joined #ocaml
mxns has joined #ocaml
narimiran has joined #ocaml
mxns has quit [Ping timeout: 260 seconds]
mfp has quit [Ping timeout: 260 seconds]
mxns has joined #ocaml
osa1 has joined #ocaml
mxns has quit [Ping timeout: 264 seconds]
mxns has joined #ocaml
mxns has quit [Ping timeout: 272 seconds]
zebrag has quit [Quit: Konversation terminated!]
zebrag has joined #ocaml
zhenchaoli has quit [Ping timeout: 264 seconds]
zhenchaoli has joined #ocaml
zebrag has quit [Quit: Konversation terminated!]
reynir has quit [Ping timeout: 240 seconds]
reynir has joined #ocaml
mxns has joined #ocaml
mmohammadi9812 has quit [Read error: Connection reset by peer]
mmohammadi9812 has joined #ocaml
mxns has quit [Ping timeout: 260 seconds]
Serpent7776 has joined #ocaml
berberman has joined #ocaml
berberman_ has quit [Ping timeout: 260 seconds]
mxns has joined #ocaml
mxns has quit [Ping timeout: 246 seconds]
mxns has joined #ocaml
mmohammadi9812 has quit [Ping timeout: 240 seconds]
mmohammadi9812 has joined #ocaml
mxns has quit [Ping timeout: 260 seconds]
amiloradovsky has quit [Remote host closed the connection]
amiloradovsky has joined #ocaml
mxns has joined #ocaml
mxns has quit [Ping timeout: 256 seconds]
zhenchaoli has quit [Ping timeout: 260 seconds]
bartholin has joined #ocaml
Haudegen has joined #ocaml
stux|RC has quit [Quit: Aloha!]
stux|RC has joined #ocaml
bartholin has quit [Quit: Leaving]
borne has joined #ocaml
amiloradovsky has quit [Remote host closed the connection]
amiloradovsky has joined #ocaml
_whitelogger has joined #ocaml
<d_bot>
<ostera> mrvn: so you'd have N values for a record with N fields?
zozozo has quit [Ping timeout: 272 seconds]
hnOsmium0001 has quit [Quit: Connection closed for inactivity]
zozozo has joined #ocaml
mxns has joined #ocaml
mxns has quit [Ping timeout: 256 seconds]
mmohammadi9812 has quit [Ping timeout: 260 seconds]
mmohammadi9812 has joined #ocaml
decentpenguin has quit [Ping timeout: 260 seconds]
mfp has joined #ocaml
<d_bot>
<Mando> guys how do I get bot titles?
<Drup>
We are totally humans
<Drup>
I promise
<Armael>
🤖
mxns has joined #ocaml
mxns has quit [Ping timeout: 265 seconds]
Haudegen has quit [Quit: Bin weg.]
<d_bot>
<stab> Lol the bots are an extremely exclusive group
<d_bot>
<stab> Obviously
<d_bot>
<stab> What’s the advantage of irc anyways, just not having to open the bloated discord app?
<d_bot>
<stab> Or do y’all want to feel like it’s 1990
<d_bot>
<psafont> I thought there were unofficial CLIs for discord. It's been years since I lost access to the server where I was running irssi, running quassel on a rpi was not stable enough 😦
<Fardale>
@stab stability, IRC is still here after all. It is simple, free, open, no need for an account, you can use whatever client to access it, it is enough for communication
kmwyard has left #ocaml [#ocaml]
<vsiles>
@stab Well, I'm working on a remote server anyway, so using tmux/irssi saves me tons of time rather than context switching to discord/chrome
steenuil has joined #ocaml
<d_bot>
<stab> Hmmm idk from using irc on an unreliable connection at work I see a big issue with like losing DMs etc
<d_bot>
<steenuil> I'm using an alternative client for discord and it's messing up the IRC bridge a bit, all the IRC users have the same name as the last person who wrote something
<d_bot>
<stab> Like not having messaging available while ur not online without a bouncer is a pain
<steenuil>
so I might just use IRC specifically for this channel :p
<vsiles>
steenuil: using for this one and #ocaml-fr mostly :D
<Fardale>
Bouncer or just an client running all the time. I agree that it is not as easy to use as discord. But once you have the setup for it, it's works fine
<d_bot>
<stab> I mean client running all the time really isn’t an option for some of us who are fairly often called in for on-site stuff etc so move a lot
<d_bot>
<stab> Like unfortunately most of my time is spent on a laptop
<steenuil>
you just have to set up a bouncer
<d_bot>
<stab> So I’d have to setup a bouncer which is sketch imo
<d_bot>
<stab> Unless ur hosting ur own
<d_bot>
<stab> I guess the argument there is do u trust discord more than ur bouncer
<d_bot>
<stab> Which I’d like to say yes but who knows
<Fardale>
I don't run the client on my laptop, I run my client on a server and connect to it when I want to read IRC
<d_bot>
<ostera> who owns the bot btw?
<d_bot>
<stab> Yeah I mean that’s basically a bouncer
<Fardale>
But again, I have access to a server to do that, which is not something everyone have
<d_bot>
<ostera> i really like the colored code-snippets in discord
<d_bot>
<ostera> but i don't like bugging people
<d_bot>
<ostera> (also how do you see gifs?)
<d_bot>
<stab> I assume the bot doesn’t pass them thru or sends the discord file link
<Fardale>
@ostera on IRC pasting code is bad practice, people use website for this and there is colored syntax on some on them
<d_bot>
<ostera> yeah, i'm aware of irc etiquette, that's why I'd like to know who owns the bot to see if there's something that can be done about it 🙂
<d_bot>
<ostera> (e.g, auto paste-bins)
<d_bot>
<stab> Altho if I upload directly to discord that might not work because if they host it I think they have access control on the file
<Fardale>
For file upload to discord, we have a link to the file on discord server if I remember correctly
<d_bot>
<stab> Yeah I just don’t think you can access that without a discord account
<d_bot>
<stab> Could be wrong tho
<steenuil>
nah you can
Haudegen has joined #ocaml
decentpenguin has joined #ocaml
raver has quit [Read error: Connection reset by peer]
mmohammadi9812 has quit [Ping timeout: 256 seconds]
mxns has joined #ocaml
mmohammadi9812 has joined #ocaml
mxns has quit [Ping timeout: 272 seconds]
olle has quit [Ping timeout: 256 seconds]
mxns has joined #ocaml
amiloradovsky has quit [Remote host closed the connection]
amiloradovsky has joined #ocaml
olle has joined #ocaml
mxns has quit [Ping timeout: 244 seconds]
mxns has joined #ocaml
<companion_cube>
the discord bridge is in Go, I heard it's easy to read and write :p
<d_bot>
<glennsl> Does anyone know if it has a name?
<d_bot>
<glennsl> Note the `identify` function, where the magic actually happens. Given two unknown types and a value of one of them, this identifies them as the same type with the help of a "witness" and "casts" it to the other unknown type.
<d_bot>
<ostera> this reminds me of some Jane Street base code
<d_bot>
<glennsl> I've simplifies it a lot from the actual code I came across, and have tried to give it more meaningful names. Therefore not unlikely that the terminology is way off.
<d_bot>
<glennsl> @ostera base is big, and this isn't where I got it from, but it wouldn't surprise me if it has something like this.
<d_bot>
<ostera> some time ago we were talking about making a type-safe process registry with @octachron and @dinosaure, and they linked the right module -- something like `univ.ml`
<d_bot>
<octachron> The identify function is not needed at all? This is the trick used for hmap in most recent implementations
<mrvn>
I've seen this as "eq" in other places too.
reynir has joined #ocaml
<d_bot>
<octachron> It is indeed the coverter function associated to `eq` that immediately use the discovered type equality to convert between the two types.
<d_bot>
<glennsl> It was named `eq` in brisk-reconciler too. I just found it confusing as it's actual purpose isn;t so much to determine equality as to make sure they're equal and "convert" the type.
<mrvn>
there is no conversion going on. It returns the value if the witnesses are equal.
<mrvn>
type equality, ergo eq
<d_bot>
<octachron> Oh, I know why you needed the identify function: without the first class module trick, you cannot remember that you only ever create `Id` extension constructor as witness.
<d_bot>
<glennsl> @mrvn: It does so by establishing type equality internally, yes, but externally it appears as a cast.
<d_bot>
<glennsl> Is "type identification by way of type witness" an accureate description?
<mrvn>
octachron: the first class module trick gives it a unique value.
<d_bot>
<glennsl> That kind of misses the casting bit though...
<d_bot>
<Drup> It's called eq because it's about establishing equality on things that are of different types.
<d_bot>
<Drup> Once you have established tags/witness's values are equal, you can deduce that types are, after all, equal too.
<octachron>
mrvn, ? the values of extension constructors are always unique.
<mrvn>
octachron: the name of the label is unqiue too
<mrvn>
although I guess you don't care about the unqiue name since it's never used again, only the field in the returned record.
<mrvn>
octachron: another reason for the first class module: Anything else is a syntax error when you try to extend the id type
<octachron>
I am not sure how first class module are supposed to protect someone from syntax errors
<mrvn>
octachron: you can't say "type _ id += ..." in a function. You need a module for that.
<d_bot>
<glennsl> Yeah I think it's just to allow the type definition/extension. I see from `hmap` that you could also just return the first class module directly and define the `identify`/`eq` function outside it.
<d_bot>
<glennsl> `univ` uses `match_` for `eq`/`identify`. I think that fits better.
<mrvn>
glennsl: I ment less in the compiler output / runtime. The hmap only creates the module struct. The other code has the module struct, the function and the record. Should have a larger foodprint.
berberman has joined #ocaml
berberman_ has quit [Ping timeout: 264 seconds]
<d_bot>
<glennsl> Right. That I don't know, but your reasoning makes sense I think.
<d_bot>
<glennsl> Ok, so from the discourse post@Ulugbek linked to, this pattern seems to be called "Universal values". At least that's what Jane Street calls it. But it is effectively an implementation of dynamically typed values.
<d_bot>
<glennsl> Thanks all for digging up all this gold though!
<mrvn>
glennsl: The intention is to have universal containers. Things you can store any type in them.
<d_bot>
<ostera> @glennsl what are you using them for in Brisk? 🙂
mmohammadi9812 has quit [Ping timeout: 265 seconds]
<d_bot>
<glennsl> It's used to store the component state in the instance tree, and pass the current state to the next component render call.
<d_bot>
<glennsl> If that makes sense...
<d_bot>
<wokalski> To statically determine identity of a component
<d_bot>
<ostera> so as a universal container for a single value then
<d_bot>
<ostera> e.g, since I imagine the component state type changing from component to component
<d_bot>
<wokalski> It's not even a container. It just carries state's type.
<d_bot>
<glennsl> I think we're talking about slightly different things.
<d_bot>
<glennsl> Technically what's in brisk-reconciler is not a universal container, but just the wtiness and matching function.
<d_bot>
<glennsl> But I think you could easily bundle the witness and state into a universall value
<d_bot>
<glennsl> They're both there, just separate.
<d_bot>
<glennsl> So far as I udnerstand at least
<d_bot>
<ostera> that's what I understood as well
<d_bot>
<ostera> e.g, not bundled, but serving a similar purpose
<d_bot>
<ostera> > To statically determine identity of a component
<d_bot>
<ostera> @wokalski this threw me off tho -- are you identifying a component by the witness of its state type?
mmohammadi9812 has joined #ocaml
<d_bot>
<wokalski> it's not a witness of its state type. Practically the easiest way to think about it is unique id. Given `type t = | X: t('a) -> t` and two values of type t we can determine if 'a is the same (what i just wrote is not precisely correct but that's the mental model)
<d_bot>
<ostera> so far so good (and I get that that particular GADT is not very useful since we don't have a way of recovering that 'a)
<d_bot>
<wokalski> Or rather if both values of `'a some_other_type` have been produced by the same function.
<d_bot>
<ostera> oh! okay, i think I see that now. values produced from the same function will end up having the same id.
<d_bot>
<wokalski> It's the precise desrcription. No, it's very useful because `some_other_type` might be a record which contains functions that can operate on two `'a` values.
<d_bot>
<wokalski> So practically you get quite a bit of dynamism 🙂
<d_bot>
<ostera> as long as you pack those `'a` functions with it
<d_bot>
<ostera> afaict, that _specific_ GADT isn't, but if you replace `'a` with a `('a * 'a -> string)` for example, then it becomes useful since you can recover that type information
<d_bot>
<ostera> e.g, `type t = | X : 'a * ('a -> string) -> t`
mxns has quit [Ping timeout: 240 seconds]
<d_bot>
<ostera> or am I missing something here?
<d_bot>
<ostera> ah, wait, you have `some_other_type`.
<d_bot>
<ostera> nevermind, we're saying the same thing.
<d_bot>
<ostera> I just unpacked your type there 😛
<d_bot>
<wokalski> I was always curious if there's upper bound on the number of uniques Ids i can generate using this technique? Is there an upper bound on either number of extensible variants or maybe there's some other problem with this tehcnique?
<def>
the RAM
<def>
or rather, the address space :P
<d_bot>
<wokalski> 🙂 how is the memory representation (int value) of extensible variant even determined?
<def>
I wrote about that a long time ago, I don't know where the document is...
<def>
Basically, the witness is a pair of a string (the name of the constructor, for printing purposes) and an integer.
<def>
the integer is used to speed-up hashing and comparison. Identity is determined by the physical address of the witness.
<def>
If the constructor has no parameter, there is a single instance which is exactly the witness.
<def>
If the constructor has parameters, an instance is a block whose first field is the witness and other fields are the payload.
<d_bot>
<wokalski> Ah, I see! This makes sense
<mrvn>
wokalski: Basically the same limit as variant types.
<def>
wokalski: the integer is allocated using the same counter as for object instances
<def>
(see Oo module)
<d_bot>
<wokalski> def: I understand. Thank you. For some reason I thought that the integer value is determined in compile time and I couldn't understand how it can be done while supporting separate compilation.
<def>
So it is not guaranteed to be unique, but wrap on integer overflow.. That should be rare.
<mrvn>
heopfully it catches that and aborts
<def>
No it doesn't catch. It is not a problem, it will only cause a slightly higher change of hash collision...
<def>
chance*
<mrvn>
def: On 32bit an overflow is not that far off
<def>
wokalski: No, extensible witnesses are a dynamic entity. You would have to solve the halting problem to allocate them.
<def>
mrvn: yes, but it is fine to overflow. The integer is there to speed-up indexation, it does not affect safety.
<mrvn>
def: if the int is the first field in the record how does a collision not break things?
<def>
equality is determined by the physical address, (==)
<mrvn>
ahh, wait, it's a pointer to the witnes, not the id of the witnes.
<def>
yes, it is not the id.
<d_bot>
<wokalski> def: Thank you for the explanation.
<def>
you are welcome :)
jnavila has joined #ocaml
zebrag has quit [Quit: Konversation terminated!]
zebrag has joined #ocaml
mxns has joined #ocaml
vicfred has quit [Remote host closed the connection]
vicfred has joined #ocaml
amiloradovsky has quit [Remote host closed the connection]
amiloradovsky has joined #ocaml
larou has quit [Quit: Connection closed]
Hrundi_V_Bakshi has joined #ocaml
borne has quit [Ping timeout: 264 seconds]
Serpent7776 has quit [Quit: leaving]
jnavila_ has joined #ocaml
tane has quit [Quit: Leaving]
jnavila has quit [Ping timeout: 256 seconds]
borne has joined #ocaml
sillyotter has joined #ocaml
sillyotter has quit [Client Quit]
Hrundi_V_Bakshi has quit [Ping timeout: 244 seconds]
Hrundi_V_Bakshi has joined #ocaml
narimiran has quit [Ping timeout: 256 seconds]
jnavila_ has quit [Quit: Konversation terminated!]
neiluj has joined #ocaml
neiluj has quit [Changing host]
neiluj has joined #ocaml
amiloradovsky has quit [Ping timeout: 244 seconds]
nicoo has quit [Ping timeout: 240 seconds]
mmohammadi9812 has quit [Ping timeout: 256 seconds]
nicoo has joined #ocaml
mmohammadi9812 has joined #ocaml
neiluj has quit [Quit: leaving]
Hrundi_V_Bakshi has quit [Ping timeout: 256 seconds]