00:00:20 -!- danieljabailey has joined.
00:06:50 -!- ais523 has joined.
00:07:58 <ais523> any progress on the fixed point of Codensity?
00:08:13 <shachaf> I was going to ask you the same thing.
00:08:23 <shachaf> No, I didn't think about that type much since last time.
00:09:09 <shachaf> I think not satisfying the monad associativity law might not be so bad.
00:09:16 <shachaf> You just don't call your thing a monad.
00:11:01 <shachaf> The alternative is to explicitly make your code into a tree with "bracket $ do { ... }" calls. I think bracket is quite similar to reset from delimited continuations.
00:13:00 <shachaf> By the way, I said earlier that C mutable types were similar to e.g. refs in SML, but there's an important difference: If you have a ref containing a pair, you can't in general get a ref to each of its components.
00:13:11 <shachaf> Is there a language with explicit refs that does allow that?
00:14:14 <ais523> shachaf: the "how do you contrast elements of the pair with the pair itself" question is really, really complex
00:14:30 <ais523> and conflating them is one of the most common mistakes made in theoretical computer science
00:14:36 <ais523> I had to write quite a bit in my thesis about it
00:14:52 <shachaf> The situation in C is more complicated than I would've thought.
00:14:56 <ais523> unfortunately, this /specific/ question isn't one of the ones I have a ready-made answer to, and I don't want to throw out an answer quickly because experience shows that any simple answer here will probably be wrong
00:15:10 <shachaf> C has two "." operators for field access, one for lvalues and one for rvalues.
00:16:14 <shachaf> If read : LValue a -> RValue a, then read(lval.x) = read(lval).x, so it's easy to confuse them.
00:16:49 <ais523> the basic issue wrt pairs can be seen by trying to access both halves of the pair; is that a) a single operation that decomposes a pair into its two halves, or b) two operations, each of which reads one half of a pair?
00:17:21 <shachaf> I wish I knew a good language that doesn't have lvalues.
00:17:27 <ais523> if you're counting how many accesses are made to something (in my thesis, this came up wrt affine typing, but `volatile` is a more familiar example), the distinction is really important
00:17:35 <ais523> shachaf: but does have mutable variables?
00:17:46 <zzo38> Do you know BLISS?
00:17:48 <shachaf> No, just pointers/references.
00:17:59 <shachaf> zzo38: BLISS and ALGOL 68 are the two answers I know to this question.
00:18:21 <ais523> shachaf: well, a reference to an immutable value is normally very hard to distinguish from the value itself
00:18:56 <shachaf> "volatile" seems like a weird thing to have as a property of a variable.
00:18:58 <ais523> the only difference is that if the value is deallocated, the reference becomes invalid, but deallocation is effectively a form of mutation
00:19:09 <shachaf> It seems much more like it should be a property of the read/write operation on the variable.
00:19:27 <ais523> shachaf: well, from a mathematical point of view, it's simplest to initially treat everything as volatile and then potentially allow for optimisations that change the number of reads on something
00:19:48 <ais523> I can see an argument to have a volatile version of lvalue and of rvalue dereferencing, though
00:20:02 <ais523> hmm… half the complexity of lvalues would be simplified if they /couldn't/ be read
00:20:12 <ais523> that'd be a pretty weird language, though
00:20:17 <shachaf> read, read_volatile : Ptr a -> a
00:20:37 <ais523> int X {get; set}; setX(4); setX(getX()+1);
00:21:27 <ais523> I don't see any particular reason why this style of programming wouldn't work, and it's a lot clearer than many others (and it's more or less how object-oriented program treats exposed variables, although probably for a different reason)
00:21:55 <ais523> now pass-by-reference is accomplished via passing the setX or getX /function/ by value
00:21:56 <shachaf> I think maybe C++ was making a change like that?
00:22:09 <ais523> that's most likely for class fields
00:22:13 <ais523> I don't think anyone treats /local/ variables like this
00:22:20 <ais523> (I stole the syntax from C#)
00:22:45 <shachaf> Oh, no, it's Rust: https://doc.rust-lang.org/std/ptr/fn.read_volatile.html
00:23:15 <shachaf> I was talking about the thing I said. I'm not sure what you mean by passing the function by value.
00:23:34 <ais523> I was going to ask "why is that unsafe" and then saw it works on `*` pointers, which would be a good reason
00:24:11 <ais523> re: passing the function by value, I mean you could pass the return value of getX() (i.e. pass by value), or you could pass the getX function itself so that the callee could then call it itself (i.e. pass by reference)
00:24:31 <ais523> like the difference between passing x and passing (int const *)&x in C
00:24:32 <shachaf> Where getX is a closure or something?
00:24:41 <ais523> getX is something like a closure, I think
00:24:54 <ais523> but the point is that the variable X can't be directly referenced at all
00:25:11 <ais523> all you have is its lvalue part setX and rvalue part getX, which correspond to the operations of assigning to it and reading it
00:26:02 <shachaf> It's nice to separate it into the covariant part and contravariant part, I guess.
00:27:36 <ais523> anyway, most languages treat variables like products of their lvalue and rvalue; a product's a type of pair where the pair itself acts as a unit, any operation on the pair can say "do this on the LHS" or "do this on the RHS" but the two parts aren't separable (unless you copy out of half of the pair individually)
00:28:16 <ais523> whereas this version of things treats variables like tensors of their lvalue and rvalue; a tensor's a type of pair which is basically just a wrapper for two halves, with the wrapper having no properties of its own, rather each half has its own independent behaviour
00:29:02 <ais523> typically speaking you have to copy a product to act on both halves of it (e.g. in a stack-based language, you'd do dup, then get hold of one half, operate on it, then get hold of the other half using the copy of the pair you made earlier)
00:29:28 <ais523> whereas with a tensor, the operation you use to act on the tensor drops it into two halves of its own accord, so if you only act on one you need to explicitly pop the other one
00:29:56 <ais523> shachaf: this is a really confusing subject in general and I'm not all that great at understanding it
00:30:34 <ais523> it almost feels like the tensor/product distinction is the same sort of thing as monads, i.e. people use it all the time when writing in more mathematical languages but often only poorly understand it, except that it isn't well-known that it even is a problem
00:31:03 <shachaf> ski wrote about this a little while ago at http://slbkbs.org/ski-mercury.txt
00:31:07 <ais523> but it basically comes down to what happens when a language has some sort of metadata you can attach to a value (which is very common)
00:32:16 <shachaf> I'd like a language that makes all this very clear, most languages muddle it up or don't support talking about it at all.
00:32:40 <ais523> re: lvalue versus rvalue, OCaml is 100% explicit on the matter
00:33:19 <ais523> using := as lvalue dereference (producing a setter) and ! as rvalue dereference (which should produce a getter, although it actually executes the getter immediately; that's something of a mathematical flaw, I guess)
00:33:21 <shachaf> But can you get a ref to a part of a product inside another ref?
00:33:47 <ais523> no, you can't; that's because OCaml products are products
00:34:05 <ais523> or rather, there's a distinction
00:34:08 <ais523> do we have OCaml in hackego?
00:34:31 <ais523> anyway, in OCaml you can't get a ref to anything unless it was declared via the ref keyword
00:34:45 <ais523> so ref (1, 1) has a different type from (ref 1, ref 1)
00:35:07 <shachaf> This is what most of the explicit-about-refs languages do.
00:35:26 <shachaf> I'm interested in languages that help you talk about memory layout and so on.
00:35:40 <shachaf> When you declare a struct or union in C, what information exactly are you declaring?
00:36:02 <shachaf> I've asked that question before but I'm still not sure I have an answer.
00:36:05 <ais523> well, in the very early days of C, declaring a struct just gave you a list of constants representing memory offsets
00:36:20 <shachaf> In lvalue-land, you're declaring things like: A sizeof, an alignment, an offset for each field.
00:36:24 <ais523> like, if you wrote struct a {int b; int c}, that was more or less equivalent to "const int b = 0; const int c = 4;"
00:36:52 <ais523> (with the exception that struct a would be reported as having size 8 for the rest of the program, affecting things like sizeof, allocation of auto variables, and the like)
00:36:55 <shachaf> In rvalue-land, you're declaring something like, "this is the information that this struct consists of"
00:37:15 <shachaf> The thing in lvalue-land is effectively a memory encoding of the thing in rvalue-land.
00:37:22 <ais523> it feels like it's within the spirit of C for struct fields to not be rvalues at all
00:37:34 <shachaf> When you pass something by value to a function, the calling convention doesn't use the lvalue-land memory layout, it uses something more efficient.
00:37:37 <ais523> that said, I think they actually are in practice
00:38:18 -!- arseniiv has quit (Ping timeout: 252 seconds).
00:38:29 <ais523> functions returning structs is something of a weird case in C; it doesn't feel like it "should" be possible, and in fact many compilers need special cases for it
00:38:45 <shachaf> It seems pretty reasonable to me.
00:39:10 <ais523> `` gcc -x c /dev/stdin <<< 'int main(void) {puts("Hello, world!"); return 0;}'; ./a.out
00:39:13 <HackEso> [01m[K/dev/stdin:[m[K In function ‘[01m[Kmain[m[K’: \ [01m[K/dev/stdin:1:17:[m[K [01;35m[Kwarning: [m[Kimplicit declaration of function ‘[01m[Kputs[m[K’ [[01;35m[K-Wimplicit-function-declaration[m[K] \ int main(void) {[01;35m[Kputs[m[K("Hello, world!"); return 0;} \ [01;35m[K^~~~[m[K \ Hello, world!
00:39:34 <ais523> `` gcc -x c /dev/stdin <<< 'int main(void) {puts("Hello, world!"); return 0;}' | cat; ./a.out
00:39:35 <HackEso> [01m[K/dev/stdin:[m[K In function ‘[01m[Kmain[m[K’: \ [01m[K/dev/stdin:1:17:[m[K [01;35m[Kwarning: [m[Kimplicit declaration of function ‘[01m[Kputs[m[K’ [[01;35m[K-Wimplicit-function-declaration[m[K] \ int main(void) {[01;35m[Kputs[m[K("Hello, world!"); return 0;} \ [01;35m[K^~~~[m[K \ Hello, world!
00:39:45 <ais523> hmm, what's up with all the terminal control codes
00:39:50 <shachaf> The reason I gave f().c as an example is that it shows that a.b doesn't always mean a thing like *(&a + b_offset).
00:40:09 <ais523> `` gcc -fdiagnostics-color=never -x c /dev/stdin <<< 'int main(void) {puts("Hello, world!"); return 0;}'; ./a.out
00:40:10 <HackEso> /dev/stdin: In function ‘main’: \ /dev/stdin:1:17: warning: implicit declaration of function ‘puts’ [-Wimplicit-function-declaration] \ int main(void) {puts("Hello, world!"); return 0;} \ ^~~~ \ Hello, world!
00:40:38 <ais523> `` gcc -fnodiagnostics-show-caret -fdiagnostics-color=never -x c /dev/stdin <<< 'int main(void) {puts("Hello, world!"); return 0;}'; ./a.out
00:40:38 <HackEso> gcc: error: unrecognized command line option ‘-fnodiagnostics-show-caret’; did you mean ‘-fno-diagnostics-show-caret’? \ Hello, world!
00:40:43 <ais523> `` gcc -fno-diagnostics-show-caret -fdiagnostics-color=never -x c /dev/stdin <<< 'int main(void) {puts("Hello, world!"); return 0;}'; ./a.out
00:40:44 <HackEso> /dev/stdin: In function ‘main’: \ /dev/stdin:1:17: warning: implicit declaration of function ‘puts’ [-Wimplicit-function-declaration] \ Hello, world!
00:41:09 <shachaf> `runc int main() { puts("hi"); return 0; }
00:41:17 <ais523> shachaf: I agree that C currently works like this; however, I believe that all the cases that force structs to be treated as rvalues are weird special cases that /shouldn't/ have been in C
00:41:25 <zzo38> There is also LLVM, but does not have macros though
00:41:43 <shachaf> ais523: Do you also think struct assignments shouldn't be allowed?
00:42:04 <shachaf> Hm. They seem pretty reasonable to me.
00:42:20 <ais523> actually, there's a related question which is something that I've been really interested in over the past few months in general, and past few days more earnestly
00:42:21 <shachaf> What about passing structs as arguments by value?
00:42:42 <ais523> which is that languages seem to often use the same sort of language feature for a) large, complex values, and b) stateful objects
00:42:51 <ais523> I think they should be treated entirely differently
00:43:02 <ais523> things in class a) shouldn't be mutable, things in class b) shouldn't be passable by value
00:43:34 <ais523> quite a few languages are skirting round the edges of this idea but I don't think any has gone the whole way
00:45:39 <shachaf> How would languages be different if they made that distinction?
00:49:58 <zzo38> I did think of a way to make "user primitives" for JavaScript that can implement (a)
00:51:31 <ais523> shachaf: well for example, you'd never need a value/reference distinction
00:52:00 <ais523> if something is a value, it's always a value; if something's an object, it isn't a value at all, it can only be manipulated via references to it (and those references are values)
00:52:17 <ais523> so the code itself sees only values
00:52:24 <ais523> (objects are manipulated via methods/accessor functions)
00:52:50 <ais523> more controversially, I /also/ think it would be beneficial if objects just persisted forever if they weren't explicitly deallocated, /but/ you could search for objects with particular properties
00:53:15 <ais523> my only argument in favour of this is that for something like the last 10 programs I've tried to seriously write, they'd be more easily written in that style than in a style that tries to maintain indexes manually
00:54:57 <zzo38> Garbage collection works for unsearchable objects
00:55:35 <ais523> shachaf: like, there's a function that returns a reference to "the object whose x property is y"
00:56:24 <ais523> zzo38: I know that garbage collection works, however I think that garbage collection of reference-like objects is normally a bad idea, because if a programmer knows what they're doing they typically know the points at which they're supposed to become no longer useful anyway
00:57:06 <zzo38> I am not so sure that is true
00:57:14 <ais523> it's only objects that act like values that really benefit from garbage collection; this is because reference+garabage collect is a more efficient way of implementing the semantics you normally want (which is to replace referencing by copying, and freeing copies that go out of scope)
01:45:11 <esowiki> [[WHY]] M https://esolangs.org/w/index.php?diff=58340&oldid=58103 * Camto * (+54) Add them categories.
02:35:18 -!- oerjan has joined.
02:43:31 <zzo38> What does that mean?
02:48:11 <shachaf> hm, it's slightly irritating that "morning" and "evenign" are singular in hebrew, but e.g. "noon" is plural
02:50:41 <oerjan> <shachaf> Maybe oerjan remembers. <-- AAAAAAAAAAA
03:04:57 <shachaf> what is it that oerjan remembers? i've forgotten hth
03:15:17 <shachaf> Oh, the thing with differentials.
03:23:34 <zzo38> Now I wrote a document for a internet protocol called Netsubscribe, which I invented, you can read and please to question, complaint, or other comments about it.
03:37:06 <zzo38> It is: http://zzo38computer.org/textfile/miscellaneous/netsubscribe Do you like this?
03:42:02 <esowiki> [[MIX (Knuth)]] https://esolangs.org/w/index.php?diff=58341&oldid=58339 * Zzo38 * (+399) Include the bootstrap card for MIXPC assembler
03:42:54 -!- ais523 has quit (Remote host closed the connection).
03:43:06 -!- ais523 has joined.
03:43:58 <ais523> zzo38: I think the specification could be organised a bit more clearly; for example, I would separate the normative description of the protocol itself from suggestions about how to implement it, and I would move any detailed description of competing protocols and protocols that you plan to replace to a separate section near the end
03:44:46 <ais523> it might also be helpful to separate the description of what data the protocol operates on from the way that those data are represented within the protocol, but I might be wrong about that
03:46:44 <zzo38> ais523: OK, I deleted some of the stuff from the introduction, such as the stuff about other protocols (which was there in order to try to make it more clearly), although one reason I put that there was to clarify it, although ideally it should be clear without.
03:47:05 <ais523> the set of error codes you have is much smaller than in most protocols; I think most protocols eventually discovered that they needed to use a system of error numbers, in which the number encoded some information about the error (so that clients knew how to handle unknown errors) but also just a code describing the cause of the error
03:47:23 <ais523> zzo38: I think that sort of information isn't necessarily useless, but people want to know the information in importance order
03:47:38 <ais523> if you have to read less important information to get to more important information it's easy to get confused
03:48:25 <zzo38> Yes, maybe there should be an error code for a permission error, and for a temporary error.
03:48:47 <zzo38> You can make other kind of suggestions about what kind of error you think needs to be mentioned.
03:49:15 -!- hexfive has joined.
03:49:22 <zzo38> Yes, I could add stuff about relation to other protocols in a section at the end, I will try to do that.
03:51:11 <zzo38> I am not sure how I should organize the suggestions how to implement it as you describe though, and I am not sure about separating the description of what data the protocol operates on from the way that those data are represented within the protocol (you say yourself you may be wrong about that, though)
03:52:19 <ais523> zzo38: well, in RFCs, advice like "don't use gets()" and similar advice about how to implement the protocol securely is often placed in a section called "security implications" at the end
03:55:20 <zzo38> I deleted the part about gets() and fgets(). And you could use fgets() anyways, as long as you check for the presence of the line break so I was wrong about that anyways.
03:58:02 <zzo38> But I will add a section of security implications.
04:00:00 -!- Taneb has quit (Quit: I seem to have stopped.).
04:01:29 -!- Taneb has joined.
04:01:37 <zzo38> Also, do you think there are any security implications that I may have missed?
04:05:13 <ais523> it's hard to get all the security implications first time with a new protocol; so I'd expect anyone to miss some the first time
04:05:27 <ais523> but I'm not really used to this protocol so I'd be even more likely to miss them
04:06:45 <zzo38> (But that is also why I ask; even if I might miss some that someone else doesn't, even if it is likely to miss them, there is also the possibility that there is one you don't miss, I suppose.)
05:20:56 -!- ais523 has quit (Quit: quit).
05:32:22 -!- xkapastel has quit (Quit: Connection closed for inactivity).
06:31:42 -!- nfd has joined.
06:35:16 -!- nfd9001 has quit (Ping timeout: 260 seconds).
06:38:55 -!- oerjan has quit (Quit: Nite).
06:42:13 <shachaf> @ask ais523 I've forgotten your idea involving generalizing Rust's ?, is it written somewhere?
08:32:27 <shachaf> @ask ais523 I vaguely remember seeing a Haskell proposal that would translate something like do { f (<- a) (<- b) } into do { x <- a; y <- b; f x y } and so on. Do you remember something like that?
08:32:35 <shachaf> Or oerjan or Taneb or whoever
08:40:35 -!- xkapastel has joined.
09:15:46 -!- nfd has quit (Ping timeout: 250 seconds).
09:51:12 -!- AnotherTest has joined.
10:09:56 <esowiki> [[Talk:Brainfoctal]] https://esolangs.org/w/index.php?diff=58342&oldid=58331 * Salpynx * (+1401) /* Numbering system */ great suggestion, thank you!!
10:10:37 -!- nfd has joined.
10:18:43 -!- imode has quit (Ping timeout: 246 seconds).
11:10:16 -!- xkapastel has quit (Quit: Connection closed for inactivity).
11:20:42 <shachaf> @tell ais523 Ah, it's https://github.com/ghc-proposals/ghc-proposals/pull/64
11:21:47 <shachaf> @tell ais523 Oh, and http://docs.idris-lang.org/en/latest/tutorial/interfaces.html#notation is even closer
11:53:55 -!- Lord_of_Life has quit (Ping timeout: 246 seconds).
11:56:20 -!- Lord_of_Life has joined.
11:56:20 -!- Lord_of_Life has quit (Changing host).
11:56:20 -!- Lord_of_Life has joined.
12:03:30 -!- wob_jonas has joined.
12:12:38 <HackEso> 2018-11-12 12:12:38.052784510+00:00
12:25:54 -!- nfd has quit (Ping timeout: 252 seconds).
12:40:08 <esowiki> [[Falsebrain9Q+Fishload]] https://esolangs.org/w/index.php?diff=58343&oldid=57914 * Joshop * (+6)
13:23:34 -!- moei has joined.
14:09:25 -!- wob_jonas has quit (Quit: http://www.kiwiirc.com/ - A hand crafted IRC client).
14:17:12 -!- john_metcalf has joined.
14:43:58 -!- arseniiv has joined.
14:52:41 -!- Essadon has joined.
15:03:11 <ski> shachaf : "The reason I gave f().c as an example is that it shows that a.b doesn't always mean a thing like *(&a + b_offset)." -- hm, i suppose that goes into the difference between "persistent" vs. "transient" values (objects ?). cf. the C++ kerfuffle with "rvalue references" in relation to "move semantics" (and "perfect forwarding")
15:03:16 <ski> shachaf : "ais523 : I've forgotten your idea involving generalizing Rust's ?, is it written somewhere?" -- hm, i vaguely remember thinking and talking about something like that, on another channel
15:03:36 <ski> (partly in relation to my "reflective syntax" idea)
15:05:10 <ski> shachaf : fwiw, did you add some follow-up comments or questions after that (paste) snippet ? i think i intended to look and continue that conversation, but i got busy and then forgot, and now it's out of my scrollback
15:18:15 -!- Sgeo__ has joined.
15:20:07 -!- MDead has joined.
15:20:51 -!- Sgeo_ has quit (Ping timeout: 260 seconds).
15:21:12 -!- MDead_ has joined.
15:22:35 -!- MDude has quit (Ping timeout: 244 seconds).
15:25:15 -!- MDead has quit (Ping timeout: 264 seconds).
15:59:03 -!- sleepnap has joined.
16:15:19 -!- xkapastel has joined.
16:53:12 -!- Phantom_Hoover has joined.
17:12:00 -!- imode has joined.
18:03:59 -!- ais523 has joined.
18:04:07 <lambdabot> shachaf asked 11h 21m 54s ago: I've forgotten your idea involving generalizing Rust's ?, is it written somewhere?
18:04:07 <lambdabot> shachaf asked 9h 31m 40s ago: I vaguely remember seeing a Haskell proposal that would translate something like do { f (<- a) (<- b) } into do { x <- a; y <- b; f x y } and so on. Do you remember
18:04:07 <lambdabot> shachaf said 6h 43m 24s ago: Ah, it's https://github.com/ghc-proposals/ghc-proposals/pull/64
18:04:07 <lambdabot> shachaf said 6h 42m 19s ago: Oh, and http://docs.idris-lang.org/en/latest/tutorial/interfaces.html#notation is even closer
18:04:48 <ais523> shachaf: I don't think I posted my generalized-? idea anywhere but IRC, and it isn't fleshed out into a formal specification or anything like that
18:06:57 <ais523> perhaps we should try to express it in Haskell notation or something like that
18:07:28 <ais523> the basic idea is that x? converts the rest of the block into a function and gives it as an argument to x
18:07:36 <ais523> which can run it once, or not run it, or run it repeatedly
18:08:05 <ais523> and the f (<- a) (<- b) idea that you mention would be necessary so that code like f(a?)(b?) would be sensible
18:09:22 <ais523> Idris ! may be equivalent, although it's weird seeing it around presumably nullary terms like "print"
18:09:37 <ais523> err, not nullary, but returning a monad that contains unit
18:10:36 <ais523> I guess that works even in Rust
18:11:33 <ais523> there's no reason why you couldn't have a Result where the "non-error" case contained no data
18:11:34 <ais523> so (print x)? would mean "print x, and return on failure, otherwise continue"
18:11:40 <ais523> that's probably a common idiom in Rust already, come to think of it
18:11:56 -!- ais523 has quit (Quit: sorry for my connection).
18:12:08 -!- ais523 has joined.
18:19:06 <ski> (s/returning a monad that contains unit/returning a monadic action whose result is unit/)
18:20:17 <ski> <ski> shachaf : "ais523 : I've forgotten your idea involving generalizing Rust's ?, is it written somewhere?" -- hm, i vaguely remember thinking and talking about something like that, on another channel (partly in relation to my "reflective syntax" idea)
18:22:29 <ais523> I guess I'm mostly thinking about this ? proposal for less heavily functional languages
18:23:03 <ais523> does Haskell have anything resembling a promise library? or does it not need one, because the language is lazy anyway?
18:23:45 <ais523> …actually, the problem with Haskell wouldn't be blocking until the result arrives, but starting to ask for the result before you need it
18:23:56 <ais523> so that it's there when you do
18:24:19 <ais523> something that was discussed on a previous work project of mine, but not implemented, was "parallel call by need evaulation"
18:24:28 -!- xkapastel has quit (Quit: Connection closed for inactivity).
18:25:02 <ais523> the idea is that when you see code "f x", you start evaluating x in the background while calling f; if f turns out to return without actually needing the value of x, you halt/discard the background evaluation
18:25:10 <ais523> (obviously, this only really works in a pure language)
18:25:30 <ais523> that style would make promises entirely irrelevant
18:28:04 <ski> iirc, the Rust `?' thing was (originally ?) about operations returning a result of option type ?
18:28:13 <ais523> anyway, re the "monad that contains" thing, I apologise for the sloppy language (but think "monadic action whose result is" is misleading; it's not really like a result at all, more like an argument)
18:28:55 <ais523> Rust's ? was probably first used with Result (the equivalent of Haskell's Either) as that's the type which most commonly needs it in practice
18:29:08 <ski> yea, i just like to emphasize that a monad is not a run-time value, really. a value of monadic type is something else
18:29:42 <ski> your description of `x?' above seemed related to CPS ?
18:30:07 <zzo38> I don't really like "monad that contains" or "monadic action whose result is". Some monads neither contain such a value nor perform an action having a result
18:30:43 <ais523> *simplest example is probably the void monad
18:30:46 <ski> (i agree about not "containing" a value)
18:30:55 <ais523> although, actually, no, that doesn't support return
18:31:08 <zzo38> And then there is stuff that can contain a value of that type but might not, such as Maybe and []
18:31:12 <ski> i'm not sure what you have in mind by that term
18:31:15 <ais523> I guess I don't intuitively see why a monad should
18:31:34 <ais523> ski: "Maybe except it always contains Nothing", for example
18:31:42 <ski> `Maybe' expresses the possibility of not ending up with a result
18:31:43 <HackEso> /srv/hackeso-code/multibot_cmds/lib/limits: line 5: exec: Maybe': not found
18:31:53 <ski> that's the effect that the `Maybe' monad expresses
18:32:23 <ais523> I guess the difference in thought between me and everyone else is that I see monad actions as not necessarily belonging to any particular monad type
18:32:31 <ski> generally, one could say that all behaviour of an action of some monad, apart from simply "yielding" a single result, is an effect
18:32:46 <ais523> Haskellers think in terms of "Maybe Integer", whereas I think more in terms of "Nothing" or "Just 6"
18:33:00 <ais523> as being of type (Monad x) => x Integer
18:33:00 <ski> so, for `Maybe' an effect is not giving a result value. for list, an effect is not giving a result value, or giving multiple result values
18:33:22 <ski> for state, an effect is depending on, and possibly changing, the implicit state
18:33:37 <ais523> ski: why are you treating the case where one result value is available as a special case?
18:33:57 <oren> hmmm, can you compose types like "SuchThat f Integer"?
18:34:01 <ais523> because that's what "pure"/"return" does, and thus it isn't an effect by definition?
18:34:14 <ski> ais523 : well, `Nothing' is of type `Maybe Integer', not of type `Monad x => x Integer', afaiac -- i'm not following your line of thought here, elaborate ?
18:34:16 <oren> e.g. an integer such that f returns true on it?
18:35:05 <ski> ais523 : "why are you treating the case where one result value is available as a special case?" because that's the non-effectful ("pure") case, which is what the `return'/"unit" monadic operation (not that greatly named in Haskell) gives you
18:35:36 <ais523> ski: I know, it isn't of type Monad x => x Integer; it's more that for me, the important thing about Nothing and Just 6 is that (Nothing (>>=)) and ((Just 6) (>>=)) are funcitons that take (Integer -> a) arguments
18:35:48 <ski> oren : in dependent typing, you can
18:36:08 <ais523> …actually, I think I've realised what's up with my understanding; I think of monads as being /just/ the >>=
18:36:14 <ais523> without caring about the "return"/"pure" part of the mat all
18:36:29 <ski> well, both are important
18:36:38 <ski> while admittedly, one is more interesting than the other
18:37:00 <ski> but when branching, you want the ability/choice to not do anything interesting in one branch
18:38:24 <ski> hm, thinking of `(Nothing >>=)' and `(Just 6 >>=)' again to me suggests thinking about continuations (CPS, or in this case, the Codensity monad, which is a kind of optimization that you sometimes want to apply)
18:38:34 <ais523> …and thinking about this even more: the behaviour of ">>=" is effectively part of the monad /action/, whereas the behaviour of "return"/"pure" isn't, it's only part of the monad /type/
18:38:41 -!- wob_jonas has joined.
18:38:59 <ski> well, in a sense, both are trivial
18:39:09 <ski> both are about *sequencing* some kind of interesting *effects*
18:39:18 <ski> but neither of them actually expresses an interesting effect
18:39:25 <oren> because if you can have a SuchThat f Integer then you can instead of hacing a function return a Maybe Integer it can *take* a SuchThat f Integer
18:39:50 <ski> if you *only* have `return' and `(>>=)' operations of a monad to work with, that's (close to) useless, you can't do much useful stuff
18:39:55 <ais523> so suppose we have code like (Haskell) do {a1 <- a; b1 <- b; return (a+b)}
18:40:11 <ais523> is it possible to make something like that work when a and b belong to /different/ monads? my guess is no
18:40:25 <ski> (actually, with higher-order operations, you can do some useful things. but only as library operations that eventually will have to be applied in a particular situation, with a particular monad with more operations available)
18:40:27 <ais523> do {a1 <- a; b1 <- b; return (a1+b1)}
18:40:45 <ski> "monad" is like an abstract data type interface, like "priority queue"
18:41:19 <ski> but, knowing that you have a priority queue, but not being given any additional, implementation-specific operations, for it, you can still do useful things
18:41:24 <ais523> I mean, and b have two different types, and each such class belongs to the typeclass Monad
18:41:25 <ski> with a monad, not so much
18:42:01 <ski> typically, you want to have some extra operations, like state operations, non-deterministic operations, exception operations, parsing, concurrency-related, continuation stuff, &c.
18:42:31 <ski> "is it possible to make something like that work when a and b belong to /different/ monads? my guess is no" -- in general, no -- in some particular cases, it may be possible
18:42:39 <ais523> OK, I think I know what goes wrong in Haskell; you'd need /two/ returns, the inner one creating a value that's pure with respect to b's effects, the outer one creating a value that's pure with respect to a's effects
18:43:09 <ski> well, that can also be useful, in certain situations
18:43:13 <ski> (but that's a different thing)
18:43:40 <ais523> the closest you can get to what I want in Haskell is do {a1 <- a; return do {b1 <- b; return (a1+b1)}}
18:43:40 <ski> oren : yep
18:44:34 <ski> let's say `a' in the state monad (`State t', say, `t' being the type of the state which the computation depends on, and may change)
18:44:47 <ski> and `b' in the environment/input/reader monad (`Reader t')
18:45:24 <ski> so, you're not interested in the final value of the state, and so you want to avoid bothering getting back the final state result from the "rightmost-leaning branch" in your computation tree
18:46:14 <ski> so, here we'd have a variant of `(>>=)', of type `m a -> (a -> n b) -> n b', where `m' here would be `State t', and `n' would be `Reader t'
18:48:36 <ski> (we also have a conversion of type `m a -> n a', which here just discards the final state, and `n a -> m a', which copies over the input state. the former operation is a post-inverse to the latter, but not the other way around. then there's some laws of interaction between these two conversions, and the `(>>=)' above, and the usual monadic operations)
18:49:03 <shachaf> ski: I don't remember what I wrote after that conversation, I didn't log it or anything.
18:49:24 <ski> (another example would be a version of lists, where we only care about the final number of solutions. so then `m = []' and `n = Const Integer' or somesuch)
18:49:30 <ski> shachaf : fair enough
18:51:02 <ski> ais523 : hm, so perhaps you could elaborate on "…and thinking about this even more: the behaviour of \">>=\" is effectively part of the monad /action/, whereas the behaviour of \"return\"/\"pure\" isn't, it's only part of the monad /type/" ?
18:52:04 <shachaf> ais523: Maybe you mean (Monad x *> x Integer) instead of (Monad x => x Integer)?
18:53:47 * ski sighs about presuppositions
18:54:41 -!- ais523 has quit (Remote host closed the connection).
18:54:59 -!- ais523 has joined.
18:55:08 <ais523> ski: well, the only "general-purpose" thing you can do with a monad action is to use its >>= (producing another monad action of the same type)
18:56:23 <ais523> so, in a sense, the monad action "is" its >>=, because anything else you could do with it is a special case
18:56:23 -!- ais523 has quit (Remote host closed the connection).
18:56:35 -!- ais523 has joined.
18:56:47 <ais523> <ais523> meanwhile, "return"/"pure" doesn't take a monad action as argument at all, it's a constructor for monad actions
18:56:58 <ais523> and the monad action you construct doesn't actually have anything to do with the monad it belongs to
18:57:10 <ais523> because all return values from "return"/"pure" have the /same/ >>=
18:57:49 <ais523> (specifically, "(>>=) (return x)" = "(\f -> return (f x))")
18:58:10 <ski> if you don't have access to other monadic operations, for some monad `m', than `return' and `(>>=)', then you can only build actions like e.g. `return x >>= \y -> return (f y)' which (by monad law) is equal to `return (f x)'
18:58:30 <ski> so, every action of type `m a' you can build will then be equal to `return x', for some `x'
18:58:35 <ski> that's not terribly exciting
18:58:55 <ais523> ski: I guess I'm assuming I have access to some constructors that return impure monad actions
18:59:19 <ski> (you can do a little more interesting stuff if you take monadic callback arguments, and express patterns of compsing them in particular ways, possibly while simutaneously traversing a data structure, or somesuch)
18:59:57 <ais523> …actually, I guess that what I'm doing is not wanting to draw a distinction between any instance of "return 4"
18:59:59 <wob_jonas> ski: I don't think you can. there's the monad associativity law that says that can't be more interesting.
19:00:17 <shachaf> I like the thing Oleg mentioned about how you can write dne :: (forall m. Monad m => (a -> m Void) -> m Void) -> a
19:00:30 <ais523> I don't see any reason why "Just 4" and "[4]" should be considered different values
19:00:39 <ski> wob_jonas : (simple) examples of such "slightly more interesting" operations i have in mind is `sequence' and `mapM'
19:01:11 <ski> (the associativity law says that the "bracketing/grouping" doesn't matter, only the order (may) matter)
19:01:11 <shachaf> It was on http://okmij.org/ftp/Computation/lem.html which is now a 404? Oh no
19:01:57 <ski> ais523 : the reason i was "singling out" `Just 4' and `[4]' above was that they can be expressed as `return x', for some `x'
19:02:12 <ski> and `return' is *the* way to express an "efectfully trivial" action
19:02:12 <shachaf> ski: Did I talk mention my weird "rest of block" programming language idea to you?
19:02:20 <ski> shachaf : i don't think so
19:02:56 <ski> ais523 : i agree this is a bit like singling out the integer zero from all the other integers ("because adding it to something doesn't change the result", so to speak)
19:03:44 <ais523> I guess from my point of view, I don't consider "Just 4" and "[4]" to be special in a different sense: the two values are indistinguishable using monad operations, even in an impure language
19:04:10 <ski> from my POV, monads are for capturing/expressing "effects". `return' is used when the interface (the type) allows the possibility of an effect, but in this particular case, we don't want one
19:04:28 <ski> (but if we never want one, then we don't need to use a monad there)
19:04:34 <ais523> if you imagine an impure language that has monads, you can do things like "x >>= \y.(unsafePerformIO (putStrLN (show y)))"
19:04:52 <ais523> and that lets you distinguish between different monadic actions in x, but you can't distinguish between the various sorts of return 4
19:05:09 <ski> hm, not sure what you have in mind by "the two values are indistinguishable using monad operations, even in an impure language"
19:05:45 <ski> ais523 : hm, what is the monad used for `(>>=)', there ?
19:06:14 <ais523> well, «(return 4) >>= (\y.(unsafePerformIO (putStrLn (show y)))» is, by monad laws, equivalent to «unsafePerformIO (putStrLn "4")»; and it doesn't matter what the monad you use is
19:06:34 <wob_jonas> but surely [4] and (Just 4) can't be completely interchangable if show can distinguish them
19:06:39 <ais523> likewise, in the original example, I'm assuming we don't know what type x has, just that it has type (Monad m) => m Integer
19:06:50 <ski> it looks to me like the type of the latter would be `()'/`unit'/`void', or however you spell it
19:07:06 <ski> which doesn't seem to fit the pattern `m a', of a monad `m' applied to a "monadic result type" `a'
19:07:21 <ais523> ski: sorry, I forgot a "return"
19:07:49 <ais523> «x >>= \y.(return (unsafePerformIO (putStrLn (show y))))»
19:08:01 * ski assumes ais523 means : just that is has type `m Integer', for some monad `m' (iow for some `m' satisfying `Monad m')
19:08:09 <wob_jonas> it's not like show is magical or breaks monad laws or purity or anything there
19:08:36 <ski> (that's why i sighed about presuppositions before. i see this sort of confusion in #haskell all the time)
19:08:37 <shachaf> I think maybe you're thinking in terms of continuations, and how "return x" always calls its continuation exactly once, or something?
19:08:55 <ais523> wob_jonas: oh, I'm assuming that our monad action x has an unknown type other than being a monad action which takes functions that take integers in its >>=, so we can't give it directly as an argument to show because we don't know it implements Show
19:08:57 <ski> ais523 : anyway, i'm still now sure where you're going with this "indistinguishable" business
19:09:51 <ais523> ski: I guess I'm imagining a language with a weaker type regime than Haskell (possibly even untyped), in which case all possible return values from "return 4" are the same value, given that you have no way to distinguish between them
19:10:16 <ski> hm, it seems to me that's already the case in Haskell
19:10:19 <ais523> so if we want a value that's "Maybe Integer" we have two possibilities: a) "return n" for any Integer n; or b) "Nothing"
19:12:21 <shachaf> I think Maybe and [] are maybe misleading, especially since Maybe is just an affine special case of [].
19:12:27 <wob_jonas> ah, so like a... language with a different type system, and Monad defined such that return isn't a method, but a function that doesn't depend on the monad tycon?
19:12:29 <shachaf> Say "m" is (e ->) or something.
19:12:53 <ais523> shachaf: which monad is that? Reader?
19:13:31 <shachaf> OK, I guess I might see what you're getting at
19:14:11 <ais523> shachaf: so with Reader, you have "return 4" being "\x.4", and you can likewise perform operations on that without knowing what x is
19:14:15 <wob_jonas> ais523: but then what would the signature of whatever becomes of the (>>=) method in that different Monad be like?
19:14:43 * ski isn't even sure what we're currently discussing, anymore
19:14:47 <shachaf> ais523: I don't think the >>=(\y.unsafePerformIO (putStrLn (show y))) thing makes sense, though
19:14:50 <ais523> wob_jonas: same as for any monad
19:15:01 <lambdabot> Monad m => m a -> (a -> m b) -> m b
19:15:52 <wob_jonas> ais523: but then how could that work on both monads created by return and monads created in other ways?
19:16:42 <ski> (s/monads/monadic actions/, sorry to bother)
19:17:11 <shachaf> ais523: Which value would that call the continuation with?
19:17:26 <ais523> OK, let's look at it this way: suppose we have an operator, let's call it (>>='), which has type (Monad m1, Monad m2) => m1 a -> (a -> m2 b) -> ? b, where ? is some monad
19:17:40 <ski> (well, have fun. i have to leave presently. will perhaps check in later)
19:17:42 <ais523> the question is, what type should ? have?
19:18:02 <ais523> and I think the answer is "in general you can't answer this, but for many specific cases there's a reasonable answer"
19:18:17 <ais523> for example, if either m1 or m2 is Identity, then you can make ? work as the other of the two monads
19:18:33 <wob_jonas> how did we even get here from places in structure fields?
19:18:37 <ais523> and if m1 = m2, then the unknown monad at the end is the same thing
19:18:43 <wob_jonas> or, um, how did you get here while I was not looking?
19:18:59 <ais523> wob_jonas: well, this sort of topic is something that shachaf and I have been discussing on and off for weeks
19:19:53 <shachaf> wob_jonas: This is an orthogonal discussion to the one about structs and lvalues, I think.
19:20:14 <ais523> now, if we consistently use >>=' rather than >>=, then a) all existing Haskell code works because m1 and m2 will always have the same type, b) we can consistently define (return a) using the return from Identity, rather than using the original monad, and things will still work
19:22:23 <ais523> …so I guess what I want is a world in which all monads are associative in the sense that Monad1 (Monad2 x) and Monad2 (Monad1 x) are the same type
19:22:48 <wob_jonas> ais523: but isn't that impossible?
19:22:55 <ais523> maybe I should try to write a concrete language like this and see where it goes wrong
19:23:02 <ais523> wob_jonas: it depends on how many monads you support
19:23:12 <ais523> it's certianly possible if you have only a small whitelist of monads
19:23:14 <wob_jonas> well sure, if you only have Identity and nothing else that it could work
19:23:42 <ais523> for example, we could combine Maybe and List by deleting Nothiing-valued list elements
19:24:37 <shachaf> Something like https://en.wikipedia.org/wiki/Distributive_law_between_monads
19:24:49 <shachaf> I think I remember something about a system that used this? But I don't remember the details
19:27:44 <ais523> actually, an even better way to think about this is to think about the mathematical definition of monads (which uses two operations, one of type (x → m x), one of type (m m x → m x)); the ideal would be for the (m m x → m x) to work with two /different/ ms on the LHS
19:28:18 <ais523> in Haskell, at the moment, it's common to use monad transformers for that sort of thing
19:28:44 <ais523> e.g. it's easy enough to write a function (Reader (IO x)) → ((ReaderT IO) x)
19:29:01 -!- nfd has joined.
19:29:27 <ais523> …do monad /transformers/ always commute with each other? my guess is "not always, but they often do"
19:30:00 <shachaf> Monad transformers are kind of ad-hoc
19:30:22 -!- xkapastel has joined.
19:38:56 <shachaf> ski: So the idea is that you have a bunch of control flow things that affect "the rest of the block"
19:39:13 <shachaf> ski: Like { if(p); ... } for what's normally written as if (p) { ... }
19:39:27 -!- john_metcalf has quit (Ping timeout: 240 seconds).
19:39:31 <shachaf> And { x := for(xs); ... } for what's normally for (x : xs) { ... } or something
19:40:19 <shachaf> I now think that maybe this should be marked more explicitly, something like { if(p)`; ... }, where ` on a value means "pass the rest of the block as a continuation"
19:41:14 <shachaf> I think this is maybe similar to delimited continuations in a restricted form, with {} having a role similar to reset?
19:41:23 <shachaf> And { A; B; C; } meaning { A; { B; C; } }
19:43:49 <shachaf> Do you know of something like that?
19:44:19 <wob_jonas> yeah, you've asked about that earlier here, I think
19:44:39 <zzo38> I did think some time I wanted to have the possibility to have a macro in JavaScript that allows passing the rest of the function as a continuation.
19:44:53 <wob_jonas> there's prolog's nondeterminism which you could think of as a special case of that
19:55:48 <wob_jonas> but it's not delimited, it takes the whole rest of the run of the program, not just the rest of the "block"
19:58:28 <ais523> well, unless you have an alternative (based on ; or on a second definition of the same predicate)
20:37:47 <zzo38> I have now added two new responses to the Netsubscribe protocol, which are & (deferred processing) and T (timeout).
20:42:05 <esowiki> [[Esolang:Featured languages/Candidates]] https://esolangs.org/w/index.php?diff=58344&oldid=57018 * Camto * (+69) Burlesque
20:44:41 -!- wob_jonas has quit (Quit: http://www.kiwiirc.com/ - A hand crafted IRC client).
20:45:00 -!- wob_jonas has joined.
20:45:04 -!- wob_jonas has quit (Client Quit).
21:05:16 <esowiki> [[A]] https://esolangs.org/w/index.php?diff=58345&oldid=58336 * Cortex * (+23)
21:06:20 <esowiki> [[A]] https://esolangs.org/w/index.php?diff=58346&oldid=58345 * Cortex * (+0) /* Numbers from 1 to 10 */
21:11:34 <esowiki> [[A]] https://esolangs.org/w/index.php?diff=58347&oldid=58346 * Cortex * (+168)
21:11:58 <esowiki> [[A]] https://esolangs.org/w/index.php?diff=58348&oldid=58347 * Cortex * (+4)
21:32:16 <esowiki> [[Web framework list]] M https://esolangs.org/w/index.php?diff=58349&oldid=50039 * Camto * (+21) Retrieved from Wayback Machine.
21:52:52 -!- moei has quit (Quit: Leaving...).
22:37:38 <esowiki> [[User:JonoCode9374]] https://esolangs.org/w/index.php?diff=58350&oldid=57956 * JonoCode9374 * (+76)
23:14:57 -!- sleepnap has quit (Quit: Leaving.).
23:33:27 -!- AnotherTest has quit (Ping timeout: 240 seconds).
23:37:38 -!- tromp has quit (Remote host closed the connection).
23:37:54 -!- tromp has joined.
23:40:34 -!- Essadon has quit (Quit: Qutting).
23:53:23 -!- Lord_of_Life_ has joined.
23:56:36 -!- Lord_of_Life has quit (Ping timeout: 268 seconds).
23:56:37 -!- Lord_of_Life_ has changed nick to Lord_of_Life.
23:56:37 -!- Lord_of_Life has quit (Changing host).
23:56:37 -!- Lord_of_Life has joined.