00:57 <discocaml> <elliottcable> hrm. is there a way to create a _local_ module-type in a `.mli`?

00:59 <discocaml> <elliottcable> I know I can *alias* a module that already exists at another path (`Foo := Some.Path`); but what if I need to create a temporary *entire module* that isn't then present in the exported interface?

01:17 <discocaml> <deepspacejohn> I’m not sure if I understand how that would work. Creating a “temporary” module in an interface which isn’t exposed by the interface seems like a contradiction.

01:19 <discocaml> <elliottcable> I've got a different workaround to my original problem, and what I described is probably a dangerous idea anyway for readability — but just for clarity, I'm saying something like:

01:19 <discocaml> <elliottcable> "be able to use `Foo.bar` and `Foo.baz` in `widget.mli`, without consumers seeing `Widget.Foo` existing, and without having to create `foo.mli` just for this purpose."

01:22 <discocaml> <deepspacejohn> You could define `type foo_bar = Foo.bar` in the ml and expose an abstract foo_bar in the mli.

01:46 <companion_cube> module type of struct... end?

12:37 <discocaml> <kakadu18> hey. Is there any simple explanation why we can't write a function with a type `(module M: MONAD) -> 'a M.t -> 'a M.t`

12:38 <discocaml> <kakadu18> I found explanations whey we can't return `SomeFunctor(M).t` (the type of result of a function depends on a value of the function argument)

12:38 <discocaml> <kakadu18> But in simplified case it seems that this issue doesn't appear

12:52 <discocaml> <octachron> Types inside first-class modules are existentially quantified, `(module M: monad) -> 'a M.t` is an escaping existential.

13:03 <discocaml> <kakadu18> OK, but why. Can we construct a case, when allowing polymorphism will lead to crash?

15:10 <Anarchos> I use dune to compile a lilbrary and it prefixes all the modules by Util__ which is the name of the lib. How can i get a more standard "Util." prefix ?

15:12 <companion_cube> if the library's name is `Util` then it's already the case

15:13 <Anarchos> yes my library is named util. is it a conflict with a standard name ?

15:14 <companion_cube> I'm not sure, it does sound like an extremely general name if you intend to publish it on opam

15:15 <Anarchos> it was just an little personnal utilities lib

15:28 <companion_cube> then maybe try to find a more unique name for it? :)

15:30 <Armael> independently of the name, you should get a Util. prefix?

15:30 <Armael> dune creates a util module and aliases all the util__foo modules in it, so you can do Util.Foo

15:41 <companion_cube> but the library name affects the prefix

15:41 <Armael> of course

18:43 <discocaml> <octachron> @kakadu18 , ? an escaping existential is just non-sensical

19:06 <discocaml> <kakadu18> Do you wanna say, that replacement of existential quantifier by the universal one in the context of my example, will lead to unsoundness, similar to https://counterexamples.org/scope-escape.html ?

19:27 <discocaml> <leviroth> Perhaps a related question is why we can't have the higher-kinded version of `(module Foo with type t = 'a) -> 'a`. Clearly there's no problem with escaping here.

19:56 <discocaml> <octachron> Replacing the existential quantifier on M.t by universally one would indeed directly gives you a proof of false as a one-liner.

20:16 <discocaml> <kakadu18> I have difficultuies with extending Curry-Howard isomarphism in the presence of type operators....

20:25 <discocaml> <kakadu18> It would OK, if someone would point to a recommended reading about this. (Ideally, finishable during Sunday). (Writing very long messages in Discord could be painful.) I case of questions I will return to this next week

20:25 <discocaml> <kakadu18> It would be OK, if someone would point to a recommended reading about this. (Ideally, finishable during Sunday). (Writing very long messages in Discord could be painful.) I case of questions I will return to this next week

20:25 <discocaml> <kakadu18> It would be OK, if someone would point to a recommended reading about this. (Ideally, finishable during Sunday). (Writing very long messages in Discord could be painful.) In case of questions I will return to this next week

20:48 <discocaml> <octachron> @leviroth, as far as I imperfectly understand, the current implement mostly work because replacing a zero-artiy type constructor can be done with a hack: the type of the module `M with type t = a` can , be edited on the fly to replace `t` by the type `a`, and then harmonizing the internal and external view only requires substituting a type variable, rather than trying to rewrite type digraphs.

22:26 <discocaml> <kakadu18> I thought a little bit about this, and maybe it is more obvious than I thought. If we can type-check something to `forall a . (M: sig type 'a t end) -> 'a M.t` than it should have questionable semantics for modules like `struct type _ t = I : int t | F: float t`. The same problems arise, when we want to return a GADT value from parser (we need to pack it to make it compilable).

22:27 <discocaml> <kakadu18> This intuition raises questions why the PR about modular explicits makes sense, but I will leave it for a new day...

22:29 <discocaml> <._null._> What's problematic here ?

22:30 <discocaml> <._null._> @kakadu18 What's problematic here ?

22:38 <Anarchos> kakadu18 did you find a good link to curry howard ?

22:51 <discocaml> <gooby_clown> When OCaml gets unboxed types will we get int64, int32 etc as separate types?

23:56 <companion_cube> They're already there, just not inboxed