companion_cube changed the topic of #ocaml to: Discussions about the OCaml programming language | http://www.ocaml.org | OCaml 4.11 release notes: https://caml.inria.fr/pub/distrib/ocaml-4.11/notes/Changes | Try OCaml in your browser: http://try.ocamlpro.com | Public channel logs at http://irclog.whitequark.org/ocaml
amiloradovsky has joined #ocaml
amiloradovsky has quit [Remote host closed the connection]
amiloradovsky has joined #ocaml
<d_bot> <stab> "Semantic foundations of program analysis." has the proof that it's a special case of solving a dynamic system, but im gonna be honest it's a bit above my paygrade
<d_bot> <stab> im not very smart, all the Cosout papers make me feel very uneducated
<companion_cube> ah, yeah, I don't know much about that either
<companion_cube> and the tendency to say "everything is just abstract interpretation" is annoying
<d_bot> <stab> Yeah idk I’ve been meaning to read the paper that talks about doing the proof theoretic approach via abstract interpretation
<companion_cube> I've heard that cousot papers are always unreadable
<d_bot> <stab> Yeah it’s pretty rough
<d_bot> <stab> I’ve also tried watching a talk by him and holy shit
<companion_cube> I think it's ok to read papers by other authors
<companion_cube> (what's the "proof theoretic approach"?)
<d_bot> <stab> Yeah idk there aren’t many foundational abstract interpretation papers by anyone else
<d_bot> <stab> Proof theoretic is Cosouts word for like Hoare logic type approaches
<d_bot> <stab> Deductive logics etc
<d_bot> <stab> Like the stuff infer does with separation logic
yomimono has quit [Ping timeout: 246 seconds]
<companion_cube> ahahahah, why would you use abstract interpretation for that :D
<d_bot> <stab> I think the paper is about combining the two
<d_bot> <stab> So sound approximations by exchanging information between both analyses
<companion_cube> ah, like a product of a lattice and the proof triplets?
<d_bot> <stab> Yeah I’d assume but I haven’t read the paper
yomimono has joined #ocaml
<d_bot> <stab> I’ve been putting it off because those papers tend to give me anxiety about my discrete math skills
<companion_cube> they don't seem to be written to be understandable :p
<companion_cube> (I once tried to read a 3 page, 2 column cousot paper, and it was hilariously ununderstandable)
<companion_cube> (so if they write papers this way, it's on them that the papers are so unreadable)
<d_bot> <stab> Yeah part of me thinks the topic is a bit dense, but I don’t know if it needs to be this unapproachable
<companion_cube> 🤷
<companion_cube> it's a bit like cousot has a hammer, and everything loooks like a nail, too
<companion_cube> looks*
<d_bot> <stab> Yeah although you can make a pretty strong argument that model checking is just a subset of abstract interpretation
jbrown has joined #ocaml
<d_bot> <stab> granted it's kinda a dumb argument lol
mxns has joined #ocaml
mxns has quit [Ping timeout: 265 seconds]
mxns has joined #ocaml
rgrmrts has joined #ocaml
rgrmrts has quit [Client Quit]
djellemah has joined #ocaml
mxns has quit [Ping timeout: 240 seconds]
aaaaaa has joined #ocaml
rgrmrts has joined #ocaml
amiloradovsky has quit [Ping timeout: 240 seconds]
aaaaaa has quit [Ping timeout: 258 seconds]
aaaaaa has joined #ocaml
aaaaaa has quit [Ping timeout: 256 seconds]
_whitelogger has joined #ocaml
yomimono_ has joined #ocaml
yomimono has quit [Ping timeout: 272 seconds]
rgrmrts has quit [Quit: beep boop]
unihernandez22 has joined #ocaml
laokz has joined #ocaml
nicoo has quit [Remote host closed the connection]
nicoo has joined #ocaml
caente has quit [Ping timeout: 252 seconds]
yomimono_ has quit [Ping timeout: 246 seconds]
yomimono has joined #ocaml
<snowpanda> In Java we can have List<Object> to hold objects of any type. What would the equivalent in OCaml be?
<brettgilio> snowpanda: Any polymorphic type list ('a list)
<brettgilio> Do you have a context application in mind?
quazimodo has quit [Remote host closed the connection]
<brettgilio> That might help give a more specific answer.
<companion_cube> snowpanda: not really, OCaml doesn't have reflection so `object` would be pretty useless
<brettgilio> ^ agreed
<companion_cube> then you can use existentials if you want a list of things with a same behavior, but it's not a particularly common pattern
<companion_cube> (as in: `type show = Show : 'a * ('a -> string) -> show` and then a `show list` can work)
sleepingisfun has joined #ocaml
djellemah has quit [Ping timeout: 244 seconds]
<snowpanda> companion_cube: I don't understand what your last line is doing, sorry. I'm new to OCaml
ski has quit [Ping timeout: 260 seconds]
<snowpanda> brettgilio: Hmm I'm not sure I understand what you're saying either above
<snowpanda> As a context application, I was wondering how we could create a list where we could keep adding values of any type we want
<brettgilio> snowpanda: what you are looking for is a record with type polymorphism
delysin has joined #ocaml
<snowpanda> brettgilio: But with type polymorphism, the set of possible types is still limited by the definition isn't it?
<companion_cube> snowpanda: a list with any type inside is useless
<companion_cube> when you access the list, you'd have elements on which you have 0 information (and hence can do nothing with)
<snowpanda> companion_cube: Yeah, I was just wondering more out of curiosity
<companion_cube> `type any = Any : 'a -> any`
<companion_cube> ^ with this you can put any type in a list: `let l = [Any 1; Any "foo"]`
<companion_cube> except it's useless
<snowpanda> companion_cube: I see. What's the right way to read that line? type any is defined to have a type constructor Any which takes a value of any type and returns an any?
<companion_cube> it's a GADT
<snowpanda> companion_cube: Thanks. I'm reading through the book https://www.cs.cornell.edu/courses/cs3110/2019sp/textbook/intro/intro.html and don't see GADTs anywhere
<snowpanda> In case you happen to be familiar with that book, do you know if it's just not covered in there?
<companion_cube> I have no idea
<companion_cube> it's a somewhat advanced feature
aaaaaa has joined #ocaml
<snowpanda> companion_cube: I see, thanks
<brettgilio> snowpanda: there is a 2020fa iteration of that book
<brettgilio> follow that instead
<brettgilio> youre 3 versions behind
unihernandez22 has quit [Quit: Leaving]
<companion_cube> anyway, good night
<brettgilio> companion_cube: o/
<snowpanda> thanks good night
<snowpanda> brettgilio: Oops I linked the wrong version, I am actually reading the 2020 sp version (so one version behind)
<snowpanda> I'm still pretty sure that it doesn't cover GADTs though
mbuf has joined #ocaml
waleee-cl has quit [Quit: Connection closed for inactivity]
narimiran has joined #ocaml
laokz has quit [Ping timeout: 260 seconds]
osa1 has joined #ocaml
narimiran has quit [Ping timeout: 272 seconds]
rpcope has quit [Ping timeout: 256 seconds]
narimiran has joined #ocaml
rpcope has joined #ocaml
<d_bot> <Drup> @stab I've heard decent feedback on https://mitpress.mit.edu/books/introduction-static-analysis
<d_bot> <Drup> (haven't read it myself)
Haudegen has joined #ocaml
laokz has joined #ocaml
snowpanda has quit [Quit: Leaving...]
yomimono has quit [Ping timeout: 272 seconds]
yomimono has joined #ocaml
olle has joined #ocaml
laokz has quit [Ping timeout: 260 seconds]
laokz has joined #ocaml
mbuf has quit [Ping timeout: 244 seconds]
bartholin has joined #ocaml
hnOsmium0001 has quit [Quit: Connection closed for inactivity]
bartholin has quit [Quit: Leaving]
wingsorc has quit [Ping timeout: 244 seconds]
inkbottle has joined #ocaml
zebrag has quit [Ping timeout: 260 seconds]
zebrag has joined #ocaml
inkbottle has quit [Ping timeout: 260 seconds]
<d_bot> <ostera> i've got a copy of that on the way
Haudegen has quit [Quit: Bin weg.]
Haudegen has joined #ocaml
schlaftier has joined #ocaml
<d_bot> <stab> Yeah I worked through https://cs.au.dk/~amoeller/spa/
<d_bot> <stab> At one point. I’d say it’s the finer details of the proofs that lose me in some of the newer abstract interpretation papers
caente has joined #ocaml
motherfsck has joined #ocaml
laokz has quit [Ping timeout: 272 seconds]
mbuf has joined #ocaml
laokz has joined #ocaml
jbrown has quit [Ping timeout: 272 seconds]
ski has joined #ocaml
jbrown has joined #ocaml
mxns has joined #ocaml
waleee-cl has joined #ocaml
Anarchos has joined #ocaml
Anarchos has quit [Quit: Vision[0.10.3]: i've been blurred!]
Anarchos has joined #ocaml
Anarchos has quit [Quit: Vision[0.10.3]: i've been blurred!]
laokz has quit [Quit: Leaving]
Anarchos has joined #ocaml
<d_bot> <Lupus> @companion_cube
<d_bot> <Lupus> > type any = Any : 'a -> any
<d_bot> <Lupus> > ^ with this you can put any type in a list: let l = [Any 1; Any "foo"]
<d_bot> <Lupus> > except it's useless
<d_bot> <Lupus> not that useless!
djellemah has joined #ocaml
<companion_cube> ahah right.
<companion_cube> still very awful :p
<olle> 16:56 < d_bot> <Lupus> > type any = Any : 'a -> any
<olle> Generic blaha bla?
<companion_cube> GADT
<olle> Right, thanks ^^
<olle> Neat trick.
<companion_cube> it's more useful when you pair the 'a with a function that consumes 'a
<olle> The keyword `function`?
<companion_cube> wat
<companion_cube> no, a function type
<companion_cube> `type show = Show : 'a * ('a -> string) -> show` for example
<olle> Hm
<olle> But you still have to match on 'a?
<companion_cube> you can't, it's existential
<companion_cube> if you do `let f (Any x) = …`
<companion_cube> you cannot do anything with `x`
<companion_cube> (bar calling a few polymorphic functions like Marshal)
<olle> I thought it was possible to unpack it with match?
<d_bot> <ostera> @olle you can, but now the type `'a` has been lost so you don't know what type it actually had
<companion_cube> olle: `List.map (fun (Any x) -> …) [Any 1; Any true]`
<d_bot> <ostera> in companion_cube's example there is another function that is known to have the same type `'a`, so you can consume `x` with it
<companion_cube> what would the tyype of `x` be?
<companion_cube> type*
<companion_cube> the only way it works is that x has a totally opaque ("existential") type
<olle> match x with x : int Any -> ...
<olle> | x : string Any -> ...
<Armael> types don't exist at runtime
<olle> How dare you
<companion_cube> olle: that doesn't exist
<olle> So sad
<companion_cube> it's also part of why memory usage of OCaml is decent? :p
<companion_cube> (reflection would be useful, honestly, it's just not something that was added)
<olle> ure
<olle> Sure
DanC has joined #ocaml
dckc has quit [Read error: Connection reset by peer]
DanC is now known as dckc
<d_bot> <mseri> If you want to have somewhat constrained heterogeneous lists in ocaml, you can have a look at https://discuss.ocaml.org/t/heterogeneous-list-using-gadts and https://discuss.ocaml.org/t/a-heterogenous-list-difflist-that-you-can-both-append-to-and-safely-access-elements
<olle> What's wrong with ADT?
<companion_cube> who said that?
dckc has quit [Ping timeout: 260 seconds]
<olle> No one?
dckc has joined #ocaml
<companion_cube> -_- so what do you mean thne
<d_bot> <ostera> are we missing some messages on the discord side?
<Drup> No, it doesn't make sense on either side.
<olle> companion_cube: I was hoping someone would say GADT are overkill for this use-case
<companion_cube> this use case = a list of things of different types? nope
<olle> Depends on when you know which types you have, no?
<companion_cube> ah if it's a finite set of types, you can just a sum type, yes
<olle> Or, you mean making a lib for this.
<companion_cube> but it's quite a different use case
<olle> mm
<olle> I miss OCaml.
<olle> I remember when this channel taught me how to program in it. :) 8 years ago?
<olle> True, it was never much for smalltalk, haha.
Haudegen has quit [Quit: Bin weg.]
mbuf has quit [Quit: Leaving]
Tuplanolla has joined #ocaml
ransom has quit [Quit: My MacBook has gone to sleep. ZZZzzz…]
ransom has joined #ocaml
ransom has quit [Quit: Textual IRC Client: www.textualapp.com]
mxns has quit [Ping timeout: 240 seconds]
<caente> companion_cube: I've seen you in lobsters right?
<companion_cube> yep
waleee-cl has quit [Quit: Connection closed for inactivity]
mxns has joined #ocaml
mxns has quit [Ping timeout: 260 seconds]
ggole has joined #ocaml
olle has quit [Ping timeout: 264 seconds]
Haudegen has joined #ocaml
waleee-cl has joined #ocaml
Anarchos has quit [Quit: Vision[0.10.3]: i've been blurred!]
<d_bot> <kanishka> Is there any foundation that is planning on funding finishing Github Semantic library parsing for ocaml? It would be nice to have "go to definition" in github pull requests
<companion_cube> does github even merge this kind of PR? I haven't heard that other languages got semantic support since they released the original set
Anarchos has joined #ocaml
<d_bot> <kanishka> Looks like merges/progress is being made
Anarchos has quit [Quit: Vision[0.10.3]: i've been blurred!]
<companion_cube> did they add anything?
<d_bot> <kanishka> https://github.com/314eter?tab=overview&from=2020-09-01&to=2020-09-30 - this person has been addressing blockers and merging into libs
<companion_cube> what I mean is, did github add any language since they launched the whole thing? I doubt OCaml is the most active on that front
hnOsmium0001 has joined #ocaml
sonologico has joined #ocaml
osa1 has quit [Ping timeout: 240 seconds]
wingsorc has joined #ocaml
motherfsck has quit [Read error: Connection reset by peer]
motherfsck has joined #ocaml
Anarchos has joined #ocaml
BitPuffin has quit [Quit: killed]
aspiwack[m] has quit [Quit: killed]
bglm[m] has quit [Quit: killed]
labor[m] has quit [Quit: killed]
jimt[m] has quit [Quit: killed]
xzax_[m] has quit [Quit: killed]
pqwy[m] has quit [Quit: killed]
sepp2k has quit [Quit: killed]
aecepoglu[m] has quit [Quit: killed]
quizzop[m] has quit [Quit: killed]
flux has quit [Quit: killed]
Manis[m] has quit [Quit: killed]
peddie has quit [Quit: killed]
talyian[m] has quit [Quit: killed]
dash has quit [Quit: killed]
lnxw37d4 has quit [Quit: killed]
aterius has quit [Quit: killed]
sonologico has quit [Remote host closed the connection]
<d_bot> <kanishka> I looked for a few minutes, but I couldn't tell whether a language has transformed from proposal to fully merged in the git history.
bglm[m] has joined #ocaml
mxns has joined #ocaml
mxns has quit [Ping timeout: 258 seconds]
Hrundi_V_Bakshi has joined #ocaml
lnxw37d4 has joined #ocaml
BitPuffin has joined #ocaml
jimt[m] has joined #ocaml
xzax_[m] has joined #ocaml
aecepoglu[m] has joined #ocaml
flux has joined #ocaml
peddie has joined #ocaml
pqwy[m] has joined #ocaml
aspiwack[m] has joined #ocaml
ansiwen[m] has joined #ocaml
labor[m] has joined #ocaml
Manis[m] has joined #ocaml
aterius has joined #ocaml
dash has joined #ocaml
sepp2k has joined #ocaml
quizzop[m] has joined #ocaml
talyian[m] has joined #ocaml
mxns has joined #ocaml
amiloradovsky has joined #ocaml
narimiran has quit [Ping timeout: 240 seconds]
ggole has quit [Quit: Leaving]
nullcone has quit [Quit: Connection closed for inactivity]
reynir has quit [Ping timeout: 265 seconds]
reynir has joined #ocaml
Jesin has joined #ocaml
Hrundi_V_Bakshi has quit [Ping timeout: 240 seconds]
rgrmrts has joined #ocaml
Haudegen has quit [Ping timeout: 256 seconds]
rgrmrts has quit [Quit: beep boop]
wingsorc has quit [Quit: Leaving]
wingsorc has joined #ocaml
Tuplanolla has quit [Quit: Leaving.]
amiloradovsky has quit [Ping timeout: 240 seconds]
aaaaaa has quit [Quit: leaving]
webshinra_ has joined #ocaml
webshinra has quit [Read error: Connection reset by peer]
Anarchos has quit [Quit: Vision[0.10.3]: i've been blurred!]