06:21 <d_bot> <darrenldl> @mimoo the one that doesn't exist yet https://xkcd.com/927/

07:50 <d_bot> <octachron> @EduardoRFS : a value of type `'a. 'a` is one step away from a crash. Thus, the way to obtain a value of this type without exploiting a compiler bug, the value needs to be unreachable by the runtime. Exceptions are one option and non-terminating recursive functions is another one. For instance, `let x = let rec f x = f x in f f` (which also means that theoretically `while true do ... done` could have type `'a`.

09:30 <d_bot> <bikal> ah ok

09:32 <d_bot> <bikal> There really is no way to recover that value of `a` in this code `type t = T : 'a -> t` is it?

09:33 <d_bot> <bikal> I thought I would use `Obj` but oh well.

09:33 <d_bot> <bikal> 🙂

09:33 <olle> "value" of 'a?

09:33 <olle> types don't exist at runtime?

09:34 <d_bot> <bikal> i.e. when you do `match (T 100) with | a -> a `

09:35 <d_bot> <bikal> the type of a is `$T_'a`

09:35 <d_bot> <bikal> There really is no way to convert it back to `int`

09:36 <d_bot> <bikal> yeah, I realize that. This is where I miss .NET reflection sometimes

09:41 <d_bot> <dinosaure> you need something which say that the value is an `int`

09:41 <d_bot> <dinosaure> such as `type 'a w = Int : int w type t = T : 'a w * 'a -> t`

09:42 <d_bot> <dinosaure> then, `match T (Int, 100) with T (Int, v) -> v`

09:42 <Armael> with `type t = T : 'a -> t`, values of type t contain a value of type "some a"

09:42 <Armael> not "all a"

09:42 <Armael> it's an existential quantification, not universal

09:43 <Armael> so yeah you know it has some type but not which type (and certainly not any type)

09:49 <d_bot> <octachron> In other words, `type any = T: 'a -> any` is ((mostly)) useless. You can never use the stored value.

10:01 <d_bot> <bikal> ok

10:01 <d_bot> <bikal> yeah

10:05 <d_bot> <bikal> yep. realizing that now. Working with GADT ... it seems different typing rules apply. Previously I thought GADT was equivalent to normal variants but nope, it seems it has different use cases albeit a very narrow one and even that use case seems - to me - quite awkward to use.

10:06 <d_bot> <bikal> yeah, I can grok the type witness thing a bit more now. However, my requirement was to not have any type variable in the type.

10:07 <d_bot> <bikal> which is why I went with the opaque type but as octachrom surmised that value of `'a` is useless

10:07 <d_bot> <dinosaure> as @Armael said, `'a` in your GADT is **not** any type 🙂 (or `for all`)

10:08 <d_bot> <dinosaure> `type 'a w` restricts possibilities (in my case `Int`) of `'a`

10:10 <d_bot> <bikal> Ah, is this where the terms existential and universal are applicable? I always wondered about those terms ...

10:11 <d_bot> <bikal> got it. it makes sense now, i.e. my understanding of existential and universal.

10:13 <d_bot> <bikal> and in order for `'a` to be universal we need a type witness - the `'a w` - in your example, right?

10:14 <d_bot> <dinosaure> no, `'a` in your `T` constructor still is existential. The `'a w * 'a` just puts an equality constraint on what we have in `'a w` and what we have in `'a`

10:17 <d_bot> <dinosaure> you should take a look on this tutorial 🙂 https://www.cl.cam.ac.uk/teaching/1415/L28/gadts.pdf

10:18 <d_bot> <dinosaure> it explains GADT very well

10:18 <d_bot> <bikal> thanks. looking at it now

10:19 <d_bot> <dinosaure> the manual is pretty good too: https://ocaml.org/manual/gadts.html

10:20 <d_bot> <dinosaure> the best to learn GADT (imho) is to fail (many times) to express what you want - by this way, you understand more clearly the scope of GADTs

10:20 <d_bot> <dinosaure> (it's how I learned GADT, fail to express some useless assertions, peano number is a good start to play a battle with the compiler)

10:23 <d_bot> <octachron> GADTs are quite equivalent to normal ADTs, they have mostly one supplementary ability: they can introduce type equations on pattern matching.

10:23 <d_bot> <octachron> Part of the issue is that it may looks like GADTs allow you to lift type discipline, when it is the reverse that it is true: GADTs enforce a much finer-grained type discipline.

10:24 <d_bot> <octachron> (An universal type is more something like `type id = { id: 'a. 'a -> 'a } let id = { id = fun x -> x }` where the identity function is still the identity function for every possible types.

10:28 <d_bot> <dinosaure> I would like to say that GADT is not strictly the best solution (for a production perspective). @octachron said that it introduces type equation on pattern matching. By this way, you can ensure an exhaustive pattern-matching with less constructor than your GADT according to your type equation. GADT comes useful to delete an `assert false` and prove with types that the case can never occur. But the cost to explain to the type sy

10:30 <d_bot> <dinosaure> it still is my opinion - but I mostly use GADT for restricted and well-define problems than to try to use them systematically

10:30 <d_bot> <dinosaure> (and we mostly need time to really understand any paths of your code to be able then to discard, with types, some of them)

10:34 <d_bot> <octachron> Yes, GADTs might allow you to prove to the type system that some cases cannot happen, which is great. But that also means that you have to write a proof, and in a non-proof oriented language ... which is less great.

11:52 <d_bot> <bikal> @octachron how does one use `'a key` and `'a` in dbuenli's `Hmap.iter` given that iter is `val iter : (binding -> unit) -> t -> unit` and binding is `type binding = B : 'a key * 'a -> binding`? Isn't the find quite useless?

11:58 <d_bot> <bikal> https://github.com/dbuenzli/hmap/blob/master/src/hmap.mli#L76

12:00 <d_bot> <octachron> With `B: 'a key * 'a` , even after forgetting the type `'a`, you remember that the the type `'a` of the key and of the element is the same.

12:01 <d_bot> <octachron> Thus, if you have a key `'b key`, you can check if the two keys are equals, and if they are you recover the information that `'a` = `'b`.

12:03 <d_bot> <octachron> Maybe one point that you were missing, is that for some GADTs, it is possible to implement a function `'a t -> 'b t -> ('a,'b) eq option`. In other words, you can test equalities over the whole family of types, ignoring the indexing types.

12:04 <d_bot> <octachron> And yes, to use the value part of a binding, you need to not only know a key but also the type of this key from another source.

12:10 <d_bot> <bikal> ok ... hmm looking at the hmap now to see how he's done it

12:15 <hannes> FWIW, I developed a related library - https://github.com/hannesm/gmap - where you specify your GADT and comparison, and get a Map.S from it.

12:16 <hannes> the difference is the implementation strategy, and that in Hmap you dynamically insert keys and their types, while in Gmap you need to know the set of keys upfront. the motivation for Gmap was e.g. DNS resource records - where depending on the type you have different values (A record contains ip addresses, MX records contains mail server names, ...)

12:17 <olle> ha!

12:17 <olle> someone on #proglangdesign recommended gmap yesterday

12:30 <hannes> and really, my motivation (and usage) is in https://github.com/mirage/ocaml-dns, and also X509 (extensions) https://github.com/mirleft/ocaml-x509 -- but now lots of things in network protocols look like a good fit for gmap (basically everything where you have optional fields with tag, and value -- plus constraints such as "may only occur once")

12:30 <d_bot> <dinosaure> yeah, strategies differ between `gmap` and `hmap`. `hmap` has a big issue in my opinion when two keys with the same type are not equal such as `let k0 : int key = Hmap.Key.create () ;; let k1 : int key = Hmap.Key,create () ;; Hmap.Key.(equal (hide_type k0) (hide_type k1)) = false`

14:59 <dukester> Ocaml noob here. https://www.cs.cornell.edu/courses/cs3110/2020fa/textbook/basics/intro.html What a GREAT tutorial IMHO !!

15:50 <d_bot> <bikal> @hannes this is very nice .. https://github.com/hannesm/gmap/blob/master/gmap.ml#L96 👍

15:51 <d_bot> <bikal> @octachron I think I got the "missing piece" you were talking about in gmap.

16:23 <MangaD> Hello, I am having a problem with my code that perhaps someone can help me with. I have the following function:

16:24 <MangaD> let foo s = (int_of_string ("0x" ^ s))

16:24 <MangaD> And I get this error: Error: This expression has type string but an expression was expected of type Val.t

16:29 <Fardale> MangaD: what if you replace "0x" ^ s by String.concat "" ["0x"; s]?

16:45 <MangaD> Fardale: Apologies for the late response. I did that right now and the error is exactly the same.

16:46 <MangaD> https://imgur.com/ca6oL4w.png

16:48 <octachron> You probably have shadowed `int_of_string`. Use `Stdlib.int_of_string`, or `Pervasives.int_of_string` if you are using a old OCaml version.

16:50 <MangaD> octachron: life saver <3

20:57 <d_bot> <bikal> Is it the requirement that `'a t` have to be a GADT? i.e. not `type 'a t = a` but `type 'a t = A : int t | B: float t .. etc`

21:02 <d_bot> <octachron> Yes.

23:31 <dukester> Is there a way to still use ``ocamlbuild'' after using ``ocamlc''? I don't like all the directories ``dune'' creates.

23:39 <dukester> Got it! ``opam install ocamlbuild''

23:52 <companion_cube> dune only creates `_build` though?

23:55 <dukester> companion_cube, it seems that there was a lot of other directories and crap in `_build'.

23:55 <companion_cube> _build/default/ contains most of what you need

23:55 <companion_cube> anyway, good luck with ocamlbuild :p

23:55 <dukester> I just tried it! Not too bad

23:56 <dukester> I'm a noob - so I'l probably change my mind down the road