Stumpfenstiel has quit [Ping timeout: 268 seconds]
Haudegen has quit [Ping timeout: 240 seconds]
nd__ has joined #ocaml
nd__ has quit [Ping timeout: 265 seconds]
spip has quit [Quit: Konversation terminated!]
waleee has quit [Quit: uppdatar data]
waleee has joined #ocaml
genpaku has quit [Remote host closed the connection]
nd__ has joined #ocaml
nd__ has quit [Ping timeout: 276 seconds]
nd__ has joined #ocaml
nd__ has quit [Ping timeout: 255 seconds]
nd__ has joined #ocaml
nd__ has quit [Ping timeout: 265 seconds]
chrisz has quit [Ping timeout: 265 seconds]
chrisz has joined #ocaml
waleee has quit [Ping timeout: 240 seconds]
nd__ has joined #ocaml
nd__ has quit [Ping timeout: 240 seconds]
<discocaml>
<darrenldl> @ilo Kali do you happen to know if notty works well with ansiterminal?
rf has quit [Quit: Leaving]
<discocaml>
<Kali> i am not familiar with ansiterminal, my apologies
<discocaml>
<Kali> your best bet would be to try it yourself
mbuf has joined #ocaml
trev has joined #ocaml
nd__ has joined #ocaml
nd__ has quit [Ping timeout: 276 seconds]
<discocaml>
<darrenldl> it seems that i don't need ansiterminal after all as notty should be using the same escape codes
<discocaml>
<darrenldl> thanks anyhow!
Haudegen has joined #ocaml
nd__ has joined #ocaml
nd__ has quit [Ping timeout: 240 seconds]
nd__ has joined #ocaml
nd__ has quit [Ping timeout: 276 seconds]
bgs has joined #ocaml
azimut has joined #ocaml
nd__ has joined #ocaml
Johann has quit [Ping timeout: 260 seconds]
Fardale has quit [Ping timeout: 246 seconds]
asm has quit [Ping timeout: 248 seconds]
noze` has quit [Ping timeout: 248 seconds]
Fardale has joined #ocaml
Techcable has quit [Ping timeout: 268 seconds]
Johann has joined #ocaml
asm has joined #ocaml
asm has quit [Changing host]
asm has joined #ocaml
Techcable has joined #ocaml
mro has joined #ocaml
bartholin has joined #ocaml
Serpent7776 has joined #ocaml
mro has quit [Remote host closed the connection]
mro has joined #ocaml
olle has joined #ocaml
spip has joined #ocaml
gentauro has quit [Ping timeout: 248 seconds]
gentauro has joined #ocaml
gentauro has quit [Ping timeout: 268 seconds]
gentauro has joined #ocaml
bartholin has quit [Quit: Leaving]
mbuf has quit [Ping timeout: 276 seconds]
mbuf has joined #ocaml
mro has quit [Remote host closed the connection]
mro has joined #ocaml
omegatron has quit [Quit: No Ping reply in 180 seconds.]
neiluj has joined #ocaml
Haudegen has quit [Quit: Bin weg.]
<companion_cube>
anyone knows a reference on how labelled arguments/optional arguments are implemented in the compiler? particularly in the type inference?
<octachron>
There is also a corner case for infered labels where label commutation is not allowed.
<companion_cube>
you mean, when a variable has a type containing labels, right?
<companion_cube>
it rings a bell, I feel like I've met that
<octachron>
More when a function argument has labels that are discovered when typing the main function body: "let f g = g ~x:0 ~y:1; g ~y:0 ~x:1" is an error
<octachron>
while "let f (g: x:_ -> y:_ -> _) = g ~x:0 ~y:1; g ~y:0 ~x:1" is fine.
<companion_cube>
is it not what I said?
<octachron>
Maybe?
<companion_cube>
g is a variable whose type is inferred to be a function with labels :)
<companion_cube>
but that's cool, thanks for the corner case
<neiluj>
hey! generated some bindings to a C lib where all functions use a "recursive type" which is a pointer to an address (long). All functions take it as input or return such type as output and are actually partial functions (they take specific forms of the recursive type). I guess there is no way to write a type-safe API other than looking at the C lib documentation and adding more precise types to the
<neiluj>
signatures, right?
<neiluj>
I'm afraid that's not a scalable approach if done manually
<neiluj>
sorry that's actually not really a question about ocaml
Haudegen has joined #ocaml
rf has joined #ocaml
omegatron has quit [Quit: Power is a curious thing. It can be contained, hidden, locked away, and yet it always breaks free.]
troydm has quit [Ping timeout: 260 seconds]
<neiluj>
yeah I think I won't bother adding types to the interface since it's used for prototyping
troydm has joined #ocaml
count3rmeasure has joined #ocaml
mbuf has quit [Quit: Leaving]
Haudegen has quit [Quit: Bin weg.]
mro has quit [Remote host closed the connection]
mro has joined #ocaml
jumpnbrownweasel has joined #ocaml
count3rmeasure has quit [Ping timeout: 276 seconds]
<discocaml>
<geoff> Sounds like it might be possible to do with a GADT
count3rmeasure has joined #ocaml
mro has quit [Remote host closed the connection]
<discocaml>
<octachron> Phantom types might be a better match while interfacing with C. But the core issue that the C functions are under-typed will remain.
bronsen has left #ocaml [WeeChat 3.7.1]
<neiluj>
geoff: do you have an idea of what it would look like?
<neiluj>
maybe let chatgpt parse the docs to give a hint of type, but then again not all C functions have proper docstrings...
<neiluj>
ochtachron: oh could you show a little snippet of how phantom types would help please? :)
<neiluj>
looking at these
mro has joined #ocaml
<discocaml>
<geoff> You'd want to encode the types to tell what kind of transitions are possible basically. And each function would be constrained based on the gadt type parameters, and returning a different type variant.
<discocaml>
<geoff> A similar kind of scheme could be cooked up with modules and phantom types I think. If there are lots of states and overlaps it will get hairy though probably
Tuplanolla has joined #ocaml
mro has quit [Ping timeout: 255 seconds]
<neiluj>
geoff: the transitions being the function signatures?
<octachron>
neiluj, the advantage of phantom types is that you could bind the C function with the right type constraint informations directly
<octachron>
For instance, with a C API that uses strings/ints as type witness, you could use phantom type to add the type information while keeping the untyped implementation
<octachron>
to "val add: 'a kind -> ('a,_) number -> ('a, _) number -> ('a,write) number = add"
mbuf has joined #ocaml
<octachron>
while still keeping "'a kind = string" "('a,'b) number = custom_block_number" in the implementation
Serpent7776 has quit [Quit: WeeChat 1.9.1]
<neiluj>
oh thanks so phantom types allow for "transparent" typing, that is typing that actually doesn't change the underlying type?
<neiluj>
maybe it's not exactly that
<neiluj>
but allow to attach extra metadata?
<neiluj>
to avoid redefining the ctypes bindings with different (type-safe) signatures
<discocaml>
<geoff> Transitions being when the functions change the type
<neiluj>
thanks, hmm do you have an example?
<neiluj>
(aside: geoff will publish the ctypes binding generator next weekend :))
<octachron>
Phantom types (or more precisely phantom type parameters) are types that don't correspond to any data, but add some more type metadata to the implementation.
<neiluj>
I see, that's very suitable to the situation indeed! thanks for pointing this out
<discocaml>
<geoff> But sounds like phantom types may work for you fine
<octachron>
that says that an `Unit.t` is just a float.
mro has joined #ocaml
<octachron>
with the interface that offers only 4 way to create an `Unit.t` with type either kg Unit.t, m Unit.t, s Unit.t or scalar Unit.t .
<neiluj>
oh I see now geoff, so the constructors of the GADT encoded the structure of the recursive type, ie. how inhabitants of the type are built with extra constraints thanks to the phantom type?
<neiluj>
huh is it a phantom type in the GADT the symbol 'a
<neiluj>
?
<octachron>
Not in general.
mbuf has quit [Quit: Leaving]
<octachron>
And `'a` is not a phantom parameter in the declaration of `'a t` since a `Val` constructor carries a value of type `'a`.
<neiluj>
ah right!
mro has quit [Remote host closed the connection]
<neiluj>
gadt allow encoding relations between the constructors of the type right?
<octachron>
But if you look at the packed type, you can see that it uses the `sender`, `recver`, `relay` type in its parameters, which are empty types.
<octachron>
This means that those parameter are necessary phantom type parameters (since there are no values of empty types by definition).
<octachron>
GADTs allow you to refine the relationship between the constructors, the type of the constructors argument and the type of the variant.
<octachron>
All axes can be useful (not necessarily at the same time).
<octachron>
For instance, with "type delayed = Delay: {value: 'a; action:('a -> unit)} -> delayed"
<octachron>
there is only one constructor, the variant type is not parametric, but we are expressing a relationship between the arguments of the Delay constructor.
<octachron>
Contrarily, a type witness: "type 'a t = Int: int t | Float: float t" have no constructors with arguments, but it captures a one-to-one relationship between the value of the constructors and the type of the variants.
<neiluj>
ah right, in this case it is equivalent to `type delayed = Delay of {value: 'a; action:('a -> unit)}` right?
waleee has joined #ocaml
mro has joined #ocaml
mro has quit [Remote host closed the connection]
Haudegen has joined #ocaml
<neiluj>
brb (thanks for all the help :))
neiluj has quit [Quit: WeeChat 3.7.1]
count3rmeasure has quit [Read error: Connection reset by peer]
mro has joined #ocaml
bartholin has joined #ocaml
mro has quit [Remote host closed the connection]
waleee has quit [Ping timeout: 265 seconds]
waleee has joined #ocaml
mro has joined #ocaml
neiluj has joined #ocaml
<neiluj>
going back to the undertyped C library, one way to retrieve the subset of the types for each function is to parse the AST of the body of the C functions to determine the input/output types
<neiluj>
however libclang may be not powerful enough to achieve this...
<discocaml>
<geoff> each function can return different types? Depending on the values, or the types of the inputs?
<neiluj>
damn that makes me want to rewrite the C header file parser with frama c :)
<neiluj>
geoff: you're right...
<neiluj>
that's the point of this recursive C data type
<neiluj>
depending on the types of the inputs
<discocaml>
<geoff> I think that means that you'd have to go the GADT route, rather than phantom types. Whether it is too complex of a situation to wrangle though I can't say
<discocaml>
<geoff> at least the types don't change depending on the value I guess 😅
mro has quit [Remote host closed the connection]
* neiluj
dependent types entered the chat
<neiluj>
yeah the GADT indeed seem like the way to go
mro has joined #ocaml
b0o has quit [Ping timeout: 240 seconds]
whereiseveryone has quit [Ping timeout: 240 seconds]
pluviaq has quit [Ping timeout: 240 seconds]
seeg has quit [Read error: Connection reset by peer]
toastal has quit [Read error: Connection reset by peer]
Ankhers has quit [Read error: Connection reset by peer]
patrick has quit [Read error: Connection reset by peer]
richardhuxton has quit [Read error: Connection reset by peer]
jakzale has quit [Read error: Connection reset by peer]
ardon has quit [Read error: Connection reset by peer]
philipwhite has quit [Ping timeout: 240 seconds]
ggb has quit [Ping timeout: 240 seconds]
pluviaq has joined #ocaml
richardhuxton has joined #ocaml
b0o has joined #ocaml
philipwhite has joined #ocaml
ggb has joined #ocaml
patrick has joined #ocaml
ardon has joined #ocaml
whereiseveryone has joined #ocaml
seeg has joined #ocaml
Ankhers has joined #ocaml
toastal has joined #ocaml
jakzale has joined #ocaml
waleee has quit [Ping timeout: 265 seconds]
infinity0 has quit [Remote host closed the connection]
infinity0 has joined #ocaml
trev has quit [Remote host closed the connection]
Stumpfenstiel has joined #ocaml
count3rmeasure has joined #ocaml
mro has quit [Ping timeout: 255 seconds]
mro has joined #ocaml
nd__ has quit [Ping timeout: 276 seconds]
nd__ has joined #ocaml
Haudegen has quit [Quit: No Ping reply in 180 seconds.]
Haudegen has joined #ocaml
nd__ has quit [Ping timeout: 255 seconds]
mro has quit [Remote host closed the connection]
mro has joined #ocaml
mro has quit [Remote host closed the connection]
bartholin has quit [Quit: Leaving]
John_Ivan_ has quit [Ping timeout: 240 seconds]
John_Ivan_ has joined #ocaml
John_Ivan_ has quit [Client Quit]
waleee has joined #ocaml
olle has quit [Ping timeout: 240 seconds]
waleee has quit [Quit: WeeChat 3.8]
waleee has joined #ocaml
count3rmeasure has quit [Quit: Leaving]
nd__ has joined #ocaml
nd__ has quit [Ping timeout: 240 seconds]
neiluj has quit [Quit: WeeChat 3.7.1]
wingsorc has joined #ocaml
wingsorc has quit [Remote host closed the connection]
wingsorc has joined #ocaml
Stumpfenstiel has quit [Ping timeout: 240 seconds]