<dborisog>
In my mind, list_max t should be looking looking for [5; 2; 9; -1] and not for Some m; and max h:int m:int list returns an error in toplevel.
sarna has joined #ocaml
<malc_>
dborisog: what should it return if passed an empty list?
<dborisog>
it returns None
<dborisog>
because the first pattern matching (hidden by the function) has | [] -> None
<dborisog>
malc: I do not understand why this function works. Why [5; 2; 9; -1] is processed by "| Some m -> " of the second pattern matching, as I would expect "m" in "Some m" to be [5; 2; 9; -1], yet again "Some" in "Some m" seems out of place.
<malc_>
dborisog: this function == the incomplete thing in the url?
<malc_>
with ??? handling of the [] case?
<dborisog>
let rec list_max = function
<dborisog>
| [] -> None
<dborisog>
| h::t -> begin
<dborisog>
| None -> Some h
<dborisog>
match list_max t with
<dborisog>
| Some m -> Some (max h m)
<dborisog>
end
<malc_>
ah THAT is NOT the function in the url
<dborisog>
(sorry, should have given the code, it's the function on the bottom of the page -- I forgot about the one on the top)
<malc_>
oh sorry
<malc_>
well you see list_max is 'a list -> 'a option
<malc_>
cause returning None is the only safe bet when passed an empty list
<malc_>
(you can raise Not_found or somesuch, but that's just for kids who do not know any better)
<malc_>
and give me a moment to read the text on the page..
<dborisog>
thanks
<malc_>
so far it is saying what i just said... how stupid of me
<dborisog>
I understand part of the rational behind option data types. I do not understand the technical aspect why this function works
<malc_>
okay i've now read it
<malc_>
dborisog: what exactly forms a stumbling block for you?
<malc_>
dborisog: you can just do a mental acrobatics with a list of size 0;1;2 (as we all know programmers are simpletons who count: one two many)
<malc_>
just mentally write down what the arguments would be
<malc_>
it should make sense
<dborisog>
the function consumes list, and in the first pattern matching of the function "function | [] -> None | h::t -> " it processes list. Yet on the second pattern matching it jumps to option data type "| None -> Some h | Some m -> ". Currently, if I would apply the function to [1; 5; 2; 9; -1] I'm expecting [5; 2; 9; -1] to be processed instead of "Some m" by the second pattern matching.
<malc_>
on the first one it processes the argument (a list) on the second it processes the result an option
<malc_>
the signature of the fuction is 'a list -> 'a option so it all clicks
<dborisog>
malc: I'm missing some core piece of syntax and semantic of ocaml here, as I do not understand why it jumps to option data type on the second pattern matching.
<malc_>
| h::t -> begin
<malc_>
match list_max t with
<dborisog>
oh
<malc_>
so the "second" match is on the RESULT of the list_max
<malc_>
ie an 'a option
<dborisog>
right
<malc_>
makes sense? can i go now.. have to buy a drill...
<dborisog>
thanks you!
<malc_>
yeah! thank*s* me :) you are welcome, good luck
<dborisog>
)
malc_ has quit [Ping timeout: 264 seconds]
mbuf has quit [Ping timeout: 256 seconds]
narimiran has joined #ocaml
mbuf has joined #ocaml
mbuf has quit [Read error: Connection reset by peer]
mbuf has joined #ocaml
<dborisog>
So, if I understood the function correctly, list_max [1; 5; 2; 9; -1] is processed like Some (max 1 (max 5 (max 2 (max 9 (-1)))));;
osa1 has joined #ocaml
brown121407 has joined #ocaml
kvda has quit [Quit: My MacBook has gone to sleep. ZZZzzz…]
kvda has joined #ocaml
chripell has joined #ocaml
Haudegen has joined #ocaml
sarna has quit [Ping timeout: 256 seconds]
dckc has quit [Ping timeout: 272 seconds]
dckc has joined #ocaml
malc_ has joined #ocaml
vicfred has joined #ocaml
kvda has quit [Quit: My MacBook has gone to sleep. ZZZzzz…]
mbuf has quit [Ping timeout: 260 seconds]
vicfred has quit [Ping timeout: 272 seconds]
malc_ has quit [Remote host closed the connection]
vicfred has joined #ocaml
osa1 has quit [Ping timeout: 256 seconds]
ArthurStrong has quit [Ping timeout: 264 seconds]
ArthurStrong has joined #ocaml
olle has joined #ocaml
olle_ has joined #ocaml
malc_ has joined #ocaml
mbuf has joined #ocaml
osa1 has joined #ocaml
nullcone has quit [Quit: Connection closed for inactivity]
dborisog has quit [Ping timeout: 258 seconds]
Anarchos has joined #ocaml
Anarchos has quit [Quit: Vision[0.10.3]: i've been blurred!]
jbrown has joined #ocaml
webshinra has quit [Remote host closed the connection]
Haudegen has quit [Quit: Bin weg.]
sarna has joined #ocaml
kleisli_ has quit [Ping timeout: 240 seconds]
chripell has quit [Ping timeout: 256 seconds]
ArthurStrong has quit [Quit: leaving]
ggole has joined #ocaml
webshinra has joined #ocaml
mbuf has quit [Ping timeout: 244 seconds]
mbuf has joined #ocaml
chripell has joined #ocaml
Haudegen has joined #ocaml
sarna has quit [Quit: Connection closed]
malc_ has quit [Ping timeout: 256 seconds]
dckc has quit [Ping timeout: 256 seconds]
dckc has joined #ocaml
ArthurStrong has joined #ocaml
h14u has joined #ocaml
malc_ has joined #ocaml
waleee-cl has joined #ocaml
<olle_>
what a programming language where only immutable objects could be aliased?
<olle_>
what about a*
<olle_>
I wonder if that would work :d
<companion_cube>
rust? :p
<olle_>
companion_cube: rust has ownership semantics
<olle_>
my suggestion is simpler/dumber
<companion_cube>
you'd still need linear typing
<olle_>
yeah?
<olle_>
why?
<simpson>
Because you have to define mutability and aliasing in terms of logic which fundamentally knows about neither.
<olle_>
can't I just mark variables as "mutable" and then forbid lines like "let a = b" ?
<simpson>
This is why folks often say that linear logics are *substructural*; they expose structure underneath what logic can traditionally express.
<theblatte>
immutability and shareable or mutability but exclusive access is pretty much exactly rust
<vsiles>
olle_: if a is mutable, do you allow f(x, x) ?
<olle_>
vsiles: no
<vsiles>
so you'll end up having something ~like rust, I agree
<olle_>
no no no, in rust you can *transfer* ownership
<simpson>
olle_: Sure; there's a dialect of E that does this. In E or other capability-based languages, mutability is a feature of very specific box objects called "slots", and it's possible to forbid copying references to mutable slots. Note that this is just like removing or restricting mutability in any other language.
<simpson>
e.g. it's possible to remove (set!) from Schemes, too.
<olle_>
gotta google that
<companion_cube>
in rust you can also lend/borr
<companion_cube>
borrow
<companion_cube>
&Foo is exactly what you say: shared aliasing without mutability
<olle_>
yes, I'm talking about a system without borrow, not even possible to share a mutable object AS immutable
<companion_cube>
🤷
<olle_>
irssi can't show emojis, sorry ^^
<vsiles>
yes it can
<olle_>
oh
<olle_>
then my terminal sux
<simpson>
I don't have that one in my fonts either. Don't worry about it.
<vsiles>
iterm2 (macos :( ) here
<companion_cube>
it's :shrug:
<olle_>
ah
<theblatte>
borrow is there to allow you to write programs, without it the language is pretty limited (it's already quite limited with it /o\)
<olle_>
absolutely
<olle_>
just pondering the possibility
<companion_cube>
I'm not sure why you would want that, tbh
<olle_>
everyone is screaming about making everything immutable, "immutable objects are easier to reason about", bla bla bla. but maybe we should nag about forbidding aliasing instead? "languages without aliasing is easier to reason about" :)
<companion_cube>
still rust
<olle_>
companion_cube: I want that because I can't convince the mainainter of Psalm to accept ownership semantics xD
<olle_>
so, looking for alternatives that does not pollute the code-base as much as ownership
<companion_cube>
are you talking about php?
<olle_>
"languages without
<olle_>
aliasing is easier to reason about"
<companion_cube>
just stick to pragmatic type systems then
<olle_>
a medium.com blog post waiting to happen
<companion_cube>
I mean, what do you expect of linear typing in php?
<companion_cube>
the whole point of doing that in rust is so you press all the performance you can out of the cpu
<olle_>
no, that's too heavy, my idea was to ban certain expressions for tagged classes, like "$a = $b" or "$this->a = $b"
<olle_>
companion_cube: hm, the specific discussion was about query builders and how to separate the (immutable) DSL from the execution.
<olle_>
or if "$query->execute()" should be part of the builder.
<olle_>
it's also related to dependency injection, spooky-action-at-a-distance, etc.
<companion_cube>
maybe look into what nim does? idk
<companion_cube>
move semantics and such
<simpson>
olle_: I dunno how to tell you this, but immutability *is* simpler to reason about. Extra rules are required to add mutability to systems; mathematical reasoning starts from the immutable.
<olle_>
Will check out nim
<olle_>
simpson: One can make this argument, yes :)
<simpson>
companion_cube: Sure, I've seen that post. I'm not defending HOL or any other sort of computer-oriented prover, but the underlying principles which users of the system are expected to absorb.
<companion_cube>
well the post's conclusion resonates with me
<simpson>
Although honestly I should stop having opinions, because they just seem to lead to arguments.
<companion_cube>
you typically have to weight FP vs imperative when it comes to formal reasoning
<companion_cube>
and FP is not necessarily simpler (cause of the higher order)
<olle_>
companion_cube: hey, that's exactly what I was talking about :)
<olle_>
well, not exactly
<olle_>
good link
<simpson>
companion_cube: Oh. Yeah, opinion incoming: I'm not on the FP side of things. I'm suggesting that *all* formal provers suffer from a mismatch between what is expressible in their proof languages vs. what we imagine when we are in the process of cognitively understanding the proof.
<simpson>
E's auditor subsystem exposes E ASTs directly to provers, and E is plenty imperative. I don't particularly like it, though. I don't really like *any* formal provers; they're all small-minded in their own ways.
nullcone has joined #ocaml
malc_ has left #ocaml ["ERC (IRC client for Emacs 28.0.50)"]
<companion_cube>
or maybe it's that they're hard to create
<companion_cube>
but anyway, I was answering to the idea that mathematical reasoning starts at the immutable
<companion_cube>
and I don't think it's true
<simpson>
Meh. I don't like it either. But that's how it is. Transformations and symmetries need some sort of notion of identity and sameness, and we normally build mutable sameness out of immutable sameness and various temporal/modal claims.
<companion_cube>
sure, but when you reason about imperative stuff you use Hoare logic, which is also a series of transitions
<companion_cube>
(or TLA, etc.)
<simpson>
And plenty of languages with mutability front-and-center have made concessions to this. Java and Python have had hilariously bureaucratic efforts to understand value objects, for example.
<companion_cube>
that's not harder than induction over recursive functions
<simpson>
Note that things are assumed constant and unchanging here: That `2` points to the same number, that `foo` points to the same procedure.
<companion_cube>
sure, but imperative isn't worse at that than FP
<simpson>
False dichotomy, though. There's three, actually! Metamath shows off the fully-syntactic approach. No types like in HOL, but also no Hoare logic or invariants.
<simpson>
And there may be even more. Perhaps there's even one that doesn't inherently drive humans insane~
<companion_cube>
I don't see the connection
<companion_cube>
hoare logic can be simulated in all these things
<companion_cube>
type theory, HOL, metamath, you name it
<simpson>
Things being simulated in other things isn't important. What's important is that people need to understand the proof in order to be able to derive algorithms from it. That understanding is typically not much connected to the formal proof, other than that the formal proof is one of those derived algorithms.
<simpson>
If we want to do better on this front, then we need proof systems that not just prove like people, but *under the hood* are proving like people. And that's not what any of the existing proof systems give anybody.
<simpson>
And one of the things that people have, when doing proofs, is a concept of sameness; they have a concept for when various references on a page are pointing to the same object.
<companion_cube>
you mean, equality?
<companion_cube>
or like equality up to isomorphism?
<simpson>
Like, metatheoretic equality of referent symbols. The equality *outside* of whatever says `f : X -> Y` and `g : Y -> Z` can be composed to build `f;g : X -> Z`.
<simpson>
We know how it's defined, for each different proof settting. My point is that it even needs definition.
<simpson>
I dunno. This isn't relevant to anything. Never mind.
simpson has left #ocaml ["WeeChat 1.0.1"]
narimiran has quit [Ping timeout: 265 seconds]
<olle_>
i'm glad i'm not alone in ranting :)
<companion_cube>
we're all good at ranting here
<olle_>
this week i managed to get banned from both ##php and ##java when trying to discuss ownership and aliasing :|
<olle_>
;)
<companion_cube>
well it turns out it's overkill when you have a GC? :p
<olle_>
companion_cube: so why do they all promote immutability?
<olle_>
and alias control is needed for typestate, which is my holy graal, so...
osa1 has quit [Ping timeout: 264 seconds]
<companion_cube>
does java promote immutability?!
<olle_>
companion_cube: everyone that can spell "agile" does
<olle_>
"always define your classes final"
<olle_>
as it said in your link
<olle_>
"Immutable objects are simply objects whose state (the object's data) cannot change after construction"
<olle_>
etc
<olle_>
wait
<olle_>
ignore
Haudegen has quit [Quit: Bin weg.]
<olle_>
(not java as a language, but the programming community in large, I think)
olle_ has quit [Ping timeout: 272 seconds]
olle has quit [Ping timeout: 256 seconds]
raver has quit [Ping timeout: 256 seconds]
artymort has quit [Read error: Connection reset by peer]
artymort has joined #ocaml
osa1 has joined #ocaml
tane has joined #ocaml
Haudegen has joined #ocaml
chripell has quit [Ping timeout: 264 seconds]
osa1 has quit [Quit: osa1]
muskan has joined #ocaml
mbuf has quit [Quit: Leaving]
ggole has quit [Quit: Leaving]
muskan has quit [Ping timeout: 245 seconds]
muskan has joined #ocaml
superherointj has joined #ocaml
<superherointj>
Hello. What is the usual/popular/mainstream/used name for the function that takes an Option List and makes it a value list?
<octachron>
filter_map (fun x -> x) ?
<superherointj>
Any other suggestion for the specific 'option list' to 'value list' case?
<theblatte>
Base.List has "filter_opt : 'a option list -> 'a list"
<flux1>
I wonder, is the time right for an identity function to stdlib?-)
<flux1>
I guess `(fun x -> x)` is always shorter, though perhaps not as pretty
<companion_cube>
containers has `keep_some` for that
<superherointj>
Hello flux1
<superherointj>
Thanks for all the ideas!
<octachron>
flux1, we do have Fun.id in the stdlib
<flux1>
we have Fun in stdlib?! wow, we truly live the future :)
<flux1>
id and flip must be the functions I've written most of the times from scratch in OCaml
<ollehar>
"Marron believes we can do better by getting rid of sources of complexity like loops, mutable state, and reference equality. The result is Bosque, which represents a programming paradigm that Marron, in a paper he wrote, calls "regularized programming." "
<ollehar>
hm, no, maybe just same research department or something
<superherointj>
What I was looking after was really `List.filter_map`. I've recreated this function and was trying to find a good name for it. One day I hope I'll stop doing this. :)
<waleee-cl>
ollehar: microsoft research does a bunch of experimental languages and stuff, eg project verona, F*, &c
<ollehar>
they do, yes
<waleee-cl>
oh, and apparently F# was a ms research language in the beginning
<ollehar>
it's like they threw everything at the wall and checked what stuck :)
<ollehar>
can't really see an over-arching design goal
<ksft>
how ca I work with large lists without stack overflows?
<ksft>
can*
<ksft>
I have a list of length ~300000, and calling `List.rev` or `List.mapi` on it causes the program to crash
<companion_cube>
List.rev should definitely not crah
<companion_cube>
crash
<ollehar>
crash how?
<ollehar>
oh, stack overflow
<ksft>
oh, huh, I'm susre I tested that, but now it seems it isn't
<ksft>
sure*
<ollehar>
maybe use arrays instead?
<companion_cube>
mapi can stack overflow though
h14u has quit [Remote host closed the connection]
h14u has joined #ocaml
<ksft>
Array.mapi seems to work
<ksft>
I'm trying to filter and then map the data
<ksft>
but List.map crashes, and Array.filter doesn't exist
<thizanne>
why do you have a list in the first place?
<thizanne>
maybe sequences would be better suited
<ksft>
converting back and forth works, but the code is really hard to read
<octachron>
If you have more than 30_000 you want to keep an array all the time.
<ksft>
oh, I didn't know about sequences
<ksft>
octachron: is Array.filter just named something else, then?
<octachron>
Just implement it yourself?
<ksft>
it seems a little weird that that isn't built in
muskan88 has joined #ocaml
<octachron>
Not really? Array is not the really the right structure for filter, the stdlib try to not implement unnatural function
<ksft>
but you think it's the one I should be using?
narimiran has joined #ocaml
<octachron>
No, I am telling that using List is a probably really bad option
muskan has quit [Ping timeout: 245 seconds]
<octachron>
And going back and forth between lists and arrays, even more so. Going through Seq is probably better.
<octachron>
On the other hand, if you are doing a lot of work for each element of the lists, maybe just writing the tail-rec version of map is better?
superherointj has quit [Quit: Leaving]
<ollehar>
hm, not sure if OCaml learning material should be more clear about list use-cases
<ollehar>
with regard to size, I mean
<octachron>
The manual states that if you have more than 10_000 elements, you should be careful with non tail-rec functions
Hrundi_V_Bakshi has joined #ocaml
<ksft>
I assumed the standard library functions would be tail recursive where possible
<octachron>
The tailrec functions are slower on smaller lists, and lists are often not the right structure for large dataset (they are not space efficient, lead to a lot of pointer chasing, etc...)
<companion_cube>
yeah well you can mix the approaches
<octachron>
Indeed, and I would personnally prefer that we use the mixed approach for stdlib.
<companion_cube>
yeah, me too
<companion_cube>
octachron: hey you control releases now right? :D
<companion_cube>
so you could cross your arms and demand the stdlib be fixed before you do anything :-°
<octachron>
The concept of stdlib strike sounds interesting if vaguely inefficient.
<octachron>
But it seems that gasche is finally nearing the end of its TRMC re-implementation
<companion_cube>
oh really? cool
<companion_cube>
octachron: if it was just up to me I'd merge half of containers into the stdlib and call it a day
<octachron>
So we may get a good enough implementation by letting the compiler generate the code that people didn't want to see.
<companion_cube>
sadly each small change needs to be bikeshed for months :s
<ollehar>
just vote?
<companion_cube>
just vote for what?
<octachron>
Speaking of merging containers, I would be in favor in of merging at least oseq into the Seq module.
<companion_cube>
ah well
<companion_cube>
go for it :p (although it probably contains too much stuff)
<d_bot>
<mseri> ksft the documentation is explicit on tail-recursion though. For lists you need to use rev_map instead of map or fold_left (if I remember correctly)
<ollehar>
(vote instead of bikeshedding)
muskan88 has quit [Ping timeout: 245 seconds]
<ksft>
oh, so it is
<ksft>
no rev_mapi, though, it seems
brown121407 has quit [Remote host closed the connection]
tane has quit [Quit: Leaving]
narimiran has quit [Ping timeout: 256 seconds]
rfv has quit [Ping timeout: 246 seconds]
higherorder has quit [Ping timeout: 240 seconds]
rgrinberg has quit [Ping timeout: 246 seconds]
bitonic has quit [Ping timeout: 240 seconds]
rfv has joined #ocaml
higherorder has joined #ocaml
<ollehar>
is there a use-case where you absolutely need both mutability and aliasing?
<ollehar>
double-linked list?
<ollehar>
or maybe a graph datastructure
jeroud has quit [Ping timeout: 260 seconds]
eterps has quit [Ping timeout: 260 seconds]
wildsebastian has quit [Ping timeout: 244 seconds]
chewbranca has quit [Ping timeout: 240 seconds]
bytesighs has quit [Ping timeout: 240 seconds]
angerman has quit [Ping timeout: 244 seconds]
metadave has quit [Ping timeout: 256 seconds]
higherorder has quit [Ping timeout: 244 seconds]
rfv has quit [Ping timeout: 244 seconds]
lopex has quit [Ping timeout: 272 seconds]
j14159_ has quit [Ping timeout: 272 seconds]
ipavlo has quit [Ping timeout: 272 seconds]
adi_________ has quit [Ping timeout: 246 seconds]
JSharp has quit [Ping timeout: 260 seconds]
mrallen1 has quit [Ping timeout: 260 seconds]
Duns_Scrotus has quit [Ping timeout: 260 seconds]
robmyers has quit [Ping timeout: 272 seconds]
<companion_cube>
a concurrent table/queue
terrorjack has quit [Ping timeout: 246 seconds]
cbarrett has quit [Ping timeout: 244 seconds]
l1x has quit [Ping timeout: 244 seconds]
strmpnk has quit [Ping timeout: 260 seconds]
jmct has quit [Ping timeout: 258 seconds]
SrPx has quit [Ping timeout: 244 seconds]
mgsk has quit [Ping timeout: 244 seconds]
sspi__ has quit [Ping timeout: 272 seconds]
banjiewen has quit [Ping timeout: 272 seconds]
waleee-cl has quit [Ping timeout: 260 seconds]
cemerick has quit [Ping timeout: 260 seconds]
sz0 has quit [Ping timeout: 244 seconds]
nullcone has quit [Ping timeout: 256 seconds]
<Armael>
a double-linked list yes
mjvoge02 has quit [Ping timeout: 246 seconds]
cqc has quit [Ping timeout: 246 seconds]
ec has quit [Ping timeout: 260 seconds]
stephe has quit [Ping timeout: 240 seconds]
conjunctive has quit [Ping timeout: 244 seconds]
stylewarning has quit [Ping timeout: 244 seconds]
adrianbrink has quit [Ping timeout: 272 seconds]
rdivyanshu__ has quit [Ping timeout: 272 seconds]
caasih has quit [Ping timeout: 272 seconds]
Boarders has quit [Ping timeout: 272 seconds]
Hrundi_V_Bakshi has quit [Ping timeout: 258 seconds]
Haudegen has quit [Ping timeout: 256 seconds]
oriba has joined #ocaml
oriba has quit [Client Quit]
<ollehar>
well shit
<ollehar>
or, maybe external alias free is "enough"