IRCBrowse

2021/11/06

2021-11-06 00:00:19 +0100 <joel135> wait, how does Fix take two arguments?
2021-11-06 00:00:58 +0100 <ski> imagine a `Fix :: ((* -> *) -> (* -> *)) -> (* -> *)'
2021-11-06 00:01:10 +0100 <joel135> ok
2021-11-06 00:01:16 +0100son0p(~ff@181.136.122.143)
2021-11-06 00:01:26 +0100 <ski> (or `forall k. (k -> k) -> k', although that seems harder to define)
2021-11-06 00:01:35 +0100raehik(~raehik@cpc95906-rdng25-2-0-cust156.15-3.cable.virginm.net) (Ping timeout: 264 seconds)
2021-11-06 00:01:39 +0100 <joel135> yes
2021-11-06 00:02:53 +0100 <joel135> are you saying that exponentiation requires you to use two precisely two levels of ContT?
2021-11-06 00:02:58 +0100 <ski> idea being that you can take limit of `o',`o -> o',`(o -> o) -> (o -> o)',`((o -> o) -> (o -> o)) -> ((o -> o) -> (o -> o))',&c. .. or, in my case, rather allow the user to pick the depth, at run-time
2021-11-06 00:03:25 +0100raehik(~raehik@cpc95906-rdng25-2-0-cust156.15-3.cable.virginm.net)
2021-11-06 00:03:27 +0100MoC(~moc@user/moc) (Quit: Konversation terminated!)
2021-11-06 00:03:48 +0100brainfreeze(~brainfree@2a03:1b20:4:f011::20d)
2021-11-06 00:04:35 +0100 <ski> no, i was saying that `exp :: Church o -> Church o -> Church o' where `type Church o = (o -> o) -> (o -> o)' doesn't work, you need `exp :: (forall o. Church o) -> (forall o. Church o) -> (forall o. Church o)'
2021-11-06 00:05:23 +0100 <ski> (i guess, allowing the user to pick the depth is like having a stream of progressively deeper nestings)
2021-11-06 00:06:16 +0100 <joel135> this limit of o',`o -> o',`(o -> o) -> (o -> o)',`((o -> o) -> (o -> o)) -> ((o -> o) -> (o -> o))',&c reminds me of stuff i recently learned about untyped lambda calculus
2021-11-06 00:06:40 +0100 <ski> anyway, using a third level to represent polynomials sounds interesting. i'd have to investigate that, and how that could align with what i've been pondering here
2021-11-06 00:06:47 +0100dolio(~dolio@130.44.130.54) (Quit: ZNC 1.8.2 - https://znc.in)
2021-11-06 00:06:48 +0100 <ski> yes ?
2021-11-06 00:08:04 +0100 <ski> `TPoly' is dual numbers over `Poly' ?
2021-11-06 00:08:18 +0100 <joel135> yes
2021-11-06 00:09:14 +0100 <joel135> i believe this T : Type -> Type in general, but not sure how to construct it for other types
2021-11-06 00:10:11 +0100 <joel135> it constructs the tangent bundle of a type, and it is supposed to "know" somehow that Poly is a smooth thing
2021-11-06 00:10:19 +0100 <ski> joel135 : it might be interesting to spell out the type applications in your code, to see where you just pass on the same `s', and where you pass on something different
2021-11-06 00:10:41 +0100 <ski> (if you do)
2021-11-06 00:11:38 +0100dsrt^(~dsrt@h50.174.139.63.static.ip.windstream.net)
2021-11-06 00:13:11 +0100 <joel135> i *think* the only lines are 64 and 85
2021-11-06 00:13:25 +0100 <joel135> but i may be wrong about this after line 85
2021-11-06 00:14:02 +0100 <ski> well, line 64 is `s = Coeffs', i'd guess, yes ?
2021-11-06 00:14:12 +0100 <joel135> yes
2021-11-06 00:14:29 +0100 <joel135> and later it is s = TPoly
2021-11-06 00:14:40 +0100 <ski> and line 85 is `s = (Poly,Poly)', i think ?
2021-11-06 00:14:45 +0100 <joel135> yes
2021-11-06 00:14:47 +0100 <ski> yea
2021-11-06 00:14:57 +0100mc47(~mc47@xmonad/TheMC47) (Remote host closed the connection)
2021-11-06 00:15:30 +0100 <ski> i wonder if you could reduce that to `s1 = ..s0..', if you start by "opening up" the `Poly' that you're attempting to produce, calling its parameter `s0'
2021-11-06 00:16:16 +0100 <ski> (i did such reductions for addition, multiplication, exponentiation, starting with an impredicative thing, and ending up with an equivalent predicative thing)
2021-11-06 00:17:29 +0100 <joel135> ok i will try to rewrite it in terms of a single type variable like s and see if it works out
2021-11-06 00:17:46 +0100 <joel135> by the way, when you did the logic programming stuff, what was the target language? did you compile it to actual machine code?
2021-11-06 00:18:17 +0100alzgh(~alzgh@user/alzgh) (Remote host closed the connection)
2021-11-06 00:18:41 +0100 <joel135> (assuming my question makes sense)
2021-11-06 00:19:35 +0100 <ski> it was just a Haskell combinator library
2021-11-06 00:19:45 +0100 <joel135> ok
2021-11-06 00:19:56 +0100 <ski> (partially inspired by a paper by Seres and Spivey, and a later one by Koen Claessen)
2021-11-06 00:20:22 +0100 <ski> it would be interesting to ponder how one'd do it, in terms of something WAM-like, say
2021-11-06 00:20:36 +0100alzgh(~alzgh@user/alzgh)
2021-11-06 00:20:55 +0100 <ski> (iow, consider ways to improve the resource management, rather than just deferring to GC for everything)
2021-11-06 00:20:57 +0100 <joel135> also by the way, this limit of `o',`o -> o',`(o -> o) -> (o -> o)',`((o -> o) -> (o -> o)) -> ((o -> o) -> (o -> o))',&c reminds me of the colimit of ΩⁿΣⁿX which is called "stabilization" or something like that
2021-11-06 00:21:25 +0100 <joel135> (https://ncatlab.org/nlab/show/spectrum)
2021-11-06 00:22:08 +0100 <joel135> i looked a bit a barendregt's book on lambda calculus and there are some parallels i think, but i haven't thought it through fully
2021-11-06 00:22:15 +0100 <joel135> at*
2021-11-06 00:23:08 +0100 <ski> you know how you can define an implication `( Antecedent => Consequent )' (commonly spelled `forall(Antecedent,Consquent)' in implementations) in Prolog as `\+ ( Antecedent,\+ Consequent )', yes ? (where (\+)/1 is the usual negation-as-failure (imperfect, sometimes unsound) approximation to a sound logical negation)
2021-11-06 00:23:51 +0100 <joel135> WAM = https://en.wikipedia.org/wiki/Warren_Abstract_Machine ?
2021-11-06 00:24:00 +0100 <ski> operationally, what happens is that you'll enumerate all solutions of `Antecedent', and then check that `Consequent' holds for that solution. the enumeration is aborted if `Consequent' fails
2021-11-06 00:24:04 +0100 <ski> yea
2021-11-06 00:24:08 +0100 <joel135> ok
2021-11-06 00:24:21 +0100qwedfg(~qwedfg@user/qwedfg) (Remote host closed the connection)
2021-11-06 00:24:57 +0100 <joel135> i don't have much practical experience with prolog so i have to read what you just wrote slowly
2021-11-06 00:25:11 +0100 <ski> if you have variables which occur (only) in `Antecedent' and `Consequent', then they behave as if they were universally quantified over the implication (hence the name forall/2). (because they behave as existentially quantified just inside the outer negation)
2021-11-06 00:25:38 +0100ec(~ec@gateway/tor-sasl/ec) (Remote host closed the connection)
2021-11-06 00:26:01 +0100 <ski> now, the problem with this is that you can't use this to export information (other than success/failure) (unless you use side-effects, mutation that survives backtracking ..)
2021-11-06 00:26:06 +0100ec(~ec@gateway/tor-sasl/ec)
2021-11-06 00:26:58 +0100 <ski> so, it's great to check that every solution of `Antecedent' actually satisfies `Consequent' .. but if `Antecedent' is e.g. enumerating elements of some kind of collection, you unfortunately can't use this to let `Consequent' instantiate those elements
2021-11-06 00:27:18 +0100qwedfg(~qwedfg@user/qwedfg)
2021-11-06 00:27:43 +0100 <joel135> i don't know what you mean by instantiate
2021-11-06 00:27:55 +0100dolio(~dolio@130.44.130.54)
2021-11-06 00:28:46 +0100 <ski> give a definite value
2021-11-06 00:29:32 +0100 <ski> in Haskell, as soon as you introduce a binder for a variable, it will, at run-time, be asssociated with a value (or rather, with a computation that will eventually produce a value)
2021-11-06 00:29:35 +0100 <joel135> do you mean that if the implication fails one would like this to give a definite value to the variables that are universally quantified over?
2021-11-06 00:30:20 +0100 <ski> in logic programming, these two steps are decoupled from each other. you introduce a variable with the existential (or universal) quantifier. then (possibly much) later, you can associate a value with it
2021-11-06 00:32:01 +0100 <ski> not the universally quantified variables (which are local, so private), but other (free/nonlocal) variables which are put in some relation (usually using equality) with those universally quantified variables, inside of `Consequent'
2021-11-06 00:33:11 +0100 <joel135> ok, then i seem to see sort of what you are talking about
2021-11-06 00:33:47 +0100 <ski> take `append(Xs,Ys,Zs)', which expresses what one would state as `zs = xs ++ ys' in Haskell
2021-11-06 00:34:01 +0100 <joel135> ok
2021-11-06 00:34:26 +0100 <ski> predicates/relations in logic programming have no predetermined input vs. output status of parameters. sometimes a parameter is input, sometimes it's output
2021-11-06 00:34:54 +0100 <joel135> right, as = is undirected
2021-11-06 00:35:22 +0100 <ski> if you call `append([0,1,2],[3,4],L)', the system will instantiate `L', having the query/goal succeed, and the answer `L = [0,1,2,3,4]' is reported
2021-11-06 00:36:02 +0100 <ski> each call will either succeed or fail. it can succeed many times (with possibly different solutions/answers). and then it fails at the end, meaning "no (more) solutions"
2021-11-06 00:37:05 +0100 <joel135> sort of like the list monad?
2021-11-06 00:38:10 +0100 <ski> in a conjunction, you start by calling the first conjunct. if it succeeds, you proceed to the next one. if a conjunct fails, backtracking starts, and you "execute backwards", going back to the previous conjunct (undoing any instantiations to variables that were done in the meantime), asking it to produce an alternative solution, if it can. if it does, then that conjuct succeeds, and normal left-to-right
2021-11-06 00:38:16 +0100 <ski> execution proceeds. otherwise, backtracking continues to the left
2021-11-06 00:38:17 +0100 <ski> yes
2021-11-06 00:38:23 +0100 <syd> just going off the last few messages of the exchange, but you may find this paper interesting: https://rkrishnan.org/files/wadler-1985.pdf
2021-11-06 00:38:52 +0100 <joel135> syd: wadler has some good titles :)
2021-11-06 00:39:06 +0100 <ski> so, `generate(X),test(X)' is a common basic paradigm of looping. generate/1 generates candidate solutions, and test/1 checks them. so, it'll go ping-pong until some candidate passes
2021-11-06 00:39:37 +0100 <ski> syd : read it, years ago :)
2021-11-06 00:40:00 +0100 <syd> joel135: makes them easy to find again too, there's always a couple of idiosyncratic word choices that are guaranteed to be the top google result ;p
2021-11-06 00:41:09 +0100 <ski> anyway, `append([0,1,2],[3,4],[0,1,2,3,4])' and `append([0,1,2],[3,4],[0,1,5,3,4])' are calls that will simply either succeed or fail, not binding any variables (since there are none in the calls), so not providing/exporting any information apart from the success/failure status
2021-11-06 00:42:10 +0100 <ski> while `append(Front,Back,[0,1,2])' will enumerate four solutions. first `Front = [],Back = [0,1,2]', then, when you ask for more (by forcing backtracking), you'll get `Front = [1],Back = [1,2]',&c.
2021-11-06 00:42:26 +0100vysn(~vysn@user/vysn) (Ping timeout: 260 seconds)
2021-11-06 00:42:31 +0100 <ski> similarly, `member(X,[0,1,2])' will enumerate solutions `X = 0',`X = 1',`X = 2'
2021-11-06 00:43:07 +0100 <joel135> i have a strange question
2021-11-06 00:43:25 +0100 <ski> yes ?
2021-11-06 00:44:23 +0100 <joel135> if you ask `member(X,[0,1,2])' for the next solution after it has produced `X = 2', should this cause some sort of "backtracking to outside of the logical programming process"?
2021-11-06 00:44:58 +0100 <joel135> assuming `member(...)' is the first instruction of the program
2021-11-06 00:45:37 +0100 <ski> syd : "How to add laziness to a strict language, without even being odd" by Philip Wadler,Walid Taha,David MacQueen in 1998-09 at <https://homepages.inf.ed.ac.uk/wadler/topics/language-design.html#lazyinstrict> is another nice title :)
2021-11-06 00:46:07 +0100merijn(~merijn@83-160-49-249.ip.xs4all.nl)
2021-11-06 00:46:27 +0100 <joel135> i think you would need to have a logic programming language within another logic programming language in order for my question to make sense
2021-11-06 00:46:35 +0100 <ski> joel135 : well, when you're testing / fooling around with Prolog programs, you usually work in the interactor / rppl (read-prove-print-loop), prompt being `?-'
2021-11-06 00:47:10 +0100 <ski> so, `?- member(X,[0,1,2]).', after `X = 2', failure would cause execution to "hit the left margin", and so the whole query fails
2021-11-06 00:47:19 +0100 <syd> again, sorry for butting in, but have you tried miniKanren ski?
2021-11-06 00:47:32 +0100 <syd> untyped (the racket impl. at least) but lots of fun.
2021-11-06 00:48:06 +0100 <ski> (so, in terms of delimited continuation barriers, if you want to think of it like that, each query is delimited from other queries. as soon as a query is finished, you won't later attempt to backtrack it)
2021-11-06 00:48:17 +0100 <joel135> i think i have a very old miniKanren bookmark on youtube that i never followed up
2021-11-06 00:48:26 +0100 <ski> syd : i've heard nice things about it, but i've yet to dive into what it offers
2021-11-06 00:49:22 +0100 <ski> anyway, consider `( member(X,Xs) => between(1,6,X) )' .. `between(1,6,X)' is like `x <- [1 .. 6]'. so, this can be used to check that every element of `Xs' is in the requisite range
2021-11-06 00:50:11 +0100 <joel135> ok
2021-11-06 00:50:17 +0100__monty__(~toonn@user/toonn) (Quit: leaving)
2021-11-06 00:50:28 +0100uiltondutra(~uiltondut@45.183.251.42)
2021-11-06 00:50:34 +0100 <ski> however, i'd like for this query/goal to also work, even if the elements of `Xs' aren't known/initialized/instantiated yet (but they length would have to be known, or else we're in more trouble, having infinite number of solutions .. and traversal order starts to matter, for completeness. Prolog uses depth-first)
2021-11-06 00:50:55 +0100 <ski> iow, then it ought to enumerate all possible selections of the elements from the range (with replacement)
2021-11-06 00:51:31 +0100zincy_(~zincy@2a00:23c8:970c:4801:350f:7ee:191a:6f65) (Remote host closed the connection)
2021-11-06 00:51:55 +0100 <ski> the usual encoding (which has some uses, for sure) of implication, in terms of negation(-as-failure) can't do this, because it can't export information from a query, apart from answering yes/no
2021-11-06 00:52:12 +0100 <ski> but, this is exactly what my prototype managed to do :)
2021-11-06 00:52:23 +0100 <joel135> hmm, let me think about that for a moment
2021-11-06 00:53:19 +0100uiltondutra(~uiltondut@45.183.251.42) ()
2021-11-06 00:53:26 +0100 <joel135> is this related to what you wrote above? >>> also an interesting "duality" of sorts between logic variables and skolems/atoms emerged
2021-11-06 00:53:40 +0100 <ski> yes
2021-11-06 00:54:39 +0100faultline(~christian@nat-eduroam-01.scc.kit.edu)
2021-11-06 00:54:47 +0100 <syd> Can't Constraint Handling Rules help with that kind of thing? miniKanren doesn't have range constraints, but it does have (=/=) and asbent(o).
2021-11-06 00:55:02 +0100 <ski> you can define `false' as `\succeed fail -> fail', and `true' as `\succeed fail -> succeed fail'. the first fails immediately. the second succeeds, but if later code attempts to redo it (asking for another solution), it fails
2021-11-06 00:55:35 +0100faultline(~christian@nat-eduroam-01.scc.kit.edu) (Remote host closed the connection)
2021-11-06 00:56:25 +0100 <ski> disjunction `g0 \/ g1' is `\succeed fail -> g0 succeed (g1 succeed fail)', and conjunction `g0 /\ g1' is `\succeed fail0 -> g0 (\fail1 -> g1 gail1 succeed) fail0'
2021-11-06 00:56:42 +0100 <ski> here, a goal is construed as having type `(o -> o) -> (o -> o)'
2021-11-06 00:56:52 +0100faultline(~christian@nat-eduroam-01.scc.kit.edu)
2021-11-06 00:57:23 +0100 <ski> (if you implement this in a strict language, you'll have to sprinkle some `() ->'s in there, to delay stuff appropriately)
2021-11-06 00:57:48 +0100 <ski> syd : CHR helping with what ?
2021-11-06 00:58:32 +0100 <syd> the length of xs elements having to be known, even if it isn't instantiated yet
2021-11-06 00:58:41 +0100 <ski> CHR is a paradigm of forward-chaining (reasoning forwards from assumptions/facts/axioms), embedded in Prolog (which is natively backward-chaining, reasoning backwards from the goal)
2021-11-06 00:58:55 +0100 <joel135> succeed : o -> o ?
2021-11-06 00:59:00 +0100 <ski> yes
2021-11-06 00:59:49 +0100 <ski> (if you like, you could eta-expand my definition of disjunction and conjunction above a bit, specifically eta-expand `succeed' in the body .. but i figured i'd avoid some clutter)
2021-11-06 00:59:59 +0100 <syd> perhaps I'm erroneously assuming CHR is related to miniKanren constraints, but you can have side conditions like the query variable being x succeeding, such that it is not equal to some other value, or it is absent from another query variable which is a list etc.
2021-11-06 01:00:12 +0100 <ski> (oh, and as i said, disjunction is addition, and conjunction is multiplication)
2021-11-06 01:00:40 +0100 <syd> anyway I'll stop chiming in, it's rude to interrupt.
2021-11-06 01:00:49 +0100 <ski> no, no worry !
2021-11-06 01:01:13 +0100 <joel135> no problem from my side either!
2021-11-06 01:01:38 +0100Gurkenglas(~Gurkengla@dslb-002-203-144-204.002.203.pools.vodafone-ip.de) (Ping timeout: 260 seconds)
2021-11-06 01:01:48 +0100 <syd> appreciate it :)
2021-11-06 01:01:53 +0100 <joel135> i see that _\/_ is like addition of Church numerals, i am not seeing that _/\_ is multiplication
2021-11-06 01:02:26 +0100 <joel135> oh sorry there was a linewrap that i missed. let me retry reading it
2021-11-06 01:03:27 +0100 <ski> syd : anyway, possibly "the length of xs elements having to be known, even if it isn't instantiated yet" was a misunderstanding (possibly due to me being a bit too vague) .. i meant that i'd prefer it being allowed if the elements themselves were (initially) unknown/uninstantiated (so, to-be output), while the length (the skeleton of the list) would still be known
2021-11-06 01:03:48 +0100 <ski> (so, if the length is know, then it definitely is "instantiated")
2021-11-06 01:04:21 +0100 <ski> joel135 : perhaps i'd help to eta-reduce conjunction ?
2021-11-06 01:04:23 +0100cosimone(~user@93-44-186-19.ip98.fastwebnet.it) (Ping timeout: 256 seconds)
2021-11-06 01:04:43 +0100 <joel135> does `g1 gail1 succeed` really have the arguments in the right order?
2021-11-06 01:04:57 +0100yushyin(rzPUwQNnp2@karif.server-speed.net) (Quit: WeeChat 3.3)
2021-11-06 01:04:57 +0100 <ski> oh, sorry. yea, i just noticed that was wrong order
2021-11-06 01:05:06 +0100yushyin(XNontZhIIh@karif.server-speed.net)
2021-11-06 01:05:28 +0100 <ski> (g0 /\ g1) succeed fail = g0 (g1 succeed) fail
2021-11-06 01:05:33 +0100 <ski> (g0 /\ g1) succeed = g0 (g1 succeed)
2021-11-06 01:05:41 +0100 <ski> g0 /\ g1 = g0 . g1
2021-11-06 01:06:07 +0100 <joel135> these names "succeed" and "fail" are very intriguing.
2021-11-06 01:06:21 +0100 <ski> it's standard terminology in logic programming
2021-11-06 01:06:39 +0100 <joel135> yes but in the context of Church numerals
2021-11-06 01:07:09 +0100 <ski> although, sometimes, (in "four-port execution model"), "exit" would be used instead of "fail". also "redo" would be used. but `redo' is a failure continuation, "seen from the other side"
2021-11-06 01:07:38 +0100 <syd> (define succeed (== #t #t)) and (define fail (== #t #f)) is how I've seen them, fwiw.
2021-11-06 01:08:30 +0100zincy_(~zincy@2a00:23c8:970c:4801:350f:7ee:191a:6f65)
2021-11-06 01:08:32 +0100 <syd> oh, no idea about the relation to church numerals, missed that bit sorry.
2021-11-06 01:08:55 +0100 <joel135> i see, this http://www.cs.otago.ac.nz/cosc347/References/LP/LeedsTutorial/node48.html kind of thing
2021-11-06 01:08:56 +0100 <ski> first you Call a predicate. it may then Exit, having instantiated some variables, passing control to later code, which may further down the line backtrack back to this point (undoing said instantiations), Redo-ing the call (asking for alternative solutions). after a sequence of (zero or more) Exit-Redo pairs, the call will eventually Fail
2021-11-06 01:09:34 +0100 <joel135> is it a coincidence that there are four o's in (o -> o) -> (o -> o) just like this box has four ports?
2021-11-06 01:09:49 +0100 <ski> no
2021-11-06 01:09:54 +0100 <joel135> ok
2021-11-06 01:10:59 +0100 <ski> {- call :: -} ({- exit,succeed :: -} ({- redo :: -} o) -> o) -> (({- fail :: -} o) -> o)
2021-11-06 01:12:30 +0100 <ski> or, if you want to associate the ports with the results of the associated underlying invokations :
2021-11-06 01:13:12 +0100 <ski> (({- redo -} o) -> ({- exit -} o)) -> (({- fail -} o) -> ({- call -} o))
2021-11-06 01:13:14 +0100zincy_(~zincy@2a00:23c8:970c:4801:350f:7ee:191a:6f65) (Ping timeout: 268 seconds)
2021-11-06 01:14:41 +0100 <joel135> i see
2021-11-06 01:15:07 +0100 <joel135> could you then imagine what ((o -> o) -> (o -> o)) -> ((o -> o) -> (o -> o)) would mean in the context of logic programming?
2021-11-06 01:16:23 +0100 <ski> (in a more practical implementation, there'd also be a "Commit" port, asking a predicate call to commit to the current solution, discarding remaining alternative ones, cleaning up resources. and, commonly, there's also an "Exception" port, for exception handling. and, sometimes there's an optional "Unify" port that happens just after Call and Redo, corresponding to "head unifications" in a predicate clause
2021-11-06 01:16:29 +0100 <ski> (more or less, like pattern-matching on arguments left of the `='))
2021-11-06 01:16:55 +0100 <ski> well .. i haven't considered it from your polynomial perspective ..
2021-11-06 01:17:13 +0100 <ski> but doing that kind of thing is exactly what i did, for my goal implications
2021-11-06 01:18:51 +0100chexum(~quassel@gateway/tor-sasl/chexum) (Remote host closed the connection)
2021-11-06 01:18:59 +0100 <joel135> by the way, i also found some other truly beautiful stuff when investigating the interrelationships between o, (o -> o), ((o -> o) -> (o -> o)), &c but let's cotinue talking about your stuff
2021-11-06 01:19:10 +0100 <ski> the usual CPS encoding of LP goals, with backtracking, is `ContT () (ContT o m)', for some suitable base monad `m' (e.g. `IO' or `ST s', since you likely want to implement logic variables via mutation, and possibly you want to be able to do I/O as well)
2021-11-06 01:19:15 +0100chexum(~quassel@gateway/tor-sasl/chexum)
2021-11-06 01:19:32 +0100 <ski> (well, i guess `o' would also be `()' there)
2021-11-06 01:20:18 +0100merijn(~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 260 seconds)
2021-11-06 01:20:35 +0100 <ski> so, what i do for implication, `( Antecedent => Consequent )', is i shift the continuation levels for `Antecedent', one step. so, `Antecedent' (but not `Consequent') now is interpreted a la `((o -> o) -> (o -> o)) -> ((o -> o) -> (o -> o))'
2021-11-06 01:21:20 +0100 <ski> except, of course this implication may itself be left-nested in an outer implication, in which case our `Antecedent' has four continuation levels, and `Consequent' has three .. and so on
2021-11-06 01:21:43 +0100faultline(~christian@nat-eduroam-01.scc.kit.edu) (Remote host closed the connection)
2021-11-06 01:22:16 +0100 <ski> (the top-level call fixes/picks the number of continuation levels to two, using the base monad `m' under that. implication chooses the number of levels for `Antecedent' to be one more, so that's where the extra levels come from)
2021-11-06 01:22:27 +0100faultline(~christian@nat-eduroam-01.scc.kit.edu)
2021-11-06 01:23:06 +0100 <joel135> wait wait. this sounds super cool for lack of a better word
2021-11-06 01:23:44 +0100Lord_of_Life(~Lord@user/lord-of-life/x-2819915) (Ping timeout: 268 seconds)
2021-11-06 01:24:01 +0100Lord_of_Life(~Lord@user/lord-of-life/x-2819915)
2021-11-06 01:24:17 +0100 <unit73e> so I was doing texture clipping and now I have to deal with aeson. I'll just make a pause...
2021-11-06 01:25:09 +0100 <joel135> do you think of this ((o -> o) -> (o -> o)) -> ((o -> o) -> (o -> o)) as ((O -> O) -> (O -> O)) or as (_ -> ((o -> o) -> (o -> o))), if the question makes sense?
2021-11-06 01:25:46 +0100 <ski> (fun fact .. this all started by me boredly translating a Sudoku solver from Common Lisp to Prolog, getting side-tracked on how to nicely represent arrays (quickly jumping to multi-dimensional ones), wanting to write higher-order predicates for iterating over them, then noticing some weird unexpected (incorrect) behaviour, attempting to fix it with low-level (mutation) primitives (which can possibly violate
2021-11-06 01:25:53 +0100 <ski> the declarative/pure logical reading of the code) .. then, when that didn't work (i suspect because of optimizations assuming purity, or somesuch), started thinking about what i wanted, got into thinking about how to "backtrack backtracking")
2021-11-06 01:26:33 +0100 <unit73e> in college the teachers made a competition of who could make the best sodoku solver
2021-11-06 01:26:45 +0100 <unit73e> the teacher that won used prolog
2021-11-06 01:26:55 +0100 <unit73e> it was so fast that the solution was faster than printing
2021-11-06 01:27:00 +0100 <joel135> is this "shift" a variant of this from above? >>> exponentiation seems to require `Codensity' (iow, you pass around `forall o.'-ed stuff, rank-2)
2021-11-06 01:27:51 +0100 <ski> joel135 : hmm .. implication definitely eliminates the top continuation layer of `Antecent', which i guess would correspond to your second alternative ? .. but when thinking about the execution of `Antecedent' itself, in isolation, i would say the first alternative, i think
2021-11-06 01:28:07 +0100 <unit73e> the teacher that was talking about this competition used Java (lol) and he was saying the one that used prolog cheated because it was prolog
2021-11-06 01:28:42 +0100cheater(~Username@user/cheater) (Ping timeout: 260 seconds)
2021-11-06 01:29:42 +0100 <syd> (what is it with punning usernames here?! I like it.)
2021-11-06 01:29:45 +0100 <ski> "normally", success and failure continuations are not mixed up with each other. but for implication, when `Consequent' succeeds, that is then interpreted by `Antecedent' as a failure, a prod for it to generate another solution (spawning a new, conceptually separate, call to `Consequent')
2021-11-06 01:30:40 +0100 <joel135> i need to think more about what you just wrote ^
2021-11-06 01:30:51 +0100 <joel135> but in the meanwhile, assuming Antecedent has type ((o -> o) -> (o -> o)) -> ((o -> o) -> (o -> o)) and Consequent has type ((o -> o) -> (o -> o)), is Antecedent => Consequent simply interpreted as Antecedent Consequent of type ((o -> o) -> (o -> o)) ?
2021-11-06 01:30:56 +0100 <ski> unit73e : hm, did it use some constraint programming ? imho, that would be ideal
2021-11-06 01:31:25 +0100 <ski> "is this "shift" a variant of this from above?" -- i think it's related, at least
2021-11-06 01:32:32 +0100 <ski> yes, `Consequent' and `( Antecedent => Consequent )' would have the same type, the same number of continuation levels
2021-11-06 01:33:16 +0100 <joel135> and if you have antecedent (lowercase) of type ((O -> O) -> (O -> O)) where O is a type variable, would you somehow "upgrade" it to Antecedent by setting O := (o -> o) ?
2021-11-06 01:33:37 +0100 <ski> yes
2021-11-06 01:33:47 +0100 <ski> (modulo some fiddly stuff with the base monad)
2021-11-06 01:34:22 +0100 <joel135> do you know what the inverse of this "upgrade" operation is? this is what i referred to above as "some other truly beautiful stuff"
2021-11-06 01:35:21 +0100 <ski> hm, i don't think so
2021-11-06 01:37:09 +0100 <joel135> the "downgrade" from forall o. (((o -> o) -> (o -> o)) -> ((o -> o) -> (o -> o))) to forall O. ((O -> O) -> (O -> O)) is a nondeterministic operation that basically takes a polynomial as input and chooses a term (in the sense of polynomials) of this polynomial, and returns its exponent.
2021-11-06 01:38:06 +0100 <ski> hmm .. exponent
2021-11-06 01:38:54 +0100yauhsien(~yauhsien@118-167-41-229.dynamic-ip.hinet.net)
2021-11-06 01:38:59 +0100random-jellyfish(~random-je@user/random-jellyfish) (Ping timeout: 256 seconds)
2021-11-06 01:39:03 +0100 <ski> i wonder if there's possibly two distinct "downgrades" (or two distinct "upgrades" ?)
2021-11-06 01:40:15 +0100 <joel135> if a term T of type forall o. (((o -> o) -> (o -> o)) -> ((o -> o) -> (o -> o))) is thought of as a type containing a free type variable (the polynomial x : (o -> o) -> (o -> o) being this variable) and you have a partial term t of this type T(x), then the type downgrade(T)_t : forall O. (O -> O) -> (O -> O) is the type of holes of type x inside t : T(x).
2021-11-06 01:41:30 +0100 <ski> g₀ ⇒ g₁ : Ω ⊣ g₀,g₁ : Ω
2021-11-06 01:41:37 +0100 <ski> (g₀ ⇒ g₁) ω s f = g₀ (ω → ω) (λ s₀ ↦ λ f′ ↦
2021-11-06 01:41:43 +0100 <ski> g₁ ω (λ f″ ↦ s₀ f″) f′) (λ f‴ ↦ s f‴) f
2021-11-06 01:41:46 +0100 <ski> = g₀ (ω → ω) (g₁ ω) s f
2021-11-06 01:42:20 +0100 <joel135> there may in principle be k different upgrades when you have k levels of (_->_)-nesting, but i haven't thought it through fully. for instance a relatable example is that you could take a *polynomial* p as input and return the upgraded *operator* p(d/dx) as output.
2021-11-06 01:42:20 +0100 <ski> that's my implication, given ⌜Ω = (ω :) ⋆ → (ω → ω) → (ω → ω)⌝
2021-11-06 01:42:55 +0100zincy_(~zincy@2a00:23c8:970c:4801:350f:7ee:191a:6f65)
2021-11-06 01:43:24 +0100 <ski> (hm, i guess you can think of `x' as an oracle ..)
2021-11-06 01:43:38 +0100yauhsien(~yauhsien@118-167-41-229.dynamic-ip.hinet.net) (Ping timeout: 260 seconds)
2021-11-06 01:43:45 +0100 <joel135> (the level of operators being something like ((((o -> o) -> (o -> o)) -> ((o -> o) -> (o -> o)))) -> ((((o -> o) -> (o -> o)) -> ((o -> o) -> (o -> o)))))
2021-11-06 01:44:14 +0100 <joel135> hang on, i need to read what you wrote
2021-11-06 01:46:36 +0100 <joel135> i can't parse Ω = (ω :) ⋆ → (ω → ω) → (ω → ω)
2021-11-06 01:47:15 +0100 <ski> Omega = (o : Set) -> (o -> o) -> (o -> o) -- in Agda notation
2021-11-06 01:47:47 +0100zincy_(~zincy@2a00:23c8:970c:4801:350f:7ee:191a:6f65) (Ping timeout: 264 seconds)
2021-11-06 01:48:12 +0100 <joel135> ok right, you use ω → ω for ω
2021-11-06 01:48:13 +0100 <ski> `Omega' just being a type of "logic programming goals/queries", which also "just happens" to be church numerals
2021-11-06 01:49:11 +0100 <ski> (having stripped away everything from the type that one'd use practically, for say instantiation / logic programming, or I/O, just focusing on the basic backtracking behaviour)
2021-11-06 01:49:31 +0100 <ski> (er, s/logic programming/logic variables/)
2021-11-06 01:49:55 +0100 <joel135> right
2021-11-06 01:51:05 +0100SeungheonOh(~Thunderbi@2600:1700:5168:1400:1574:2437:4f0d:50e6)
2021-11-06 01:51:49 +0100 <ski> (fwiw, i'm not following "you have a partial term t of this type T(x)" .. `t' being (thought of as) an inhabitant of a polynomial `a_0 + a_1*x + a_2*x^2 + ..' ?)
2021-11-06 01:52:52 +0100 <joel135> (let's maybe use the names ℕ₀(o) = o, ℕₙ₊₁(o) = (ℕₙ(o) → ℕₙ(o)) and ℕₙ = ∀o. ℕₙ(o) sometimes for readability, so e.g. ℕ₃ = Poly)
2021-11-06 01:53:21 +0100 <ski> (fwiw, when i said `Consequent' and `( Antecedent => Consequent )' would have "the same number of continuation levels", i mean that the same `o' that is passed to the latter, is passed (type application, polymorphic instantiation) to the former)
2021-11-06 01:55:06 +0100 <joel135> a partial term is a term that is specified as far as the type is specified. the type variable x is considered to be an unknown, so it is not clear what a term of type T(x) is precisely yet. a partial term t : T(x) thus contains holes of type x but no other holes. this is what i mean by partial here.
2021-11-06 01:55:35 +0100 <ski> "wait wait. this sounds super cool for lack of a better word" -- yeah, that's what i first thought, when discovering this stuff :D
2021-11-06 01:55:55 +0100 <joel135> :D
2021-11-06 01:56:39 +0100 <ski> hm, holes
2021-11-06 01:57:02 +0100 <ski> (makes me wonder about relation to McBride type differentiation)
2021-11-06 01:57:26 +0100 <joel135> holes ... derivatives ... of types or of polynomials :)
2021-11-06 01:57:40 +0100 <ski> yup
2021-11-06 01:58:46 +0100 <ski> <joel135> is this related to what you wrote above? >>> also an interesting "duality" of sorts between logic variables and skolems/atoms emerged
2021-11-06 01:59:40 +0100 <ski> so, i realized that, after doing this shift of one continuation level, when going to `Antecedent', i couldn't let any instantiations made by `Antecedent' "escape" the implications
2021-11-06 02:00:17 +0100 <ski> because the solutions of `Antecedent' are merely hypothetical .. by the time the implication has succeeded, `Antecedent' has exhausted its solutions, and failed finally
2021-11-06 02:00:42 +0100 <ski> this makes sense, since there's a polarity shift/swap, the antecedent is in a negated context
2021-11-06 02:01:10 +0100 <ski> but, i'd still like `Consequent' to be able to make instantiations, which survived .. so the question was how to achieve this
2021-11-06 02:01:18 +0100ubert(~Thunderbi@p200300ecdf4fcafee019fddc82d0353e.dip0.t-ipconnect.de) (Ping timeout: 260 seconds)
2021-11-06 02:01:24 +0100ub(~Thunderbi@p200300ecdf4fca30e019fddc82d0353e.dip0.t-ipconnect.de)
2021-11-06 02:01:34 +0100 <joel135> (i don't have quite enough practical experience with logic programming to have intuition for the things you just said)
2021-11-06 02:01:49 +0100 <ski> `Consequent' here wouldn't (usually) communicate directly to the surrounding goals, and their logic variables, but only do so *via* `Antecedent'
2021-11-06 02:02:54 +0100 <joel135> i think i need to try studying your code. do you still have it?
2021-11-06 02:03:16 +0100 <ski> in the example with enumerating elements of a collection, `Antecedent' would set up a *temporary* link between an element of the collection, and a logic variable, and then `Consequent' would go on to instantiate the element to something, *via* this link. after that, the link would be removed (and a new link to a different element be instated), but the instantiation to the element ought still to persist
2021-11-06 02:03:43 +0100ububert
2021-11-06 02:04:10 +0100raehik(~raehik@cpc95906-rdng25-2-0-cust156.15-3.cable.virginm.net) (Ping timeout: 260 seconds)
2021-11-06 02:04:48 +0100 <ski> hm. i know where i have one version, however it might still have a bug (in unification machinery, iirc), that i managed to fix in the end (turned out to be a silly mistake, like a boolean flip, or wrong argument passed, iirc)
2021-11-06 02:05:38 +0100 <joel135> when you say "link between ... and a logic variable" is "a logic variable" referring to X or Xs? ( member(X,Xs) => between(1,6,X) )
2021-11-06 02:06:04 +0100 <joel135> i am guessing X
2021-11-06 02:06:17 +0100 <ski> when we're *using* a polymorphic operation, say `length :: forall a. [a] -> Int', then `a' gets replaced by a logic variable, so that we have `length :: [_a] -> Int' for this particular occurance/use of `length', and then unification will instantiate `_a' to something appropriate
2021-11-06 02:06:24 +0100 <ski> `X', yes
2021-11-06 02:06:29 +0100 <joel135> ok
2021-11-06 02:07:06 +0100burnsidesLlama(~burnsides@dhcp168-023.wadham.ox.ac.uk) (Remote host closed the connection)
2021-11-06 02:08:06 +0100 <ski> but when we're defining `length', checking its definition, `a' becomes replaced by a skolem constant, say `?a', so that we're checking `length :: [?a] -> Int'. `?a' is an opaque/abstract type that is only known to be equal to itself
2021-11-06 02:08:25 +0100 <ski> the same phenomenon happens in logic programming
2021-11-06 02:09:46 +0100acidsys(~LSD@2.lsd.systems) (Excess Flood)
2021-11-06 02:10:04 +0100 <ski> if you have a goal `some [X] ( member(X,Xs) )' (Mercury syntax) / `sigma X\ member X Xs' (lambdaProlog syntax), then `X' will become a logic variable, that can be further instantiated, when we attempt to unify it with stuff
2021-11-06 02:10:21 +0100acidsys(~LSD@2.lsd.systems)
2021-11-06 02:10:46 +0100 <joel135> (i think ghc referred to skolem-something before i changed `type Poly` to `data Poly`)
2021-11-06 02:11:59 +0100 <ski> if you have a goal `all [X] ( X = X )' / `pi X\ X = X', then `X' will become a skolem constant. this way, if you attempt the goal `pi X\ pi Y\ X = Y', you'll compare two skolem constants that are not known to be equal, and therefore this goal will fail
2021-11-06 02:12:21 +0100 <ski> (while, using `sigma' instead of `pi', it would succeed)
2021-11-06 02:13:08 +0100 <ski> so, considering `( member(X,Xs) => between(1,6,X) )', which logically ought to be treated as `all [X] ( member(X,Xs) => between(1,6,X) )' here, `X' ought to become a skolem constant
2021-11-06 02:13:29 +0100Athas(athas@2a01:7c8:aaac:1cf:a0d4:8908:cfdb:b9c0) (Quit: ZNC 1.8.2 - https://znc.in)
2021-11-06 02:13:45 +0100Athas(athas@2a01:7c8:aaac:1cf:a0d4:8908:cfdb:b9c0)
2021-11-06 02:14:14 +0100 <ski> but, once inside the antecedent (which involves shifting continuation levels), we'd like `X' to not act like a constant (we'd not like to instantiate the element in the collection `Xs' with some opaque constant), but rather as a logic variable, which is now known to be equal to whatever the element is equal to
2021-11-06 02:15:50 +0100 <unit73e> ski, no idea what he did but from what I remember it was based on just telling the rules
2021-11-06 02:15:51 +0100 <ski> so .. from this, i got the idea that, perhaps, we could represent logical variables, and skolem constants, in the *same* way, except for a single bit/boolean that tells which is which .. and then, whenever you shift continuation levels (odd number of levels), you flip a global boolean flag that changes the interpretation of the bit in logic variables and skolems !
2021-11-06 02:16:17 +0100 <ski> and the amazing thing is that this crazy idea actually worked ! :D
2021-11-06 02:16:17 +0100 <joel135> hmm
2021-11-06 02:16:19 +0100zincy_(~zincy@2a00:23c8:970c:4801:350f:7ee:191a:6f65)
2021-11-06 02:16:54 +0100 <joel135> i really want to try this
2021-11-06 02:17:21 +0100 <geekosaur> covariance/contravariance?
2021-11-06 02:17:39 +0100geekosaurdoesn't quite follow all of the above, but what the heck
2021-11-06 02:19:01 +0100 <joel135> i have no intuition for this logic variable vs skolem atom distinction though
2021-11-06 02:19:14 +0100 <ski> (i know my implementation have another problem, causing unsoundness. basically, for `sigma X\ pi Y\ X = Y', what i've said above is not enough. this query ought to fail, there is not something which is equal to everything. so, one needs to also ensure that skolems don't "escape" in some sense. it seems that one way one could do this is adding timestamps of some kind to logic variables and skolems, and check
2021-11-06 02:19:20 +0100 <ski> them, when unifying .. i believe this can be done, but i haven't worked through the details)
2021-11-06 02:19:55 +0100 <ski> (recently, i was (re)looking at Lolli, a linear logic programming language, and they did something like this, that i'd have to study to understand how it works)
2021-11-06 02:20:00 +0100 <joel135> it seems like logic variables are "positive" in the sense of girard whereas skolem atoms are "negative"
2021-11-06 02:20:31 +0100zincy_(~zincy@2a00:23c8:970c:4801:350f:7ee:191a:6f65) (Ping timeout: 245 seconds)
2021-11-06 02:20:51 +0100 <ski> in terms of typechecking, the usual term is "meta variable" (or maybe "placeholder"), rather than "logic variable". but it's the same idea
2021-11-06 02:21:21 +0100 <ski> note that it's incorrect to think that logic variables are associated with existential quantification, and skolems with universal quantification
2021-11-06 02:21:55 +0100 <joel135> ok good that you pointed that out
2021-11-06 02:22:07 +0100pretty_dumm_guy(trottel@gateway/vpn/protonvpn/prettydummguy/x-88029655) (Quit: WeeChat 3.3)
2021-11-06 02:22:12 +0100lavaman(~lavaman@98.38.249.169) (Remote host closed the connection)
2021-11-06 02:22:35 +0100 <ski> logic variables are generated by existential goals *and* universal clauses. while skolems are generated by universal goals and existential clauses (except usually the last thing isn't allowed in logic programming. i think possibly some experimental deductive databases may allow such)
2021-11-06 02:23:43 +0100 <ski> similarly, checking the callee/definer/implementor/producer of a `forall a. ..a..' involves skolems, while the caller/user/consumer involves meta variables
2021-11-06 02:23:55 +0100 <ski> (and the opposite, for `exists a. ..a..')
2021-11-06 02:24:46 +0100ec(~ec@gateway/tor-sasl/ec) (Remote host closed the connection)
2021-11-06 02:25:11 +0100 <ski> clauses are the stuff that you assume, the axioms/rules/hypotheses that you tell the logic programming system to believe. goals are the queries/questions that you ask the system to check, to try to solve, generate solutions for (thinking about solving equation systems is a nice analogy)
2021-11-06 02:25:20 +0100ec(~ec@gateway/tor-sasl/ec)
2021-11-06 02:26:41 +0100 <ski> in Prolog, clauses are either facts, like `member(X,[X|_]).', or rules, like `member(X,[_|Xs]) :- member(X,Xs).' (`:-' is reverse implication, `<='). `member(X,Xs)' here, the body of the rule, is a goal
2021-11-06 02:27:24 +0100 <ski> (and variables are implicitly universally quantified around clauses. if the variable only occurs in the body, then this is equivalent to it being implicitly existentially quantified in the body)
2021-11-06 02:29:48 +0100lbseale_(~lbseale@user/ep1ctetus) (Read error: Connection reset by peer)
2021-11-06 02:29:58 +0100 <unit73e> geekosaur, the covariance/contravariance has to do with subtyping. it's talked a lot in scala because a list of cats should be compatible with a list of animals, and that's because it's covariant.
2021-11-06 02:30:01 +0100 <joel135> ok so from one perspective is `append([0,1,2],[3,4],L)` is a clause and `L` is a goal. and from another perspective a clause is like a polynomial ideal and a goal is like a polynomial that you're examining in relation to this ideal (maybe testing for membership or similar)
2021-11-06 02:30:10 +0100 <ski> unit73e : anyway, Prolog is great for non-deterministic search :) (although, for larger search spaces, you'd usually want to try to be smarter, if you can, pruning irrelevant sub-search-trees, or "failing earlier" (reordering goals (conjuncts) so that something that's (more) likely to fail is checked first, so that you avoid wastefully checking an expensive condition)
2021-11-06 02:30:50 +0100 <joel135> or maybe i am wrong to call `L` a goal and it is `member(X,Xs)` that is the goal as you say.
2021-11-06 02:31:26 +0100 <ski> (and constraint logic programming (CLP) can be great at implicitly doing both of those, while keeping the source code rather readable .. a bit similar to how laziness can improve modularity, by allowing reasonable efficiency while maintaining separation of concerns / modularity)
2021-11-06 02:32:10 +0100 <ski> joel135 : yes, `L' is a term (a variable in this case), and `member(X,Xs)' is a goal
2021-11-06 02:32:22 +0100 <unit73e> functors are a classic for the covariant/contravariant mambo jambo, it doesn't matter that much tbh
2021-11-06 02:32:43 +0100shriekingnoise(~shrieking@186.137.144.80) (Quit: Quit)
2021-11-06 02:33:29 +0100 <ski> (whether something is a clause or goal can't, in general, be determined in isolation, just by looking at the thing is question. what determines it is the context in which it occurs. so it's an extrinsic notion, not an intrisic)
2021-11-06 02:34:28 +0100 <joel135> > logic variables are generated by existential goals *and* universal clauses. while skolems are generated by universal goals and existential clauses
2021-11-06 02:34:29 +0100 <lambdabot> error:
2021-11-06 02:34:30 +0100 <lambdabot> Variable not in scope:
2021-11-06 02:34:30 +0100 <lambdabot> logic :: t0 -> t1 -> t2 -> t3 -> t4 -> t5 -> t Bool -> Boolerror: Vari...
2021-11-06 02:34:37 +0100shriekingnoise(~shrieking@186.137.144.80)
2021-11-06 02:34:49 +0100 <ski> @botsmack
2021-11-06 02:34:49 +0100 <lambdabot> :)
2021-11-06 02:35:03 +0100 <joel135> this feels reminiscent of the distinction between additive and multiplicative connectives
2021-11-06 02:35:11 +0100 <joel135> rather than positive and negative connectives
2021-11-06 02:35:31 +0100syd(~syd@cpc91646-hart11-2-0-cust432.11-3.cable.virginm.net) (Read error: No route to host)
2021-11-06 02:35:47 +0100 <ski> meta/logic variable vs. skolem is an operational/procedural issue
2021-11-06 02:35:47 +0100 <nitrix> Poor ski, perpetually doomed now talking about logic programming. I'm sorry I did this to you.
2021-11-06 02:35:57 +0100machinedgod(~machinedg@135-23-192-217.cpe.pppoe.ca) (Quit: Lost terminal)
2021-11-06 02:36:05 +0100 <ski> nitrix : nah, you didn't, that i can recall :b
2021-11-06 02:36:06 +0100 <joel135> which i think leads us back to the notion of "upgrade" which does connect addition to multiplication, just like the exponential function does
2021-11-06 02:36:17 +0100 <unit73e> logic programming does have it's uses
2021-11-06 02:36:24 +0100 <geekosaur> unit73e, I was asking if the flipping between logic variables and skolems could be seen as co- vs. contravariance, not asking what they were
2021-11-06 02:36:45 +0100 <unit73e> yeah I found it strange if you didn't know lol
2021-11-06 02:37:35 +0100 <unit73e> regardless, scala guys like to talk about that
2021-11-06 02:37:45 +0100 <unit73e> with all the + and - stuff
2021-11-06 02:37:46 +0100 <joel135> this kind of fits with your finding that one changes between variables and atoms when going inside the antecedent position of an implication, but it is still a bit strange that one should alternate back and forth
2021-11-06 02:37:51 +0100machinedgod(~machinedg@135-23-192-217.cpe.pppoe.ca)
2021-11-06 02:38:46 +0100 <ski> geekosaur : contravariance represents a flipping of polarity (while covariance is a non-flipping). logic variables vs. skolems is not about flipping or not, but rather is (in my prototype) what was being flipped around (exchanging the interpretation so that logic variables are now interpreted as skolems, and vice versa, upon flipping)
2021-11-06 02:40:14 +0100 <unit73e> he.. I also find it confusing. I kind of get it but to me it's much simpler to think as "can I polymorph up or down"
2021-11-06 02:40:54 +0100 <unit73e> because I see the image in my head
2021-11-06 02:47:36 +0100harveypwca(~harveypwc@2601:246:c180:a570:3828:d8:e523:3f67)
2021-11-06 02:48:39 +0100a6a45081-2b83(~aditya@2603-6080-0800-8e4a-0000-0000-0000-01a8.res6.spectrum.com)
2021-11-06 02:49:38 +0100 <joel135> going back to the upgrade/downgrade business: one way of thinking about this that i found is that this downgrade styled "hole" together with another downgrade (not competely sure if that it qualifies as a "downgrade" though) styled "partial term" combine to form the basis for a type checker.
2021-11-06 02:50:21 +0100 <joel135> this connects again to your question earlier about whether there could be several differerent upgrades/downgrades
2021-11-06 02:51:46 +0100a6a45081-2b83(~aditya@2603-6080-0800-8e4a-0000-0000-0000-01a8.res6.spectrum.com) (Read error: Connection reset by peer)
2021-11-06 02:51:49 +0100 <joel135> <ski> i wonder if there's possibly two distinct "downgrades" (or two distinct "upgrades" ?)
2021-11-06 02:53:00 +0100zincy_(~zincy@2a00:23c8:970c:4801:350f:7ee:191a:6f65)
2021-11-06 02:56:03 +0100a6a45081-2b83(~aditya@2603-6080-0800-8e4a-0000-0000-0000-01a8.res6.spectrum.com)
2021-11-06 02:56:19 +0100 <joel135> i am imagining that the collection of all possible upgrades and downgrades form a simplicial set. perhaps ℕ₃ = Poly is like a triangle, of which the notions of "partial term" and "hole" are two edges that meet together at a single vertex, which is the source of the induction-recursion needed to type these notions.
2021-11-06 02:58:04 +0100zincy_(~zincy@2a00:23c8:970c:4801:350f:7ee:191a:6f65) (Ping timeout: 268 seconds)
2021-11-06 02:58:19 +0100a6a45081-2b83(~aditya@2603-6080-0800-8e4a-0000-0000-0000-01a8.res6.spectrum.com) (Read error: Connection reset by peer)
2021-11-06 02:58:48 +0100a6a45081-2b83(~aditya@2603-6080-0800-8e4a-0000-0000-0000-01a8.res6.spectrum.com)
2021-11-06 02:59:36 +0100DNH(~DNH@2a02:8108:1100:16d8:e9ee:3bd5:4988:8148) (Quit: Textual IRC Client: www.textualapp.com)
2021-11-06 02:59:54 +0100a6a45081-2b83(~aditya@2603-6080-0800-8e4a-0000-0000-0000-01a8.res6.spectrum.com) (Remote host closed the connection)
2021-11-06 03:00:33 +0100hololeap(~hololeap@user/hololeap) (Remote host closed the connection)
2021-11-06 03:01:48 +0100v01d4lph4(~v01d4lph4@user/v01d4lph4)
2021-11-06 03:01:59 +0100hololeap(~hololeap@user/hololeap)
2021-11-06 03:03:25 +0100Cajun(~Cajun@user/cajun)
2021-11-06 03:06:23 +0100v01d4lph4(~v01d4lph4@user/v01d4lph4) (Ping timeout: 264 seconds)
2021-11-06 03:07:34 +0100hololeap(~hololeap@user/hololeap) (Remote host closed the connection)
2021-11-06 03:07:41 +0100unit73e(~emanuel@2001:818:e8dd:7c00:32b5:c2ff:fe6b:5291) (Quit: Leaving)
2021-11-06 03:08:33 +0100machinedgod(~machinedg@135-23-192-217.cpe.pppoe.ca) (Ping timeout: 268 seconds)
2021-11-06 03:08:34 +0100 <Cajun> ive been looking into effect systems and found the usual sort: mtl, fused effects, polysemy, freer-simple/freer, and eff. the ones based on free monads seem really cool, but the others tend to be faster (eff is the exception). i also watched the vod of the eff dev mentioning issues with scoped effects which was highly discouraging. im wondering in
2021-11-06 03:08:34 +0100 <Cajun> general whats the best system to use, considering speed and ease of use?
2021-11-06 03:08:46 +0100 <joel135> (and upgrading a polynomial p : ℕ₃ to an operator p(d/dx) : ℕ₄ would be the middle degeneracy that takes you from the simplex with 3 vertices to the simplex with 4 vertices)
2021-11-06 03:08:51 +0100hololeap(~hololeap@user/hololeap)
2021-11-06 03:13:56 +0100alx741(~alx741@181.196.68.55) (Quit: alx741)
2021-11-06 03:19:35 +0100merijn(~merijn@83-160-49-249.ip.xs4all.nl)
2021-11-06 03:23:27 +0100alzgh(~alzgh@user/alzgh) (Remote host closed the connection)
2021-11-06 03:28:00 +0100Tuplanolla(~Tuplanoll@91-159-69-50.elisa-laajakaista.fi) (Quit: Leaving.)
2021-11-06 03:32:11 +0100EvanR(~evan@user/evanr) (Ping timeout: 245 seconds)
2021-11-06 03:42:17 +0100jpds1(~jpds@gateway/tor-sasl/jpds) (Remote host closed the connection)
2021-11-06 03:42:42 +0100jpds1(~jpds@gateway/tor-sasl/jpds)
2021-11-06 03:43:43 +0100zincy_(~zincy@2a00:23c8:970c:4801:350f:7ee:191a:6f65)
2021-11-06 03:45:50 +0100xff0x(~xff0x@2001:1a81:5273:3700:28cd:42fe:3b9:2637) (Ping timeout: 260 seconds)
2021-11-06 03:47:41 +0100xff0x(~xff0x@2001:1a81:52b1:3000:b3ef:fedd:d143:889a)
2021-11-06 03:48:38 +0100zincy_(~zincy@2a00:23c8:970c:4801:350f:7ee:191a:6f65) (Ping timeout: 268 seconds)
2021-11-06 03:51:02 +0100merijn(~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 260 seconds)
2021-11-06 04:00:00 +0100sander(~sander@user/sander) (Quit: So long! :))
2021-11-06 04:01:29 +0100sander(~sander@user/sander)
2021-11-06 04:06:28 +0100faultline(~christian@nat-eduroam-01.scc.kit.edu) (Remote host closed the connection)
2021-11-06 04:07:45 +0100Square(~a@178.62.91.8) (Changing host)
2021-11-06 04:07:45 +0100Square(~a@user/square)
2021-11-06 04:08:19 +0100 <lyxia> Use IO and don't get into situations where you need anything else.
2021-11-06 04:08:25 +0100EvanR(~evan@2600:1700:ba69:10:98b6:b5c4:3b00:4c9a)
2021-11-06 04:13:18 +0100EvanR(~evan@2600:1700:ba69:10:98b6:b5c4:3b00:4c9a) (Ping timeout: 268 seconds)
2021-11-06 04:15:33 +0100slack1256(~slack1256@191.125.99.211)
2021-11-06 04:18:19 +0100zincy_(~zincy@2a00:23c8:970c:4801:350f:7ee:191a:6f65)
2021-11-06 04:23:11 +0100zincy_(~zincy@2a00:23c8:970c:4801:350f:7ee:191a:6f65) (Ping timeout: 268 seconds)
2021-11-06 04:34:35 +0100nosewings(~ngpc@2603-8081-3e05-e2d0-91fa-0be4-4222-fe4b.res6.spectrum.com) (Remote host closed the connection)
2021-11-06 04:39:30 +0100finn_elija(~finn_elij@user/finn-elija/x-0085643)
2021-11-06 04:39:30 +0100FinnElija(~finn_elij@user/finn-elija/x-0085643) (Killed (NickServ (Forcing logout FinnElija -> finn_elija)))
2021-11-06 04:39:30 +0100finn_elijaFinnElija
2021-11-06 04:47:30 +0100waleee(~waleee@h-98-128-228-119.NA.cust.bahnhof.se) (Ping timeout: 260 seconds)
2021-11-06 04:51:29 +0100zincy_(~zincy@2a00:23c8:970c:4801:350f:7ee:191a:6f65)
2021-11-06 04:55:52 +0100zincy_(~zincy@2a00:23c8:970c:4801:350f:7ee:191a:6f65) (Ping timeout: 268 seconds)
2021-11-06 04:56:43 +0100a6a45081-2b83(~aditya@2603-6080-0800-8e4a-0000-0000-0000-01a8.res6.spectrum.com)
2021-11-06 04:57:12 +0100 <a6a45081-2b83> how can I define something similar for `Ratio Integer` (https://hackage.haskell.org/package/memoize-0.8.1/docs/src/Data.Function.Memoize.html#memoFix)
2021-11-06 04:59:24 +0100 <a6a45081-2b83> my plan is to have `instace Memoizable (Ratio Integer) where memoize f = let f' (a,b) = f (a%b) in memoize f'`
2021-11-06 04:59:27 +0100 <a6a45081-2b83> or something like that
2021-11-06 04:59:34 +0100hiruji(~hiruji@user/hiruji) (Ping timeout: 268 seconds)
2021-11-06 05:01:02 +0100yauhsien(~yauhsien@118-167-41-229.dynamic-ip.hinet.net)
2021-11-06 05:05:34 +0100Cajun(~Cajun@user/cajun) (Quit: Client closed)
2021-11-06 05:05:42 +0100yauhsien(~yauhsien@118-167-41-229.dynamic-ip.hinet.net) (Ping timeout: 260 seconds)
2021-11-06 05:11:05 +0100mcglk(~mcglk@131.191.49.120) (Read error: Connection reset by peer)
2021-11-06 05:11:21 +0100Cajun(~Cajun@user/cajun)
2021-11-06 05:12:12 +0100 <ski> joel135 : sorry, i became stuck for a bit, trying to get my old code to work (finally managed) .. if you want to, i could send you the code
2021-11-06 05:13:47 +0100a6a45081-2b83(~aditya@2603-6080-0800-8e4a-0000-0000-0000-01a8.res6.spectrum.com) (Read error: Connection reset by peer)
2021-11-06 05:13:52 +0100mcglk(~mcglk@131.191.49.120)
2021-11-06 05:15:18 +0100bitdex(~bitdex@gateway/tor-sasl/bitdex)
2021-11-06 05:16:07 +0100img(~img@user/img) (Quit: ZNC 1.8.2 - https://znc.in)
2021-11-06 05:18:08 +0100a6a45081-2b83(~aditya@2603-6080-0800-8e4a-0000-0000-0000-01a8.res6.spectrum.com)
2021-11-06 05:18:53 +0100a6a45081-2b83(~aditya@2603-6080-0800-8e4a-0000-0000-0000-01a8.res6.spectrum.com) (Read error: Connection reset by peer)
2021-11-06 05:19:21 +0100a6a45081-2b83(~aditya@2603-6080-0800-8e4a-0000-0000-0000-01a8.res6.spectrum.com)
2021-11-06 05:19:27 +0100a6a45081-2b83(~aditya@2603-6080-0800-8e4a-0000-0000-0000-01a8.res6.spectrum.com) (Client Quit)
2021-11-06 05:19:30 +0100img(~img@user/img)
2021-11-06 05:35:04 +0100slowButPresent(~slowButPr@user/slowbutpresent) (Quit: leaving)
2021-11-06 05:35:47 +0100[itchyjunk](~itchyjunk@user/itchyjunk/x-7353470) (Read error: Connection reset by peer)
2021-11-06 05:45:25 +0100zincy_(~zincy@2a00:23c8:970c:4801:350f:7ee:191a:6f65)
2021-11-06 05:47:02 +0100zebrag(~chris@user/zebrag) (Quit: Konversation terminated!)
2021-11-06 05:47:34 +0100v01d4lph4(~v01d4lph4@user/v01d4lph4)
2021-11-06 05:47:35 +0100merijn(~merijn@83-160-49-249.ip.xs4all.nl)
2021-11-06 05:48:01 +0100ishutin(~ishutin@62-165-208-189.pool.digikabel.hu) (Ping timeout: 245 seconds)
2021-11-06 05:50:03 +0100ishutin(~ishutin@92-249-179-61.pool.digikabel.hu)
2021-11-06 05:50:07 +0100zincy_(~zincy@2a00:23c8:970c:4801:350f:7ee:191a:6f65) (Ping timeout: 268 seconds)
2021-11-06 05:50:48 +0100 <ski> joel135 : perhaps you could elaborate on the "upgrading a polynomial p : ℕ₃ to an operator p(d/dx)" part (what is meant by that)
2021-11-06 06:07:11 +0100SeungheonOh(~Thunderbi@2600:1700:5168:1400:1574:2437:4f0d:50e6) (Quit: SeungheonOh)
2021-11-06 06:07:35 +0100emf(~emf@2620:10d:c090:400::5:38d) (Ping timeout: 264 seconds)
2021-11-06 06:10:50 +0100emf(~emf@163.114.132.5)
2021-11-06 06:15:24 +0100emf(~emf@163.114.132.5) (Read error: Connection reset by peer)
2021-11-06 06:16:15 +0100emf(~emf@2620:10d:c090:400::5:f801)
2021-11-06 06:17:45 +0100slack1256(~slack1256@191.125.99.211) (Ping timeout: 256 seconds)
2021-11-06 06:18:44 +0100mrianbloom(sid350277@id-350277.ilkley.irccloud.com) (Ping timeout: 252 seconds)
2021-11-06 06:18:44 +0100vito(sid1962@user/vito) (Ping timeout: 252 seconds)
2021-11-06 06:18:51 +0100pepeiborra(sid443799@id-443799.ilkley.irccloud.com) (Ping timeout: 245 seconds)
2021-11-06 06:18:51 +0100lightandlight(sid135476@id-135476.helmsley.irccloud.com) (Ping timeout: 245 seconds)
2021-11-06 06:18:54 +0100whez(sid470288@id-470288.lymington.irccloud.com) (Ping timeout: 260 seconds)
2021-11-06 06:18:59 +0100gregberns__(sid315709@id-315709.helmsley.irccloud.com) (Ping timeout: 264 seconds)
2021-11-06 06:18:59 +0100parseval(sid239098@id-239098.helmsley.irccloud.com) (Ping timeout: 264 seconds)
2021-11-06 06:19:07 +0100bitmapper(uid464869@id-464869.lymington.irccloud.com) (Ping timeout: 268 seconds)
2021-11-06 06:19:08 +0100carter(sid14827@id-14827.helmsley.irccloud.com) (Ping timeout: 260 seconds)
2021-11-06 06:19:08 +0100truckasaurus(sid457088@id-457088.helmsley.irccloud.com) (Ping timeout: 260 seconds)
2021-11-06 06:19:08 +0100NemesisD(sid24071@id-24071.lymington.irccloud.com) (Ping timeout: 260 seconds)
2021-11-06 06:19:08 +0100supersven(sid501114@id-501114.ilkley.irccloud.com) (Ping timeout: 260 seconds)
2021-11-06 06:19:08 +0100systemfault(sid267009@id-267009.uxbridge.irccloud.com) (Ping timeout: 260 seconds)
2021-11-06 06:19:08 +0100nrr_(sid20938@id-20938.lymington.irccloud.com) (Ping timeout: 260 seconds)
2021-11-06 06:19:09 +0100aria(sid380617@id-380617.lymington.irccloud.com) (Ping timeout: 265 seconds)
2021-11-06 06:19:10 +0100sa(sid1055@id-1055.tinside.irccloud.com) (Ping timeout: 260 seconds)
2021-11-06 06:19:10 +0100cbarrett(sid192934@id-192934.helmsley.irccloud.com) (Ping timeout: 260 seconds)
2021-11-06 06:19:10 +0100bw(sid2730@user/betawaffle) (Ping timeout: 260 seconds)
2021-11-06 06:19:16 +0100hamishmack(sid389057@id-389057.hampstead.irccloud.com) (Ping timeout: 245 seconds)
2021-11-06 06:19:16 +0100glowcoil(sid3405@id-3405.tinside.irccloud.com) (Ping timeout: 245 seconds)
2021-11-06 06:19:16 +0100idnar(sid12240@debian/mithrandi) (Ping timeout: 245 seconds)
2021-11-06 06:19:35 +0100aristid(sid1599@id-1599.uxbridge.irccloud.com) (Ping timeout: 264 seconds)
2021-11-06 06:19:36 +0100SanchayanMaity(sid478177@id-478177.hampstead.irccloud.com) (Ping timeout: 260 seconds)
2021-11-06 06:19:36 +0100alanz(sid110616@id-110616.uxbridge.irccloud.com) (Ping timeout: 260 seconds)
2021-11-06 06:19:41 +0100jackdk(sid373013@cssa/jackdk) (Ping timeout: 245 seconds)
2021-11-06 06:19:41 +0100meinside(uid24933@id-24933.helmsley.irccloud.com) (Ping timeout: 245 seconds)
2021-11-06 06:19:41 +0100dpratt_(sid193493@id-193493.helmsley.irccloud.com) (Ping timeout: 245 seconds)
2021-11-06 06:19:41 +0100obviyus(sid415299@user/obviyus) (Ping timeout: 245 seconds)
2021-11-06 06:19:41 +0100Pent(sid313808@id-313808.lymington.irccloud.com) (Ping timeout: 245 seconds)
2021-11-06 06:19:41 +0100edmundnoble(sid229620@id-229620.helmsley.irccloud.com) (Ping timeout: 245 seconds)
2021-11-06 06:19:41 +0100taktoa[c](sid282096@id-282096.tinside.irccloud.com) (Ping timeout: 245 seconds)
2021-11-06 06:19:41 +0100gonz___(sid304396@id-304396.lymington.irccloud.com) (Ping timeout: 245 seconds)
2021-11-06 06:19:41 +0100bbhoss(sid18216@id-18216.tinside.irccloud.com) (Ping timeout: 245 seconds)
2021-11-06 06:19:43 +0100servytor(uid525486@id-525486.hampstead.irccloud.com) (Ping timeout: 268 seconds)
2021-11-06 06:19:45 +0100dsal(sid13060@id-13060.lymington.irccloud.com) (Ping timeout: 260 seconds)
2021-11-06 06:20:04 +0100SethTisue__(sid14912@id-14912.ilkley.irccloud.com) (Ping timeout: 260 seconds)
2021-11-06 06:20:04 +0100hendi(sid489601@id-489601.lymington.irccloud.com) (Ping timeout: 260 seconds)
2021-11-06 06:20:04 +0100christiaanb(sid84827@id-84827.lymington.irccloud.com) (Ping timeout: 260 seconds)
2021-11-06 06:20:04 +0100kaychaks__(sid236345@id-236345.helmsley.irccloud.com) (Ping timeout: 260 seconds)
2021-11-06 06:20:06 +0100agander_m(sid407952@id-407952.tinside.irccloud.com) (Ping timeout: 245 seconds)
2021-11-06 06:20:11 +0100JSharp(sid4580@id-4580.lymington.irccloud.com) (Ping timeout: 264 seconds)
2021-11-06 06:20:18 +0100pjlsergeant(sid143467@id-143467.hampstead.irccloud.com) (Ping timeout: 260 seconds)
2021-11-06 06:20:18 +0100rubin55(sid175221@id-175221.hampstead.irccloud.com) (Ping timeout: 260 seconds)
2021-11-06 06:20:20 +0100ysh(sid6017@id-6017.ilkley.irccloud.com) (Ping timeout: 260 seconds)
2021-11-06 06:20:20 +0100alinab(sid468903@id-468903.helmsley.irccloud.com) (Ping timeout: 260 seconds)
2021-11-06 06:20:20 +0100econo(uid147250@user/econo) (Ping timeout: 268 seconds)
2021-11-06 06:20:20 +0100rtpg(sid443069@id-443069.ilkley.irccloud.com) (Ping timeout: 260 seconds)
2021-11-06 06:20:20 +0100gmc(sid58314@id-58314.ilkley.irccloud.com) (Ping timeout: 260 seconds)
2021-11-06 06:20:21 +0100whatsupdoc(uid509081@id-509081.hampstead.irccloud.com) (Ping timeout: 268 seconds)
2021-11-06 06:20:23 +0100S11001001(sid42510@id-42510.ilkley.irccloud.com) (Ping timeout: 252 seconds)
2021-11-06 06:20:23 +0100sa1(sid7690@id-7690.ilkley.irccloud.com) (Ping timeout: 252 seconds)
2021-11-06 06:20:26 +0100zincy_(~zincy@2a00:23c8:970c:4801:350f:7ee:191a:6f65)
2021-11-06 06:20:32 +0100tritlo(sid58727@user/tritlo) (Ping timeout: 260 seconds)
2021-11-06 06:20:32 +0100ehamberg(sid18208@id-18208.hampstead.irccloud.com) (Ping timeout: 260 seconds)
2021-11-06 06:20:32 +0100aarchi(sid486183@id-486183.uxbridge.irccloud.com) (Ping timeout: 260 seconds)
2021-11-06 06:20:32 +0100ephemient(uid407513@id-407513.lymington.irccloud.com) (Ping timeout: 260 seconds)
2021-11-06 06:20:32 +0100scav(sid309693@id-309693.helmsley.irccloud.com) (Ping timeout: 260 seconds)
2021-11-06 06:20:32 +0100hubvu(sid495858@user/hubvu) (Ping timeout: 260 seconds)
2021-11-06 06:20:32 +0100NiKaN(sid385034@id-385034.helmsley.irccloud.com) (Ping timeout: 260 seconds)
2021-11-06 06:20:32 +0100b20n(sid115913@id-115913.uxbridge.irccloud.com) (Ping timeout: 260 seconds)
2021-11-06 06:20:39 +0100jakesyl_(sid56879@id-56879.hampstead.irccloud.com) (Ping timeout: 268 seconds)
2021-11-06 06:20:46 +0100pony(sid524992@smol/hors) (Ping timeout: 260 seconds)
2021-11-06 06:20:55 +0100mcfilib(sid302703@user/mcfilib) (Ping timeout: 260 seconds)
2021-11-06 06:20:55 +0100integral(sid296274@user/integral) (Ping timeout: 260 seconds)
2021-11-06 06:20:55 +0100awpr(uid446117@id-446117.lymington.irccloud.com) (Ping timeout: 260 seconds)
2021-11-06 06:20:58 +0100hongminhee(sid295@id-295.tinside.irccloud.com) (Ping timeout: 268 seconds)
2021-11-06 06:21:00 +0100stevenxl(sid133530@id-133530.uxbridge.irccloud.com) (Ping timeout: 260 seconds)
2021-11-06 06:21:00 +0100tnks(sid412124@id-412124.helmsley.irccloud.com) (Ping timeout: 260 seconds)
2021-11-06 06:21:00 +0100bjs(sid190364@user/bjs) (Ping timeout: 260 seconds)
2021-11-06 06:21:00 +0100Firedancer(sid336191@id-336191.hampstead.irccloud.com) (Ping timeout: 260 seconds)
2021-11-06 06:21:04 +0100lightandlight(sid135476@id-135476.helmsley.irccloud.com)
2021-11-06 06:21:08 +0100parseval(sid239098@id-239098.helmsley.irccloud.com)
2021-11-06 06:21:09 +0100ysh(sid6017@id-6017.ilkley.irccloud.com)
2021-11-06 06:21:10 +0100hubvu(sid495858@user/hubvu)
2021-11-06 06:21:10 +0100scav(sid309693@id-309693.helmsley.irccloud.com)
2021-11-06 06:21:10 +0100bitmapper(uid464869@id-464869.lymington.irccloud.com)
2021-11-06 06:21:11 +0100S11001001(sid42510@id-42510.ilkley.irccloud.com)
2021-11-06 06:21:15 +0100NemesisD(sid24071@id-24071.lymington.irccloud.com)
2021-11-06 06:21:16 +0100aristid(sid1599@id-1599.uxbridge.irccloud.com)
2021-11-06 06:21:18 +0100gregberns__(sid315709@helmsley.irccloud.com)
2021-11-06 06:21:19 +0100SethTisue__(sid14912@ilkley.irccloud.com)
2021-11-06 06:21:19 +0100sa1(sid7690@id-7690.ilkley.irccloud.com)
2021-11-06 06:21:20 +0100dsal(sid13060@id-13060.lymington.irccloud.com)
2021-11-06 06:21:21 +0100whez(sid470288@lymington.irccloud.com)
2021-11-06 06:21:21 +0100bjs(sid190364@user/bjs)
2021-11-06 06:21:22 +0100bbhoss(sid18216@id-18216.tinside.irccloud.com)
2021-11-06 06:21:24 +0100mrianbloom(sid350277@ilkley.irccloud.com)
2021-11-06 06:21:24 +0100glowcoil(sid3405@tinside.irccloud.com)
2021-11-06 06:21:24 +0100supersven(sid501114@ilkley.irccloud.com)
2021-11-06 06:21:27 +0100sa(sid1055@id-1055.tinside.irccloud.com)
2021-11-06 06:21:29 +0100vito(sid1962@id-1962.uxbridge.irccloud.com)
2021-11-06 06:21:30 +0100hongminhee(sid295@id-295.tinside.irccloud.com)
2021-11-06 06:21:30 +0100hendi(sid489601@id-489601.lymington.irccloud.com)
2021-11-06 06:21:31 +0100vito(sid1962@id-1962.uxbridge.irccloud.com) (Changing host)
2021-11-06 06:21:31 +0100vito(sid1962@user/vito)
2021-11-06 06:21:39 +0100servytor(uid525486@2a03:5180:f:4::8:4ae)
2021-11-06 06:21:39 +0100JSharp(sid4580@id-4580.lymington.irccloud.com)
2021-11-06 06:21:42 +0100meinside(uid24933@helmsley.irccloud.com)
2021-11-06 06:21:44 +0100alinab(sid468903@helmsley.irccloud.com)
2021-11-06 06:21:44 +0100Pent(sid313808@2a03:5180:f:2::4:c9d0)
2021-11-06 06:21:45 +0100gmc(sid58314@ilkley.irccloud.com)
2021-11-06 06:21:46 +0100gonz___(sid304396@2a03:5180:f:2::4:a50c)
2021-11-06 06:21:46 +0100aria(sid380617@lymington.irccloud.com)
2021-11-06 06:21:48 +0100idnar(sid12240@debian/mithrandi)
2021-11-06 06:21:49 +0100rtpg(sid443069@2a03:5180:f:3::6:c2bd)
2021-11-06 06:21:52 +0100hamishmack(sid389057@2a03:5180:f:4::5:efc1)
2021-11-06 06:21:52 +0100awpr(uid446117@lymington.irccloud.com)
2021-11-06 06:21:53 +0100systemfault(sid267009@2a03:5180:f:5::4:1301)
2021-11-06 06:21:54 +0100christiaanb(sid84827@id-84827.lymington.irccloud.com)
2021-11-06 06:21:58 +0100bw(sid2730@user/betawaffle)
2021-11-06 06:21:58 +0100truckasaurus(sid457088@id-457088.helmsley.irccloud.com)
2021-11-06 06:21:59 +0100agander_m(sid407952@2a03:5180:f::6:3990)
2021-11-06 06:21:59 +0100merijn(~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 264 seconds)
2021-11-06 06:21:59 +0100obviyus(sid415299@user/obviyus)
2021-11-06 06:22:00 +0100tnks(sid412124@2a03:5180:f:1::6:49dc)
2021-11-06 06:22:00 +0100mcfilib(sid302703@2a03:5180:f:1::4:9e6f)
2021-11-06 06:22:00 +0100mcfilib(sid302703@2a03:5180:f:1::4:9e6f) (Changing host)
2021-11-06 06:22:00 +0100mcfilib(sid302703@user/mcfilib)
2021-11-06 06:22:01 +0100taktoa[c](sid282096@id-282096.tinside.irccloud.com)
2021-11-06 06:22:02 +0100nrr_(sid20938@id-20938.lymington.irccloud.com)
2021-11-06 06:22:04 +0100kaychaks__(sid236345@2a03:5180:f:1::3:9b39)
2021-11-06 06:22:05 +0100ephemient(uid407513@2a03:5180:f:2::6:37d9)
2021-11-06 06:22:06 +0100edmundnoble(sid229620@2a03:5180:f:1::3:80f4)
2021-11-06 06:22:08 +0100cbarrett(sid192934@2a03:5180:f:1::2:f1a6)
2021-11-06 06:22:11 +0100jackdk(sid373013@cssa/jackdk)
2021-11-06 06:22:11 +0100econo(uid147250@user/econo)
2021-11-06 06:22:14 +0100integral(sid296274@user/integral)
2021-11-06 06:22:18 +0100whatsupdoc(uid509081@2a03:5180:f:4::7:c499)
2021-11-06 06:22:20 +0100carter(sid14827@id-14827.helmsley.irccloud.com)
2021-11-06 06:22:21 +0100b20n(sid115913@2a03:5180:f:5::1:c4c9)
2021-11-06 06:22:22 +0100stevenxl(sid133530@2a03:5180:f:5::2:99a)
2021-11-06 06:22:22 +0100dpratt_(sid193493@helmsley.irccloud.com)
2021-11-06 06:22:24 +0100pony(sid524992@smol/hors)
2021-11-06 06:22:25 +0100aarchi(sid486183@2a03:5180:f:5::7:6b27)
2021-11-06 06:22:25 +0100SanchayanMaity(sid478177@2a03:5180:f:4::7:4be1)
2021-11-06 06:22:25 +0100Firedancer(sid336191@2a03:5180:f:4::5:213f)
2021-11-06 06:22:25 +0100pepeiborra(sid443799@2a03:5180:f:3::6:c597)
2021-11-06 06:22:25 +0100alanz(sid110616@2a03:5180:f:5::1:b018)
2021-11-06 06:22:27 +0100pjlsergeant(sid143467@2a03:5180:f:4::2:306b)
2021-11-06 06:22:29 +0100rubin55(sid175221@2a03:5180:f:4::2:ac75)
2021-11-06 06:22:47 +0100NiKaN(sid385034@2a03:5180:f:1::5:e00a)
2021-11-06 06:22:49 +0100jakesyl_(sid56879@2a03:5180:f:4::de2f)
2021-11-06 06:24:11 +0100ehamberg(sid18208@id-18208.hampstead.irccloud.com)
2021-11-06 06:24:16 +0100tritlo(sid58727@user/tritlo)
2021-11-06 06:25:17 +0100zincy_(~zincy@2a00:23c8:970c:4801:350f:7ee:191a:6f65) (Ping timeout: 268 seconds)
2021-11-06 06:27:01 +0100EvanR(~evan@2600:1700:ba69:10:acd9:793b:27c9:b878)
2021-11-06 06:36:26 +0100yauhsien(~yauhsien@2402:7500:4e4:2cb1:35e8:471e:a055:9d52)
2021-11-06 06:41:06 +0100Cajun(~Cajun@user/cajun) (Quit: Client closed)
2021-11-06 06:42:24 +0100Cajun(~Cajun@user/cajun)
2021-11-06 06:55:31 +0100zincy_(~zincy@2a00:23c8:970c:4801:350f:7ee:191a:6f65)
2021-11-06 07:00:23 +0100zincy_(~zincy@2a00:23c8:970c:4801:350f:7ee:191a:6f65) (Ping timeout: 264 seconds)
2021-11-06 07:05:10 +0100v01d4lph4(~v01d4lph4@user/v01d4lph4) (Read error: Connection reset by peer)
2021-11-06 07:05:32 +0100v01d4lph4(~v01d4lph4@user/v01d4lph4)
2021-11-06 07:06:42 +0100hololeap(~hololeap@user/hololeap) (Remote host closed the connection)
2021-11-06 07:08:14 +0100hololeap(~hololeap@user/hololeap)
2021-11-06 07:13:59 +0100euandreh(~euandreh@2804:14c:33:9fe5:90d0:563b:3279:f95b) (Ping timeout: 268 seconds)
2021-11-06 07:15:47 +0100chexum(~quassel@gateway/tor-sasl/chexum) (Remote host closed the connection)
2021-11-06 07:16:08 +0100chexum(~quassel@gateway/tor-sasl/chexum)
2021-11-06 07:21:51 +0100chomwitt(~chomwitt@2a02:587:dc02:9f00:12c3:7bff:fe6d:d374)
2021-11-06 07:25:05 +0100xff0x(~xff0x@2001:1a81:52b1:3000:b3ef:fedd:d143:889a) (Ping timeout: 268 seconds)
2021-11-06 07:25:35 +0100EvanR(~evan@2600:1700:ba69:10:acd9:793b:27c9:b878) (Ping timeout: 264 seconds)
2021-11-06 07:25:53 +0100xff0x(~xff0x@2001:1a81:52b1:3000:355a:710f:ac35:1a61)
2021-11-06 07:32:50 +0100MidAutumnMoon(~MidAutumn@user/midautumnmoon) (Quit: Leaving for a break - theLounge)
2021-11-06 07:33:26 +0100MidAutumnMoon(~MidAutumn@user/midautumnmoon)
2021-11-06 07:35:54 +0100chexum(~quassel@gateway/tor-sasl/chexum) (Remote host closed the connection)
2021-11-06 07:36:05 +0100chexum(~quassel@gateway/tor-sasl/chexum)
2021-11-06 07:38:42 +0100chomwitt(~chomwitt@2a02:587:dc02:9f00:12c3:7bff:fe6d:d374) (Ping timeout: 260 seconds)
2021-11-06 07:40:06 +0100xff0x(~xff0x@2001:1a81:52b1:3000:355a:710f:ac35:1a61) (Ping timeout: 245 seconds)
2021-11-06 07:41:05 +0100xff0x(~xff0x@2001:1a81:52b1:3000:7ef:3640:6d4d:8cb8)
2021-11-06 07:42:31 +0100aegon(~mike@174.127.249.180) (Remote host closed the connection)
2021-11-06 07:46:06 +0100zincy_(~zincy@2a00:23c8:970c:4801:350f:7ee:191a:6f65)
2021-11-06 07:48:56 +0100alzgh(~alzgh@user/alzgh)
2021-11-06 07:50:31 +0100zincy_(~zincy@2a00:23c8:970c:4801:350f:7ee:191a:6f65) (Ping timeout: 245 seconds)
2021-11-06 07:54:16 +0100yauhsien(~yauhsien@2402:7500:4e4:2cb1:35e8:471e:a055:9d52) (Remote host closed the connection)
2021-11-06 07:54:34 +0100vysn(~vysn@user/vysn)
2021-11-06 08:08:11 +0100econo(uid147250@user/econo) (Quit: Connection closed for inactivity)
2021-11-06 08:12:29 +0100yauhsien(~yauhsien@118-167-41-229.dynamic-ip.hinet.net)
2021-11-06 08:12:38 +0100yauhsien(~yauhsien@118-167-41-229.dynamic-ip.hinet.net) (Remote host closed the connection)
2021-11-06 08:16:30 +0100chomwitt(~chomwitt@athedsl-32204.home.otenet.gr)
2021-11-06 08:17:07 +0100Sgeo_(~Sgeo@user/sgeo) (Read error: Connection reset by peer)
2021-11-06 08:18:01 +0100merijn(~merijn@83-160-49-249.ip.xs4all.nl)
2021-11-06 08:19:02 +0100geekosaur(~geekosaur@xmonad/geekosaur) (Remote host closed the connection)
2021-11-06 08:20:02 +0100geekosaur(~geekosaur@xmonad/geekosaur)
2021-11-06 08:21:21 +0100lavaman(~lavaman@98.38.249.169)
2021-11-06 08:22:25 +0100zincy_(~zincy@2a00:23c8:970c:4801:350f:7ee:191a:6f65)
2021-11-06 08:25:31 +0100lavaman(~lavaman@98.38.249.169) (Ping timeout: 245 seconds)
2021-11-06 08:27:14 +0100zincy_(~zincy@2a00:23c8:970c:4801:350f:7ee:191a:6f65) (Ping timeout: 260 seconds)
2021-11-06 08:27:58 +0100eggplantade(~Eggplanta@108-201-191-115.lightspeed.sntcca.sbcglobal.net) (Remote host closed the connection)
2021-11-06 08:31:14 +0100max22-(~maxime@lfbn-ren-1-762-224.w81-53.abo.wanadoo.fr)
2021-11-06 08:33:49 +0100brainfreeze(~brainfree@2a03:1b20:4:f011::20d) (Remote host closed the connection)
2021-11-06 08:38:17 +0100gehmehgeh(~user@user/gehmehgeh)
2021-11-06 08:43:43 +0100yauhsien(~yauhsien@118-167-41-229.dynamic-ip.hinet.net)
2021-11-06 08:48:26 +0100yauhsien(~yauhsien@118-167-41-229.dynamic-ip.hinet.net) (Ping timeout: 245 seconds)
2021-11-06 08:51:54 +0100bitmapper(uid464869@id-464869.lymington.irccloud.com) (Quit: Connection closed for inactivity)
2021-11-06 08:52:11 +0100merijn(~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 245 seconds)
2021-11-06 08:59:40 +0100cheater(~Username@user/cheater)
2021-11-06 09:05:03 +0100hendursaga(~weechat@user/hendursaga)
2021-11-06 09:05:39 +0100v01d4lph4(~v01d4lph4@user/v01d4lph4) (Remote host closed the connection)
2021-11-06 09:05:52 +0100johnny_sitar(~artur@078088015209.bialystok.vectranet.pl)
2021-11-06 09:07:05 +0100madjestic(~madjestic@88-159-247-120.fixed.kpn.net)
2021-11-06 09:08:30 +0100hendursa1(~weechat@user/hendursaga) (Ping timeout: 276 seconds)
2021-11-06 09:12:53 +0100zincy_(~zincy@2a00:23c8:970c:4801:350f:7ee:191a:6f65)
2021-11-06 09:14:47 +0100emf(~emf@2620:10d:c090:400::5:f801) (Ping timeout: 264 seconds)
2021-11-06 09:17:11 +0100zincy_(~zincy@2a00:23c8:970c:4801:350f:7ee:191a:6f65) (Ping timeout: 245 seconds)
2021-11-06 09:17:27 +0100geekosaur(~geekosaur@xmonad/geekosaur) (Remote host closed the connection)
2021-11-06 09:17:36 +0100hendursaga(~weechat@user/hendursaga) (Ping timeout: 276 seconds)
2021-11-06 09:17:51 +0100geekosaur(~geekosaur@xmonad/geekosaur)
2021-11-06 09:19:26 +0100hendursaga(~weechat@user/hendursaga)
2021-11-06 09:21:40 +0100emf(~emf@c-73-97-137-43.hsd1.wa.comcast.net)
2021-11-06 09:26:47 +0100madjestic(~madjestic@88-159-247-120.fixed.kpn.net) (Ping timeout: 264 seconds)
2021-11-06 09:28:59 +0100eggplantade(~Eggplanta@108-201-191-115.lightspeed.sntcca.sbcglobal.net)
2021-11-06 09:29:05 +0100mei3(~mei@user/mei)
2021-11-06 09:33:34 +0100eggplantade(~Eggplanta@108-201-191-115.lightspeed.sntcca.sbcglobal.net) (Ping timeout: 260 seconds)
2021-11-06 09:39:36 +0100madjestic(~madjestic@88-159-247-120.fixed.kpn.net)
2021-11-06 09:43:20 +0100wonko(~wjc@user/wonko)
2021-11-06 09:55:16 +0100tzh(~tzh@c-24-21-73-154.hsd1.or.comcast.net) (Quit: zzz)
2021-11-06 09:55:57 +0100v01d4lph4(~v01d4lph4@106.215.93.204)
2021-11-06 09:55:57 +0100v01d4lph4(~v01d4lph4@106.215.93.204) (Changing host)
2021-11-06 09:55:57 +0100v01d4lph4(~v01d4lph4@user/v01d4lph4)
2021-11-06 10:00:03 +0100cloudy(~cloudy@2001:470:69fc:105::50c0) (Quit: You have been kicked for being idle)
2021-11-06 10:00:35 +0100merijn(~merijn@83-160-49-249.ip.xs4all.nl)
2021-11-06 10:02:09 +0100v01d4lph4(~v01d4lph4@user/v01d4lph4) (Remote host closed the connection)
2021-11-06 10:02:35 +0100random-jellyfish(~random-je@user/random-jellyfish)
2021-11-06 10:08:11 +0100johnny_sitar(~artur@078088015209.bialystok.vectranet.pl) (Ping timeout: 264 seconds)
2021-11-06 10:12:55 +0100v01d4lph4(~v01d4lph4@user/v01d4lph4)
2021-11-06 10:15:08 +0100Lycurgus(~juan@98.4.112.204)
2021-11-06 10:15:18 +0100ByronJohnson(~bairyn@50-250-232-19-static.hfc.comcastbusiness.net) (Ping timeout: 268 seconds)
2021-11-06 10:19:55 +0100boxscape_(~boxscape_@mue-88-130-59-018.dsl.tropolys.de)
2021-11-06 10:26:22 +0100_ht(~quassel@82-169-194-8.biz.kpn.net)
2021-11-06 10:26:54 +0100ByronJohnson(~bairyn@50-250-232-19-static.hfc.comcastbusiness.net)
2021-11-06 10:29:33 +0100johnny_sitar(~artur@078088015209.bialystok.vectranet.pl)
2021-11-06 10:33:56 +0100v01d4lph4(~v01d4lph4@user/v01d4lph4) (Remote host closed the connection)
2021-11-06 10:36:35 +0100v01d4lph4(~v01d4lph4@user/v01d4lph4)
2021-11-06 10:44:47 +0100kuribas(~user@ptr-25vy0i7euy3zycfmzaa.18120a2.ip6.access.telenet.be)
2021-11-06 10:47:18 +0100arahael(~arahael@124.148.78.199) (Ping timeout: 260 seconds)
2021-11-06 10:50:13 +0100Lycurgus(~juan@98.4.112.204) (Quit: Exeunt)
2021-11-06 10:53:39 +0100Athas(athas@2a01:7c8:aaac:1cf:a0d4:8908:cfdb:b9c0) (Quit: ZNC 1.8.2 - https://znc.in)
2021-11-06 10:53:49 +0100Athas(athas@sigkill.dk)
2021-11-06 10:55:06 +0100wonko(~wjc@user/wonko) (Ping timeout: 245 seconds)
2021-11-06 10:59:16 +0100emanuele6(~emanuele6@user/emanuele6) (WeeChat 3.3)
2021-11-06 10:59:47 +0100johnny_sitar(~artur@078088015209.bialystok.vectranet.pl) (Remote host closed the connection)
2021-11-06 11:00:04 +0100johnny_sitar(~artur@078088015209.bialystok.vectranet.pl)
2021-11-06 11:00:21 +0100v01d4lph4(~v01d4lph4@user/v01d4lph4) (Remote host closed the connection)
2021-11-06 11:04:16 +0100merijn(~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 245 seconds)
2021-11-06 11:07:19 +0100chomwitt(~chomwitt@athedsl-32204.home.otenet.gr) (Ping timeout: 256 seconds)
2021-11-06 11:12:36 +0100arahael(~arahael@202-159-171-156.tpgi.com.au)
2021-11-06 11:13:01 +0100Tuplanolla(~Tuplanoll@91-159-69-50.elisa-laajakaista.fi)
2021-11-06 11:17:26 +0100mc47(~mc47@xmonad/TheMC47)
2021-11-06 11:22:18 +0100 <joel135> ski: by p(d/dx) i mean for example the differential operator f ↦ f + 5 d²f/dx², if p(t) is 1 + 5 t^2. the idea that you get the typing p(d/dx) : ℕ₄ is unfortunately only approximate, since supposedly ℕ₄ consists of just the "algebraic" operators (formed from the progression of constants 0, 1, x, I and corresponding binary operators _+_, _*_, _∘_, _▫_ (for lack of more standard notation)),
2021-11-06 11:23:05 +0100 <joel135> among which d/dx and p(d/dx) don't seem to quite fit in although do they live "at the right level" in that they are operators that can be turned into functions ℕ₃ → ℕ₃ (i.e. forall o. ⋯ → forall o. ⋯).
2021-11-06 11:29:55 +0100mmhat(~mmh@55d4b9d8.access.ecotel.net)
2021-11-06 11:35:52 +0100Inst(~Inst@2601:6c4:4080:3f80:40a:9f91:8f3e:4f02)
2021-11-06 11:36:03 +0100 <Inst> a gonad is just a gonoid in the category of endofunctors ;)
2021-11-06 11:44:56 +0100zer0bitz(~zer0bitz@dsl-hkibng31-54fae3-116.dhcp.inet.fi)
2021-11-06 11:45:13 +0100kuribas(~user@ptr-25vy0i7euy3zycfmzaa.18120a2.ip6.access.telenet.be) (Remote host closed the connection)
2021-11-06 11:47:05 +0100whatsupdoc(uid509081@2a03:5180:f:4::7:c499) (Quit: Connection closed for inactivity)
2021-11-06 11:47:42 +0100 <joel135> the reason that i want to call it a "middle degeneracy" is that addition is sent to addition ((p+q)(d/dx) = p(d/dx)+q(d/dx), the "same level") whereas multiplication of pure powers tᵃtᵇ is sent to operator composition ((tᵃtᵇ)(d/dx) = dᵃ⁺ᵇ/dxᵃ⁺ᵇ = dᵃ/dxᵃ ▫ dᵇ/dxᵇ = (tᵃ)(d/dx) ▫ (tᵇ)(d/dx), a "higher level" in the progression of _+_, _*_, _∘_, _▫_, ...)
2021-11-06 11:51:08 +0100 <joel135> anything that is not acting in the "middle" of this progression of operators would either leave it alone (sending p to \_ -> p) or shift the entire hierarchy by one or more steps like you do for the Antecedent (sending p to p)
2021-11-06 12:00:50 +0100alx741(~alx741@181.196.68.55)
2021-11-06 12:05:18 +0100tremon(~tremon@217-63-61-89.cable.dynamic.v4.ziggo.nl) (Quit: getting boxed in)
2021-11-06 12:05:30 +0100Pickchea(~private@user/pickchea)
2021-11-06 12:07:19 +0100Gurkenglas(~Gurkengla@dslb-002-203-144-204.002.203.pools.vodafone-ip.de)
2021-11-06 12:10:16 +0100cocreatu1cocreature
2021-11-06 12:14:20 +0100desantra(~skykanin@user/skykanin)
2021-11-06 12:21:34 +0100zincy_(~zincy@2a00:23c8:970c:4801:350f:7ee:191a:6f65)
2021-11-06 12:22:48 +0100rond_(~rond_@2a02:a31a:a23c:f480:2fd7:e087:5546:a438)
2021-11-06 12:23:02 +0100lavaman(~lavaman@98.38.249.169)
2021-11-06 12:23:27 +0100 <joel135> <ski> "normally", success and failure continuations are not mixed up with each other. but for implication, when `Consequent' succeeds, that is then interpreted by `Antecedent' as a failure, a prod for it to generate another solution (spawning a new, conceptually separate, call to `Consequent')
2021-11-06 12:24:43 +0100 <joel135> ah, after a night's sleep am beginning to understand this now. it is an astute observation
2021-11-06 12:25:46 +0100johnny_sitar(~artur@078088015209.bialystok.vectranet.pl) (Ping timeout: 260 seconds)
2021-11-06 12:27:08 +0100desantra(~skykanin@user/skykanin) (Quit: WeeChat 3.3)
2021-11-06 12:27:20 +0100desantra(~skykanin@user/skykanin)
2021-11-06 12:28:55 +0100lavaman(~lavaman@98.38.249.169) (Ping timeout: 256 seconds)
2021-11-06 12:31:16 +0100eggplantade(~Eggplanta@108-201-191-115.lightspeed.sntcca.sbcglobal.net)
2021-11-06 12:32:07 +0100 <joel135> by the way, did you represent your type of multidimensional arrays (assuming you mean something like a list of lists, but with the constraint that they form a rectangular grid in the end) by some kind of Church encoding? i don't see how to accomplish that off the top of my head.
2021-11-06 12:32:21 +0100zincy_(~zincy@2a00:23c8:970c:4801:350f:7ee:191a:6f65) (Remote host closed the connection)
2021-11-06 12:35:43 +0100eggplantade(~Eggplanta@108-201-191-115.lightspeed.sntcca.sbcglobal.net) (Ping timeout: 256 seconds)
2021-11-06 12:36:37 +0100desantra(~skykanin@user/skykanin) (Quit: WeeChat 3.3)
2021-11-06 12:37:49 +0100desantra(~skykanin@user/skykanin)
2021-11-06 12:40:42 +0100chomwitt(~chomwitt@athedsl-32204.home.otenet.gr)
2021-11-06 12:42:25 +0100cosimone(~user@2001:b07:ae5:db26:c24a:d20:4d91:1e20)
2021-11-06 12:44:41 +0100madjestic(~madjestic@88-159-247-120.fixed.kpn.net) (Ping timeout: 245 seconds)
2021-11-06 12:48:09 +0100fendor(~fendor@91.141.74.77.wireless.dyn.drei.com)
2021-11-06 12:49:44 +0100DNH(~DNH@2a02:8108:1100:16d8:9554:7177:bc66:d82f)
2021-11-06 12:49:47 +0100DNH(~DNH@2a02:8108:1100:16d8:9554:7177:bc66:d82f) (Client Quit)
2021-11-06 12:50:41 +0100cosimone(~user@2001:b07:ae5:db26:c24a:d20:4d91:1e20) (Ping timeout: 268 seconds)
2021-11-06 12:52:18 +0100boxscape_(~boxscape_@mue-88-130-59-018.dsl.tropolys.de) (Ping timeout: 260 seconds)
2021-11-06 12:59:16 +0100FinnElija(~finn_elij@user/finn-elija/x-0085643) (Remote host closed the connection)
2021-11-06 12:59:47 +0100FinnElija(~finn_elij@user/finn-elija/x-0085643)
2021-11-06 13:01:18 +0100 <alzgh> hello, I'm trying to rewrite `tupledMonad1` using bind notation `>>=`. Any help and hint is appreciated https://paste.tomsmeding.com/odkcLN80
2021-11-06 13:01:31 +0100basti_(~basti@ip-84-119-8-195.unity-media.net)
2021-11-06 13:02:05 +0100merijn(~merijn@83-160-49-249.ip.xs4all.nl)
2021-11-06 13:03:20 +0100tfeb(~tfb@88.98.95.237)
2021-11-06 13:04:34 +0100alx741(~alx741@181.196.68.55) (Quit: alx741)
2021-11-06 13:05:13 +0100cosimone(~user@93-47-229-157.ip115.fastwebnet.it)
2021-11-06 13:07:42 +0100tfeb(~tfb@88.98.95.237) (Client Quit)
2021-11-06 13:08:01 +0100Gurkenglas(~Gurkengla@dslb-002-203-144-204.002.203.pools.vodafone-ip.de) (Ping timeout: 256 seconds)
2021-11-06 13:11:50 +0100fendor_(~fendor@91.141.74.77.wireless.dyn.drei.com)
2021-11-06 13:11:51 +0100zincy_(~zincy@2a00:23c8:970c:4801:350f:7ee:191a:6f65)
2021-11-06 13:12:36 +0100zincy_(~zincy@2a00:23c8:970c:4801:350f:7ee:191a:6f65) (Remote host closed the connection)
2021-11-06 13:14:15 +0100fendor(~fendor@91.141.74.77.wireless.dyn.drei.com) (Ping timeout: 256 seconds)
2021-11-06 13:17:30 +0100fendor_fendor
2021-11-06 13:22:38 +0100 <Pickchea> Hey, is there a way to make the type checker accept this? \p q -> p q p
2021-11-06 13:24:24 +0100[itchyjunk](~itchyjunk@user/itchyjunk/x-7353470)
2021-11-06 13:24:39 +0100 <hpc> wrap it in Fix maybe?
2021-11-06 13:25:54 +0100 <hpc> what type do you want p to have?
2021-11-06 13:26:00 +0100 <ski> joel135 : by ⌜f ↦ f + 5 d²f/dx²⌝, you mean ⌜f ↦ x ↦ f x + 5 ⋅ d² (f x) / (d x)²⌝ ? what's ⌜I⌝,⌜▫⌝ ?
2021-11-06 13:26:30 +0100 <ski> ("ah, after a night's sleep .." -- ok, good)
2021-11-06 13:27:45 +0100 <joel135> yes that is what i mean
2021-11-06 13:28:26 +0100 <ski> joel135 : no, iirc just nested "arrays" (implemented as compound terms, using the standard arg/3 to access at a positive integer index). this was before i got to thinking about "backtracking backtracking", and started fiddling with continuation levels
2021-11-06 13:29:27 +0100jess(~jess@libera/staff/jess)
2021-11-06 13:30:41 +0100 <joel135> of type ℕ₄, I and _▫_ are just id and comp
2021-11-06 13:31:15 +0100 <joel135> of type ℕ₅, I and _▫_ are pure id and liftA2 comp
2021-11-06 13:31:23 +0100 <joel135> and so on
2021-11-06 13:31:24 +0100 <ski> (i then tried using some (iirc) setarg/3 (low-level mutation), in order to attempt to make some changes survive backtracking. recently i found a linkarg/3 (more unsafe), which i think maybe could have been used to avoid (what i deemed to be) problems caused by optimizations assuming purity (no mutation))
2021-11-06 13:31:34 +0100shapr(~user@pool-100-36-247-68.washdc.fios.verizon.net) (Ping timeout: 260 seconds)
2021-11-06 13:32:22 +0100 <Pickchea> hpc, couldn't figure it out with fix. I'm just playing around. Say `true a b = a' and `false a b = b'. It would follow that `and a b = a b a'.
2021-11-06 13:32:26 +0100 <ski> hm, so just continuing the pattern of successively (environment-)lifted identity and composition, ok
2021-11-06 13:32:52 +0100 <ski> (i still wonder about a "numerical" interpretation of them)
2021-11-06 13:34:03 +0100 <ski> Pickchea : what about `and a b p q = a (b p q) q' ?
2021-11-06 13:34:03 +0100 <joel135> I is to be that operator which given a polynomial returns that polynomial without modification
2021-11-06 13:34:05 +0100merijn(~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 256 seconds)
2021-11-06 13:35:19 +0100 <joel135> another operator of the same type would be p(x) ↦ p(x+n) for a fixed natural number n. this is a bona fide operator of type ℕ₄.
2021-11-06 13:35:45 +0100 <ski> "operator" here being an operator on polynomials, presumably generated from an "oracle"/indeterminate/unknown/variable/formal such operator ?
2021-11-06 13:35:56 +0100slowButPresent(~slowButPr@user/slowbutpresent)
2021-11-06 13:37:08 +0100 <ski> (i take that to mean ⌜p ↦ x ↦ p (x + n)⌝)
2021-11-06 13:37:37 +0100 <Pickchea> ski, what are you, some kind genius? :-D
2021-11-06 13:37:58 +0100 <ski> Pickchea : or, you could declare `type ChurchBool = forall o. o -> o -> o' (and enable `Rank2Types'), i think ?
2021-11-06 13:38:07 +0100jumper149(~jumper149@80.240.31.34)
2021-11-06 13:38:46 +0100 <ski> (i think, using that, you may be able to get `and a b = a b a' to check)
2021-11-06 13:39:24 +0100 <ski> Pickchea : i was just talking, some hours ago, about Church numerals :)
2021-11-06 13:40:13 +0100 <ski> (oh, and obviously you'd need the type signature that you expect, on `and', for that to possibly work)
2021-11-06 13:43:44 +0100max22-(~maxime@lfbn-ren-1-762-224.w81-53.abo.wanadoo.fr) (Ping timeout: 268 seconds)
2021-11-06 13:44:34 +0100favonia(~favonia@user/favonia)
2021-11-06 13:45:37 +0100 <Pickchea> ski, couldn't do it with Rank2Types. But interesting stuff. If it works with `and a b p q = a (b p q) q' I wonder why `and a b = a b a' can't pass the type check.
2021-11-06 13:45:47 +0100 <Pickchea> Seems complicated :-D
2021-11-06 13:46:17 +0100 <hpc> it's the same reason you can't write (\x -> x x) in simply typed lambda calculus
2021-11-06 13:47:48 +0100 <hpc> the unifier has to solve a = b -> a -> c
2021-11-06 13:47:59 +0100 <hpc> which is a = b -> (b -> (b -> (...
2021-11-06 13:48:02 +0100 <hpc> which is an infinite type
2021-11-06 13:49:32 +0100 <Pickchea> Yeah, I thought something like that!
2021-11-06 13:49:45 +0100unit73e(~emanuel@2001:818:e8dd:7c00:32b5:c2ff:fe6b:5291)
2021-11-06 13:50:10 +0100 <Pickchea> This point goes to Lisp I guess :-D
2021-11-06 13:51:44 +0100aleator(~aleator@178-55-117-52.bb.dnainternet.fi)
2021-11-06 13:52:09 +0100 <ski> Pickchea : did you try adding a type signature for `and' ?
2021-11-06 13:53:02 +0100 <joel135> ski: yes, an operator on polynomials, and it is correct to write it as p ↦ x ↦ p (x + n) where then p : ((o -> o) -> (o -> o)) -> ((o -> o) -> (o -> o)) and x : ((o -> o) -> (o -> o)) and o is a type variable
2021-11-06 13:53:05 +0100 <ski> Pickchea : oh .. and if you want to play around with cyclic / "infinite" (/ equi-recursive) types, you could use `ocaml -rectypes'
2021-11-06 13:53:47 +0100 <unit73e> I don't know why aeson only has these super simple examples
2021-11-06 13:53:54 +0100 <unit73e> the best I found was this guy: https://artyom.me/aeson
2021-11-06 13:54:12 +0100 <joel135> note the distinction between the type ℕ₃ → ℕ₃ of arbitrary recursively defined operators on polynomials, and the more modest type ℕ₄ of "algebraically defined" operators on polynomials
2021-11-06 13:54:36 +0100 <joel135> the latter includes the translation operator from above, but presumably it doesn't include the differentiation operator
2021-11-06 13:55:02 +0100 <ski> (but there's a reason why static type systems normally don't allow that .. namely that there's a lot of false negatives, common type errors that now become type-correct, with strange inferred cyclic types, and only at a later time and place the issue may be noticed, the error location usually pointing to the "wrong place")
2021-11-06 13:55:57 +0100 <ski> joel135 : *nod*, interesting
2021-11-06 13:58:04 +0100 <ski> (this relates to my idea of, in implication chains in proofs, whenever possible, working inside/within a universal, rather than using (the more powerful) reasoning between universals. a kind of "principle of least power" or something)
2021-11-06 13:58:09 +0100 <unit73e> however I agree that artyom should show the efficient way of using aeson. I don't like when you're tuturials show the wrong way. Why? Makes no sense to me.
2021-11-06 13:59:14 +0100 <ski> (hm, now i'm associating the above to minimal logic, and to the meta-distinction between derivable and admissible inference rules)
2021-11-06 14:01:04 +0100raehik(~raehik@cpc95906-rdng25-2-0-cust156.15-3.cable.virginm.net)
2021-11-06 14:01:05 +0100 <ski> joel135 : would this indeterminate operator that generates "operanomials" have any kind of "distribute" laws or something, wrt the other algebraic operations ?
2021-11-06 14:02:18 +0100aleator(~aleator@178-55-117-52.bb.dnainternet.fi) (Ping timeout: 260 seconds)
2021-11-06 14:02:27 +0100Alex_test(~al_test@94.233.241.187) (Quit: ;-)
2021-11-06 14:02:30 +0100AlexZenon(~alzenon@94.233.241.187) (Quit: ;-)
2021-11-06 14:02:59 +0100AlexNoo(~AlexNoo@94.233.241.187) (Quit: Leaving)
2021-11-06 14:03:53 +0100chomwitt(~chomwitt@athedsl-32204.home.otenet.gr) (Remote host closed the connection)
2021-11-06 14:03:57 +0100 <Inst> erm
2021-11-06 14:03:59 +0100 <Inst> looking for some help
2021-11-06 14:04:13 +0100 <Inst> in Haskell code, provided I'm running on a Windows system
2021-11-06 14:04:40 +0100 <Inst> how do I call the Windows API to create a default system "open file / save file" dialogue, then bind it to Haskell IO?
2021-11-06 14:05:00 +0100 <joel135> i think all generalized operators satisfy a one-sided distributive law like (A *ₖ B) *ₗ C = (A *ₗ C ) *ₖ (B *ₗ C) for k < l (or k > l, depending on conventions)
2021-11-06 14:05:50 +0100 <joel135> where *ₖ and *ₗ have the same type ℕₙ → ℕₙ → ℕₙ
2021-11-06 14:06:23 +0100 <joel135> generalized nullary/binary operators, i should say
2021-11-06 14:06:33 +0100 <Pickchea> ski, thanks! :-)
2021-11-06 14:06:34 +0100basti_(~basti@ip-84-119-8-195.unity-media.net) (Ping timeout: 260 seconds)
2021-11-06 14:08:50 +0100 <hpc> Inst: there's a win32 package, and bindings to various ui toolkits
2021-11-06 14:09:16 +0100 <Inst> win32 package and bindings to various ui toolkits?
2021-11-06 14:09:25 +0100 <Inst> iirc there's a package to set up windows GUI, etc
2021-11-06 14:09:30 +0100 <hpc> yeah, one of those might have it
2021-11-06 14:09:40 +0100 <Inst> "might"
2021-11-06 14:09:41 +0100 <Inst> sigh
2021-11-06 14:09:48 +0100 <hpc> windows has so many random ways of doing things i don't know exactly what the api call for that dialogue is
2021-11-06 14:10:08 +0100jinsun(~quassel@user/jinsun) (Read error: Connection reset by peer)
2021-11-06 14:10:18 +0100 <hpc> worst case scenario, you get a gtk window instead of a native window
2021-11-06 14:10:28 +0100 <hpc> so that way is guaranteed to work with some effort
2021-11-06 14:10:40 +0100 <hpc> can't help more, myself :(
2021-11-06 14:13:19 +0100burnsidesLlama(~burnsides@dhcp168-023.wadham.ox.ac.uk)
2021-11-06 14:13:48 +0100zincy(~tom@2a00:23c8:970c:4801:e02d:7bbd:5337:7d58) (Remote host closed the connection)
2021-11-06 14:14:02 +0100 <joel135> ski: yes, these contemplations about "power" and "meta-inferences" seem relevant here
2021-11-06 14:16:34 +0100azimut_(~azimut@gateway/tor-sasl/azimut)
2021-11-06 14:17:03 +0100 <Inst> can this handle it for me?
2021-11-06 14:17:04 +0100 <Inst> https://hackage.haskell.org/package/Win32
2021-11-06 14:17:13 +0100 <Inst> it's a win32 api binding for windows
2021-11-06 14:18:02 +0100EvanR(~evan@2600:1700:ba69:10:75fc:f740:4c21:d03d)
2021-11-06 14:19:12 +0100 <ski> joel135 : hm, i see
2021-11-06 14:20:30 +0100azimut(~azimut@gateway/tor-sasl/azimut) (Ping timeout: 276 seconds)
2021-11-06 14:21:05 +0100AlexNoo(~AlexNoo@94.233.241.187)
2021-11-06 14:21:08 +0100AlexZenon(~alzenon@94.233.241.187)
2021-11-06 14:22:03 +0100jinsun(~quassel@user/jinsun)
2021-11-06 14:22:13 +0100 <ski> (it's not really clear to me why polynomials, or "operanomials", crop up here .. also, i'm now vaguely recalling some paper that talked about representing numbers in terms of endofunctions on endofunctions, and, iirc, introduced extra conditions for when one could form e.g. various rationals (in addition to the negatives, which require bijectivity on the inner endos))
2021-11-06 14:22:29 +0100Alex_test(~al_test@94.233.241.187)
2021-11-06 14:25:10 +0100ski. o O ( "Continuity of Gödel's system T definable functionals via effectful forcing" by Martín Escardó in 2013 at <https://www.cs.bham.ac.uk/~mhe/dialogue/dialogue.pdf> .. has oracles )
2021-11-06 14:26:47 +0100raehik(~raehik@cpc95906-rdng25-2-0-cust156.15-3.cable.virginm.net) (Ping timeout: 256 seconds)
2021-11-06 14:27:33 +0100 <tomjaguarpaw> How do I get Haddock to link to a constructor or pattern rather than a data type?
2021-11-06 14:28:12 +0100 <tomjaguarpaw> For example if I have data Foo = Bar; data Baz = Foo how do I get the Haddock syntax 'Foo' to link to the constructor of Bar ?
2021-11-06 14:29:29 +0100 <tomjaguarpaw> Ah, it's v'Foo'
2021-11-06 14:29:34 +0100rond_(~rond_@2a02:a31a:a23c:f480:2fd7:e087:5546:a438) (Quit: Client closed)
2021-11-06 14:29:41 +0100 <tomjaguarpaw> https://github.com/haskell/haddock/issues/667
2021-11-06 14:36:18 +0100max22-(~maxime@2a01cb08833598005d78e1cb2fc9f4a2.ipv6.abo.wanadoo.fr)
2021-11-06 14:40:28 +0100gehmehgeh(~user@user/gehmehgeh) (Quit: Leaving)
2021-11-06 14:40:31 +0100MidAutumnMoon(~MidAutumn@user/midautumnmoon) (Quit: Ping timeout (120 seconds))
2021-11-06 14:40:44 +0100MidAutumnMoon(~MidAutumn@user/midautumnmoon)
2021-11-06 14:40:49 +0100johnny_sitar(~artur@078088015209.bialystok.vectranet.pl)
2021-11-06 14:41:42 +0100max22-(~maxime@2a01cb08833598005d78e1cb2fc9f4a2.ipv6.abo.wanadoo.fr) (Ping timeout: 268 seconds)
2021-11-06 14:48:52 +0100 <gentauro> built my first ARM (M1) Haskell binary with stack/cabal. Not that hard. The worst part? Is going from NixOS + Xmonad to `macOS`. Gosh, that OS is absolutely rubbish :-\
2021-11-06 14:49:31 +0100 <joel135> ski: that stuff of representing numbers (not just the semiring of natural numbers N but also N[x] and so on) in terms of endofunctions on endofunctions is the sort of stuff i was thinking briefly about earlier this week
2021-11-06 14:49:40 +0100gentauroI would <3 that somebody managed to make the `fancy` Apple hardware work on NixOS xD
2021-11-06 14:49:56 +0100raehik(~raehik@cpc95906-rdng25-2-0-cust156.15-3.cable.virginm.net)
2021-11-06 14:50:08 +0100 <joel135> also N[eps] := N[x]/(x^2)
2021-11-06 14:50:47 +0100 <joel135> for what o is this the same as the type (o -> o) -> (o -> o) ? trippy question
2021-11-06 14:52:47 +0100unit73e(~emanuel@2001:818:e8dd:7c00:32b5:c2ff:fe6b:5291) (Ping timeout: 268 seconds)
2021-11-06 14:56:38 +0100favonia(~favonia@user/favonia) (Remote host closed the connection)
2021-11-06 14:57:36 +0100favonia(~favonia@user/favonia)
2021-11-06 14:59:42 +0100 <ski> hmm
2021-11-06 15:04:27 +0100 <tomjaguarpaw> c
2021-11-06 15:08:08 +0100rembo10(~rembo10@remulis.com) (Quit: ZNC 1.8.2 - https://znc.in)
2021-11-06 15:08:43 +0100machinedgod(~machinedg@24.105.81.50)
2021-11-06 15:09:11 +0100rembo10(~rembo10@remulis.com)
2021-11-06 15:12:15 +0100pretty_dumm_guy(trottel@gateway/vpn/protonvpn/prettydummguy/x-88029655)
2021-11-06 15:14:55 +0100jumper149(~jumper149@80.240.31.34) (Quit: WeeChat 3.3)
2021-11-06 15:20:52 +0100max22-(~maxime@2a01cb0883359800bbde3f2c88505b2a.ipv6.abo.wanadoo.fr)
2021-11-06 15:23:38 +0100gg(~gg@2a01:e0a:819:1510:89f0:97ca:21c4:6ea6) (Ping timeout: 268 seconds)
2021-11-06 15:27:32 +0100 <Inst> my problem is partially solved
2021-11-06 15:27:42 +0100 <Inst> turns out there's haskell libs binding to FLTK
2021-11-06 15:27:46 +0100 <Inst> FLTK has native window open close support
2021-11-06 15:28:04 +0100 <Inst> erm, support for opening native file open / save apps
2021-11-06 15:31:16 +0100merijn(~merijn@83-160-49-249.ip.xs4all.nl)
2021-11-06 15:31:24 +0100kspalaiologos(~kspalaiol@user/kspalaiologos)
2021-11-06 15:32:23 +0100hendursaga(~weechat@user/hendursaga) (Remote host closed the connection)
2021-11-06 15:33:05 +0100hendursaga(~weechat@user/hendursaga)
2021-11-06 15:33:30 +0100eggplantade(~Eggplanta@108-201-191-115.lightspeed.sntcca.sbcglobal.net)
2021-11-06 15:38:11 +0100eggplantade(~Eggplanta@108-201-191-115.lightspeed.sntcca.sbcglobal.net) (Ping timeout: 256 seconds)
2021-11-06 15:42:55 +0100__monty__(~toonn@user/toonn)
2021-11-06 15:46:44 +0100burnsidesLlama(~burnsides@dhcp168-023.wadham.ox.ac.uk) (Remote host closed the connection)
2021-11-06 15:47:38 +0100acidjnk(~acidjnk@p200300d0c7263574f86fe22bbcd0fec5.dip0.t-ipconnect.de)
2021-11-06 15:49:20 +0100robertfry(~robertfry@cosh-19-b2-v4wan-161499-cust683.vm10.cable.virginm.net)
2021-11-06 15:53:45 +0100hendursaga(~weechat@user/hendursaga) (Remote host closed the connection)
2021-11-06 15:54:17 +0100hendursaga(~weechat@user/hendursaga)
2021-11-06 15:55:06 +0100TheCoffeMaker_(~TheCoffeM@125-121-245-190.fibertel.com.ar) (Quit: So long and thanks for all the fish)
2021-11-06 15:57:03 +0100TheCoffeMaker(~TheCoffeM@user/thecoffemaker)
2021-11-06 15:57:54 +0100aqua0210(~user@101.85.11.168)
2021-11-06 16:02:18 +0100hololeap_(~hololeap@user/hololeap)
2021-11-06 16:02:33 +0100hololeap(~hololeap@user/hololeap) (Ping timeout: 276 seconds)
2021-11-06 16:03:56 +0100mrkrktsndctcrpt(~mrkrktsnd@50.228.44.6)
2021-11-06 16:05:23 +0100merijn(~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 256 seconds)
2021-11-06 16:08:10 +0100basti_(~basti@ip-84-119-8-195.unity-media.net)
2021-11-06 16:11:38 +0100 <dsal> gentauro: I run nix on macos
2021-11-06 16:12:05 +0100 <dsal> Not xmonad, though. I run that on nixos
2021-11-06 16:13:37 +0100 <gentauro> dsal: yeah, I run the `nix` (package manager) as well on the `macOS`
2021-11-06 16:13:50 +0100 <gentauro> but I would rather run `NixOS` on the Apple hardware ;)
2021-11-06 16:14:17 +0100TranquilEcho(~grom@user/tranquilecho)
2021-11-06 16:15:53 +0100 <geekosaur> xmonad's a bad fit for macos anyway, because of how its x11 emulation works
2021-11-06 16:16:10 +0100 <geekosaur> and you can't use xmonad to manage native windows
2021-11-06 16:16:35 +0100Pickchea(~private@user/pickchea) (Quit: Leaving)
2021-11-06 16:18:08 +0100 <gentauro> dsal: another `bad` thing about `nix` vs `NixOS`, is that you don't have a `stable` channel for packages
2021-11-06 16:18:32 +0100hiruji(~hiruji@user/hiruji)
2021-11-06 16:18:37 +0100 <gentauro> I mean, I tried to build an application on the `macOS` and the `llvm rc-compiler` is broken ..
2021-11-06 16:18:52 +0100 <gentauro> not very "optimal" for a "workstation"
2021-11-06 16:19:41 +0100 <dsal> Heh, I've never been a fan of stable. Makes me think of debian where everything I care about is too old to be useful.
2021-11-06 16:19:52 +0100 <dsal> That's not as much of an issue on nixos, though.
2021-11-06 16:21:59 +0100max22-(~maxime@2a01cb0883359800bbde3f2c88505b2a.ipv6.abo.wanadoo.fr) (Remote host closed the connection)
2021-11-06 16:23:16 +0100aman(~aman@user/aman)
2021-11-06 16:23:33 +0100random-jellyfish(~random-je@user/random-jellyfish) (Ping timeout: 256 seconds)
2021-11-06 16:24:23 +0100burnsidesLlama(~burnsides@dhcp168-023.wadham.ox.ac.uk)
2021-11-06 16:27:41 +0100 <gentauro> dsal: at the moment I can't `build` C/C++ app's on my apple-device. Makes it pretty useless, don't you think?
2021-11-06 16:27:45 +0100acidjnk(~acidjnk@p200300d0c7263574f86fe22bbcd0fec5.dip0.t-ipconnect.de) (Ping timeout: 268 seconds)
2021-11-06 16:27:52 +0100 <EvanR> it's late 2021 does haskell have a decent way to make a global variable
2021-11-06 16:28:10 +0100gentaurounless you want to go the "manual" / `homebrew` way which I don't want to
2021-11-06 16:28:27 +0100 <geekosaur> it probably never will
2021-11-06 16:28:35 +0100 <hpc> EvanR: does it have to be mutable?
2021-11-06 16:28:37 +0100 <gentauro> EvanR: there no concept of `variables`
2021-11-06 16:28:39 +0100 <dsal> gentauro: I have some...
2021-11-06 16:28:39 +0100 <geekosaur> isn't that kinda the point of fp?
2021-11-06 16:28:42 +0100 <gentauro> everything are `values`
2021-11-06 16:28:51 +0100burnsidesLlama(~burnsides@dhcp168-023.wadham.ox.ac.uk) (Ping timeout: 245 seconds)
2021-11-06 16:29:03 +0100 <EvanR> yeah I get it, but instead we have several shitty ways to do it xD
2021-11-06 16:29:18 +0100 <gentauro> dsal: I have setup `nix` + `home-manager` to handle "software". It's the closest I can get to `NixOS` …
2021-11-06 16:29:33 +0100 <hpc> to be fair, there's no good way to do global mutable state :P
2021-11-06 16:29:50 +0100 <dsal> Yeah, "global variables" is one of those engineering practices that people tend to strive for.
2021-11-06 16:30:07 +0100 <geekosaur> yeh, haskell just uncovers all the ugly cracks in the concept
2021-11-06 16:30:10 +0100 <dsal> gentauro: yep, that's how I do it
2021-11-06 16:30:13 +0100 <gentauro> main state = …
2021-11-06 16:30:23 +0100 <gentauro> EvanR: just pass it as a parameter on your main function?
2021-11-06 16:30:25 +0100 <gentauro> :P
2021-11-06 16:30:44 +0100 <hpc> main = newIORef >>= main'
2021-11-06 16:30:59 +0100 <dsal> EvanR: what would you do with a global variable if you had one?
2021-11-06 16:31:17 +0100max22-(~maxime@lfbn-ren-1-762-224.w81-53.abo.wanadoo.fr)
2021-11-06 16:31:23 +0100 <EvanR> one use case would be for a throw away script (in haskell) which uses IO and modifies the globally visible ref for its own inscruptible purposes
2021-11-06 16:31:39 +0100 <gentauro> dsal: read/update from many different threads to get inconsistent resutls :P
2021-11-06 16:31:56 +0100 <[exa]> EvanR: man they literally spent 30 years getting rid of global variables
2021-11-06 16:32:14 +0100 <[exa]> y u no appreciate
2021-11-06 16:32:15 +0100 <EvanR> also, global TVar was used in a game programming example (another area that haskell "is too good for" ? xD)
2021-11-06 16:33:12 +0100 <EvanR> specifically to hold handles to driver resources that are set once
2021-11-06 16:33:28 +0100 <dsal> Sure, I put TVars in Readers for programs.
2021-11-06 16:33:29 +0100 <hpc> game programming is one of the last places you want global state, funny enough
2021-11-06 16:33:36 +0100 <hpc> global player data? what about multiplayer
2021-11-06 16:33:42 +0100 <EvanR> yeah not that
2021-11-06 16:33:43 +0100 <hpc> global viewport data? what about virtual cameras
2021-11-06 16:33:49 +0100waleee(~waleee@2001:9b0:216:8200:d457:9189:7843:1dbd)
2021-11-06 16:34:00 +0100hiruji(~hiruji@user/hiruji) (Quit: ZNC 1.8.2 - https://znc.in)
2021-11-06 16:34:52 +0100shapr(~user@pool-100-36-247-68.washdc.fios.verizon.net)
2021-11-06 16:35:41 +0100 <EvanR> so we have IVars which can be set with IO and then referenced as a pure value, but they're not "global" as such
2021-11-06 16:36:46 +0100kspalaiologos(~kspalaiol@user/kspalaiologos) (Ping timeout: 260 seconds)
2021-11-06 16:37:15 +0100 <dsal> I think there's a bit of a communication problem. Many of us have been programming for decades and have been subjected to global variables in programs and are having difficulty understanding why anyone would think that's a good idea again.
2021-11-06 16:37:17 +0100 <EvanR> doing a monadic read each time you want to access it, in this case, would be silly
2021-11-06 16:38:10 +0100 <hpc> not that silly
2021-11-06 16:38:39 +0100 <hpc> you could read the value once and pass that as a parameter to everything instead
2021-11-06 16:38:48 +0100 <hpc> same way you can read a file and pass a great big ByteString around
2021-11-06 16:41:00 +0100 <EvanR> yeah that's a case when you imagine the data involved being an unknown and potentially visible to the code
2021-11-06 16:42:14 +0100 <EvanR> unlike handles to os resources, GL objects (numbers that one should not mess with)
2021-11-06 16:43:32 +0100 <EvanR> if your program requires a single opaque context or something, it could be convenient to refer to this directly without so much ceremony
2021-11-06 16:44:26 +0100 <EvanR> an example would be a web request handler script, the request is your life, and there's only one
2021-11-06 16:45:00 +0100 <EvanR> bad example I guess, since that data is not opaque nevermind
2021-11-06 16:45:56 +0100 <hpc> i suppose if you really wanted, you could make a dupable unsafePerformIO readIORef kind of thing, and then you have something mutable you don't have to actually read from
2021-11-06 16:46:00 +0100 <hpc> but then you have Very Fun Bugs
2021-11-06 16:46:08 +0100 <EvanR> exactly
2021-11-06 16:47:12 +0100hololeap_hololeap
2021-11-06 16:52:53 +0100 <EvanR> another difficulty is realistic programs with many modules, you would need some sort of bureacracy to understand who can see the global
2021-11-06 16:53:50 +0100fendor_(~fendor@178.165.196.101.wireless.dyn.drei.com)
2021-11-06 16:54:26 +0100 <monochrom> Fortunately, today you can use the (rhetorical) question "is it thread-safe?" to exorcise any want of global variables. In C and Unix, this has happened to errno, random_r(), DNS libraries.
2021-11-06 16:54:35 +0100 <EvanR> also if its a library, how would libraries not collide on the name
2021-11-06 16:55:24 +0100 <EvanR> errno, great example of a terrible use for global variable
2021-11-06 16:55:30 +0100pretty_dumm_guy(trottel@gateway/vpn/protonvpn/prettydummguy/x-88029655) (Ping timeout: 260 seconds)
2021-11-06 16:55:47 +0100 <monochrom> Oh haha, name clash is solved by every library choosing a prefix and hoping that it's, um, universally unique :)
2021-11-06 16:56:22 +0100fendor(~fendor@91.141.74.77.wireless.dyn.drei.com) (Ping timeout: 260 seconds)
2021-11-06 17:02:00 +0100Gurkenglas(~Gurkengla@dslb-002-203-144-204.002.203.pools.vodafone-ip.de)
2021-11-06 17:02:22 +0100 <hpc> just do what ldap does and give everything an oid
2021-11-06 17:02:31 +0100 <hpc> instead of defining bitwise_and, define 1.2.840.113556.1.4.803
2021-11-06 17:02:35 +0100 <hpc> easy
2021-11-06 17:03:12 +0100x6C697370(~michael@2600:1700:7c02:3180::44)
2021-11-06 17:03:33 +0100pretty_dumm_guy(trottel@gateway/vpn/protonvpn/prettydummguy/x-88029655)
2021-11-06 17:03:42 +0100max22-(~maxime@lfbn-ren-1-762-224.w81-53.abo.wanadoo.fr) (Remote host closed the connection)
2021-11-06 17:03:59 +0100hiruji(~hiruji@user/hiruji)
2021-11-06 17:04:40 +0100max22-(~maxime@lfbn-ren-1-762-224.w81-53.abo.wanadoo.fr)
2021-11-06 17:05:08 +0100 <Inst> are there any haskellers using visual studio code?
2021-11-06 17:05:16 +0100 <Inst> I need to figure out how to install packages from hackage
2021-11-06 17:05:30 +0100 <Inst> https://hackage.haskell.org/package/fltkhs
2021-11-06 17:05:32 +0100gg(~gg@88.160.100.84)
2021-11-06 17:06:13 +0100fendor_fendor
2021-11-06 17:06:30 +0100 <[exa]> Inst: you can either make a cabal project and write it in the dependencies (will get auto-installed) or just invoke cabal from the commandline
2021-11-06 17:06:57 +0100 <Inst> I got VSC specifically to avoid using cabal / stock
2021-11-06 17:06:57 +0100 <maerwald> Inst: https://cabal.readthedocs.io/en/latest/getting-started.html
2021-11-06 17:06:59 +0100 <Inst> stack
2021-11-06 17:07:02 +0100 <Inst> thanks
2021-11-06 17:07:28 +0100 <geekosaur> I don't think you'll be able to avoid using at least one of them
2021-11-06 17:09:20 +0100 <hpc> and if you use stack, you're still not getting away from using cabal too
2021-11-06 17:10:11 +0100 <[exa]> why avoid it though?
2021-11-06 17:11:17 +0100 <Inst> minimize challenge
2021-11-06 17:11:18 +0100 <geekosaur> avoiding both is a nice way to get yourself into nasty dependency jungles
2021-11-06 17:11:21 +0100 <Inst> ugh, i'm stuck with cabal, then
2021-11-06 17:11:33 +0100 <geekosaur> which is not minimizing challenge
2021-11-06 17:11:42 +0100 <monochrom> vsc is orthogonal to avoiding cabal and stack. To avoid cabal and stack, either don't use any 3rd-party libraries or manually run Setup.hs per library.
2021-11-06 17:12:00 +0100hendursaga(~weechat@user/hendursaga) (Quit: hendursaga)
2021-11-06 17:12:01 +0100 <[exa]> Inst: honestly, setting up a cabal package (using the guide linked above) is like 2539872345x less of a trick than trying vscode do it correctly
2021-11-06 17:12:14 +0100 <Inst> thanks for the help
2021-11-06 17:12:25 +0100hendursaga(~weechat@user/hendursaga)
2021-11-06 17:12:35 +0100 <Inst> i'm trying to set up a hack to get Haskell to be able to call native Windows file open / save windows
2021-11-06 17:12:45 +0100 <Inst> I'm suspecting fltkhs might not be able to do it, though
2021-11-06 17:13:21 +0100 <monochrom> Consider https://hackage.haskell.org/package/Win32
2021-11-06 17:13:49 +0100 <monochrom> or generally https://hackage.haskell.org/packages/search?terms=win32
2021-11-06 17:13:57 +0100Sgeo(~Sgeo@user/sgeo)
2021-11-06 17:14:08 +0100[itchyjunk](~itchyjunk@user/itchyjunk/x-7353470) (Read error: Connection reset by peer)
2021-11-06 17:14:23 +0100 <[exa]> the open/save dialogs are not a part of any C-style winapi right?
2021-11-06 17:14:55 +0100 <EvanR> proper bindings to win API sounds like the right thing. But if you want hacks... write a normal windows program and control it from haskell using interprocess communication xD
2021-11-06 17:15:46 +0100 <EvanR> bonus it will work on not windows too, as soon as you implement the other native front ends
2021-11-06 17:16:57 +0100 <monochrom> Write a webapp. Then there is only one native front end. >:)
2021-11-06 17:17:22 +0100 <[exa]> Inst: if fltk fails, consider making a small C program with this library https://github.com/mlabbe/nativefiledialog
2021-11-06 17:17:27 +0100 <[exa]> and calling it from haskell via FFI
2021-11-06 17:17:39 +0100 <Inst> thanks exa, you're a lifesaver
2021-11-06 17:18:13 +0100 <Inst> exa: how did the Instagram filters go?
2021-11-06 17:18:26 +0100aman(~aman@user/aman) (Ping timeout: 245 seconds)
2021-11-06 17:18:28 +0100 <Inst> I was also thinking: "use Haskell to strip DRM from obsolete CDs"
2021-11-06 17:18:45 +0100 <Inst> or "use Haskell, with or without the assistance of a finance export / prof, to do stock market analysis"
2021-11-06 17:18:50 +0100 <Inst> those are both practical and interesting
2021-11-06 17:18:51 +0100 <[exa]> it was kinda too specific, we went with something different at the end
2021-11-06 17:19:09 +0100 <Inst> as long as it works out
2021-11-06 17:19:19 +0100 <[exa]> too much time for tuning the filters and from haskell-side the assignment is not really challenging
2021-11-06 17:19:31 +0100 <Inst> the reason I need Haskell with a file open / shut hack is so I can try to teach my fellow non-programmer friend
2021-11-06 17:19:47 +0100 <Inst> Haskell with early IO
2021-11-06 17:20:19 +0100 <EvanR> define early IO
2021-11-06 17:21:21 +0100Lycurgus(~juan@98.4.112.204)
2021-11-06 17:22:27 +0100 <Inst> main = do -> random stuff in monad-land without explaining monads -> how2io -> typeclasses, expressions, recursion, lists, etc
2021-11-06 17:23:01 +0100aqua0210(~user@101.85.11.168) (Ping timeout: 245 seconds)
2021-11-06 17:23:20 +0100 <Inst> i need to keep her engaged so she doesn't run off to Python
2021-11-06 17:23:24 +0100 <Inst> which she threatens to do
2021-11-06 17:23:33 +0100 <EvanR> oh yeah... sounds helpful to have some magic IO actions that just do stuff
2021-11-06 17:23:59 +0100 <Inst> "in media res"
2021-11-06 17:24:14 +0100 <EvanR> pickFile :: IO Filepath
2021-11-06 17:24:16 +0100 <EvanR> xD
2021-11-06 17:24:45 +0100 <Inst> you're being sarcastic, right?
2021-11-06 17:24:58 +0100 <EvanR> no?
2021-11-06 17:25:16 +0100 <Inst> thanks
2021-11-06 17:26:01 +0100desantra(~skykanin@user/skykanin) (Quit: WeeChat 3.3)
2021-11-06 17:26:11 +0100 <Inst> the idea is that IO makes everything practical now, you see immediate results, the build-up of understanding and skill via theory is immediately useful because the theory etc immediately gets translated back to practical results
2021-11-06 17:26:16 +0100 <Inst> therefore, no running off to Pythonland
2021-11-06 17:26:28 +0100 <Lycurgus> geekosaur, you cheeky debbil i just realized you pm'ed me without notice was the thing to be suppressed so soto voce?
2021-11-06 17:26:51 +0100 <Lycurgus> and how is quietism gonna work?
2021-11-06 17:27:23 +0100 <geekosaur> mostly hoping the whole thing would blow over faster if not publicly restarted
2021-11-06 17:27:57 +0100 <Lycurgus> illogical to think doing nothing will cause the desired result
2021-11-06 17:28:12 +0100 <Inst> moreover, I asked someone for a monad tutorial a while back, they suggested the best way to learn it is to run around without monads until you accidentally implement it yourself
2021-11-06 17:28:25 +0100 <Inst> Lycurgus: you know what's the easiest way to kill someone?
2021-11-06 17:28:29 +0100 <Lycurgus> doing stuff behind the scenes, yeah
2021-11-06 17:28:43 +0100 <Lycurgus> Inst, no what?
2021-11-06 17:28:50 +0100 <Inst> eat doritos
2021-11-06 17:28:51 +0100 <Inst> drink beer
2021-11-06 17:28:55 +0100 <Inst> watch TV, go on with your everyday life
2021-11-06 17:29:04 +0100 <EvanR> yes the monad tutorial fallacy
2021-11-06 17:29:06 +0100 <Inst> eventually that someone will drop dead of hopefully natural causes
2021-11-06 17:29:12 +0100 <Lycurgus> i c
2021-11-06 17:29:18 +0100 <Inst> you're in their light cone
2021-11-06 17:29:25 +0100 <Inst> technically you're a causative actor in the most minimal way possible
2021-11-06 17:29:31 +0100max22-(~maxime@lfbn-ren-1-762-224.w81-53.abo.wanadoo.fr) (Remote host closed the connection)
2021-11-06 17:29:32 +0100 <Inst> so no, doing nothing is not illogical
2021-11-06 17:29:39 +0100 <Lycurgus> and the death will be attributed to covid prolly
2021-11-06 17:29:54 +0100 <Inst> 无为
2021-11-06 17:30:06 +0100 <EvanR> Inst I think you're on the right track
2021-11-06 17:30:10 +0100 <monochrom> It is OK to learn and use IO without bringing up the monad generality.
2021-11-06 17:30:13 +0100lyxia(~lyxia@poisson.chat) (Quit: WeeChat 3.2)
2021-11-06 17:30:18 +0100 <EvanR> ^
2021-11-06 17:30:27 +0100lyxia(~lyxia@poisson.chat)
2021-11-06 17:30:35 +0100 <Inst> whitington does something similar, i.e, he teaches how to use either, maybe, and io
2021-11-06 17:30:39 +0100 <Inst> without going into monads
2021-11-06 17:31:02 +0100 <monochrom> People have already learned and are using numbers without ring field generality. Heck most of them haven't even heard of Peano axioms.
2021-11-06 17:31:03 +0100 <Inst> he says it's for another book, but i feel sufficiently functional (small f) without it
2021-11-06 17:31:09 +0100 <EvanR> if they're a complete beginner, then they won't even want to get into monad memes with you
2021-11-06 17:31:18 +0100Lycurgusabhors all mysticism and religion, taoism and quietism are no exceptions
2021-11-06 17:31:18 +0100 <Inst> I just feel hungry for burritos
2021-11-06 17:31:29 +0100 <Inst> Taoism -> philosophical and religious elements
2021-11-06 17:31:31 +0100 <Inst> but offtopic
2021-11-06 17:31:37 +0100yauhsien(~yauhsien@118-167-41-229.dynamic-ip.hinet.net)
2021-11-06 17:31:43 +0100burnsidesLlama(~burnsides@dhcp168-023.wadham.ox.ac.uk)
2021-11-06 17:31:44 +0100 <maerwald> best way to get into monads is to see what you can't do with applicative
2021-11-06 17:32:12 +0100 <EvanR> and applicative requires first explaining or demonstrating Functor, which is a lot more useful anyway xD
2021-11-06 17:32:34 +0100 <Lycurgus> or be super reductionist and say it's just a damn datastruce hs weenies use to get referential transparency
2021-11-06 17:32:35 +0100aqua0210(~user@101.85.11.168)
2021-11-06 17:32:46 +0100 <EvanR> no don't
2021-11-06 17:32:51 +0100 <monochrom> That is false.
2021-11-06 17:32:53 +0100 <Lycurgus> *data structure
2021-11-06 17:33:08 +0100 <Lycurgus> yeah it's a lil more than just reductionist
2021-11-06 17:33:22 +0100 <monochrom> Unless you decide to classify the X->Y type as a data structure too.
2021-11-06 17:33:40 +0100 <Lycurgus> but only wrong by a detail
2021-11-06 17:34:18 +0100 <EvanR> since X->Y is a negative type, perhaps you could classify it as a negative data structure xD
2021-11-06 17:35:17 +0100eggplantade(~Eggplanta@108-201-191-115.lightspeed.sntcca.sbcglobal.net)
2021-11-06 17:35:21 +0100 <maerwald> what do monads have to do with referential transparency?
2021-11-06 17:35:41 +0100 <hpc> here's a fun math game: combine related concepts to create the most confused terminology possible
2021-11-06 17:35:51 +0100 <hpc> X is negative in X -> Y, but also X -> Y = Y ** X
2021-11-06 17:35:58 +0100 <hpc> so in exponentiation, the value on the right is negative
2021-11-06 17:36:24 +0100mrkrktsn1ctcrpt(~mrkrktsnd@50.228.44.6)
2021-11-06 17:36:30 +0100 <hpc> @let negate x = (** x)
2021-11-06 17:36:31 +0100 <lambdabot> Defined.
2021-11-06 17:37:25 +0100 <geekosaur> isn't that going to collide with Prelude negate?
2021-11-06 17:37:30 +0100 <hpc> :P
2021-11-06 17:38:53 +0100mrkrktsndctcrpt(~mrkrktsnd@50.228.44.6) (Ping timeout: 256 seconds)
2021-11-06 17:39:24 +0100 <EvanR> when two negates collide, the result is a positive
2021-11-06 17:39:46 +0100eggplantade(~Eggplanta@108-201-191-115.lightspeed.sntcca.sbcglobal.net) (Ping timeout: 260 seconds)
2021-11-06 17:43:59 +0100mrkrktsn1ctcrpt(~mrkrktsnd@50.228.44.6) (Ping timeout: 256 seconds)
2021-11-06 17:46:08 +0100tfeb(~tfb@88.98.95.237)
2021-11-06 17:48:05 +0100 <xerox> > negate it
2021-11-06 17:48:07 +0100 <lambdabot> error:
2021-11-06 17:48:07 +0100 <lambdabot> • Variable not in scope: it
2021-11-06 17:48:07 +0100 <lambdabot> • Perhaps you meant one of these:
2021-11-06 17:49:32 +0100 <Lycurgus> lambdabot doesn't have prelude?
2021-11-06 17:50:00 +0100 <Lycurgus> or the same error processing as ghci igess
2021-11-06 17:51:21 +0100zaquest(~notzaques@5.128.210.178) (Quit: Leaving)
2021-11-06 17:53:26 +0100bitdex(~bitdex@gateway/tor-sasl/bitdex) (Remote host closed the connection)
2021-11-06 17:54:41 +0100whatsupdoc(uid509081@id-509081.hampstead.irccloud.com)
2021-11-06 17:54:58 +0100bitdex(~bitdex@gateway/tor-sasl/bitdex)
2021-11-06 17:55:46 +0100zaquest(~notzaques@5.128.210.178)
2021-11-06 17:56:12 +0100fendor(~fendor@178.165.196.101.wireless.dyn.drei.com) (Remote host closed the connection)
2021-11-06 17:58:27 +0100merijn(~merijn@83-160-49-249.ip.xs4all.nl)
2021-11-06 18:00:05 +0100Lord_of_Life(~Lord@user/lord-of-life/x-2819915) (Excess Flood)
2021-11-06 18:00:48 +0100fendor(~fendor@178.165.196.101.wireless.dyn.drei.com)
2021-11-06 18:00:54 +0100pavonia(~user@user/siracusa) (Quit: Bye!)
2021-11-06 18:01:26 +0100Lord_of_Life(~Lord@user/lord-of-life/x-2819915)
2021-11-06 18:04:49 +0100tfeb(~tfb@88.98.95.237) (Quit: died)
2021-11-06 18:05:11 +0100merijn(~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 264 seconds)
2021-11-06 18:07:28 +0100mrkrktsndctcrpt(~mrkrktsnd@mobile-166-171-248-94.mycingular.net)
2021-11-06 18:11:46 +0100 <geekosaur> Lycurgus, it's not ghci, no. it used to expose a variable that worked not quite like "it" but it got abused
2021-11-06 18:12:45 +0100 <hpc> yahb is ghci
2021-11-06 18:12:47 +0100 <hpc> % it
2021-11-06 18:12:48 +0100 <yahb> hpc: ()
2021-11-06 18:13:09 +0100 <hpc> you even get to execute IO
2021-11-06 18:13:56 +0100mastarija(~mastarija@2a05:4f46:e06:ff00:18c4:3126:ef80:d743)
2021-11-06 18:16:30 +0100burnsidesLlama(~burnsides@dhcp168-023.wadham.ox.ac.uk) (Remote host closed the connection)
2021-11-06 18:16:52 +0100 <Lycurgus> % negate it
2021-11-06 18:16:52 +0100 <yahb> Lycurgus: ; <interactive>:2:1: error:; * No instance for (Num ()) arising from a use of `negate'; * In the expression: negate it; In an equation for `it': it = negate it
2021-11-06 18:17:18 +0100 <Lycurgus> whatever repl i have stacked suggests id from prelude
2021-11-06 18:18:14 +0100 <Lycurgus> 'foolish consistency is the hobgoblin of small minds'
2021-11-06 18:20:34 +0100v01d4lph4(~v01d4lph4@122.177.85.95)
2021-11-06 18:20:34 +0100v01d4lph4(~v01d4lph4@122.177.85.95) (Changing host)
2021-11-06 18:20:34 +0100v01d4lph4(~v01d4lph4@user/v01d4lph4)
2021-11-06 18:20:42 +0100max22-(~maxime@lfbn-ren-1-762-224.w81-53.abo.wanadoo.fr)
2021-11-06 18:20:46 +0100 <hpc> i prefer consistent foolishness
2021-11-06 18:21:18 +0100 <monochrom> I don't see a foolish consistency there.
2021-11-06 18:21:24 +0100 <monochrom> Foolish spell-checking, maybe.
2021-11-06 18:22:18 +0100 <Lycurgus> no here it would be a foolish expectation of consistency
2021-11-06 18:22:37 +0100aleator(~aleator@87-93-222-114.bb.dnainternet.fi)
2021-11-06 18:23:10 +0100aqua0210(~user@101.85.11.168) (Ping timeout: 260 seconds)
2021-11-06 18:23:23 +0100econo(uid147250@user/econo)
2021-11-06 18:23:33 +0100 <monochrom> I guess I have a foolish expectation of accurate wording, too.
2021-11-06 18:24:31 +0100 <monochrom> Now Inst is going to breathe "the accuracy that can be accurated is not the real accuracy" down my throat :)
2021-11-06 18:24:48 +0100 <Inst> um, what, it's just noumenon vs phenomenon
2021-11-06 18:25:06 +0100 <Inst> we try to get as close as we can to the actual reality, but the actual reality is unreachable
2021-11-06 18:25:30 +0100 <Inst> good enough, back to work, have a beer after you're done
2021-11-06 18:25:32 +0100v01d4lph4(~v01d4lph4@user/v01d4lph4) (Ping timeout: 268 seconds)
2021-11-06 18:25:34 +0100 <Inst> don't be a pedant
2021-11-06 18:25:42 +0100fuzzypixelz(~fuzzypixe@eth-west-pareq2-46-193-4-100.wb.wifirst.net)
2021-11-06 18:26:38 +0100lavaman(~lavaman@98.38.249.169)
2021-11-06 18:28:10 +0100 <Lycurgus> copilot suggests "= "/" ++ it
2021-11-06 18:28:42 +0100 <Lycurgus> "
2021-11-06 18:30:31 +0100burnsidesLlama(~burnsides@dhcp168-023.wadham.ox.ac.uk)
2021-11-06 18:31:06 +0100lavaman(~lavaman@98.38.249.169) (Ping timeout: 260 seconds)
2021-11-06 18:31:34 +0100tzh(~tzh@c-24-21-73-154.hsd1.wa.comcast.net)
2021-11-06 18:32:05 +0100robertfry(~robertfry@cosh-19-b2-v4wan-161499-cust683.vm10.cable.virginm.net) (Quit: Konversation terminated!)
2021-11-06 18:32:34 +0100mrkrktsndctcrpt(~mrkrktsnd@mobile-166-171-248-94.mycingular.net) (Ping timeout: 260 seconds)
2021-11-06 18:33:27 +0100ulvarrefr(~user@185.24.53.152) (Read error: Connection reset by peer)
2021-11-06 18:33:34 +0100ulvarrefr(~user@185.24.53.152)
2021-11-06 18:35:51 +0100merijn(~merijn@83-160-49-249.ip.xs4all.nl)
2021-11-06 18:38:19 +0100aleator(~aleator@87-93-222-114.bb.dnainternet.fi) (Ping timeout: 260 seconds)
2021-11-06 18:40:09 +0100random-jellyfish(~random-je@user/random-jellyfish)
2021-11-06 18:40:58 +0100merijn(~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 268 seconds)
2021-11-06 18:43:05 +0100Lycurgus(~juan@98.4.112.204) (Quit: Exeunt)
2021-11-06 18:43:36 +0100Pickchea(~private@user/pickchea)
2021-11-06 18:45:23 +0100hiruji(~hiruji@user/hiruji) (Ping timeout: 264 seconds)
2021-11-06 18:48:30 +0100hgolden(~hgolden2@cpe-172-114-81-123.socal.res.rr.com) (Remote host closed the connection)
2021-11-06 18:48:53 +0100aqua0210(~user@101.85.11.168)
2021-11-06 18:49:48 +0100hgolden(~hgolden2@cpe-172-114-81-123.socal.res.rr.com)
2021-11-06 18:50:13 +0100Guest|10(~Guest|10@70-36-136-248.dsl.dynamic.fusionbroadband.com)
2021-11-06 18:51:05 +0100Guest|10(~Guest|10@70-36-136-248.dsl.dynamic.fusionbroadband.com) (Client Quit)
2021-11-06 18:51:15 +0100hiruji(~hiruji@user/hiruji)
2021-11-06 18:54:15 +0100aqua0210(~user@101.85.11.168) (Ping timeout: 256 seconds)
2021-11-06 18:55:57 +0100hiruji(~hiruji@user/hiruji) (Ping timeout: 256 seconds)
2021-11-06 18:59:00 +0100eggplantade(~Eggplanta@108-201-191-115.lightspeed.sntcca.sbcglobal.net)
2021-11-06 18:59:07 +0100 <tomjaguarpaw> Anyone know where there isn't a ShowTypePrec or ShowTypeParens for TypeError ? Looks like I have to either tolerate MyConstructor (Int) or MyConstructor Just a
2021-11-06 19:01:40 +0100random-jellyfish(~random-je@user/random-jellyfish) (Ping timeout: 256 seconds)
2021-11-06 19:05:14 +0100aqua0210(~user@101.85.11.168)
2021-11-06 19:06:27 +0100jess(~jess@libera/staff/jess) ()
2021-11-06 19:09:43 +0100ees(~user@pool-108-18-30-46.washdc.fios.verizon.net)
2021-11-06 19:11:47 +0100aqua0210(~user@101.85.11.168) (Ping timeout: 268 seconds)
2021-11-06 19:13:18 +0100merijn(~merijn@83-160-49-249.ip.xs4all.nl)
2021-11-06 19:13:35 +0100ees(~user@pool-108-18-30-46.washdc.fios.verizon.net) (Read error: Connection reset by peer)
2021-11-06 19:14:40 +0100ees(~user@pool-108-18-30-46.washdc.fios.verizon.net)
2021-11-06 19:23:28 +0100msmhnd^(~msmhnd@h50.174.139.63.static.ip.windstream.net) (Remote host closed the connection)
2021-11-06 19:24:43 +0100aqua0210(~user@101.85.11.168)
2021-11-06 19:30:06 +0100aqua0210(~user@101.85.11.168) (Ping timeout: 245 seconds)
2021-11-06 19:34:19 +0100eggplantade(~Eggplanta@108-201-191-115.lightspeed.sntcca.sbcglobal.net) (Remote host closed the connection)
2021-11-06 19:36:24 +0100hololeap(~hololeap@user/hololeap) (Ping timeout: 276 seconds)
2021-11-06 19:36:48 +0100hololeap(~hololeap@user/hololeap)
2021-11-06 19:38:02 +0100yauhsien(~yauhsien@118-167-41-229.dynamic-ip.hinet.net) (Remote host closed the connection)
2021-11-06 19:38:39 +0100yauhsien(~yauhsien@118-167-41-229.dynamic-ip.hinet.net)
2021-11-06 19:40:14 +0100burnsidesLlama(~burnsides@dhcp168-023.wadham.ox.ac.uk) (Remote host closed the connection)
2021-11-06 19:41:18 +0100justsomeguy(~justsomeg@user/justsomeguy)
2021-11-06 19:42:01 +0100kawzeg(kawzeg@2a01:7e01::f03c:92ff:fee2:ec34)
2021-11-06 19:43:02 +0100aqua0210(~user@101.85.11.168)
2021-11-06 19:44:40 +0100hiruji(~hiruji@user/hiruji)
2021-11-06 19:46:10 +0100 <hololeap> anyone know of a library for normalizing inequalities?
2021-11-06 19:46:30 +0100 <awpr> type-level Nat inequalities?
2021-11-06 19:46:43 +0100 <hololeap> no, just any Ord
2021-11-06 19:47:31 +0100merijn(~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 256 seconds)
2021-11-06 19:47:52 +0100 <hololeap> for instance, if I have a set of inequalities on Int, [>=4, <8, >5, <6], it would find the smallest set of inequalities that satisfy all those: [>5, <6]
2021-11-06 19:48:09 +0100eruditass(uid248673@id-248673.uxbridge.irccloud.com)
2021-11-06 19:48:10 +0100aqua0210(~user@101.85.11.168) (Ping timeout: 260 seconds)
2021-11-06 19:48:33 +0100 <awpr> hmm, I don't know of a library specifically for that, but you might be able to find an interval library that could do it with left-infinite and right-infinite intervals
2021-11-06 19:49:33 +0100yauhsien(~yauhsien@118-167-41-229.dynamic-ip.hinet.net) (Remote host closed the connection)
2021-11-06 19:50:05 +0100yauhsien(~yauhsien@118-167-41-229.dynamic-ip.hinet.net)
2021-11-06 19:52:00 +0100ees(~user@pool-108-18-30-46.washdc.fios.verizon.net) (ERC 5.4 (IRC client for GNU Emacs 28.0.60))
2021-11-06 19:52:42 +0100ees(~ees@pool-108-18-30-46.washdc.fios.verizon.net)
2021-11-06 19:54:42 +0100 <hololeap> this doesn't really match what I'm asking for, but seems interesting: https://hackage.haskell.org/package/speculate
2021-11-06 19:55:10 +0100dsrt^(~dsrt@h50.174.139.63.static.ip.windstream.net) (Ping timeout: 260 seconds)
2021-11-06 19:57:34 +0100 <hololeap> awpr: can you give an example of how intervals are relavant to my question? I'm not too familiar with the math terms behind it, so it might be helpful to me finding what I'm looking for.
2021-11-06 19:58:31 +0100chisui(~chisui@dyndsl-095-033-149-191.ewe-ip-backbone.de)
2021-11-06 19:58:38 +0100 <EvanR> so you want to merge all the half open intervals to get a two sided interval, but also track the difference between < and <=
2021-11-06 19:58:41 +0100 <geekosaur> >=4 is 4–inf, for example. then use an interval library that can find the smallest (resp. largest) bounding interval for all of your intervals
2021-11-06 20:00:02 +0100 <EvanR> if it's integers you could simplify to only <='s
2021-11-06 20:00:12 +0100 <geekosaur> and then translate back to comparisons
2021-11-06 20:00:46 +0100ees(~ees@pool-108-18-30-46.washdc.fios.verizon.net) (Killed buffer)
2021-11-06 20:01:20 +0100chisui(~chisui@dyndsl-095-033-149-191.ewe-ip-backbone.de) (Client Quit)
2021-11-06 20:01:28 +0100 <hololeap> ok
2021-11-06 20:02:37 +0100 <hololeap> this is going to be for parsing package versions from various PMSs, so it will likely be a (NonEmpty Natural) value for the comparisons
2021-11-06 20:03:07 +0100kawzeg(kawzeg@2a01:7e01::f03c:92ff:fee2:ec34) (Quit: WeeChat 3.3)
2021-11-06 20:03:55 +0100 <hololeap> but that makes sense, smallest bounding interval
2021-11-06 20:05:27 +0100kawzeg(kawzeg@2a01:7e01::f03c:92ff:fee2:ec34)
2021-11-06 20:07:14 +0100 <hololeap> hm, I might also want to normalize versions, for instance 5.0.0 = 5 (for this purpose)
2021-11-06 20:08:09 +0100yauhsien(~yauhsien@118-167-41-229.dynamic-ip.hinet.net) (Remote host closed the connection)
2021-11-06 20:08:14 +0100 <geekosaur> that might not work so well in the presence of a version like 5.0.12
2021-11-06 20:08:42 +0100yauhsien(~yauhsien@118-167-41-229.dynamic-ip.hinet.net)
2021-11-06 20:09:15 +0100 <hololeap> this is going to be for normalizing version range dependencies
2021-11-06 20:09:23 +0100 <hololeap> so >5.0.0 = >5
2021-11-06 20:09:32 +0100ees(~user@pool-108-18-30-46.washdc.fios.verizon.net)
2021-11-06 20:10:32 +0100 <hololeap> >5.0.12 /= >5
2021-11-06 20:10:49 +0100neurocyte0132889(~neurocyte@45.10.61.172)
2021-11-06 20:10:49 +0100neurocyte0132889(~neurocyte@45.10.61.172) (Changing host)
2021-11-06 20:10:49 +0100neurocyte0132889(~neurocyte@user/neurocyte)
2021-11-06 20:13:47 +0100zzz(~z@user/zero)
2021-11-06 20:13:50 +0100yauhsien(~yauhsien@118-167-41-229.dynamic-ip.hinet.net) (Ping timeout: 260 seconds)
2021-11-06 20:15:35 +0100eggplantade(~Eggplanta@108-201-191-115.lightspeed.sntcca.sbcglobal.net)
2021-11-06 20:15:48 +0100mrkrktsndctcrpt(~mrkrktsnd@c-24-6-12-87.hsd1.ca.comcast.net)
2021-11-06 20:17:53 +0100lavaman(~lavaman@98.38.249.169)
2021-11-06 20:20:34 +0100burnsidesLlama(~burnsides@dhcp168-023.wadham.ox.ac.uk)
2021-11-06 20:21:04 +0100whatsupdoc(uid509081@id-509081.hampstead.irccloud.com) (Quit: Connection closed for inactivity)
2021-11-06 20:24:23 +0100 <zzz> @def newtype N = N Int
2021-11-06 20:24:24 +0100 <lambdabot> Defined.
2021-11-06 20:24:29 +0100 <zzz> @def sup (N x) = ("sup",x)
2021-11-06 20:24:30 +0100 <lambdabot> Defined.
2021-11-06 20:24:34 +0100 <zzz> > fst $ sup undefined
2021-11-06 20:24:35 +0100 <lambdabot> "sup"
2021-11-06 20:25:10 +0100 <zzz> this patternmatches because the newtype "doesn't really exist" right?
2021-11-06 20:25:37 +0100 <dolio> Something like that.
2021-11-06 20:26:54 +0100burnsidesLlama(~burnsides@dhcp168-023.wadham.ox.ac.uk) (Ping timeout: 260 seconds)
2021-11-06 20:27:03 +0100 <zzz> somehow i feel like there's something more to say
2021-11-06 20:27:09 +0100 <tomjaguarpaw> zzz: No, why? If you defined it as data you'd get the same behaviour
2021-11-06 20:27:28 +0100 <dolio> No, with data you'd get undefined.
2021-11-06 20:27:46 +0100 <hololeap> "sup" is a literal so it doesn't need the value of x
2021-11-06 20:27:47 +0100 <tomjaguarpaw> Oh yes, so you would
2021-11-06 20:28:28 +0100 <dolio> You can also imagine that ~ is the default mode for newtype patterns.
2021-11-06 20:28:30 +0100 <tomjaguarpaw> Right, so the N pattern doesn't actually force anything whereas the D pattern would
2021-11-06 20:29:08 +0100 <c_wraith> zzz: the best way to think of it is that matching a newtype constructor is a coercion. Matching a data constructor is evaluation.
2021-11-06 20:30:02 +0100 <zzz> right
2021-11-06 20:30:44 +0100 <dolio> zzz: Sometimes you can observe incidental consequences of wrapping things in a newtype.
2021-11-06 20:31:09 +0100 <dolio> Like, if you have polymorphic stuff in a newtype, it might cause an eta expansion that makes something non-bottom.
2021-11-06 20:31:35 +0100zmt00(~zmt00@user/zmt00) (Ping timeout: 264 seconds)
2021-11-06 20:31:38 +0100 <zzz> can you provide an example of that?
2021-11-06 20:31:46 +0100 <dolio> No, I don't remember an example. :)
2021-11-06 20:32:44 +0100 <hololeap> I don't understand either, dolio
2021-11-06 20:32:57 +0100max22-(~maxime@lfbn-ren-1-762-224.w81-53.abo.wanadoo.fr) (Remote host closed the connection)
2021-11-06 20:33:45 +0100zmt00(~zmt00@user/zmt00)
2021-11-06 20:34:42 +0100aqua0210(~user@101.85.11.168)
2021-11-06 20:35:06 +0100 <c_wraith> @let newtype F = F (forall f. Functor f => () -> f ())
2021-11-06 20:35:07 +0100 <lambdabot> Defined.
2021-11-06 20:35:10 +0100 <dolio> The type was like `newtype N = N (forall a. <something>)`, and somehow it was possible that the generalization step caused by `N e` made an undefined expression `e` get expanded into something more like `\_ -> undefined`.
2021-11-06 20:35:15 +0100 <c_wraith> > seq (F undefined) ()
2021-11-06 20:35:16 +0100 <lambdabot> ()
2021-11-06 20:35:22 +0100 <c_wraith> just like that
2021-11-06 20:35:26 +0100 <dolio> Oh, nice.
2021-11-06 20:35:37 +0100FragByte(~christian@user/fragbyte) (Quit: Quit)
2021-11-06 20:36:03 +0100max22-(~maxime@2a01cb0883359800ab19ff1ba7c64c00.ipv6.abo.wanadoo.fr)
2021-11-06 20:36:05 +0100 <tomjaguarpaw> Interesting
2021-11-06 20:36:09 +0100 <c_wraith> and yeah, that's eta expansion biting
2021-11-06 20:36:36 +0100 <dolio> Yeah, the newtype still 'doesn't exist', but the generality of the type it corresponds to might have semantic consequences.
2021-11-06 20:37:10 +0100 <dolio> And might force generalizing something that wouldn't otherwise be generalized.
2021-11-06 20:37:24 +0100FragByte(~christian@user/fragbyte)
2021-11-06 20:37:33 +0100 <c_wraith> It requires the class constraint
2021-11-06 20:37:47 +0100 <c_wraith> So it has something to do with dictionary passing in the internal representation
2021-11-06 20:37:52 +0100 <tomjaguarpaw> newtype F = F (forall f. f ()) shows the same behaviour
2021-11-06 20:37:54 +0100 <hololeap> what _should_ happen in that example, c_wraith?
2021-11-06 20:38:08 +0100 <tomjaguarpaw> Err sorry, I mean newtype F = F (forall f. Functor f => f ())
2021-11-06 20:38:08 +0100 <c_wraith> tomjaguarpaw: huh, not for me. ghc 9.2.1 on my side
2021-11-06 20:38:26 +0100 <c_wraith> tomjaguarpaw: wait, no. That's not a function, so it doesn't get eta expanded.
2021-11-06 20:38:36 +0100 <c_wraith> I tested with (forall f. () -> f ())
2021-11-06 20:38:47 +0100 <c_wraith> that gives an exception
2021-11-06 20:38:58 +0100 <tomjaguarpaw> Not sure if you've seen my correction
2021-11-06 20:39:01 +0100 <c_wraith> ah, right.
2021-11-06 20:39:11 +0100 <c_wraith> definitely has to do with the dictionary-passing in core
2021-11-06 20:39:14 +0100 <tomjaguarpaw> and indeed newtype F = F (forall a. Num a => a)
2021-11-06 20:39:16 +0100 <tomjaguarpaw> Yes I agree
2021-11-06 20:39:19 +0100 <c_wraith> that must cause eta expansion
2021-11-06 20:39:32 +0100 <c_wraith> hololeap: naively, you'd expect to get an exception from evaluating undefined
2021-11-06 20:39:59 +0100aqua0210(~user@101.85.11.168) (Ping timeout: 268 seconds)
2021-11-06 20:40:09 +0100 <hololeap> so the compiler has no idea that (forall f. Functor f => () -> f ()) doesn't make sense
2021-11-06 20:40:53 +0100 <c_wraith> nope. that's irrelevant
2021-11-06 20:40:57 +0100 <hololeap> I suppose it wouldn't, since that's a result of what Functor means semantically, vs Applicative
2021-11-06 20:42:08 +0100 <hololeap> e.g. there is no pure defined for Functor, so no function could satisfy that type, unless it was also an Applicative
2021-11-06 20:42:19 +0100 <tomjaguarpaw> OK this is weird. Consider seq (F (undefined :: forall a. Num a => a)) () . It is undefined with newtype F a = F a but defined with newtype F = F (forall a. Num a => a) .
2021-11-06 20:42:22 +0100zmt01(~zmt00@user/zmt00)
2021-11-06 20:43:30 +0100 <c_wraith> huh. I didn't expect that.
2021-11-06 20:43:31 +0100burnsidesLlama(~burnsides@dhcp168-023.wadham.ox.ac.uk)
2021-11-06 20:44:27 +0100 <awpr> we actually just talked about the reason for this in the FP discord: `Functor f => ...` is a function value once you get down to Core
2021-11-06 20:44:50 +0100 <hpc> what if there isn't a class constraint?
2021-11-06 20:44:53 +0100 <c_wraith> that doesn't explain the last thing tomjaguarpaw mentioned. At least, not completely
2021-11-06 20:44:59 +0100 <awpr> yeah, getting to that
2021-11-06 20:45:31 +0100zmt00(~zmt00@user/zmt00) (Ping timeout: 245 seconds)
2021-11-06 20:45:31 +0100 <awpr> GHC wouldn't instantiate `F` impredicatively, so the former one is just `F a` for some `a`, and not constrained
2021-11-06 20:45:47 +0100 <awpr> probably defaults it to `Integer`
2021-11-06 20:46:15 +0100 <awpr> in the latter, the contents of the newtype are actually a type with a constraint, no need to infer impredicativity
2021-11-06 20:46:57 +0100 <hololeap> what was the library that was termed "a better ListT"
2021-11-06 20:47:03 +0100 <tomjaguarpaw> streaming?
2021-11-06 20:47:03 +0100 <geekosaur> logict?
2021-11-06 20:47:11 +0100zmt01(~zmt00@user/zmt00) (Ping timeout: 245 seconds)
2021-11-06 20:47:17 +0100 <hololeap> logict
2021-11-06 20:47:45 +0100 <[exa]> परोलोग
2021-11-06 20:48:06 +0100 <[exa]> whoops what happened there. I wanted to write "prolog".
2021-11-06 20:48:33 +0100 <hololeap> sanskrit?
2021-11-06 20:48:36 +0100burnsidesLlama(~burnsides@dhcp168-023.wadham.ox.ac.uk) (Ping timeout: 268 seconds)
2021-11-06 20:49:08 +0100zmt00(~zmt00@user/zmt00)
2021-11-06 20:51:06 +0100ees(~user@pool-108-18-30-46.washdc.fios.verizon.net) (Ping timeout: 260 seconds)
2021-11-06 20:53:07 +0100eggplantade(~Eggplanta@108-201-191-115.lightspeed.sntcca.sbcglobal.net) (Remote host closed the connection)
2021-11-06 20:53:27 +0100gehmehgeh(~user@user/gehmehgeh)
2021-11-06 20:53:49 +0100euandreh(~euandreh@2804:14c:65c9:5161:4d0f:6b02:d329:b5d2)
2021-11-06 20:56:24 +0100Codaraxis(~Codaraxis@user/codaraxis)
2021-11-06 20:56:46 +0100yauhsien(~yauhsien@118-167-41-229.dynamic-ip.hinet.net)
2021-11-06 20:58:00 +0100 <hololeap> ok, so I'm looking at my problem where a version inequality for a package can be normalized where >5.0.0.... = >5, but >5.0.0.0.0.1 /= >5
2021-11-06 20:58:19 +0100 <hololeap> so this looks like a depth-first search with backtracking. how can I use logict here?
2021-11-06 20:58:38 +0100pgib(~textual@173.38.117.89) (Ping timeout: 260 seconds)
2021-11-06 20:58:55 +0100 <dolio> If you just use it normally like a list, it'll be depth-first.
2021-11-06 20:59:17 +0100LiaoTao(~LiaoTao@gateway/tor-sasl/liaotao) (Quit: ZNC 1.8.2 - https://znc.in)
2021-11-06 20:59:30 +0100 <dolio> For the same reason that list is depth first. LogicT is essentially an encoded list.
2021-11-06 20:59:35 +0100 <hololeap> I haven't ever used it, normally or not, because I haven't had a use-case since I discovered it
2021-11-06 20:59:41 +0100LiaoTao(~LiaoTao@gateway/tor-sasl/liaotao)
2021-11-06 21:00:16 +0100 <dolio> The only way it'll do things out of order is if you use the additional combinators in the package, like `interleave` or >>-.
2021-11-06 21:00:52 +0100 <dolio> What I mean is that if you use it the way you'd use list monad stuff for DFS.
2021-11-06 21:01:11 +0100yauhsien(~yauhsien@118-167-41-229.dynamic-ip.hinet.net) (Ping timeout: 256 seconds)
2021-11-06 21:01:28 +0100 <hololeap> ok, so what I don't understand is what is how it is used for "backtracking"
2021-11-06 21:02:03 +0100 <hololeap> s/is what is how/is how/
2021-11-06 21:02:54 +0100 <dolio> The same way list is used for backtracking. `x <- [1,2,3]` essentially tries the rest of the computation with `1`, and gives all results, then gives all the results you'd get by using `2`, etc.
2021-11-06 21:03:25 +0100hendursaga(~weechat@user/hendursaga) (Remote host closed the connection)
2021-11-06 21:03:48 +0100hendursaga(~weechat@user/hendursaga)
2021-11-06 21:04:02 +0100 <geekosaur> that's natural for lists. ^^ and at some point you either get an answer involving the whole list (and get another if you continue), or a sublist fails (produces [] instead of the rest of the list) and it gets retried with the next list item
2021-11-06 21:05:10 +0100juhp(~juhp@128.106.188.220) (Ping timeout: 260 seconds)
2021-11-06 21:05:15 +0100 <hololeap> so, by the nature of list, you have to have seen the first element to see the second, and so on, and so you could have cached that value somewhere, allowing you to backtrack to the first value ... is that about right?
2021-11-06 21:05:20 +0100retro_(~retro@2e41e9c8.skybroadband.com)
2021-11-06 21:05:26 +0100 <geekosaur> mhh, if logs were still running I'd point you to ski's discussion last night my time
2021-11-06 21:05:57 +0100 <geekosaur> you don't need to do caching, the list monad (or, here, LogicT) does it automatically
2021-11-06 21:06:44 +0100juhp(~juhp@128.106.188.220)
2021-11-06 21:07:00 +0100harveypwca(~harveypwc@2601:246:c180:a570:3828:d8:e523:3f67) (Quit: Leaving)
2021-11-06 21:07:11 +0100 <dolio> If you ask for the first answer/head of the list, what you will get will be the result of 'backtracking' whenever some branch results in the empty list.
2021-11-06 21:07:20 +0100mrkrktsn1ctcrpt(~mrkrktsnd@c-24-6-12-87.hsd1.ca.comcast.net)
2021-11-06 21:07:31 +0100 <dolio> Becasue there will be 0 results from that branch, so to get any result, you must use another branch.
2021-11-06 21:08:32 +0100 <dolio> And the order of results is depth-first in the sense that it runs the entire rest of the computation for each choice point before considering the next value at that point.
2021-11-06 21:08:57 +0100retroid_(~retro@2e41e9c8.skybroadband.com) (Ping timeout: 268 seconds)
2021-11-06 21:09:18 +0100 <hololeap> ok, so we're specifically talking about the list monad, ([a] -> (a -> [b]) -> [b]), here?
2021-11-06 21:09:47 +0100 <dolio> That and LogicT both work essentially the same way.
2021-11-06 21:10:12 +0100 <dolio> Except LogicT uses a better behaved implementation for certain uses.
2021-11-06 21:10:21 +0100 <hololeap> so when the function `f :: a -> [b]` returns [], it naturally falls back to the previous element?
2021-11-06 21:10:50 +0100[itchyjunk](~itchyjunk@user/itchyjunk/x-7353470)
2021-11-06 21:11:06 +0100 <hololeap> because something else after it is still looking for a `b`?
2021-11-06 21:11:45 +0100 <dolio> Right, because it's concatMap. [1,2,3] >>= f = f 1 ++ f 2 ++ f 3.
2021-11-06 21:11:48 +0100LiaoTao_(~LiaoTao@gateway/tor-sasl/liaotao)
2021-11-06 21:12:15 +0100 <geekosaur> "backtracking" is actually a mischaracterization. it produces all possible values, but it does so lazily at all levels, so it *looks* like backtracking
2021-11-06 21:12:17 +0100 <hololeap> I'm still lost on how any of this is backtracking
2021-11-06 21:12:31 +0100 <hololeap> oh
2021-11-06 21:13:15 +0100 <dolio> Yeah, lazy evaluation makes lists act like backtracking computationally.
2021-11-06 21:13:15 +0100LiaoTao(~LiaoTao@gateway/tor-sasl/liaotao) (Ping timeout: 276 seconds)
2021-11-06 21:13:21 +0100 <dolio> LogicT does it with continuation passing.
2021-11-06 21:13:26 +0100 <hololeap> actually, I did write something that used this for an n-queens problem on some programming challenge thing, but I don't think I fully understood how it worked
2021-11-06 21:13:41 +0100LiaoTao_LiaoTao
2021-11-06 21:14:00 +0100 <ski> geekosaur : what's the difference ?
2021-11-06 21:15:22 +0100wootehfoot(~wootehfoo@user/wootehfoot)
2021-11-06 21:15:31 +0100 <geekosaur> not sure there is one, tbh. I haven't fully followed a computation through the list monad to see how it behaves, but I feel like there is no literal backtracking, each level is just continuing its computation regardless of what lower levels do and if those happen to fail, you get nothing from them
2021-11-06 21:15:50 +0100burnsidesLlama(~burnsides@dhcp168-023.wadham.ox.ac.uk)
2021-11-06 21:16:07 +0100 <geekosaur> and laziness means if you ask for only one result, it'll just stop and discard the whole computation after producing it
2021-11-06 21:16:16 +0100 <ski> hololeap : "you could have cached that value somewhere, allowing you to backtrack to the first value" -- iiuc, that's not what "backtracking" refers to. rather, it's about the retracing of your steps down a path in the search tree, up to a branch point where you now instead try to go down a different path
2021-11-06 21:18:36 +0100 <geekosaur> I could see this as different from backtracking, or as a "laziness implementation" of backtracking, or as semantic fiddling to no point
2021-11-06 21:19:19 +0100lavaman(~lavaman@98.38.249.169) (Ping timeout: 256 seconds)
2021-11-06 21:21:15 +0100pavonia(~user@user/siracusa)
2021-11-06 21:22:01 +0100 <ski> "each level is just continuing its computation regardless of what lower levels do and if those happen to fail, you get nothing from them" -- which gives you the behaviour of backtracking, afaiac
2021-11-06 21:22:59 +0100 <ski> sure, it's implemented differently than backtracking usually is, say in Prolog systems, or if you manually code it with loops in C or Pascal something
2021-11-06 21:23:29 +0100 <geekosaur> yeh, but I think a "conventional" view of backtracking expects that some information is propagated backwards to resume the previous level
2021-11-06 21:23:43 +0100 <geekosaur> whereas here it's just the natural behavior of a lazy list
2021-11-06 21:24:50 +0100 <dolio> Prolog does something better than depth-first backtracking search, right?
2021-11-06 21:26:41 +0100 <dolio> But, I don't really see why it wouldn't be considered backtracking, unless someone is adamant that you have to manually use mutation while keeping track of how to revert the mutable variables to older states or something.
2021-11-06 21:30:10 +0100favonia(~favonia@user/favonia) (Quit: Leaving)
2021-11-06 21:31:18 +0100mei3(~mei@user/mei) (Ping timeout: 260 seconds)
2021-11-06 21:32:42 +0100pretty_dumm_guy(trottel@gateway/vpn/protonvpn/prettydummguy/x-88029655) (Ping timeout: 260 seconds)
2021-11-06 21:34:34 +0100 <ski> (`app_ordered_selections' at <https://bpa.st/4IUQ> is an example of backtracking, in C, using a loop, as well as `goto' out of, and into, it)
2021-11-06 21:35:06 +0100 <ski> geekosaur : what kind of information ?
2021-11-06 21:35:29 +0100aqua0210(~user@101.85.11.168)
2021-11-06 21:36:42 +0100 <ski> dolio : basic Prolog behaviour is depth-first. you can use the cut to (non-declaratively) prune parts of the search tree/space, and systems also often implement indexing, which can be seen as a limited (local) breadth-first exploring of alternatives
2021-11-06 21:37:47 +0100 <dolio> Oh, I meant that I thought it was typical for some 'better' strategy than depth first to be used.
2021-11-06 21:38:09 +0100 <dolio> But I'm not that well read on implementing Prolog.
2021-11-06 21:38:26 +0100 <ski> (some systems also allow you to put a bound on depth of search, so that you can do iterative deepening, but that's not on by default. oh, and some systems have "coroutining", meaning that goals can be delayed, later being triggered, typically when some logic variable becomes instantiated. this can e.g. be used to implement breadth-first, queue-like, possibly streaming, behaviour)
2021-11-06 21:38:51 +0100 <ski> no, i think normally plain depth-first is what is used
2021-11-06 21:39:05 +0100 <dolio> Oh, huh.
2021-11-06 21:39:16 +0100 <ski> one reason is that people sometimes depend on the specific ordering that they get with the naïve depth-first
2021-11-06 21:39:50 +0100 <ski> and so implementations don't want to mess with that, unasked, in ways that's not obvious
2021-11-06 21:40:35 +0100aqua0210(~user@101.85.11.168) (Ping timeout: 264 seconds)
2021-11-06 21:43:12 +0100 <ski> e.g. interconverting between `( foo ; bar ),baz' and `( foo,baz ; bar,baz )' would be ok in the sense of preserving ordering (and multiplicity) of solutions, while interconverting between `foo,( bar ; baz )' and `( foo,bar ; foo,baz )' wouldn't (since `foo' could have multiple solutions) (.. and obviously also commutativity and idempotency of disjunction isn't used)
2021-11-06 21:44:03 +0100merijn(~merijn@83-160-49-249.ip.xs4all.nl)
2021-11-06 21:45:51 +0100 <dolio> I guess it could just be less naive implementatiaon of DFS. Like, it's conceivable that you could detect that the thing that makes a branch fail is independent of a certain choice, and so not re-evaluate the branch for each choice.
2021-11-06 21:46:13 +0100 <ski> > [[x,y] | x <- "ab" ++ "cd",y <- "ef"]
2021-11-06 21:46:14 +0100 <lambdabot> ["ae","af","be","bf","ce","cf","de","df"]
2021-11-06 21:46:15 +0100 <ski> [[x,y] | x <- "ab",y <- "ef"] ++ [[x,y] | x <- "cd",y <- "ef"]
2021-11-06 21:46:18 +0100 <ski> > [[x,y] | x <- "ab",y <- "ef"] ++ [[x,y] | x <- "cd",y <- "ef"]
2021-11-06 21:46:19 +0100 <lambdabot> ["ae","af","be","bf","ce","cf","de","df"]
2021-11-06 21:46:39 +0100 <ski> > [[x,y] | x <- "ab",y <- "cd" ++ "ef"]
2021-11-06 21:46:41 +0100 <lambdabot> ["ac","ad","ae","af","bc","bd","be","bf"]
2021-11-06 21:46:42 +0100 <ski> > [[x,y] | x <- "ab",y <- "cd"] ++ [[x,y] | x <- "ab",y <- "ef"]
2021-11-06 21:46:43 +0100 <lambdabot> ["ac","ad","bc","bd","ae","af","be","bf"]
2021-11-06 21:47:10 +0100pretty_dumm_guy(trottel@gateway/vpn/protonvpn/prettydummguy/x-88029655)
2021-11-06 21:47:44 +0100 <ski> dolio : yea, but that'd require analysis of that, and that there's no side-effects happening
2021-11-06 21:48:01 +0100 <geekosaur> ski, like in your discussion last night where success of a consequent is treated as a failure by the Antecedent
2021-11-06 21:48:10 +0100 <ski> Mercury is more free to reorder and refactor stuff, because it doesn't allow side-effects
2021-11-06 21:48:56 +0100 <ski> (although, it's possible to run Mercury in a "strict" mode where it doesn't reorder solutions)
2021-11-06 21:49:06 +0100 <ski> (or deduplicate)
2021-11-06 21:49:26 +0100 <geekosaur> whereas with laziness the "antecedent" just keeps going without considering what happened with the "consequent"
2021-11-06 21:50:23 +0100 <ski> well, what i talked about last night was not the behaviour of `(>>=)', but of another combinator
2021-11-06 21:53:44 +0100eggplantade(~Eggplanta@108-201-191-115.lightspeed.sntcca.sbcglobal.net)
2021-11-06 21:54:16 +0100kupi(uid212005@id-212005.hampstead.irccloud.com)
2021-11-06 21:54:56 +0100 <geekosaur> in any case, the naïve view of backtracking would expect that the preceding level needs to be told to restart somehow, when in the laziness implementation it would do so regardless when a(nother) value is demanded
2021-11-06 21:55:14 +0100michalz(~michalz@185.246.204.58)
2021-11-06 21:55:54 +0100 <geekosaur> and neither knows nor cares whether any value(s) have already been produced
2021-11-06 21:58:22 +0100eggplantade(~Eggplanta@108-201-191-115.lightspeed.sntcca.sbcglobal.net) (Ping timeout: 260 seconds)
2021-11-06 22:01:56 +0100 <ski> @let infixl 1 ==>; (==>) :: [a] -> (a -> [b]) -> [[b]]; (==>) = for
2021-11-06 22:01:57 +0100 <lambdabot> Defined.
2021-11-06 22:02:00 +0100 <ski> > [1,4,2,9] ==> \x -> guard (x < 10)
2021-11-06 22:02:02 +0100 <lambdabot> error:
2021-11-06 22:02:02 +0100 <lambdabot> Ambiguous occurrence ‘==>’
2021-11-06 22:02:02 +0100 <lambdabot> It could refer to
2021-11-06 22:02:08 +0100 <ski> oh
2021-11-06 22:02:16 +0100 <ski> @let infixl 1 ===>; (===>) :: [a] -> (a -> [b]) -> [[b]]; (===>) = for
2021-11-06 22:02:17 +0100 <lambdabot> Defined.
2021-11-06 22:02:21 +0100 <ski> > [1,4,2,9] ===> \x -> guard (x < 10)
2021-11-06 22:02:22 +0100 <lambdabot> [[(),(),(),()]]
2021-11-06 22:02:25 +0100 <ski> > [1,4,2,9] ===> \x -> guard (x < 5)
2021-11-06 22:02:27 +0100 <lambdabot> []
2021-11-06 22:02:51 +0100 <ski> > [1,4,2,9] ===> \x -> return (x*x)
2021-11-06 22:02:52 +0100 <lambdabot> [[1,16,4,81]]
2021-11-06 22:03:12 +0100 <ski> > [1,4,2,9] ==> \x -> do guard (x >= 0); let {y = floor (sqrt (fromIntegral x))}; guard (x == y * y); return y <|> return (-y)
2021-11-06 22:03:13 +0100 <lambdabot> error:
2021-11-06 22:03:14 +0100 <lambdabot> Ambiguous occurrence ‘==>’
2021-11-06 22:03:14 +0100 <lambdabot> It could refer to
2021-11-06 22:03:25 +0100 <ski> > [1,4,2,9] ===> \x -> do guard (x >= 0); let {y = floor (sqrt (fromIntegral x))}; guard (x == y * y); return y <|> return (-y)
2021-11-06 22:03:27 +0100 <lambdabot> []
2021-11-06 22:03:29 +0100 <ski> > [1,4,9] ===> \x -> do guard (x >= 0); let {y = floor (sqrt (fromIntegral x))}; guard (x == y * y); return y <|> return (-y)
2021-11-06 22:03:30 +0100 <lambdabot> [[1,2,3],[1,2,-3],[1,-2,3],[1,-2,-3],[-1,2,3],[-1,2,-3],[-1,-2,3],[-1,-2,-3]]
2021-11-06 22:04:07 +0100 <ski> that's basically what i implemented, except using continuations, and also supporting logic variables (implemented using mutation)
2021-11-06 22:05:10 +0100acidjnk(~acidjnk@p200300d0c72635825cb0fefbc648f0e4.dip0.t-ipconnect.de)
2021-11-06 22:05:39 +0100 <ski> (in my version, i had basically `(==>) :: Logic a -> (a -> Logic b) -> Logic b', though, so the first input is not simply a list that you could `for'/`traverse' over .. it's an action generating solutions, by calling success and failure continuations)
2021-11-06 22:07:16 +0100 <ski> geekosaur : well, fwiw, what you just said i'd argue is more or less what Prolog systems do, as well ..
2021-11-06 22:08:10 +0100pretty_dumm_guy(trottel@gateway/vpn/protonvpn/prettydummguy/x-88029655) (Ping timeout: 260 seconds)
2021-11-06 22:08:20 +0100 <geekosaur> yes, but see hololeap's confusion about it
2021-11-06 22:08:30 +0100 <ski> .. as soon as you've entered the Redo port of a predicate call, things proceed as if it was an initial Call. and the Fail port means that no (more) solutions were produced
2021-11-06 22:09:13 +0100 <geekosaur> not seeing how this corresponded to "backtracking"
2021-11-06 22:09:37 +0100 <ski> (when a Prolog system answers "no"/"No" (or sometimes "false"), it should be interpreted not as "the query was false", but that no more solutions were found. it could answer `X = 2', and then say `no'/`false' when you use `;' (meaning "or") to ask for more)
2021-11-06 22:10:21 +0100pretty_dumm_guy(trottel@gateway/vpn/protonvpn/prettydummguy/x-88029655)
2021-11-06 22:11:22 +0100 <ski> backtracking, in the simplest view, causes execution to flow "backwards", back inside the last Exit-ed call, and inside that, proceed from the end backwards, in and out of calls, (undoing variable instantiations that've been done) until it finds a location where there was an alternative choice to attempt
2021-11-06 22:11:43 +0100retro_(~retro@2e41e9c8.skybroadband.com) (Read error: Connection reset by peer)
2021-11-06 22:11:59 +0100 <geekosaur> (also last time I got to seriously use Prolog was 1992ish, sigh)
2021-11-06 22:12:04 +0100 <ski> acrual implementations record where the last choice-point was, and just jumps back to it
2021-11-06 22:12:25 +0100retroid_(~retro@2e41e9c8.skybroadband.com)
2021-11-06 22:12:56 +0100 <ski> so, when backtracking starts, because some call Fail-s, you jump back to the last choice-point, Redo-ing that call, trying the next clause of the predicate in question
2021-11-06 22:13:12 +0100 <geekosaur> confused the heck out of my boss when I used it to model a complex pricing system :)
2021-11-06 22:13:40 +0100 <ski> from the point of Redo-ing, it is as if it's the initial Call, assuming the predicate in question started at the clause in question (as if previous clauses didn't exist)
2021-11-06 22:13:49 +0100darkstardevx(~darkstard@50.39.114.152) (Read error: Connection reset by peer)
2021-11-06 22:16:41 +0100aqua0210(~user@101.85.11.168)
2021-11-06 22:17:32 +0100mrkrktsn1ctcrpt(~mrkrktsnd@c-24-6-12-87.hsd1.ca.comcast.net) (Quit: Lost terminal)
2021-11-06 22:18:22 +0100mrkrktsndctcrpt(~mrkrktsnd@c-24-6-12-87.hsd1.ca.comcast.net) (Quit: Lost terminal)
2021-11-06 22:18:23 +0100 <ski> (well, actual signature is `(==>) :: Logic m o a -> (a -> Logic m p o) -> Logic m p o' .. so, there's some "interesting" dependency (the `o') between the antecedent and the consequent)
2021-11-06 22:18:26 +0100merijn(~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 260 seconds)
2021-11-06 22:19:23 +0100 <ski> geekosaur : i guess they'd never seen it before ?
2021-11-06 22:19:34 +0100 <geekosaur> nope
2021-11-06 22:20:14 +0100 <geekosaur> my boss was a database dev turned salesman, had not much clue about languages beyond C
2021-11-06 22:21:20 +0100 <geekosaur> so I got thrown at the stuff with more "exotic" languages including a business cobol and a custom embedded-programming basic dialect
2021-11-06 22:21:36 +0100_ht(~quassel@82-169-194-8.biz.kpn.net) (Remote host closed the connection)
2021-11-06 22:21:42 +0100aqua0210(~user@101.85.11.168) (Ping timeout: 260 seconds)
2021-11-06 22:22:11 +0100 <geekosaur> and the prolog thing, which was to escape writing the same logic in C while we still weren't quite certain what it fully was, so prolog made it easier for me to tinker with it
2021-11-06 22:22:22 +0100 <geekosaur> then I rewrote it for speed when we had it firmed down
2021-11-06 22:22:25 +0100 <ski> well, a general cursory knowledge of different paradigms and approaches to programming (both general, and sometimes more specific), is unfortunately commonly lacking ..
2021-11-06 22:22:29 +0100skinods
2021-11-06 22:22:32 +0100darkstardevx(~darkstard@50.39.114.152)
2021-11-06 22:23:07 +0100 <ski> (Basic for embedded programming ?)
2021-11-06 22:23:28 +0100darkstardevx(~darkstard@50.39.114.152) (Remote host closed the connection)
2021-11-06 22:23:52 +0100darkstardevx(~darkstard@50.39.114.152)
2021-11-06 22:24:13 +0100eggplantade(~Eggplanta@108-201-191-115.lightspeed.sntcca.sbcglobal.net)
2021-11-06 22:24:14 +0100 <geekosaur> it was a highly customized basic. I don't recall all the details now but it got compiled down to code for a hard realtime controller
2021-11-06 22:24:28 +0100 <geekosaur> all this stuff was around 20 years ago
2021-11-06 22:24:53 +0100LiaoTao(~LiaoTao@gateway/tor-sasl/liaotao) (Remote host closed the connection)
2021-11-06 22:25:14 +0100LiaoTao(~LiaoTao@gateway/tor-sasl/liaotao)
2021-11-06 22:25:24 +0100 <geekosaur> mm, actually the hrt thing would have been 1987
2021-11-06 22:25:41 +0100 <ski> hm, sounds curious
2021-11-06 22:26:26 +0100skiwas recently toying around with a Prolog implementation for the Commodore 64
2021-11-06 22:26:56 +0100 <geekosaur> I only worked with it for a few weeks, then they took it away and assigned it to their engineering dept. because they didn't think someone from the front office should be working on it… think the assigned engineer still used the code I'd written though
2021-11-06 22:28:06 +0100 <ski> (now i'm tinkering a little bit with seeing how far i'd get with reverse-engineering it .. i'd like to add LCO/TCO to it (and that it'll fail directly when the last clause fails, rather than fruitlessly first attempting to look for the next clause))
2021-11-06 22:29:06 +0100aeke(~a@p200300ef973db1af4086f0a6a24fc4dd.dip0.t-ipconnect.de)
2021-11-06 22:29:59 +0100 <aeke> Hi, is beta reduction the same as function application in lambda calculus?
2021-11-06 22:30:08 +0100 <ski> no
2021-11-06 22:30:59 +0100 <ski> beta reduction amounts to removing a function application whose operand is a lambda abstraction, by substituting the actual parameter for the formal parameter, in the body of the lambda abstraction
2021-11-06 22:31:43 +0100 <ski> (\x. x * x) (2 + 3) --> (2 + 3) * (2 + 3)
2021-11-06 22:31:51 +0100 <ski> is an example of beta-reduction
2021-11-06 22:32:37 +0100 <aeke> So is function application just the juxtaposition of two lambda terms?
2021-11-06 22:33:16 +0100 <aeke> And the left term does not need to be a lambda abstraction?
2021-11-06 22:33:21 +0100 <ski> a function application is a kind of construct, a way of forming a term/expression, a node in the abstract syntax tree. beta-reduction is about how one can rewrite a term, a tree, into another one
2021-11-06 22:34:15 +0100 <ski> function application is usually written as just juxtaposition (left-associative), in lambda calculus, yes. occasionally you'll see an explicit infix operator, like `@'
2021-11-06 22:34:46 +0100 <ski> aeke : yes, the left term could be a variable, or another application, e.g.
2021-11-06 22:35:06 +0100 <ski> e.g. `f x y' is normally parsed as `(f x) y'
2021-11-06 22:36:04 +0100 <aeke> So function application is part of building up an AST while beta reduction is part of evaluation/reducing that tree (if the left term of the fun app happens to be a lambda abstraction)?
2021-11-06 22:36:32 +0100 <ski> so .. beta-reduction removes both an application, and an abstaction, from the AST. they "react", so to speak
2021-11-06 22:36:46 +0100 <ski> aeke : yes
2021-11-06 22:37:22 +0100zmt01(~zmt00@user/zmt00)
2021-11-06 22:38:01 +0100zmt00(~zmt00@user/zmt00) (Ping timeout: 245 seconds)
2021-11-06 22:38:50 +0100wonko(~wjc@user/wonko)
2021-11-06 22:43:35 +0100zmt01(~zmt00@user/zmt00) (Ping timeout: 264 seconds)
2021-11-06 22:44:39 +0100aqua0210(~user@101.85.11.168)
2021-11-06 22:44:40 +0100emf(~emf@c-73-97-137-43.hsd1.wa.comcast.net) (Remote host closed the connection)
2021-11-06 22:45:46 +0100emf(~emf@163.114.132.5)
2021-11-06 22:46:52 +0100ulvarrefr(~user@185.24.53.152) (ERC (IRC client for Emacs 27.2))
2021-11-06 22:49:42 +0100aqua0210(~user@101.85.11.168) (Ping timeout: 260 seconds)
2021-11-06 22:54:29 +0100chexum(~quassel@gateway/tor-sasl/chexum) (Remote host closed the connection)
2021-11-06 22:55:46 +0100chexum(~quassel@gateway/tor-sasl/chexum)
2021-11-06 22:57:30 +0100werneta(~werneta@70-142-214-115.lightspeed.irvnca.sbcglobal.net) (Ping timeout: 268 seconds)
2021-11-06 22:58:50 +0100jpds1(~jpds@gateway/tor-sasl/jpds) (Remote host closed the connection)
2021-11-06 22:59:32 +0100jpds1(~jpds@gateway/tor-sasl/jpds)
2021-11-06 23:00:28 +0100basti_(~basti@ip-84-119-8-195.unity-media.net) (Quit: leaving)
2021-11-06 23:02:02 +0100v01d4lph4(~v01d4lph4@user/v01d4lph4)
2021-11-06 23:05:54 +0100qwedfg(~qwedfg@user/qwedfg) (Remote host closed the connection)
2021-11-06 23:06:58 +0100v01d4lph4(~v01d4lph4@user/v01d4lph4) (Ping timeout: 260 seconds)
2021-11-06 23:08:23 +0100qwedfg(~qwedfg@user/qwedfg)
2021-11-06 23:10:05 +0100fendor(~fendor@178.165.196.101.wireless.dyn.drei.com) (Read error: Connection reset by peer)
2021-11-06 23:11:16 +0100zmt00(~zmt00@user/zmt00)
2021-11-06 23:11:26 +0100 <EvanR> often times (beta) reducing something greatly increases its size xD
2021-11-06 23:12:43 +0100werneta(~werneta@70-142-214-115.lightspeed.irvnca.sbcglobal.net)
2021-11-06 23:14:45 +0100ubert(~Thunderbi@p200300ecdf4fca30e019fddc82d0353e.dip0.t-ipconnect.de) (Ping timeout: 268 seconds)
2021-11-06 23:24:36 +0100gehmehgeh(~user@user/gehmehgeh) (Quit: Leaving)
2021-11-06 23:29:05 +0100wonko(~wjc@user/wonko) (Ping timeout: 256 seconds)
2021-11-06 23:30:08 +0100fluffyballoon(~user@131.93.208.196)
2021-11-06 23:30:41 +0100unit73e(~emanuel@2001:818:e8dd:7c00:32b5:c2ff:fe6b:5291)
2021-11-06 23:32:23 +0100pavonia(~user@user/siracusa) (Read error: Connection reset by peer)
2021-11-06 23:33:03 +0100Sgeo_(~Sgeo@user/sgeo)
2021-11-06 23:33:06 +0100cheater(~Username@user/cheater) (Ping timeout: 260 seconds)
2021-11-06 23:33:26 +0100Sgeo(~Sgeo@user/sgeo) (Ping timeout: 245 seconds)
2021-11-06 23:33:27 +0100cheater(~Username@user/cheater)
2021-11-06 23:37:05 +0100lavaman(~lavaman@98.38.249.169)
2021-11-06 23:37:34 +0100pavonia(~user@user/siracusa)
2021-11-06 23:45:27 +0100aqua0210(~user@101.85.11.168)
2021-11-06 23:46:54 +0100yauhsien(~yauhsien@118-167-41-229.dynamic-ip.hinet.net)
2021-11-06 23:49:56 +0100slack1256(~slack1256@191.125.227.73)
2021-11-06 23:50:01 +0100cosimone(~user@93-47-229-157.ip115.fastwebnet.it) (Quit: ERC (IRC client for Emacs 27.1))
2021-11-06 23:51:45 +0100yauhsien(~yauhsien@118-167-41-229.dynamic-ip.hinet.net) (Ping timeout: 256 seconds)
2021-11-06 23:57:18 +0100unit73e(~emanuel@2001:818:e8dd:7c00:32b5:c2ff:fe6b:5291) (Ping timeout: 268 seconds)
2021-11-06 23:57:26 +0100mastarija(~mastarija@2a05:4f46:e06:ff00:18c4:3126:ef80:d743) (Quit: Leaving)
2021-11-06 23:59:01 +0100ubert(~Thunderbi@p200300ecdf4fca30e019fddc82d0353e.dip0.t-ipconnect.de)
2021-11-06 23:59:09 +0100machinedgod(~machinedg@24.105.81.50) (Ping timeout: 268 seconds)