szkl has quit [Quit: Connection closed for inactivity]
casastorta has quit [Remote host closed the connection]
casastorta has joined #ocaml
Haudegen has quit [Quit: Bin weg.]
tremon has joined #ocaml
euphores has joined #ocaml
olle has quit [Ping timeout: 252 seconds]
kron has joined #ocaml
<kron>
hi, is it possible to define a general 'a -> 'b without Obj.magic?
<discocaml>
<otini_> safely? No. Unsafely? Yes
<discocaml>
<otini_> ```ocaml
<discocaml>
<otini_> external f : 'a -> 'b = "%identity"
<discocaml>
<otini_> ```
<discocaml>
<otini_> (litterally the definition of Obj.magic)
<kron>
okay, you got me, but that's the definition of Obj.magic :)
<discocaml>
<otini_> otherwise a function of this polymorphic type is not definable
<kron>
thank you for confirming that
<discocaml>
<otini_> by Curry-Howard it would be a theorem that given a proposition A you can prove any other one
<kron>
I actually want to implement a ?key:('a -> 'b) -> 'a Seq.t -> 'a Seq.t, or something like it, which just prevents a Seq.t from containing successive elements that map to equal values according to the key function
<discocaml>
<otini_> ah, that’s completely possible
<kron>
it works, but it has ?(key = Obj.magic) as a default, and that's too scary
<discocaml>
<otini_> It could have been ?(key = Fun.id)
<discocaml>
<otini_> less scary
<kron>
I tried ?(key = Fun.id), but then the type of key is inferred to be ('a -> 'a) option
<kron>
but I want to accept key functions that map to a different type, I just need to be able to use (=) on that type
<discocaml>
<otini_> right, what I said doesn’t work
<discocaml>
<otini_> well, polymorphic equality is a bit unsafe anyway
<kron>
here's my example code, it works if you replace Fun.id with Obj.magic: https://termbin.com/ppzcw
<discocaml>
<otini_> ideally you would have ?key:('a -> 'b) -> ?equal:('b -> 'b -> bool) -> 'a Seq.t -> 'a Seq.t, or even just ?equal, so you don’t need to use polymorphic equality
<kron>
what makes polymorphic equality unsafe?
<octachron>
Function equality is not defined
<discocaml>
<otini_> you need it to behave the right way for all key types that you may use
<discocaml>
<otini_> so you couldn’t have functions as keys as octachron said, or use a more involved notion of equality than (=) (such as some custom equivalence)
<kron>
so it's unsafe in the sense of unpredictability, because I'm not explicit about what equality means for this type, rather than memory unsafety in the Obj.magic sense?
<octachron>
Obj.magic doesn't exist.
<kron>
I'll be happy to forget about it, if I can remove it from this function :)
<octachron>
It is unsafe in the sense that it can raise an exception, and it is only a meaningful equality for some types
<octachron>
You can make the key a mandatory argument
<discocaml>
<otini_> it may also not terminate on cyclic structures
<octachron>
with a simpler function specialized for the `Fun.id` case
<discocaml>
<otini_> ^
<kron>
you make some good points, I'll add an ?equal
<kron>
but supposing I check that (=) is appropriate (for int), a ~key:String.length argument could still be more readable than ~equal:(fun a b -> String.length a = String.length b)
<kron>
I know I could have different code paths depending on whether a non-defaulted ?key contains a None, but just to clarify: there is no default value I could set to save a code path?
<kron>
or maybe differently:
<kron>
utop # let f: 'a -> 'b = fun x -> x;;
<kron>
val f : 'b -> 'b = <fun>
* kron
has hurt itself in its confusion
bartholin has joined #ocaml
<kron>
otini_, octachron: thank you for your time and help, I'll do more AoC and forget about Obj.magic :)
Haudegen has joined #ocaml
<discocaml>
<otini_> >but supposing I check that (=) is appropriate (for int), a ~key:String.length argument could still be more readable than ~equal:(fun a b -> String.length a = String.length b)
<discocaml>
<otini_> kron: it could be ~key:String.length ~key_equal:Int.equal
<discocaml>
<otini_> (or ~key_equal:(=), same thing in this case)
<discocaml>
<otini_> annotating with : 'a -> 'b only requires that there exists two types 'a and 'b such that f is of type 'a -> 'b
<discocaml>
<otini_> which is true of the identity, for 'a = 'b 😉
<discocaml>
<otini_> to avoid that you can explicitly quantify a type variable universally:
<discocaml>
<otini_> ```
<discocaml>
<otini_> # let f : 'a 'b. 'a -> 'b = fun x -> x;;
<discocaml>
<otini_> Error: This definition has type 'c. 'c -> 'c which is less general than
<discocaml>
<otini_> 'a 'b. 'a -> 'b
<discocaml>
<otini_> ```
szkl has joined #ocaml
<kron>
having the type of the comparison change depending on whether an argument was passed was the initial mistake
<kron>
a separate dedup_on with a non-optional key function, and then a dedup that calls it with Fun.id works just fine
<kron>
(or at least, I couldn't figure out how to make the key function optional)
<discocaml>
<otini_> good
Everything has joined #ocaml
tremon has quit [Quit: getting boxed in]
rgrinberg has joined #ocaml
Everything has quit [Quit: Lost terminal]
pippijn_ has quit [Ping timeout: 248 seconds]
pippijn has joined #ocaml
bartholin has quit [Quit: Leaving]
Stumpfenstiel has joined #ocaml
ygrek has quit [Remote host closed the connection]
Serpent7776 has quit [Ping timeout: 264 seconds]
rgrinberg has quit [Quit: My Unrecognized Mac has gone to sleep. ZZZzzz…]
<discocaml>
<barconstruction> @otini_ @kron
<discocaml>
<barconstruction> I object to the use of Curry-Howard here. Unlike Coq or the simply typed lambda calculus OCaml is a Turing complete programming language and is such "inconsistent".
<discocaml>
<barconstruction> All types in OCaml are inhabited. In particular the type `'a -> 'b` is inhabited by
<discocaml>
<barconstruction> ```ocaml
<discocaml>
<barconstruction> let rec f (a: 'a) : 'b = f a`
<discocaml>
<barconstruction> ```
rgrinberg has joined #ocaml
<discocaml>
<deepspacejohn> how often does sherlocode.com update? I feel like every time I use it, half of the links to code are 404'd or for outdated line numbers.