<companion_cube>
🎿 it's basically like linear types
<companion_cube>
ski :*
<companion_cube>
borrowing is like giving and receiving back at the end, only more convenient and efficient
olle has quit [Ping timeout: 264 seconds]
olle has joined #ocaml
theblatte has quit [Ping timeout: 250 seconds]
perrierjouet has joined #ocaml
theblatte has joined #ocaml
<dh`>
the search keyword is "affine types"
<wpcarro>
is String.get the idiomatic way to index into a string in ocaml?
<companion_cube>
either that, or `s.[i]`
<wpcarro>
oh the second one is what I was hoping for :)
<wpcarro>
ty companion_cube
waleee has quit [Ping timeout: 268 seconds]
<wpcarro>
does Queue.add actually add elements to a queue...? Just looking for a data structure with a similar API to a dynamic array
<wpcarro>
maybe "vector" is a better word
<wpcarro>
strange Queue.push works but not Queue.add but docs say it's synonym?
<companion_cube>
there is no dynamic array (yet)
<wpcarro>
companion_cube ack
<wpcarro>
I haven't started install 3rd party packages with opam yet
<companion_cube>
some people find it not useless, pff
<wpcarro>
still just trying to use the stdlib
<wpcarro>
last question for today (i think) - is there anything like pythons `in` operator that tests set membership of some 'a over a polymorphic collection type?
<wpcarro>
e.g. `if "t" in "testing"` or `if 1 in [1, 2, 3, 4]`, etc
theblatte has quit [Ping timeout: 268 seconds]
<companion_cube>
no, there is not
<wpcarro>
ty :)
chrisz has quit [Ping timeout: 250 seconds]
chrisz has joined #ocaml
<ski>
companion_cube : well, point was that it's not, it's perhaps in some regards more like the opposite
<companion_cube>
what's even the opposite of linear?
<ski>
(and ditto for affine types)
<companion_cube>
polynomial? :D
spip has quit [Ping timeout: 246 seconds]
bobo_ has joined #ocaml
<ski>
well, here the opposite, in the vague handwavy sense of time (past vs. future) that i sketched above
<companion_cube>
sounds like it's both
<companion_cube>
rust definitely has linear semantics around non-Copy types
<companion_cube>
(which plays well with its move semantics)
<companion_cube>
I suppose uniqueness describes rust references
<ski>
(but yea .. in a more math sense, one could say affine is sortof the opposite of "relevant" (by which i mean a polynomial which has zero as a root, iow has constant coefficient). for the latter, you have no "weakening", for the former, you have no "contraction")
<ski>
what do you mean by "linear semantics" ?
<companion_cube>
well, non-Copy types (that is, most types) cannot be duplicated
<ski>
(if it's not related to Girard's linear logic, then that's not what i'm talking about)
<ski>
hm, can it express internal choice ?
<companion_cube>
wdym
<companion_cube>
(also, you have functions that take their argument by move, consuming it; or return it by move)
<ski>
where you are offered two (or more) resources, and you've got to pick exactly one (or at most one, if you're doing affine) of them, no more
<ski>
(this is called "with", or "additive conjunction", in linear logic)
<companion_cube>
I'm not sure how the offering mechanism would work
<companion_cube>
beyond things like concurrent channels, that is
<ski>
well, think of a `struct'/record, with fields, except the fields are exclusive. once you've picked one to use, you can't select another one
<companion_cube>
there's sum types?
<ski>
no, not talking about sum types
<companion_cube>
but no, for records, if you consume one field, you consume the whole record (it's kind of rough)
<companion_cube>
(in practice you can also swap with a value you already have, but well)
<ski>
(which would be "additive *dis*junction", "either .. or ..", "*ex*ternal choice" (someone else makes the choice of which alternative you get to see))
<companion_cube>
well, rust is a programming language used in practice, it doesn't really need not-your-choice-non-determinism of this form :p
<ski>
"how the offering mechanism would work" -- the type system would simply prevent you from using more (and possibly also less) than one field of it
<companion_cube>
ah this kind of choice, my bad
<ski>
(and then the implementation could possibly do optimization tricks, based on this knowledge)
<companion_cube>
I suppose you could emulate what you say with a custom type `Choice<T,U>`, containing a T and a U, and two self-consuming methods that just erase the other un-picked element
<ski>
(e.g. if the choices aren't materialized at first, and will take up more space when materialized, you could possibly arrange to have the extra space where they'll be materialized be overlapping, since only one of them will be actualized out of potential anyway)
<ski>
"not-your-choice-non-determinism" -- well, one man's free choice is another man's imposed choice
<ski>
these things are dual, seen from opposite sides of abstraction interfaces (caller/user/destructer/consumer vs. callee/definer/constructer/producer)
<companion_cube>
you could possibly store closures :)
<companion_cube>
`Choice(|| compute_val_1, || compute_val_2)` with methods that evaluate the right closure…
<companion_cube>
however these closure can't capture the same thing, so I doubt it works like you want
<companion_cube>
so I guess it might have a linear arrow (more or less), but not the rest
<ski>
anyway, i'll have to look more into the non-Copy types (istr Ada had a feature with non-duplicable records or object ..), to see how they do it, and how it behaves. ty for the suggestion
<companion_cube>
(Copy is not the default, btw. It's only a thing to make some types implicitly copyable because otherwise life is too painful; e.g. all integer and floating point types)
<ski>
"these closure can't capture the same thing" -- yes, that's another essential part of "internal choice" (at least in the potential version). since only one will be actualized, you're free to use the same resources for both (would be expected to, in the linear rather than affine case)
<companion_cube>
(otherwise you have to opt-in into it, for small structs/sum types)
<companion_cube>
yeah, I think this part wouldn't work.
<zebrag>
ski: so it was all along about mezzo language
<ski>
yea, the category of linear types has a subcategory of duplicable (and discardable) types
<companion_cube>
right, exactly
<companion_cube>
in rust, Copy types can't also implement Drop (which is the trait for things with a destructor)
<companion_cube>
(meaning that they live and die at relatively predictable places, unlike an integer)
<ski>
mhm
<ski>
zebrag : some intermediate code format from the Mezzo compiler ?
<ski>
"for records, if you consume one field, you consume the whole record" -- standard Rust behaviour ?
<companion_cube>
yep
<companion_cube>
there is no way to have a partial record
<companion_cube>
(as I said, you can also swap a field with a value you hold, without breaking the record)
terrorjack has joined #ocaml
<ski>
hm, "partial record" meaning ?
<ski>
oh, i suppose you mean if you use up a value
<ski>
.. i really think something like Mercury's "inst" (instantiation state) system would fit quite nicely in a systems level language, like e.g. Rust
<ski>
Mercury can statically express which parts of a structure are instantiated (initialized), and which are not, and disallows you from reading that part if the part in question's not instantiated
<ski>
you could e.g. have one procedure initialize one part of a structure, and another one initialize another part
williewillus` has joined #ocaml
williewillus` has quit [Changing host]
williewillus` has joined #ocaml
williewillus` is now known as williewillus
<companion_cube>
right
<companion_cube>
I suppose the type system was complicated enough already :D
<ski>
(and you can also move instantiation state on from `free' (uninstantiated) to `bound', further to `dead' (if it pointed somewhere, that may have been deallocated not). there's also backtracking, where you can undo instantiation, going back from `bound' to `free', to instantiate again (to something else e.g.) .. and there's `mostly_dead', which can also be backtracked back to `bound' (you may be able to
<ski>
recompute the dead part, depending))
<ski>
(s/deallocated not/deallocated now/)
<ski>
in Mercury, insts (and modes, which are inst transitions (across calls/goals), and also dets (determinisms) which track how many solutions a call/goal could possibly have (minimum zero or one, maximum zero or one or infinity), which is related to backtracking) are not part of the type system, but a separate part. it's still static checking, though (just like checking variables are in scope is)
<ski>
(`bound' is a generic inst, that just says something is instantiated. one can have specific insts that say something is instantiated to a particular form. e.g. a list is non-empty (or even has an even (or odd) number of elements .. prime or triangular or square would be hard to do, though ..). perhaps one could also be able to do things like specifying a red-black tree actually is upholding the red-black
<ski>
invariant .. i think that can't be done with current system, but maybe one could add such capability. AVL would require GADTs, i think. anyway, easy to e.g. disallow a particular kind of node(s) from a tree, which would be useful after a compiler pass e.g.)
<ski>
(and then there's `unique', which is like `bound', except saying you have a unique reference. also can be more specific to particular shapes, like `bound' can)
theblatte has joined #ocaml
zebrag has quit [Quit: Konversation terminated!]
mbuf has joined #ocaml
bgs has joined #ocaml
Haudegen has joined #ocaml
adanwan has quit [Remote host closed the connection]
adanwan has joined #ocaml
jao has quit [Ping timeout: 268 seconds]
Serpent7776 has joined #ocaml
rwmjones_ has joined #ocaml
rwmjones has quit [Ping timeout: 252 seconds]
azimut has joined #ocaml
williewillus has quit [Quit: ERC 5.4 (IRC client for GNU Emacs 28.2)]
<olle>
Rust programs have a static semantics that determine the types of values produced by each expression, as well as the predicates that hold over slots in the environment at each point in time during execution.
<wpcarro>
when i run `dune build hello_world.exe` dune complains that it doesn't know how to build hello_world.exe
<wpcarro>
i'm just trying to learn enough dune to install third party libraries (e.g. yojson, core)
olle has quit [Ping timeout: 252 seconds]
phao has quit [Quit: Leaving]
<wpcarro>
build systems in new langs are always the death of me
gentauro has quit [Read error: Connection reset by peer]
gentauro has joined #ocaml
<qwr>
tbh, imho the build systems are overrated - small programs can often easily built by invoking compiler directly and on linux install everything needed with package manager
<qwr>
or in case of ocaml, i'm currently writing utility using only standard library and only interpreting it with ocaml foo.ml...