Logs on 2021-11-06 (liberachat/#haskell)
| 00:00:12 | <ski> | (oh, and as i said, disjunction is addition, and conjunction is multiplication) |
| 00:00:40 | <syd> | anyway I'll stop chiming in, it's rude to interrupt. |
| 00:00:49 | <ski> | no, no worry ! |
| 00:01:13 | <joel135> | no problem from my side either! |
| 00:01:38 | × | Gurkenglas quits (~Gurkengla@dslb-002-203-144-204.002.203.pools.vodafone-ip.de) (Ping timeout: 260 seconds) |
| 00:01:48 | <syd> | appreciate it :) |
| 00:01:53 | <joel135> | i see that _\/_ is like addition of Church numerals, i am not seeing that _/\_ is multiplication |
| 00:02:26 | <joel135> | oh sorry there was a linewrap that i missed. let me retry reading it |
| 00:03:27 | <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 |
| 00:03:48 | <ski> | (so, if the length is know, then it definitely is "instantiated") |
| 00:04:21 | <ski> | joel135 : perhaps i'd help to eta-reduce conjunction ? |
| 00:04:23 | × | cosimone quits (~user@93-44-186-19.ip98.fastwebnet.it) (Ping timeout: 256 seconds) |
| 00:04:43 | <joel135> | does `g1 gail1 succeed` really have the arguments in the right order? |
| 00:04:57 | × | yushyin quits (rzPUwQNnp2@karif.server-speed.net) (Quit: WeeChat 3.3) |
| 00:04:57 | <ski> | oh, sorry. yea, i just noticed that was wrong order |
| 00:05:06 | → | yushyin joins (XNontZhIIh@karif.server-speed.net) |
| 00:05:28 | <ski> | (g0 /\ g1) succeed fail = g0 (g1 succeed) fail |
| 00:05:33 | <ski> | (g0 /\ g1) succeed = g0 (g1 succeed) |
| 00:05:41 | <ski> | g0 /\ g1 = g0 . g1 |
| 00:06:07 | <joel135> | these names "succeed" and "fail" are very intriguing. |
| 00:06:21 | <ski> | it's standard terminology in logic programming |
| 00:06:39 | <joel135> | yes but in the context of Church numerals |
| 00:07:09 | <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" |
| 00:07:38 | <syd> | (define succeed (== #t #t)) and (define fail (== #t #f)) is how I've seen them, fwiw. |
| 00:08:30 | → | zincy_ joins (~zincy@2a00:23c8:970c:4801:350f:7ee:191a:6f65) |
| 00:08:32 | <syd> | oh, no idea about the relation to church numerals, missed that bit sorry. |
| 00:08:55 | <joel135> | i see, this http://www.cs.otago.ac.nz/cosc347/References/LP/LeedsTutorial/node48.html kind of thing |
| 00:08:56 | <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 |
| 00:09:34 | <joel135> | is it a coincidence that there are four o's in (o -> o) -> (o -> o) just like this box has four ports? |
| 00:09:49 | <ski> | no |
| 00:09:54 | <joel135> | ok |
| 00:10:59 | <ski> | {- call :: -} ({- exit,succeed :: -} ({- redo :: -} o) -> o) -> (({- fail :: -} o) -> o) |
| 00:12:30 | <ski> | or, if you want to associate the ports with the results of the associated underlying invokations : |
| 00:13:12 | <ski> | (({- redo -} o) -> ({- exit -} o)) -> (({- fail -} o) -> ({- call -} o)) |
| 00:13:14 | × | zincy_ quits (~zincy@2a00:23c8:970c:4801:350f:7ee:191a:6f65) (Ping timeout: 268 seconds) |
| 00:14:41 | <joel135> | i see |
| 00:15:07 | <joel135> | could you then imagine what ((o -> o) -> (o -> o)) -> ((o -> o) -> (o -> o)) would mean in the context of logic programming? |
| 00:16:23 | <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 |
| 00:16:29 | <ski> | (more or less, like pattern-matching on arguments left of the `=')) |
| 00:16:55 | <ski> | well .. i haven't considered it from your polynomial perspective .. |
| 00:17:13 | <ski> | but doing that kind of thing is exactly what i did, for my goal implications |
| 00:18:51 | × | chexum quits (~quassel@gateway/tor-sasl/chexum) (Remote host closed the connection) |
| 00:18:59 | <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 |
| 00:19:10 | <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) |
| 00:19:15 | → | chexum joins (~quassel@gateway/tor-sasl/chexum) |
| 00:19:32 | <ski> | (well, i guess `o' would also be `()' there) |
| 00:20:18 | × | merijn quits (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 260 seconds) |
| 00:20:35 | <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))' |
| 00:21:20 | <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 |
| 00:21:43 | × | faultline quits (~christian@nat-eduroam-01.scc.kit.edu) (Remote host closed the connection) |
| 00:22:16 | <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) |
| 00:22:27 | → | faultline joins (~christian@nat-eduroam-01.scc.kit.edu) |
| 00:23:06 | <joel135> | wait wait. this sounds super cool for lack of a better word |
| 00:23:44 | × | Lord_of_Life quits (~Lord@user/lord-of-life/x-2819915) (Ping timeout: 268 seconds) |
| 00:24:01 | → | Lord_of_Life joins (~Lord@user/lord-of-life/x-2819915) |
| 00:24:17 | <unit73e> | so I was doing texture clipping and now I have to deal with aeson. I'll just make a pause... |
| 00:25:09 | <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? |
| 00:25:46 | <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 |
| 00:25:53 | <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") |
| 00:26:33 | <unit73e> | in college the teachers made a competition of who could make the best sodoku solver |
| 00:26:45 | <unit73e> | the teacher that won used prolog |
| 00:26:55 | <unit73e> | it was so fast that the solution was faster than printing |
| 00:27:00 | <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) |
| 00:27:51 | <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 |
| 00:28:07 | <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 |
| 00:28:42 | × | cheater quits (~Username@user/cheater) (Ping timeout: 260 seconds) |
| 00:29:42 | <syd> | (what is it with punning usernames here?! I like it.) |
| 00:29:45 | <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') |
| 00:30:40 | <joel135> | i need to think more about what you just wrote ^ |
| 00:30:51 | <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)) ? |
| 00:30:56 | <ski> | unit73e : hm, did it use some constraint programming ? imho, that would be ideal |
| 00:31:25 | <ski> | "is this "shift" a variant of this from above?" -- i think it's related, at least |
| 00:32:32 | <ski> | yes, `Consequent' and `( Antecedent => Consequent )' would have the same type, the same number of continuation levels |
| 00:33:16 | <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) ? |
| 00:33:37 | <ski> | yes |
| 00:33:47 | <ski> | (modulo some fiddly stuff with the base monad) |
| 00:34:22 | <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" |
| 00:35:21 | <ski> | hm, i don't think so |
| 00:37:09 | <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. |
| 00:38:06 | <ski> | hmm .. exponent |
| 00:38:54 | → | yauhsien joins (~yauhsien@118-167-41-229.dynamic-ip.hinet.net) |
| 00:38:59 | × | random-jellyfish quits (~random-je@user/random-jellyfish) (Ping timeout: 256 seconds) |
| 00:39:03 | <ski> | i wonder if there's possibly two distinct "downgrades" (or two distinct "upgrades" ?) |
| 00:40:15 | <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). |
| 00:41:30 | <ski> | g₀ ⇒ g₁ : Ω ⊣ g₀,g₁ : Ω |
| 00:41:37 | <ski> | (g₀ ⇒ g₁) ω s f = g₀ (ω → ω) (λ s₀ ↦ λ f′ ↦ |
| 00:41:43 | <ski> | g₁ ω (λ f″ ↦ s₀ f″) f′) (λ f‴ ↦ s f‴) f |
| 00:41:46 | <ski> | = g₀ (ω → ω) (g₁ ω) s f |
| 00:42:20 | <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. |
| 00:42:20 | <ski> | that's my implication, given ⌜Ω = (ω :) ⋆ → (ω → ω) → (ω → ω)⌝ |
| 00:42:55 | → | zincy_ joins (~zincy@2a00:23c8:970c:4801:350f:7ee:191a:6f65) |
| 00:43:24 | <ski> | (hm, i guess you can think of `x' as an oracle ..) |
| 00:43:38 | × | yauhsien quits (~yauhsien@118-167-41-229.dynamic-ip.hinet.net) (Ping timeout: 260 seconds) |
| 00:43:45 | <joel135> | (the level of operators being something like ((((o -> o) -> (o -> o)) -> ((o -> o) -> (o -> o)))) -> ((((o -> o) -> (o -> o)) -> ((o -> o) -> (o -> o))))) |
| 00:44:14 | <joel135> | hang on, i need to read what you wrote |
| 00:46:36 | <joel135> | i can't parse Ω = (ω :) ⋆ → (ω → ω) → (ω → ω) |
| 00:47:15 | <ski> | Omega = (o : Set) -> (o -> o) -> (o -> o) -- in Agda notation |
| 00:47:47 | × | zincy_ quits (~zincy@2a00:23c8:970c:4801:350f:7ee:191a:6f65) (Ping timeout: 264 seconds) |
| 00:48:12 | <joel135> | ok right, you use ω → ω for ω |
| 00:48:13 | <ski> | `Omega' just being a type of "logic programming goals/queries", which also "just happens" to be church numerals |
| 00:49:11 | <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) |
| 00:49:31 | <ski> | (er, s/logic programming/logic variables/) |
| 00:49:55 | <joel135> | right |
| 00:51:05 | → | SeungheonOh joins (~Thunderbi@2600:1700:5168:1400:1574:2437:4f0d:50e6) |
| 00:51:49 | <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 + ..' ?) |
| 00:52:52 | <joel135> | (let's maybe use the names ℕ₀(o) = o, ℕₙ₊₁(o) = (ℕₙ(o) → ℕₙ(o)) and ℕₙ = ∀o. ℕₙ(o) sometimes for readability, so e.g. ℕ₃ = Poly) |
| 00:53:21 | <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) |
| 00:55:06 | <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. |
| 00:55:35 | <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 |
| 00:55:55 | <joel135> | :D |
| 00:56:39 | <ski> | hm, holes |
| 00:57:02 | <ski> | (makes me wonder about relation to McBride type differentiation) |
| 00:57:26 | <joel135> | holes ... derivatives ... of types or of polynomials :) |
| 00:57:40 | <ski> | yup |
| 00:58:46 | <ski> | <joel135> is this related to what you wrote above? >>> also an interesting "duality" of sorts between logic variables and skolems/atoms emerged |
| 00:59:40 | <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 |
| 01:00:17 | <ski> | because the solutions of `Antecedent' are merely hypothetical .. by the time the implication has succeeded, `Antecedent' has exhausted its solutions, and failed finally |
| 01:00:42 | <ski> | this makes sense, since there's a polarity shift/swap, the antecedent is in a negated context |
| 01:01:10 | <ski> | but, i'd still like `Consequent' to be able to make instantiations, which survived .. so the question was how to achieve this |
| 01:01:18 | × | ubert quits (~Thunderbi@p200300ecdf4fcafee019fddc82d0353e.dip0.t-ipconnect.de) (Ping timeout: 260 seconds) |
| 01:01:24 | → | ub joins (~Thunderbi@p200300ecdf4fca30e019fddc82d0353e.dip0.t-ipconnect.de) |
| 01:01:34 | <joel135> | (i don't have quite enough practical experience with logic programming to have intuition for the things you just said) |
| 01:01:49 | <ski> | `Consequent' here wouldn't (usually) communicate directly to the surrounding goals, and their logic variables, but only do so *via* `Antecedent' |
| 01:02:54 | <joel135> | i think i need to try studying your code. do you still have it? |
| 01:03:16 | <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 |
| 01:03:43 | ub | is now known as ubert |
| 01:04:10 | × | raehik quits (~raehik@cpc95906-rdng25-2-0-cust156.15-3.cable.virginm.net) (Ping timeout: 260 seconds) |
| 01:04:48 | <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) |
| 01:05:38 | <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) ) |
| 01:06:04 | <joel135> | i am guessing X |
| 01:06:17 | <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 |
| 01:06:24 | <ski> | `X', yes |
| 01:06:29 | <joel135> | ok |
| 01:07:06 | × | burnsidesLlama quits (~burnsides@dhcp168-023.wadham.ox.ac.uk) (Remote host closed the connection) |
| 01:08:06 | <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 |
| 01:08:25 | <ski> | the same phenomenon happens in logic programming |
| 01:09:46 | × | acidsys quits (~LSD@2.lsd.systems) (Excess Flood) |
| 01:10:04 | <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 |
| 01:10:21 | → | acidsys joins (~LSD@2.lsd.systems) |
| 01:10:46 | <joel135> | (i think ghc referred to skolem-something before i changed `type Poly` to `data Poly`) |
| 01:11:59 | <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 |
| 01:12:21 | <ski> | (while, using `sigma' instead of `pi', it would succeed) |
| 01:13:08 | <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 |
| 01:13:29 | × | Athas quits (athas@2a01:7c8:aaac:1cf:a0d4:8908:cfdb:b9c0) (Quit: ZNC 1.8.2 - https://znc.in) |
| 01:13:45 | → | Athas joins (athas@2a01:7c8:aaac:1cf:a0d4:8908:cfdb:b9c0) |
| 01:14:14 | <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 |
| 01:15:50 | <unit73e> | ski, no idea what he did but from what I remember it was based on just telling the rules |
| 01:15:51 | <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 ! |
| 01:16:17 | <ski> | and the amazing thing is that this crazy idea actually worked ! :D |
| 01:16:17 | <joel135> | hmm |
| 01:16:19 | → | zincy_ joins (~zincy@2a00:23c8:970c:4801:350f:7ee:191a:6f65) |
| 01:16:54 | <joel135> | i really want to try this |
| 01:17:21 | <geekosaur> | covariance/contravariance? |
| 01:17:39 | geekosaur | doesn't quite follow all of the above, but what the heck |
| 01:19:01 | <joel135> | i have no intuition for this logic variable vs skolem atom distinction though |
| 01:19:14 | <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 |
| 01:19:20 | <ski> | them, when unifying .. i believe this can be done, but i haven't worked through the details) |
| 01:19:55 | <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) |
| 01:20:00 | <joel135> | it seems like logic variables are "positive" in the sense of girard whereas skolem atoms are "negative" |
| 01:20:31 | × | zincy_ quits (~zincy@2a00:23c8:970c:4801:350f:7ee:191a:6f65) (Ping timeout: 245 seconds) |
| 01:20:51 | <ski> | in terms of typechecking, the usual term is "meta variable" (or maybe "placeholder"), rather than "logic variable". but it's the same idea |
| 01:21:21 | <ski> | note that it's incorrect to think that logic variables are associated with existential quantification, and skolems with universal quantification |
| 01:21:55 | <joel135> | ok good that you pointed that out |
| 01:22:07 | × | pretty_dumm_guy quits (trottel@gateway/vpn/protonvpn/prettydummguy/x-88029655) (Quit: WeeChat 3.3) |
| 01:22:12 | × | lavaman quits (~lavaman@98.38.249.169) (Remote host closed the connection) |
| 01:22:35 | <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) |
| 01:23:43 | <ski> | similarly, checking the callee/definer/implementor/producer of a `forall a. ..a..' involves skolems, while the caller/user/consumer involves meta variables |
| 01:23:55 | <ski> | (and the opposite, for `exists a. ..a..') |
| 01:24:46 | × | ec quits (~ec@gateway/tor-sasl/ec) (Remote host closed the connection) |
| 01:25:11 | <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) |
| 01:25:20 | → | ec joins (~ec@gateway/tor-sasl/ec) |
| 01:26:41 | <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 |
| 01:27:24 | <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) |
| 01:29:48 | × | lbseale_ quits (~lbseale@user/ep1ctetus) (Read error: Connection reset by peer) |
| 01:29:58 | <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. |
| 01:30:01 | <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) |
| 01:30:10 | <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) |
| 01:30:50 | <joel135> | or maybe i am wrong to call `L` a goal and it is `member(X,Xs)` that is the goal as you say. |
| 01:31:26 | <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) |
| 01:32:10 | <ski> | joel135 : yes, `L' is a term (a variable in this case), and `member(X,Xs)' is a goal |
| 01:32:22 | <unit73e> | functors are a classic for the covariant/contravariant mambo jambo, it doesn't matter that much tbh |
| 01:32:43 | × | shriekingnoise quits (~shrieking@186.137.144.80) (Quit: Quit) |
| 01:33:29 | <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) |
| 01:34:28 | <joel135> | > logic variables are generated by existential goals *and* universal clauses. while skolems are generated by universal goals and existential clauses |
| 01:34:29 | <lambdabot> | error: |
| 01:34:30 | <lambdabot> | Variable not in scope: |
| 01:34:30 | <lambdabot> | logic :: t0 -> t1 -> t2 -> t3 -> t4 -> t5 -> t Bool -> Boolerror: Vari... |
| 01:34:37 | → | shriekingnoise joins (~shrieking@186.137.144.80) |
| 01:34:49 | <ski> | @botsmack |
| 01:34:49 | <lambdabot> | :) |
| 01:35:03 | <joel135> | this feels reminiscent of the distinction between additive and multiplicative connectives |
| 01:35:11 | <joel135> | rather than positive and negative connectives |
| 01:35:31 | × | syd quits (~syd@cpc91646-hart11-2-0-cust432.11-3.cable.virginm.net) (Read error: No route to host) |
| 01:35:47 | <ski> | meta/logic variable vs. skolem is an operational/procedural issue |
| 01:35:47 | <nitrix> | Poor ski, perpetually doomed now talking about logic programming. I'm sorry I did this to you. |
| 01:35:57 | × | machinedgod quits (~machinedg@135-23-192-217.cpe.pppoe.ca) (Quit: Lost terminal) |
| 01:36:05 | <ski> | nitrix : nah, you didn't, that i can recall :b |
| 01:36:06 | <joel135> | which i think leads us back to the notion of "upgrade" which does connect addition to multiplication, just like the exponential function does |
| 01:36:17 | <unit73e> | logic programming does have it's uses |
| 01:36:24 | <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 |
| 01:36:45 | <unit73e> | yeah I found it strange if you didn't know lol |
| 01:37:35 | <unit73e> | regardless, scala guys like to talk about that |
| 01:37:45 | <unit73e> | with all the + and - stuff |
| 01:37:46 | <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 |
| 01:37:51 | → | machinedgod joins (~machinedg@135-23-192-217.cpe.pppoe.ca) |
| 01:38:46 | <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) |
| 01:40:14 | <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" |
| 01:40:54 | <unit73e> | because I see the image in my head |
| 01:47:36 | → | harveypwca joins (~harveypwc@2601:246:c180:a570:3828:d8:e523:3f67) |
| 01:48:39 | → | a6a45081-2b83 joins (~aditya@2603-6080-0800-8e4a-0000-0000-0000-01a8.res6.spectrum.com) |
| 01:49:38 | <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. |
| 01:50:21 | <joel135> | this connects again to your question earlier about whether there could be several differerent upgrades/downgrades |
| 01:51:46 | × | a6a45081-2b83 quits (~aditya@2603-6080-0800-8e4a-0000-0000-0000-01a8.res6.spectrum.com) (Read error: Connection reset by peer) |
| 01:51:49 | <joel135> | <ski> i wonder if there's possibly two distinct "downgrades" (or two distinct "upgrades" ?) |
| 01:53:00 | → | zincy_ joins (~zincy@2a00:23c8:970c:4801:350f:7ee:191a:6f65) |
| 01:56:03 | → | a6a45081-2b83 joins (~aditya@2603-6080-0800-8e4a-0000-0000-0000-01a8.res6.spectrum.com) |
| 01:56:19 | <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. |
| 01:58:04 | × | zincy_ quits (~zincy@2a00:23c8:970c:4801:350f:7ee:191a:6f65) (Ping timeout: 268 seconds) |
| 01:58:19 | × | a6a45081-2b83 quits (~aditya@2603-6080-0800-8e4a-0000-0000-0000-01a8.res6.spectrum.com) (Read error: Connection reset by peer) |
| 01:58:48 | → | a6a45081-2b83 joins (~aditya@2603-6080-0800-8e4a-0000-0000-0000-01a8.res6.spectrum.com) |
| 01:59:36 | × | DNH quits (~DNH@2a02:8108:1100:16d8:e9ee:3bd5:4988:8148) (Quit: Textual IRC Client: www.textualapp.com) |
| 01:59:54 | × | a6a45081-2b83 quits (~aditya@2603-6080-0800-8e4a-0000-0000-0000-01a8.res6.spectrum.com) (Remote host closed the connection) |
| 02:00:33 | × | hololeap quits (~hololeap@user/hololeap) (Remote host closed the connection) |
| 02:01:48 | → | v01d4lph4 joins (~v01d4lph4@user/v01d4lph4) |
| 02:01:59 | → | hololeap joins (~hololeap@user/hololeap) |
| 02:03:25 | → | Cajun joins (~Cajun@user/cajun) |
| 02:06:23 | × | v01d4lph4 quits (~v01d4lph4@user/v01d4lph4) (Ping timeout: 264 seconds) |
| 02:07:34 | × | hololeap quits (~hololeap@user/hololeap) (Remote host closed the connection) |
| 02:07:41 | × | unit73e quits (~emanuel@2001:818:e8dd:7c00:32b5:c2ff:fe6b:5291) (Quit: Leaving) |
| 02:08:33 | × | machinedgod quits (~machinedg@135-23-192-217.cpe.pppoe.ca) (Ping timeout: 268 seconds) |
| 02:08:34 | <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 |
| 02:08:34 | <Cajun> | general whats the best system to use, considering speed and ease of use? |
| 02:08:46 | <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) |
| 02:08:51 | → | hololeap joins (~hololeap@user/hololeap) |
| 02:13:56 | × | alx741 quits (~alx741@181.196.68.55) (Quit: alx741) |
| 02:19:35 | → | merijn joins (~merijn@83-160-49-249.ip.xs4all.nl) |
| 02:23:27 | × | alzgh quits (~alzgh@user/alzgh) (Remote host closed the connection) |
| 02:28:00 | × | Tuplanolla quits (~Tuplanoll@91-159-69-50.elisa-laajakaista.fi) (Quit: Leaving.) |
| 02:32:11 | × | EvanR quits (~evan@user/evanr) (Ping timeout: 245 seconds) |
| 02:42:17 | × | jpds1 quits (~jpds@gateway/tor-sasl/jpds) (Remote host closed the connection) |
| 02:42:42 | → | jpds1 joins (~jpds@gateway/tor-sasl/jpds) |
| 02:43:43 | → | zincy_ joins (~zincy@2a00:23c8:970c:4801:350f:7ee:191a:6f65) |
| 02:45:50 | × | xff0x quits (~xff0x@2001:1a81:5273:3700:28cd:42fe:3b9:2637) (Ping timeout: 260 seconds) |
| 02:47:41 | → | xff0x joins (~xff0x@2001:1a81:52b1:3000:b3ef:fedd:d143:889a) |
| 02:48:38 | × | zincy_ quits (~zincy@2a00:23c8:970c:4801:350f:7ee:191a:6f65) (Ping timeout: 268 seconds) |
| 02:51:02 | × | merijn quits (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 260 seconds) |
| 03:00:00 | × | sander quits (~sander@user/sander) (Quit: So long! :)) |
| 03:01:29 | → | sander joins (~sander@user/sander) |
| 03:06:28 | × | faultline quits (~christian@nat-eduroam-01.scc.kit.edu) (Remote host closed the connection) |
| 03:07:45 | × | Square quits (~a@178.62.91.8) (Changing host) |
| 03:07:45 | → | Square joins (~a@user/square) |
| 03:08:19 | <lyxia> | Use IO and don't get into situations where you need anything else. |
| 03:08:25 | → | EvanR joins (~evan@2600:1700:ba69:10:98b6:b5c4:3b00:4c9a) |
| 03:13:18 | × | EvanR quits (~evan@2600:1700:ba69:10:98b6:b5c4:3b00:4c9a) (Ping timeout: 268 seconds) |
| 03:15:33 | → | slack1256 joins (~slack1256@191.125.99.211) |
| 03:18:19 | → | zincy_ joins (~zincy@2a00:23c8:970c:4801:350f:7ee:191a:6f65) |
| 03:23:11 | × | zincy_ quits (~zincy@2a00:23c8:970c:4801:350f:7ee:191a:6f65) (Ping timeout: 268 seconds) |
| 03:34:35 | × | nosewings quits (~ngpc@2603-8081-3e05-e2d0-91fa-0be4-4222-fe4b.res6.spectrum.com) (Remote host closed the connection) |
| 03:39:30 | → | finn_elija joins (~finn_elij@user/finn-elija/x-0085643) |
| 03:39:30 | × | FinnElija quits (~finn_elij@user/finn-elija/x-0085643) (Killed (NickServ (Forcing logout FinnElija -> finn_elija))) |
| 03:39:30 | finn_elija | is now known as FinnElija |
| 03:47:30 | × | waleee quits (~waleee@h-98-128-228-119.NA.cust.bahnhof.se) (Ping timeout: 260 seconds) |
| 03:51:29 | → | zincy_ joins (~zincy@2a00:23c8:970c:4801:350f:7ee:191a:6f65) |
| 03:55:52 | × | zincy_ quits (~zincy@2a00:23c8:970c:4801:350f:7ee:191a:6f65) (Ping timeout: 268 seconds) |
| 03:56:43 | → | a6a45081-2b83 joins (~aditya@2603-6080-0800-8e4a-0000-0000-0000-01a8.res6.spectrum.com) |
| 03:57:12 | <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) |
| 03:59:24 | <a6a45081-2b83> | my plan is to have `instace Memoizable (Ratio Integer) where memoize f = let f' (a,b) = f (a%b) in memoize f'` |
| 03:59:27 | <a6a45081-2b83> | or something like that |
| 03:59:34 | × | hiruji quits (~hiruji@user/hiruji) (Ping timeout: 268 seconds) |
| 04:01:02 | → | yauhsien joins (~yauhsien@118-167-41-229.dynamic-ip.hinet.net) |
| 04:05:34 | × | Cajun quits (~Cajun@user/cajun) (Quit: Client closed) |
| 04:05:42 | × | yauhsien quits (~yauhsien@118-167-41-229.dynamic-ip.hinet.net) (Ping timeout: 260 seconds) |
| 04:11:05 | × | mcglk quits (~mcglk@131.191.49.120) (Read error: Connection reset by peer) |
| 04:11:21 | → | Cajun joins (~Cajun@user/cajun) |
| 04:12:12 | <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 |
| 04:13:47 | × | a6a45081-2b83 quits (~aditya@2603-6080-0800-8e4a-0000-0000-0000-01a8.res6.spectrum.com) (Read error: Connection reset by peer) |
| 04:13:52 | → | mcglk joins (~mcglk@131.191.49.120) |
| 04:15:18 | → | bitdex joins (~bitdex@gateway/tor-sasl/bitdex) |
| 04:16:07 | × | img quits (~img@user/img) (Quit: ZNC 1.8.2 - https://znc.in) |
| 04:18:08 | → | a6a45081-2b83 joins (~aditya@2603-6080-0800-8e4a-0000-0000-0000-01a8.res6.spectrum.com) |
| 04:18:53 | × | a6a45081-2b83 quits (~aditya@2603-6080-0800-8e4a-0000-0000-0000-01a8.res6.spectrum.com) (Read error: Connection reset by peer) |
| 04:19:21 | → | a6a45081-2b83 joins (~aditya@2603-6080-0800-8e4a-0000-0000-0000-01a8.res6.spectrum.com) |
| 04:19:27 | × | a6a45081-2b83 quits (~aditya@2603-6080-0800-8e4a-0000-0000-0000-01a8.res6.spectrum.com) (Client Quit) |
| 04:19:30 | → | img joins (~img@user/img) |
| 04:35:04 | × | slowButPresent quits (~slowButPr@user/slowbutpresent) (Quit: leaving) |
| 04:35:47 | × | [itchyjunk] quits (~itchyjunk@user/itchyjunk/x-7353470) (Read error: Connection reset by peer) |
| 04:45:25 | → | zincy_ joins (~zincy@2a00:23c8:970c:4801:350f:7ee:191a:6f65) |
| 04:47:02 | × | zebrag quits (~chris@user/zebrag) (Quit: Konversation terminated!) |
| 04:47:34 | → | v01d4lph4 joins (~v01d4lph4@user/v01d4lph4) |
| 04:47:35 | → | merijn joins (~merijn@83-160-49-249.ip.xs4all.nl) |
| 04:48:01 | × | ishutin quits (~ishutin@62-165-208-189.pool.digikabel.hu) (Ping timeout: 245 seconds) |
| 04:50:03 | → | ishutin joins (~ishutin@92-249-179-61.pool.digikabel.hu) |
| 04:50:07 | × | zincy_ quits (~zincy@2a00:23c8:970c:4801:350f:7ee:191a:6f65) (Ping timeout: 268 seconds) |
| 04:50:48 | <ski> | joel135 : perhaps you could elaborate on the "upgrading a polynomial p : ℕ₃ to an operator p(d/dx)" part (what is meant by that) |
| 05:07:11 | × | SeungheonOh quits (~Thunderbi@2600:1700:5168:1400:1574:2437:4f0d:50e6) (Quit: SeungheonOh) |
| 05:07:35 | × | emf quits (~emf@2620:10d:c090:400::5:38d) (Ping timeout: 264 seconds) |
| 05:10:50 | → | emf joins (~emf@163.114.132.5) |
| 05:15:24 | × | emf quits (~emf@163.114.132.5) (Read error: Connection reset by peer) |
| 05:16:15 | → | emf joins (~emf@2620:10d:c090:400::5:f801) |
| 05:17:45 | × | slack1256 quits (~slack1256@191.125.99.211) (Ping timeout: 256 seconds) |
| 05:18:44 | × | mrianbloom quits (sid350277@id-350277.ilkley.irccloud.com) (Ping timeout: 252 seconds) |
| 05:18:44 | × | vito quits (sid1962@user/vito) (Ping timeout: 252 seconds) |
| 05:18:51 | × | pepeiborra quits (sid443799@id-443799.ilkley.irccloud.com) (Ping timeout: 245 seconds) |
| 05:18:51 | × | lightandlight quits (sid135476@id-135476.helmsley.irccloud.com) (Ping timeout: 245 seconds) |
| 05:18:54 | × | whez quits (sid470288@id-470288.lymington.irccloud.com) (Ping timeout: 260 seconds) |
| 05:18:59 | × | gregberns__ quits (sid315709@id-315709.helmsley.irccloud.com) (Ping timeout: 264 seconds) |
| 05:18:59 | × | parseval quits (sid239098@id-239098.helmsley.irccloud.com) (Ping timeout: 264 seconds) |
| 05:19:07 | × | bitmapper quits (uid464869@id-464869.lymington.irccloud.com) (Ping timeout: 268 seconds) |
| 05:19:08 | × | carter quits (sid14827@id-14827.helmsley.irccloud.com) (Ping timeout: 260 seconds) |
| 05:19:08 | × | truckasaurus quits (sid457088@id-457088.helmsley.irccloud.com) (Ping timeout: 260 seconds) |
| 05:19:08 | × | NemesisD quits (sid24071@id-24071.lymington.irccloud.com) (Ping timeout: 260 seconds) |
| 05:19:08 | × | supersven quits (sid501114@id-501114.ilkley.irccloud.com) (Ping timeout: 260 seconds) |
| 05:19:08 | × | systemfault quits (sid267009@id-267009.uxbridge.irccloud.com) (Ping timeout: 260 seconds) |
| 05:19:08 | × | nrr_ quits (sid20938@id-20938.lymington.irccloud.com) (Ping timeout: 260 seconds) |
| 05:19:09 | × | aria quits (sid380617@id-380617.lymington.irccloud.com) (Ping timeout: 265 seconds) |
| 05:19:10 | × | sa quits (sid1055@id-1055.tinside.irccloud.com) (Ping timeout: 260 seconds) |
| 05:19:10 | × | cbarrett quits (sid192934@id-192934.helmsley.irccloud.com) (Ping timeout: 260 seconds) |
| 05:19:10 | × | bw quits (sid2730@user/betawaffle) (Ping timeout: 260 seconds) |
| 05:19:16 | × | hamishmack quits (sid389057@id-389057.hampstead.irccloud.com) (Ping timeout: 245 seconds) |
| 05:19:16 | × | glowcoil quits (sid3405@id-3405.tinside.irccloud.com) (Ping timeout: 245 seconds) |
| 05:19:16 | × | idnar quits (sid12240@debian/mithrandi) (Ping timeout: 245 seconds) |
| 05:19:35 | × | aristid quits (sid1599@id-1599.uxbridge.irccloud.com) (Ping timeout: 264 seconds) |
| 05:19:36 | × | SanchayanMaity quits (sid478177@id-478177.hampstead.irccloud.com) (Ping timeout: 260 seconds) |
| 05:19:36 | × | alanz quits (sid110616@id-110616.uxbridge.irccloud.com) (Ping timeout: 260 seconds) |
| 05:19:41 | × | jackdk quits (sid373013@cssa/jackdk) (Ping timeout: 245 seconds) |
| 05:19:41 | × | meinside quits (uid24933@id-24933.helmsley.irccloud.com) (Ping timeout: 245 seconds) |
| 05:19:41 | × | dpratt_ quits (sid193493@id-193493.helmsley.irccloud.com) (Ping timeout: 245 seconds) |
| 05:19:41 | × | obviyus quits (sid415299@user/obviyus) (Ping timeout: 245 seconds) |
| 05:19:41 | × | Pent quits (sid313808@id-313808.lymington.irccloud.com) (Ping timeout: 245 seconds) |
| 05:19:41 | × | edmundnoble quits (sid229620@id-229620.helmsley.irccloud.com) (Ping timeout: 245 seconds) |
| 05:19:41 | × | taktoa[c] quits (sid282096@id-282096.tinside.irccloud.com) (Ping timeout: 245 seconds) |
| 05:19:41 | × | gonz___ quits (sid304396@id-304396.lymington.irccloud.com) (Ping timeout: 245 seconds) |
| 05:19:41 | × | bbhoss quits (sid18216@id-18216.tinside.irccloud.com) (Ping timeout: 245 seconds) |
| 05:19:43 | × | servytor quits (uid525486@id-525486.hampstead.irccloud.com) (Ping timeout: 268 seconds) |
| 05:19:45 | × | dsal quits (sid13060@id-13060.lymington.irccloud.com) (Ping timeout: 260 seconds) |
| 05:20:04 | × | SethTisue__ quits (sid14912@id-14912.ilkley.irccloud.com) (Ping timeout: 260 seconds) |
| 05:20:04 | × | hendi quits (sid489601@id-489601.lymington.irccloud.com) (Ping timeout: 260 seconds) |
| 05:20:04 | × | christiaanb quits (sid84827@id-84827.lymington.irccloud.com) (Ping timeout: 260 seconds) |
| 05:20:04 | × | kaychaks__ quits (sid236345@id-236345.helmsley.irccloud.com) (Ping timeout: 260 seconds) |
| 05:20:06 | × | agander_m quits (sid407952@id-407952.tinside.irccloud.com) (Ping timeout: 245 seconds) |
| 05:20:11 | × | JSharp quits (sid4580@id-4580.lymington.irccloud.com) (Ping timeout: 264 seconds) |
| 05:20:18 | × | pjlsergeant quits (sid143467@id-143467.hampstead.irccloud.com) (Ping timeout: 260 seconds) |
| 05:20:18 | × | rubin55 quits (sid175221@id-175221.hampstead.irccloud.com) (Ping timeout: 260 seconds) |
| 05:20:20 | × | ysh quits (sid6017@id-6017.ilkley.irccloud.com) (Ping timeout: 260 seconds) |
| 05:20:20 | × | alinab quits (sid468903@id-468903.helmsley.irccloud.com) (Ping timeout: 260 seconds) |
| 05:20:20 | × | econo quits (uid147250@user/econo) (Ping timeout: 268 seconds) |
| 05:20:20 | × | rtpg quits (sid443069@id-443069.ilkley.irccloud.com) (Ping timeout: 260 seconds) |
| 05:20:20 | × | gmc quits (sid58314@id-58314.ilkley.irccloud.com) (Ping timeout: 260 seconds) |
| 05:20:21 | × | whatsupdoc quits (uid509081@id-509081.hampstead.irccloud.com) (Ping timeout: 268 seconds) |
| 05:20:23 | × | S11001001 quits (sid42510@id-42510.ilkley.irccloud.com) (Ping timeout: 252 seconds) |
| 05:20:23 | × | sa1 quits (sid7690@id-7690.ilkley.irccloud.com) (Ping timeout: 252 seconds) |
| 05:20:26 | → | zincy_ joins (~zincy@2a00:23c8:970c:4801:350f:7ee:191a:6f65) |
| 05:20:32 | × | tritlo quits (sid58727@user/tritlo) (Ping timeout: 260 seconds) |
| 05:20:32 | × | ehamberg quits (sid18208@id-18208.hampstead.irccloud.com) (Ping timeout: 260 seconds) |
| 05:20:32 | × | aarchi quits (sid486183@id-486183.uxbridge.irccloud.com) (Ping timeout: 260 seconds) |
| 05:20:32 | × | ephemient quits (uid407513@id-407513.lymington.irccloud.com) (Ping timeout: 260 seconds) |
| 05:20:32 | × | scav quits (sid309693@id-309693.helmsley.irccloud.com) (Ping timeout: 260 seconds) |
| 05:20:32 | × | hubvu quits (sid495858@user/hubvu) (Ping timeout: 260 seconds) |
| 05:20:32 | × | NiKaN quits (sid385034@id-385034.helmsley.irccloud.com) (Ping timeout: 260 seconds) |
| 05:20:32 | × | b20n quits (sid115913@id-115913.uxbridge.irccloud.com) (Ping timeout: 260 seconds) |
| 05:20:39 | × | jakesyl_ quits (sid56879@id-56879.hampstead.irccloud.com) (Ping timeout: 268 seconds) |
| 05:20:46 | × | pony quits (sid524992@smol/hors) (Ping timeout: 260 seconds) |
| 05:20:55 | × | mcfilib quits (sid302703@user/mcfilib) (Ping timeout: 260 seconds) |
| 05:20:55 | × | integral quits (sid296274@user/integral) (Ping timeout: 260 seconds) |
| 05:20:55 | × | awpr quits (uid446117@id-446117.lymington.irccloud.com) (Ping timeout: 260 seconds) |
| 05:20:58 | × | hongminhee quits (sid295@id-295.tinside.irccloud.com) (Ping timeout: 268 seconds) |
| 05:21:00 | × | stevenxl quits (sid133530@id-133530.uxbridge.irccloud.com) (Ping timeout: 260 seconds) |
| 05:21:00 | × | tnks quits (sid412124@id-412124.helmsley.irccloud.com) (Ping timeout: 260 seconds) |
| 05:21:00 | × | bjs quits (sid190364@user/bjs) (Ping timeout: 260 seconds) |
| 05:21:00 | × | Firedancer quits (sid336191@id-336191.hampstead.irccloud.com) (Ping timeout: 260 seconds) |
| 05:21:04 | → | lightandlight joins (sid135476@id-135476.helmsley.irccloud.com) |
| 05:21:08 | → | parseval joins (sid239098@id-239098.helmsley.irccloud.com) |
| 05:21:09 | → | ysh joins (sid6017@id-6017.ilkley.irccloud.com) |
| 05:21:10 | → | hubvu joins (sid495858@user/hubvu) |
| 05:21:10 | → | scav joins (sid309693@id-309693.helmsley.irccloud.com) |
| 05:21:10 | → | bitmapper joins (uid464869@id-464869.lymington.irccloud.com) |
| 05:21:11 | → | S11001001 joins (sid42510@id-42510.ilkley.irccloud.com) |
| 05:21:15 | → | NemesisD joins (sid24071@id-24071.lymington.irccloud.com) |
| 05:21:16 | → | aristid joins (sid1599@id-1599.uxbridge.irccloud.com) |
| 05:21:18 | → | gregberns__ joins (sid315709@helmsley.irccloud.com) |
| 05:21:19 | → | SethTisue__ joins (sid14912@ilkley.irccloud.com) |
| 05:21:19 | → | sa1 joins (sid7690@id-7690.ilkley.irccloud.com) |
| 05:21:20 | → | dsal joins (sid13060@id-13060.lymington.irccloud.com) |
| 05:21:21 | → | whez joins (sid470288@lymington.irccloud.com) |
| 05:21:21 | → | bjs joins (sid190364@user/bjs) |
| 05:21:22 | → | bbhoss joins (sid18216@id-18216.tinside.irccloud.com) |
| 05:21:24 | → | mrianbloom joins (sid350277@ilkley.irccloud.com) |
| 05:21:24 | → | glowcoil joins (sid3405@tinside.irccloud.com) |
| 05:21:24 | → | supersven joins (sid501114@ilkley.irccloud.com) |
| 05:21:27 | → | sa joins (sid1055@id-1055.tinside.irccloud.com) |
| 05:21:29 | → | vito joins (sid1962@id-1962.uxbridge.irccloud.com) |
| 05:21:30 | → | hongminhee joins (sid295@id-295.tinside.irccloud.com) |
| 05:21:30 | → | hendi joins (sid489601@id-489601.lymington.irccloud.com) |
| 05:21:31 | × | vito quits (sid1962@id-1962.uxbridge.irccloud.com) (Changing host) |
| 05:21:31 | → | vito joins (sid1962@user/vito) |
| 05:21:39 | → | servytor joins (uid525486@2a03:5180:f:4::8:4ae) |
| 05:21:39 | → | JSharp joins (sid4580@id-4580.lymington.irccloud.com) |
| 05:21:42 | → | meinside joins (uid24933@helmsley.irccloud.com) |
| 05:21:44 | → | alinab joins (sid468903@helmsley.irccloud.com) |
| 05:21:44 | → | Pent joins (sid313808@2a03:5180:f:2::4:c9d0) |
| 05:21:45 | → | gmc joins (sid58314@ilkley.irccloud.com) |
| 05:21:46 | → | gonz___ joins (sid304396@2a03:5180:f:2::4:a50c) |
| 05:21:46 | → | aria joins (sid380617@lymington.irccloud.com) |
| 05:21:48 | → | idnar joins (sid12240@debian/mithrandi) |
| 05:21:49 | → | rtpg joins (sid443069@2a03:5180:f:3::6:c2bd) |
| 05:21:52 | → | hamishmack joins (sid389057@2a03:5180:f:4::5:efc1) |
| 05:21:52 | → | awpr joins (uid446117@lymington.irccloud.com) |
| 05:21:53 | → | systemfault joins (sid267009@2a03:5180:f:5::4:1301) |
| 05:21:54 | → | christiaanb joins (sid84827@id-84827.lymington.irccloud.com) |
| 05:21:58 | → | bw joins (sid2730@user/betawaffle) |
| 05:21:58 | → | truckasaurus joins (sid457088@id-457088.helmsley.irccloud.com) |
| 05:21:59 | → | agander_m joins (sid407952@2a03:5180:f::6:3990) |
| 05:21:59 | × | merijn quits (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 264 seconds) |
| 05:21:59 | → | obviyus joins (sid415299@user/obviyus) |
| 05:22:00 | → | tnks joins (sid412124@2a03:5180:f:1::6:49dc) |
| 05:22:00 | → | mcfilib joins (sid302703@2a03:5180:f:1::4:9e6f) |
| 05:22:00 | × | mcfilib quits (sid302703@2a03:5180:f:1::4:9e6f) (Changing host) |
| 05:22:00 | → | mcfilib joins (sid302703@user/mcfilib) |
| 05:22:01 | → | taktoa[c] joins (sid282096@id-282096.tinside.irccloud.com) |
| 05:22:02 | → | nrr_ joins (sid20938@id-20938.lymington.irccloud.com) |
| 05:22:04 | → | kaychaks__ joins (sid236345@2a03:5180:f:1::3:9b39) |
| 05:22:05 | → | ephemient joins (uid407513@2a03:5180:f:2::6:37d9) |
| 05:22:06 | → | edmundnoble joins (sid229620@2a03:5180:f:1::3:80f4) |
| 05:22:08 | → | cbarrett joins (sid192934@2a03:5180:f:1::2:f1a6) |
| 05:22:11 | → | jackdk joins (sid373013@cssa/jackdk) |
| 05:22:11 | → | econo joins (uid147250@user/econo) |
| 05:22:14 | → | integral joins (sid296274@user/integral) |
| 05:22:18 | → | whatsupdoc joins (uid509081@2a03:5180:f:4::7:c499) |
| 05:22:20 | → | carter joins (sid14827@id-14827.helmsley.irccloud.com) |
| 05:22:21 | → | b20n joins (sid115913@2a03:5180:f:5::1:c4c9) |
| 05:22:22 | → | stevenxl joins (sid133530@2a03:5180:f:5::2:99a) |
| 05:22:22 | → | dpratt_ joins (sid193493@helmsley.irccloud.com) |
| 05:22:24 | → | pony joins (sid524992@smol/hors) |
| 05:22:25 | → | aarchi joins (sid486183@2a03:5180:f:5::7:6b27) |
| 05:22:25 | → | SanchayanMaity joins (sid478177@2a03:5180:f:4::7:4be1) |
| 05:22:25 | → | Firedancer joins (sid336191@2a03:5180:f:4::5:213f) |
| 05:22:25 | → | pepeiborra joins (sid443799@2a03:5180:f:3::6:c597) |
| 05:22:25 | → | alanz joins (sid110616@2a03:5180:f:5::1:b018) |
| 05:22:27 | → | pjlsergeant joins (sid143467@2a03:5180:f:4::2:306b) |
| 05:22:29 | → | rubin55 joins (sid175221@2a03:5180:f:4::2:ac75) |
| 05:22:47 | → | NiKaN joins (sid385034@2a03:5180:f:1::5:e00a) |
| 05:22:49 | → | jakesyl_ joins (sid56879@2a03:5180:f:4::de2f) |
| 05:24:11 | → | ehamberg joins (sid18208@id-18208.hampstead.irccloud.com) |
| 05:24:16 | → | tritlo joins (sid58727@user/tritlo) |
| 05:25:17 | × | zincy_ quits (~zincy@2a00:23c8:970c:4801:350f:7ee:191a:6f65) (Ping timeout: 268 seconds) |
| 05:27:01 | → | EvanR joins (~evan@2600:1700:ba69:10:acd9:793b:27c9:b878) |
| 05:36:26 | → | yauhsien joins (~yauhsien@2402:7500:4e4:2cb1:35e8:471e:a055:9d52) |
| 05:41:06 | × | Cajun quits (~Cajun@user/cajun) (Quit: Client closed) |
| 05:42:24 | → | Cajun joins (~Cajun@user/cajun) |
| 05:55:31 | → | zincy_ joins (~zincy@2a00:23c8:970c:4801:350f:7ee:191a:6f65) |
| 06:00:23 | × | zincy_ quits (~zincy@2a00:23c8:970c:4801:350f:7ee:191a:6f65) (Ping timeout: 264 seconds) |
| 06:05:10 | × | v01d4lph4 quits (~v01d4lph4@user/v01d4lph4) (Read error: Connection reset by peer) |
| 06:05:32 | → | v01d4lph4 joins (~v01d4lph4@user/v01d4lph4) |
| 06:06:42 | × | hololeap quits (~hololeap@user/hololeap) (Remote host closed the connection) |
| 06:08:14 | → | hololeap joins (~hololeap@user/hololeap) |
| 06:13:59 | × | euandreh quits (~euandreh@2804:14c:33:9fe5:90d0:563b:3279:f95b) (Ping timeout: 268 seconds) |
| 06:15:47 | × | chexum quits (~quassel@gateway/tor-sasl/chexum) (Remote host closed the connection) |
| 06:16:08 | → | chexum joins (~quassel@gateway/tor-sasl/chexum) |
| 06:21:51 | → | chomwitt joins (~chomwitt@2a02:587:dc02:9f00:12c3:7bff:fe6d:d374) |
| 06:25:05 | × | xff0x quits (~xff0x@2001:1a81:52b1:3000:b3ef:fedd:d143:889a) (Ping timeout: 268 seconds) |
| 06:25:35 | × | EvanR quits (~evan@2600:1700:ba69:10:acd9:793b:27c9:b878) (Ping timeout: 264 seconds) |
| 06:25:53 | → | xff0x joins (~xff0x@2001:1a81:52b1:3000:355a:710f:ac35:1a61) |
| 06:32:50 | × | MidAutumnMoon quits (~MidAutumn@user/midautumnmoon) (Quit: Leaving for a break - theLounge) |
| 06:33:26 | → | MidAutumnMoon joins (~MidAutumn@user/midautumnmoon) |
| 06:35:54 | × | chexum quits (~quassel@gateway/tor-sasl/chexum) (Remote host closed the connection) |
| 06:36:05 | → | chexum joins (~quassel@gateway/tor-sasl/chexum) |
| 06:38:42 | × | chomwitt quits (~chomwitt@2a02:587:dc02:9f00:12c3:7bff:fe6d:d374) (Ping timeout: 260 seconds) |
| 06:40:06 | × | xff0x quits (~xff0x@2001:1a81:52b1:3000:355a:710f:ac35:1a61) (Ping timeout: 245 seconds) |
| 06:41:05 | → | xff0x joins (~xff0x@2001:1a81:52b1:3000:7ef:3640:6d4d:8cb8) |
| 06:42:31 | × | aegon quits (~mike@174.127.249.180) (Remote host closed the connection) |
| 06:46:06 | → | zincy_ joins (~zincy@2a00:23c8:970c:4801:350f:7ee:191a:6f65) |
| 06:48:56 | → | alzgh joins (~alzgh@user/alzgh) |
| 06:50:31 | × | zincy_ quits (~zincy@2a00:23c8:970c:4801:350f:7ee:191a:6f65) (Ping timeout: 245 seconds) |
| 06:54:16 | × | yauhsien quits (~yauhsien@2402:7500:4e4:2cb1:35e8:471e:a055:9d52) (Remote host closed the connection) |
| 06:54:34 | → | vysn joins (~vysn@user/vysn) |
| 07:08:11 | × | econo quits (uid147250@user/econo) (Quit: Connection closed for inactivity) |
| 07:12:29 | → | yauhsien joins (~yauhsien@118-167-41-229.dynamic-ip.hinet.net) |
| 07:12:38 | × | yauhsien quits (~yauhsien@118-167-41-229.dynamic-ip.hinet.net) (Remote host closed the connection) |
| 07:16:30 | → | chomwitt joins (~chomwitt@athedsl-32204.home.otenet.gr) |
| 07:17:07 | × | Sgeo_ quits (~Sgeo@user/sgeo) (Read error: Connection reset by peer) |
| 07:18:01 | → | merijn joins (~merijn@83-160-49-249.ip.xs4all.nl) |
| 07:19:02 | × | geekosaur quits (~geekosaur@xmonad/geekosaur) (Remote host closed the connection) |
| 07:20:02 | → | geekosaur joins (~geekosaur@xmonad/geekosaur) |
| 07:21:21 | → | lavaman joins (~lavaman@98.38.249.169) |
| 07:22:25 | → | zincy_ joins (~zincy@2a00:23c8:970c:4801:350f:7ee:191a:6f65) |
| 07:25:31 | × | lavaman quits (~lavaman@98.38.249.169) (Ping timeout: 245 seconds) |
| 07:27:14 | × | zincy_ quits (~zincy@2a00:23c8:970c:4801:350f:7ee:191a:6f65) (Ping timeout: 260 seconds) |
| 07:27:58 | × | eggplantade quits (~Eggplanta@108-201-191-115.lightspeed.sntcca.sbcglobal.net) (Remote host closed the connection) |
| 07:31:14 | → | max22- joins (~maxime@lfbn-ren-1-762-224.w81-53.abo.wanadoo.fr) |
| 07:33:49 | × | brainfreeze quits (~brainfree@2a03:1b20:4:f011::20d) (Remote host closed the connection) |
| 07:38:17 | → | gehmehgeh joins (~user@user/gehmehgeh) |
| 07:43:43 | → | yauhsien joins (~yauhsien@118-167-41-229.dynamic-ip.hinet.net) |
| 07:48:26 | × | yauhsien quits (~yauhsien@118-167-41-229.dynamic-ip.hinet.net) (Ping timeout: 245 seconds) |
| 07:51:54 | × | bitmapper quits (uid464869@id-464869.lymington.irccloud.com) (Quit: Connection closed for inactivity) |
| 07:52:11 | × | merijn quits (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 245 seconds) |
| 07:59:40 | → | cheater joins (~Username@user/cheater) |
| 08:05:03 | → | hendursaga joins (~weechat@user/hendursaga) |
| 08:05:39 | × | v01d4lph4 quits (~v01d4lph4@user/v01d4lph4) (Remote host closed the connection) |
| 08:05:52 | → | johnny_sitar joins (~artur@078088015209.bialystok.vectranet.pl) |
| 08:07:05 | → | madjestic joins (~madjestic@88-159-247-120.fixed.kpn.net) |
| 08:08:30 | × | hendursa1 quits (~weechat@user/hendursaga) (Ping timeout: 276 seconds) |
| 08:12:53 | → | zincy_ joins (~zincy@2a00:23c8:970c:4801:350f:7ee:191a:6f65) |
| 08:14:47 | × | emf quits (~emf@2620:10d:c090:400::5:f801) (Ping timeout: 264 seconds) |
| 08:17:11 | × | zincy_ quits (~zincy@2a00:23c8:970c:4801:350f:7ee:191a:6f65) (Ping timeout: 245 seconds) |
| 08:17:27 | × | geekosaur quits (~geekosaur@xmonad/geekosaur) (Remote host closed the connection) |
| 08:17:36 | × | hendursaga quits (~weechat@user/hendursaga) (Ping timeout: 276 seconds) |
| 08:17:51 | → | geekosaur joins (~geekosaur@xmonad/geekosaur) |
| 08:19:26 | → | hendursaga joins (~weechat@user/hendursaga) |
| 08:21:40 | → | emf joins (~emf@c-73-97-137-43.hsd1.wa.comcast.net) |
| 08:26:47 | × | madjestic quits (~madjestic@88-159-247-120.fixed.kpn.net) (Ping timeout: 264 seconds) |
| 08:28:59 | → | eggplantade joins (~Eggplanta@108-201-191-115.lightspeed.sntcca.sbcglobal.net) |
| 08:29:05 | → | mei3 joins (~mei@user/mei) |
| 08:33:34 | × | eggplantade quits (~Eggplanta@108-201-191-115.lightspeed.sntcca.sbcglobal.net) (Ping timeout: 260 seconds) |
| 08:39:36 | → | madjestic joins (~madjestic@88-159-247-120.fixed.kpn.net) |
| 08:43:20 | → | wonko joins (~wjc@user/wonko) |
| 08:55:16 | × | tzh quits (~tzh@c-24-21-73-154.hsd1.or.comcast.net) (Quit: zzz) |
| 08:55:57 | → | v01d4lph4 joins (~v01d4lph4@106.215.93.204) |
| 08:55:57 | × | v01d4lph4 quits (~v01d4lph4@106.215.93.204) (Changing host) |
| 08:55:57 | → | v01d4lph4 joins (~v01d4lph4@user/v01d4lph4) |
| 09:00:03 | × | cloudy quits (~cloudy@2001:470:69fc:105::50c0) (Quit: You have been kicked for being idle) |
| 09:00:35 | → | merijn joins (~merijn@83-160-49-249.ip.xs4all.nl) |
| 09:02:09 | × | v01d4lph4 quits (~v01d4lph4@user/v01d4lph4) (Remote host closed the connection) |
| 09:02:35 | → | random-jellyfish joins (~random-je@user/random-jellyfish) |
| 09:08:11 | × | johnny_sitar quits (~artur@078088015209.bialystok.vectranet.pl) (Ping timeout: 264 seconds) |
| 09:12:55 | → | v01d4lph4 joins (~v01d4lph4@user/v01d4lph4) |
| 09:15:08 | → | Lycurgus joins (~juan@98.4.112.204) |
| 09:15:18 | × | ByronJohnson quits (~bairyn@50-250-232-19-static.hfc.comcastbusiness.net) (Ping timeout: 268 seconds) |
| 09:19:55 | → | boxscape_ joins (~boxscape_@mue-88-130-59-018.dsl.tropolys.de) |
| 09:26:22 | → | _ht joins (~quassel@82-169-194-8.biz.kpn.net) |
| 09:26:54 | → | ByronJohnson joins (~bairyn@50-250-232-19-static.hfc.comcastbusiness.net) |
| 09:29:33 | → | johnny_sitar joins (~artur@078088015209.bialystok.vectranet.pl) |
| 09:33:56 | × | v01d4lph4 quits (~v01d4lph4@user/v01d4lph4) (Remote host closed the connection) |
| 09:36:35 | → | v01d4lph4 joins (~v01d4lph4@user/v01d4lph4) |
| 09:44:47 | → | kuribas joins (~user@ptr-25vy0i7euy3zycfmzaa.18120a2.ip6.access.telenet.be) |
| 09:47:18 | × | arahael quits (~arahael@124.148.78.199) (Ping timeout: 260 seconds) |
| 09:50:13 | × | Lycurgus quits (~juan@98.4.112.204) (Quit: Exeunt) |
| 09:53:39 | × | Athas quits (athas@2a01:7c8:aaac:1cf:a0d4:8908:cfdb:b9c0) (Quit: ZNC 1.8.2 - https://znc.in) |
| 09:53:49 | → | Athas joins (athas@sigkill.dk) |
| 09:55:06 | × | wonko quits (~wjc@user/wonko) (Ping timeout: 245 seconds) |
| 09:59:16 | ← | emanuele6 parts (~emanuele6@user/emanuele6) (WeeChat 3.3) |
| 09:59:47 | × | johnny_sitar quits (~artur@078088015209.bialystok.vectranet.pl) (Remote host closed the connection) |
| 10:00:04 | → | johnny_sitar joins (~artur@078088015209.bialystok.vectranet.pl) |
| 10:00:21 | × | v01d4lph4 quits (~v01d4lph4@user/v01d4lph4) (Remote host closed the connection) |
| 10:04:16 | × | merijn quits (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 245 seconds) |
| 10:07:19 | × | chomwitt quits (~chomwitt@athedsl-32204.home.otenet.gr) (Ping timeout: 256 seconds) |
| 10:12:36 | → | arahael joins (~arahael@202-159-171-156.tpgi.com.au) |
| 10:13:01 | → | Tuplanolla joins (~Tuplanoll@91-159-69-50.elisa-laajakaista.fi) |
| 10:17:26 | → | mc47 joins (~mc47@xmonad/TheMC47) |
| 10:22:18 | <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)), |
| 10:23:05 | <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. ⋯). |
| 10:29:55 | → | mmhat joins (~mmh@55d4b9d8.access.ecotel.net) |
| 10:35:52 | → | Inst joins (~Inst@2601:6c4:4080:3f80:40a:9f91:8f3e:4f02) |
| 10:36:03 | <Inst> | a gonad is just a gonoid in the category of endofunctors ;) |
| 10:44:56 | → | zer0bitz joins (~zer0bitz@dsl-hkibng31-54fae3-116.dhcp.inet.fi) |
| 10:45:13 | × | kuribas quits (~user@ptr-25vy0i7euy3zycfmzaa.18120a2.ip6.access.telenet.be) (Remote host closed the connection) |
| 10:47:05 | × | whatsupdoc quits (uid509081@2a03:5180:f:4::7:c499) (Quit: Connection closed for inactivity) |
| 10:47:42 | <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 _+_, _*_, _∘_, _▫_, ...) |
| 10:51:08 | <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) |
| 11:00:50 | → | alx741 joins (~alx741@181.196.68.55) |
| 11:05:18 | × | tremon quits (~tremon@217-63-61-89.cable.dynamic.v4.ziggo.nl) (Quit: getting boxed in) |
| 11:05:30 | → | Pickchea joins (~private@user/pickchea) |
| 11:07:19 | → | Gurkenglas joins (~Gurkengla@dslb-002-203-144-204.002.203.pools.vodafone-ip.de) |
| 11:10:16 | cocreatu1 | is now known as cocreature |
| 11:14:20 | → | desantra joins (~skykanin@user/skykanin) |
| 11:21:34 | → | zincy_ joins (~zincy@2a00:23c8:970c:4801:350f:7ee:191a:6f65) |
| 11:22:48 | → | rond_ joins (~rond_@2a02:a31a:a23c:f480:2fd7:e087:5546:a438) |
| 11:23:02 | → | lavaman joins (~lavaman@98.38.249.169) |
| 11:23:27 | <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') |
| 11:24:43 | <joel135> | ah, after a night's sleep am beginning to understand this now. it is an astute observation |
| 11:25:46 | × | johnny_sitar quits (~artur@078088015209.bialystok.vectranet.pl) (Ping timeout: 260 seconds) |
| 11:27:08 | × | desantra quits (~skykanin@user/skykanin) (Quit: WeeChat 3.3) |
| 11:27:20 | → | desantra joins (~skykanin@user/skykanin) |
| 11:28:55 | × | lavaman quits (~lavaman@98.38.249.169) (Ping timeout: 256 seconds) |
| 11:31:16 | → | eggplantade joins (~Eggplanta@108-201-191-115.lightspeed.sntcca.sbcglobal.net) |
| 11:32:07 | <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. |
| 11:32:21 | × | zincy_ quits (~zincy@2a00:23c8:970c:4801:350f:7ee:191a:6f65) (Remote host closed the connection) |
| 11:35:43 | × | eggplantade quits (~Eggplanta@108-201-191-115.lightspeed.sntcca.sbcglobal.net) (Ping timeout: 256 seconds) |
| 11:36:37 | × | desantra quits (~skykanin@user/skykanin) (Quit: WeeChat 3.3) |
| 11:37:49 | → | desantra joins (~skykanin@user/skykanin) |
| 11:40:42 | → | chomwitt joins (~chomwitt@athedsl-32204.home.otenet.gr) |
| 11:42:25 | → | cosimone joins (~user@2001:b07:ae5:db26:c24a:d20:4d91:1e20) |
| 11:44:41 | × | madjestic quits (~madjestic@88-159-247-120.fixed.kpn.net) (Ping timeout: 245 seconds) |
| 11:48:09 | → | fendor joins (~fendor@91.141.74.77.wireless.dyn.drei.com) |
| 11:49:44 | → | DNH joins (~DNH@2a02:8108:1100:16d8:9554:7177:bc66:d82f) |
| 11:49:47 | × | DNH quits (~DNH@2a02:8108:1100:16d8:9554:7177:bc66:d82f) (Client Quit) |
| 11:50:41 | × | cosimone quits (~user@2001:b07:ae5:db26:c24a:d20:4d91:1e20) (Ping timeout: 268 seconds) |
| 11:52:18 | × | boxscape_ quits (~boxscape_@mue-88-130-59-018.dsl.tropolys.de) (Ping timeout: 260 seconds) |
| 11:59:16 | × | FinnElija quits (~finn_elij@user/finn-elija/x-0085643) (Remote host closed the connection) |
| 11:59:47 | → | FinnElija joins (~finn_elij@user/finn-elija/x-0085643) |
| 12:01:18 | <alzgh> | hello, I'm trying to rewrite `tupledMonad1` using bind notation `>>=`. Any help and hint is appreciated https://paste.tomsmeding.com/odkcLN80 |
| 12:01:31 | → | basti_ joins (~basti@ip-84-119-8-195.unity-media.net) |
| 12:02:05 | → | merijn joins (~merijn@83-160-49-249.ip.xs4all.nl) |
| 12:03:20 | → | tfeb joins (~tfb@88.98.95.237) |
| 12:04:34 | × | alx741 quits (~alx741@181.196.68.55) (Quit: alx741) |
| 12:05:13 | → | cosimone joins (~user@93-47-229-157.ip115.fastwebnet.it) |
| 12:07:42 | × | tfeb quits (~tfb@88.98.95.237) (Client Quit) |
| 12:08:01 | × | Gurkenglas quits (~Gurkengla@dslb-002-203-144-204.002.203.pools.vodafone-ip.de) (Ping timeout: 256 seconds) |
| 12:11:50 | → | fendor_ joins (~fendor@91.141.74.77.wireless.dyn.drei.com) |
| 12:11:51 | → | zincy_ joins (~zincy@2a00:23c8:970c:4801:350f:7ee:191a:6f65) |
| 12:12:36 | × | zincy_ quits (~zincy@2a00:23c8:970c:4801:350f:7ee:191a:6f65) (Remote host closed the connection) |
| 12:14:15 | × | fendor quits (~fendor@91.141.74.77.wireless.dyn.drei.com) (Ping timeout: 256 seconds) |
| 12:17:30 | fendor_ | is now known as fendor |
| 12:22:38 | <Pickchea> | Hey, is there a way to make the type checker accept this? \p q -> p q p |
| 12:24:24 | → | [itchyjunk] joins (~itchyjunk@user/itchyjunk/x-7353470) |
| 12:24:39 | <hpc> | wrap it in Fix maybe? |
| 12:25:54 | <hpc> | what type do you want p to have? |
| 12:26:00 | <ski> | joel135 : by ⌜f ↦ f + 5 d²f/dx²⌝, you mean ⌜f ↦ x ↦ f x + 5 ⋅ d² (f x) / (d x)²⌝ ? what's ⌜I⌝,⌜▫⌝ ? |
| 12:26:30 | <ski> | ("ah, after a night's sleep .." -- ok, good) |
| 12:27:45 | <joel135> | yes that is what i mean |
| 12:28:26 | <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 |
| 12:29:27 | → | jess joins (~jess@libera/staff/jess) |
| 12:30:41 | <joel135> | of type ℕ₄, I and _▫_ are just id and comp |
| 12:31:15 | <joel135> | of type ℕ₅, I and _▫_ are pure id and liftA2 comp |
| 12:31:23 | <joel135> | and so on |
| 12:31:24 | <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)) |
| 12:31:34 | × | shapr quits (~user@pool-100-36-247-68.washdc.fios.verizon.net) (Ping timeout: 260 seconds) |
| 12:32:22 | <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'. |
| 12:32:26 | <ski> | hm, so just continuing the pattern of successively (environment-)lifted identity and composition, ok |
| 12:32:52 | <ski> | (i still wonder about a "numerical" interpretation of them) |
| 12:34:03 | <ski> | Pickchea : what about `and a b p q = a (b p q) q' ? |
| 12:34:03 | <joel135> | I is to be that operator which given a polynomial returns that polynomial without modification |
| 12:34:05 | × | merijn quits (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 256 seconds) |
| 12:35:19 | <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 ℕ₄. |
| 12:35:45 | <ski> | "operator" here being an operator on polynomials, presumably generated from an "oracle"/indeterminate/unknown/variable/formal such operator ? |
| 12:35:56 | → | slowButPresent joins (~slowButPr@user/slowbutpresent) |
| 12:37:08 | <ski> | (i take that to mean ⌜p ↦ x ↦ p (x + n)⌝) |
| 12:37:37 | <Pickchea> | ski, what are you, some kind genius? :-D |
| 12:37:58 | <ski> | Pickchea : or, you could declare `type ChurchBool = forall o. o -> o -> o' (and enable `Rank2Types'), i think ? |
| 12:38:07 | → | jumper149 joins (~jumper149@80.240.31.34) |
| 12:38:46 | <ski> | (i think, using that, you may be able to get `and a b = a b a' to check) |
| 12:39:24 | <ski> | Pickchea : i was just talking, some hours ago, about Church numerals :) |
| 12:40:13 | <ski> | (oh, and obviously you'd need the type signature that you expect, on `and', for that to possibly work) |
| 12:43:44 | × | max22- quits (~maxime@lfbn-ren-1-762-224.w81-53.abo.wanadoo.fr) (Ping timeout: 268 seconds) |
| 12:44:34 | → | favonia joins (~favonia@user/favonia) |
| 12:45:37 | <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. |
| 12:45:47 | <Pickchea> | Seems complicated :-D |
| 12:46:17 | <hpc> | it's the same reason you can't write (\x -> x x) in simply typed lambda calculus |
| 12:47:48 | <hpc> | the unifier has to solve a = b -> a -> c |
| 12:47:59 | <hpc> | which is a = b -> (b -> (b -> (... |
| 12:48:02 | <hpc> | which is an infinite type |
| 12:49:32 | <Pickchea> | Yeah, I thought something like that! |
| 12:49:45 | → | unit73e joins (~emanuel@2001:818:e8dd:7c00:32b5:c2ff:fe6b:5291) |
| 12:50:10 | <Pickchea> | This point goes to Lisp I guess :-D |
| 12:51:44 | → | aleator joins (~aleator@178-55-117-52.bb.dnainternet.fi) |
| 12:52:09 | <ski> | Pickchea : did you try adding a type signature for `and' ? |
| 12:53:02 | <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 |
| 12:53:05 | <ski> | Pickchea : oh .. and if you want to play around with cyclic / "infinite" (/ equi-recursive) types, you could use `ocaml -rectypes' |
| 12:53:47 | <unit73e> | I don't know why aeson only has these super simple examples |
| 12:53:54 | <unit73e> | the best I found was this guy: https://artyom.me/aeson |
| 12:54:12 | <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 |
| 12:54:36 | <joel135> | the latter includes the translation operator from above, but presumably it doesn't include the differentiation operator |
| 12:55:02 | <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") |
| 12:55:57 | <ski> | joel135 : *nod*, interesting |
| 12:58:04 | <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) |
| 12:58:09 | <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. |
| 12:59:14 | <ski> | (hm, now i'm associating the above to minimal logic, and to the meta-distinction between derivable and admissible inference rules) |
| 13:01:04 | → | raehik joins (~raehik@cpc95906-rdng25-2-0-cust156.15-3.cable.virginm.net) |
| 13:01:05 | <ski> | joel135 : would this indeterminate operator that generates "operanomials" have any kind of "distribute" laws or something, wrt the other algebraic operations ? |
| 13:02:18 | × | aleator quits (~aleator@178-55-117-52.bb.dnainternet.fi) (Ping timeout: 260 seconds) |
| 13:02:27 | × | Alex_test quits (~al_test@94.233.241.187) (Quit: ;-) |
| 13:02:30 | × | AlexZenon quits (~alzenon@94.233.241.187) (Quit: ;-) |
| 13:02:59 | × | AlexNoo quits (~AlexNoo@94.233.241.187) (Quit: Leaving) |
| 13:03:53 | × | chomwitt quits (~chomwitt@athedsl-32204.home.otenet.gr) (Remote host closed the connection) |
| 13:03:57 | <Inst> | erm |
| 13:03:59 | <Inst> | looking for some help |
| 13:04:13 | <Inst> | in Haskell code, provided I'm running on a Windows system |
| 13:04:40 | <Inst> | how do I call the Windows API to create a default system "open file / save file" dialogue, then bind it to Haskell IO? |
| 13:05:00 | <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) |
| 13:05:50 | <joel135> | where *ₖ and *ₗ have the same type ℕₙ → ℕₙ → ℕₙ |
| 13:06:23 | <joel135> | generalized nullary/binary operators, i should say |
| 13:06:33 | <Pickchea> | ski, thanks! :-) |
| 13:06:34 | × | basti_ quits (~basti@ip-84-119-8-195.unity-media.net) (Ping timeout: 260 seconds) |
| 13:08:50 | <hpc> | Inst: there's a win32 package, and bindings to various ui toolkits |
| 13:09:16 | <Inst> | win32 package and bindings to various ui toolkits? |
| 13:09:25 | <Inst> | iirc there's a package to set up windows GUI, etc |
| 13:09:30 | <hpc> | yeah, one of those might have it |
| 13:09:40 | <Inst> | "might" |
| 13:09:41 | <Inst> | sigh |
| 13:09:48 | <hpc> | windows has so many random ways of doing things i don't know exactly what the api call for that dialogue is |
| 13:10:08 | × | jinsun quits (~quassel@user/jinsun) (Read error: Connection reset by peer) |
| 13:10:18 | <hpc> | worst case scenario, you get a gtk window instead of a native window |
| 13:10:28 | <hpc> | so that way is guaranteed to work with some effort |
| 13:10:40 | <hpc> | can't help more, myself :( |
| 13:13:19 | → | burnsidesLlama joins (~burnsides@dhcp168-023.wadham.ox.ac.uk) |
| 13:13:48 | × | zincy quits (~tom@2a00:23c8:970c:4801:e02d:7bbd:5337:7d58) (Remote host closed the connection) |
| 13:14:02 | <joel135> | ski: yes, these contemplations about "power" and "meta-inferences" seem relevant here |
| 13:16:34 | → | azimut_ joins (~azimut@gateway/tor-sasl/azimut) |
| 13:17:03 | <Inst> | can this handle it for me? |
| 13:17:04 | <Inst> | https://hackage.haskell.org/package/Win32 |
| 13:17:13 | <Inst> | it's a win32 api binding for windows |
| 13:18:02 | → | EvanR joins (~evan@2600:1700:ba69:10:75fc:f740:4c21:d03d) |
| 13:19:12 | <ski> | joel135 : hm, i see |
| 13:20:30 | × | azimut quits (~azimut@gateway/tor-sasl/azimut) (Ping timeout: 276 seconds) |
| 13:21:05 | → | AlexNoo joins (~AlexNoo@94.233.241.187) |
| 13:21:08 | → | AlexZenon joins (~alzenon@94.233.241.187) |
| 13:22:03 | → | jinsun joins (~quassel@user/jinsun) |
| 13:22:13 | <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)) |
| 13:22:29 | → | Alex_test joins (~al_test@94.233.241.187) |
| 13:25:10 | ski | . 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 ) |
| 13:26:47 | × | raehik quits (~raehik@cpc95906-rdng25-2-0-cust156.15-3.cable.virginm.net) (Ping timeout: 256 seconds) |
| 13:27:33 | <tomjaguarpaw> | How do I get Haddock to link to a constructor or pattern rather than a data type? |
| 13:28:12 | <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 ? |
| 13:29:29 | <tomjaguarpaw> | Ah, it's v'Foo' |
| 13:29:34 | × | rond_ quits (~rond_@2a02:a31a:a23c:f480:2fd7:e087:5546:a438) (Quit: Client closed) |
| 13:29:41 | <tomjaguarpaw> | https://github.com/haskell/haddock/issues/667 |
| 13:36:18 | → | max22- joins (~maxime@2a01cb08833598005d78e1cb2fc9f4a2.ipv6.abo.wanadoo.fr) |
| 13:40:28 | × | gehmehgeh quits (~user@user/gehmehgeh) (Quit: Leaving) |
| 13:40:31 | × | MidAutumnMoon quits (~MidAutumn@user/midautumnmoon) (Quit: Ping timeout (120 seconds)) |
| 13:40:44 | → | MidAutumnMoon joins (~MidAutumn@user/midautumnmoon) |
| 13:40:49 | → | johnny_sitar joins (~artur@078088015209.bialystok.vectranet.pl) |
| 13:41:42 | × | max22- quits (~maxime@2a01cb08833598005d78e1cb2fc9f4a2.ipv6.abo.wanadoo.fr) (Ping timeout: 268 seconds) |
| 13:48:52 | <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 :-\ |
| 13:49:31 | <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 |
| 13:49:40 | gentauro | I would <3 that somebody managed to make the `fancy` Apple hardware work on NixOS xD |
| 13:49:56 | → | raehik joins (~raehik@cpc95906-rdng25-2-0-cust156.15-3.cable.virginm.net) |
| 13:50:08 | <joel135> | also N[eps] := N[x]/(x^2) |
| 13:50:47 | <joel135> | for what o is this the same as the type (o -> o) -> (o -> o) ? trippy question |
| 13:52:47 | × | unit73e quits (~emanuel@2001:818:e8dd:7c00:32b5:c2ff:fe6b:5291) (Ping timeout: 268 seconds) |
| 13:56:38 | × | favonia quits (~favonia@user/favonia) (Remote host closed the connection) |
| 13:57:36 | → | favonia joins (~favonia@user/favonia) |
| 13:59:42 | <ski> | hmm |
| 14:04:27 | <tomjaguarpaw> | c |
| 14:08:08 | × | rembo10 quits (~rembo10@remulis.com) (Quit: ZNC 1.8.2 - https://znc.in) |
| 14:08:43 | → | machinedgod joins (~machinedg@24.105.81.50) |
| 14:09:11 | → | rembo10 joins (~rembo10@remulis.com) |
| 14:12:15 | → | pretty_dumm_guy joins (trottel@gateway/vpn/protonvpn/prettydummguy/x-88029655) |
| 14:14:55 | × | jumper149 quits (~jumper149@80.240.31.34) (Quit: WeeChat 3.3) |
| 14:20:52 | → | max22- joins (~maxime@2a01cb0883359800bbde3f2c88505b2a.ipv6.abo.wanadoo.fr) |
| 14:23:38 | × | gg quits (~gg@2a01:e0a:819:1510:89f0:97ca:21c4:6ea6) (Ping timeout: 268 seconds) |
| 14:27:32 | <Inst> | my problem is partially solved |
| 14:27:42 | <Inst> | turns out there's haskell libs binding to FLTK |
| 14:27:46 | <Inst> | FLTK has native window open close support |
| 14:28:04 | <Inst> | erm, support for opening native file open / save apps |
| 14:31:16 | → | merijn joins (~merijn@83-160-49-249.ip.xs4all.nl) |
| 14:31:24 | → | kspalaiologos joins (~kspalaiol@user/kspalaiologos) |
| 14:32:23 | × | hendursaga quits (~weechat@user/hendursaga) (Remote host closed the connection) |
| 14:33:05 | → | hendursaga joins (~weechat@user/hendursaga) |
| 14:33:30 | → | eggplantade joins (~Eggplanta@108-201-191-115.lightspeed.sntcca.sbcglobal.net) |
| 14:38:11 | × | eggplantade quits (~Eggplanta@108-201-191-115.lightspeed.sntcca.sbcglobal.net) (Ping timeout: 256 seconds) |
| 14:42:55 | → | __monty__ joins (~toonn@user/toonn) |
| 14:46:44 | × | burnsidesLlama quits (~burnsides@dhcp168-023.wadham.ox.ac.uk) (Remote host closed the connection) |
| 14:47:38 | → | acidjnk joins (~acidjnk@p200300d0c7263574f86fe22bbcd0fec5.dip0.t-ipconnect.de) |
| 14:49:20 | → | robertfry joins (~robertfry@cosh-19-b2-v4wan-161499-cust683.vm10.cable.virginm.net) |
| 14:53:45 | × | hendursaga quits (~weechat@user/hendursaga) (Remote host closed the connection) |
| 14:54:17 | → | hendursaga joins (~weechat@user/hendursaga) |
| 14:55:06 | × | TheCoffeMaker_ quits (~TheCoffeM@125-121-245-190.fibertel.com.ar) (Quit: So long and thanks for all the fish) |
| 14:57:03 | → | TheCoffeMaker joins (~TheCoffeM@user/thecoffemaker) |
| 14:57:54 | → | aqua0210 joins (~user@101.85.11.168) |
| 15:02:18 | → | hololeap_ joins (~hololeap@user/hololeap) |
| 15:02:33 | × | hololeap quits (~hololeap@user/hololeap) (Ping timeout: 276 seconds) |
| 15:03:56 | → | mrkrktsndctcrpt joins (~mrkrktsnd@50.228.44.6) |
| 15:05:23 | × | merijn quits (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 256 seconds) |
| 15:08:10 | → | basti_ joins (~basti@ip-84-119-8-195.unity-media.net) |
| 15:11:38 | <dsal> | gentauro: I run nix on macos |
| 15:12:05 | <dsal> | Not xmonad, though. I run that on nixos |
| 15:13:37 | <gentauro> | dsal: yeah, I run the `nix` (package manager) as well on the `macOS` |
| 15:13:50 | <gentauro> | but I would rather run `NixOS` on the Apple hardware ;) |
| 15:14:17 | → | TranquilEcho joins (~grom@user/tranquilecho) |
| 15:15:53 | <geekosaur> | xmonad's a bad fit for macos anyway, because of how its x11 emulation works |
| 15:16:10 | <geekosaur> | and you can't use xmonad to manage native windows |
| 15:16:35 | × | Pickchea quits (~private@user/pickchea) (Quit: Leaving) |
| 15:18:08 | <gentauro> | dsal: another `bad` thing about `nix` vs `NixOS`, is that you don't have a `stable` channel for packages |
| 15:18:32 | → | hiruji joins (~hiruji@user/hiruji) |
| 15:18:37 | <gentauro> | I mean, I tried to build an application on the `macOS` and the `llvm rc-compiler` is broken .. |
| 15:18:52 | <gentauro> | not very "optimal" for a "workstation" |
| 15:19:41 | <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. |
| 15:19:52 | <dsal> | That's not as much of an issue on nixos, though. |
| 15:21:59 | × | max22- quits (~maxime@2a01cb0883359800bbde3f2c88505b2a.ipv6.abo.wanadoo.fr) (Remote host closed the connection) |
| 15:23:16 | → | aman joins (~aman@user/aman) |
| 15:23:33 | × | random-jellyfish quits (~random-je@user/random-jellyfish) (Ping timeout: 256 seconds) |
| 15:24:23 | → | burnsidesLlama joins (~burnsides@dhcp168-023.wadham.ox.ac.uk) |
| 15:27:41 | <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? |
| 15:27:45 | × | acidjnk quits (~acidjnk@p200300d0c7263574f86fe22bbcd0fec5.dip0.t-ipconnect.de) (Ping timeout: 268 seconds) |
| 15:27:52 | <EvanR> | it's late 2021 does haskell have a decent way to make a global variable |
| 15:28:10 | gentauro | unless you want to go the "manual" / `homebrew` way which I don't want to |
| 15:28:27 | <geekosaur> | it probably never will |
| 15:28:35 | <hpc> | EvanR: does it have to be mutable? |
| 15:28:37 | <gentauro> | EvanR: there no concept of `variables` |
| 15:28:39 | <dsal> | gentauro: I have some... |
| 15:28:39 | <geekosaur> | isn't that kinda the point of fp? |
| 15:28:42 | <gentauro> | everything are `values` |
| 15:28:51 | × | burnsidesLlama quits (~burnsides@dhcp168-023.wadham.ox.ac.uk) (Ping timeout: 245 seconds) |
| 15:29:03 | <EvanR> | yeah I get it, but instead we have several shitty ways to do it xD |
| 15:29:18 | <gentauro> | dsal: I have setup `nix` + `home-manager` to handle "software". It's the closest I can get to `NixOS` … |
| 15:29:33 | <hpc> | to be fair, there's no good way to do global mutable state :P |
| 15:29:50 | <dsal> | Yeah, "global variables" is one of those engineering practices that people tend to strive for. |
| 15:30:07 | <geekosaur> | yeh, haskell just uncovers all the ugly cracks in the concept |
| 15:30:10 | <dsal> | gentauro: yep, that's how I do it |
| 15:30:13 | <gentauro> | main state = … |
| 15:30:23 | <gentauro> | EvanR: just pass it as a parameter on your main function? |
| 15:30:25 | <gentauro> | :P |
| 15:30:44 | <hpc> | main = newIORef >>= main' |
| 15:30:59 | <dsal> | EvanR: what would you do with a global variable if you had one? |
| 15:31:17 | → | max22- joins (~maxime@lfbn-ren-1-762-224.w81-53.abo.wanadoo.fr) |
| 15:31:23 | <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 |
| 15:31:39 | <gentauro> | dsal: read/update from many different threads to get inconsistent resutls :P |
| 15:31:56 | <[exa]> | EvanR: man they literally spent 30 years getting rid of global variables |
| 15:32:14 | <[exa]> | y u no appreciate |
| 15:32:15 | <EvanR> | also, global TVar was used in a game programming example (another area that haskell "is too good for" ? xD) |
| 15:33:12 | <EvanR> | specifically to hold handles to driver resources that are set once |
| 15:33:28 | <dsal> | Sure, I put TVars in Readers for programs. |
| 15:33:29 | <hpc> | game programming is one of the last places you want global state, funny enough |
| 15:33:36 | <hpc> | global player data? what about multiplayer |
| 15:33:42 | <EvanR> | yeah not that |
| 15:33:43 | <hpc> | global viewport data? what about virtual cameras |
| 15:33:49 | → | waleee joins (~waleee@2001:9b0:216:8200:d457:9189:7843:1dbd) |
| 15:34:00 | × | hiruji quits (~hiruji@user/hiruji) (Quit: ZNC 1.8.2 - https://znc.in) |
| 15:34:52 | → | shapr joins (~user@pool-100-36-247-68.washdc.fios.verizon.net) |
| 15:35:41 | <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 |
| 15:36:46 | × | kspalaiologos quits (~kspalaiol@user/kspalaiologos) (Ping timeout: 260 seconds) |
| 15:37:15 | <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. |
| 15:37:17 | <EvanR> | doing a monadic read each time you want to access it, in this case, would be silly |
| 15:38:10 | <hpc> | not that silly |
| 15:38:39 | <hpc> | you could read the value once and pass that as a parameter to everything instead |
| 15:38:48 | <hpc> | same way you can read a file and pass a great big ByteString around |
| 15:41:00 | <EvanR> | yeah that's a case when you imagine the data involved being an unknown and potentially visible to the code |
| 15:42:14 | <EvanR> | unlike handles to os resources, GL objects (numbers that one should not mess with) |
| 15:43:32 | <EvanR> | if your program requires a single opaque context or something, it could be convenient to refer to this directly without so much ceremony |
| 15:44:26 | <EvanR> | an example would be a web request handler script, the request is your life, and there's only one |
| 15:45:00 | <EvanR> | bad example I guess, since that data is not opaque nevermind |
| 15:45:56 | <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 |
| 15:46:00 | <hpc> | but then you have Very Fun Bugs |
| 15:46:08 | <EvanR> | exactly |
| 15:47:12 | hololeap_ | is now known as hololeap |
| 15:52:53 | <EvanR> | another difficulty is realistic programs with many modules, you would need some sort of bureacracy to understand who can see the global |
| 15:53:50 | → | fendor_ joins (~fendor@178.165.196.101.wireless.dyn.drei.com) |
| 15:54:26 | <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. |
| 15:54:35 | <EvanR> | also if its a library, how would libraries not collide on the name |
| 15:55:24 | <EvanR> | errno, great example of a terrible use for global variable |
| 15:55:30 | × | pretty_dumm_guy quits (trottel@gateway/vpn/protonvpn/prettydummguy/x-88029655) (Ping timeout: 260 seconds) |
| 15:55:47 | <monochrom> | Oh haha, name clash is solved by every library choosing a prefix and hoping that it's, um, universally unique :) |
| 15:56:22 | × | fendor quits (~fendor@91.141.74.77.wireless.dyn.drei.com) (Ping timeout: 260 seconds) |
| 16:02:00 | → | Gurkenglas joins (~Gurkengla@dslb-002-203-144-204.002.203.pools.vodafone-ip.de) |
| 16:02:22 | <hpc> | just do what ldap does and give everything an oid |
| 16:02:31 | <hpc> | instead of defining bitwise_and, define 1.2.840.113556.1.4.803 |
| 16:02:35 | <hpc> | easy |
| 16:03:12 | → | x6C697370 joins (~michael@2600:1700:7c02:3180::44) |
| 16:03:33 | → | pretty_dumm_guy joins (trottel@gateway/vpn/protonvpn/prettydummguy/x-88029655) |
| 16:03:42 | × | max22- quits (~maxime@lfbn-ren-1-762-224.w81-53.abo.wanadoo.fr) (Remote host closed the connection) |
| 16:03:59 | → | hiruji joins (~hiruji@user/hiruji) |
| 16:04:40 | → | max22- joins (~maxime@lfbn-ren-1-762-224.w81-53.abo.wanadoo.fr) |
| 16:05:08 | <Inst> | are there any haskellers using visual studio code? |
| 16:05:16 | <Inst> | I need to figure out how to install packages from hackage |
| 16:05:30 | <Inst> | https://hackage.haskell.org/package/fltkhs |
| 16:05:32 | → | gg joins (~gg@88.160.100.84) |
| 16:06:13 | fendor_ | is now known as fendor |
| 16:06:30 | <[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 |
| 16:06:57 | <Inst> | I got VSC specifically to avoid using cabal / stock |
| 16:06:57 | <maerwald> | Inst: https://cabal.readthedocs.io/en/latest/getting-started.html |
| 16:06:59 | <Inst> | stack |
| 16:07:02 | <Inst> | thanks |
| 16:07:28 | <geekosaur> | I don't think you'll be able to avoid using at least one of them |
| 16:09:20 | <hpc> | and if you use stack, you're still not getting away from using cabal too |
| 16:10:11 | <[exa]> | why avoid it though? |
| 16:11:17 | <Inst> | minimize challenge |
| 16:11:18 | <geekosaur> | avoiding both is a nice way to get yourself into nasty dependency jungles |
| 16:11:21 | <Inst> | ugh, i'm stuck with cabal, then |
| 16:11:33 | <geekosaur> | which is not minimizing challenge |
| 16:11:42 | <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. |
| 16:12:00 | × | hendursaga quits (~weechat@user/hendursaga) (Quit: hendursaga) |
| 16:12:01 | <[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 |
| 16:12:14 | <Inst> | thanks for the help |
| 16:12:25 | → | hendursaga joins (~weechat@user/hendursaga) |
| 16:12:35 | <Inst> | i'm trying to set up a hack to get Haskell to be able to call native Windows file open / save windows |
| 16:12:45 | <Inst> | I'm suspecting fltkhs might not be able to do it, though |
| 16:13:21 | <monochrom> | Consider https://hackage.haskell.org/package/Win32 |
| 16:13:49 | <monochrom> | or generally https://hackage.haskell.org/packages/search?terms=win32 |
| 16:13:57 | → | Sgeo joins (~Sgeo@user/sgeo) |
| 16:14:08 | × | [itchyjunk] quits (~itchyjunk@user/itchyjunk/x-7353470) (Read error: Connection reset by peer) |
| 16:14:23 | <[exa]> | the open/save dialogs are not a part of any C-style winapi right? |
| 16:14:55 | <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 |
| 16:15:46 | <EvanR> | bonus it will work on not windows too, as soon as you implement the other native front ends |
| 16:16:57 | <monochrom> | Write a webapp. Then there is only one native front end. >:) |
| 16:17:22 | <[exa]> | Inst: if fltk fails, consider making a small C program with this library https://github.com/mlabbe/nativefiledialog |
| 16:17:27 | <[exa]> | and calling it from haskell via FFI |
| 16:17:39 | <Inst> | thanks exa, you're a lifesaver |
| 16:18:13 | <Inst> | exa: how did the Instagram filters go? |
| 16:18:26 | × | aman quits (~aman@user/aman) (Ping timeout: 245 seconds) |
| 16:18:28 | <Inst> | I was also thinking: "use Haskell to strip DRM from obsolete CDs" |
| 16:18:45 | <Inst> | or "use Haskell, with or without the assistance of a finance export / prof, to do stock market analysis" |
| 16:18:50 | <Inst> | those are both practical and interesting |
| 16:18:51 | <[exa]> | it was kinda too specific, we went with something different at the end |
| 16:19:09 | <Inst> | as long as it works out |
| 16:19:19 | <[exa]> | too much time for tuning the filters and from haskell-side the assignment is not really challenging |
| 16:19:31 | <Inst> | the reason I need Haskell with a file open / shut hack is so I can try to teach my fellow non-programmer friend |
| 16:19:47 | <Inst> | Haskell with early IO |
| 16:20:19 | <EvanR> | define early IO |
| 16:21:21 | → | Lycurgus joins (~juan@98.4.112.204) |
| 16:22:27 | <Inst> | main = do -> random stuff in monad-land without explaining monads -> how2io -> typeclasses, expressions, recursion, lists, etc |
| 16:23:01 | × | aqua0210 quits (~user@101.85.11.168) (Ping timeout: 245 seconds) |
| 16:23:20 | <Inst> | i need to keep her engaged so she doesn't run off to Python |
| 16:23:24 | <Inst> | which she threatens to do |
| 16:23:33 | <EvanR> | oh yeah... sounds helpful to have some magic IO actions that just do stuff |
| 16:23:59 | <Inst> | "in media res" |
| 16:24:14 | <EvanR> | pickFile :: IO Filepath |
| 16:24:16 | <EvanR> | xD |
| 16:24:45 | <Inst> | you're being sarcastic, right? |
| 16:24:58 | <EvanR> | no? |
| 16:25:16 | <Inst> | thanks |
| 16:26:01 | × | desantra quits (~skykanin@user/skykanin) (Quit: WeeChat 3.3) |
| 16:26:11 | <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 |
| 16:26:16 | <Inst> | therefore, no running off to Pythonland |
| 16:26:28 | <Lycurgus> | geekosaur, you cheeky debbil i just realized you pm'ed me without notice was the thing to be suppressed so soto voce? |
| 16:26:51 | <Lycurgus> | and how is quietism gonna work? |
| 16:27:23 | <geekosaur> | mostly hoping the whole thing would blow over faster if not publicly restarted |
| 16:27:57 | <Lycurgus> | illogical to think doing nothing will cause the desired result |
| 16:28:12 | <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 |
| 16:28:25 | <Inst> | Lycurgus: you know what's the easiest way to kill someone? |
| 16:28:29 | <Lycurgus> | doing stuff behind the scenes, yeah |
| 16:28:43 | <Lycurgus> | Inst, no what? |
| 16:28:50 | <Inst> | eat doritos |
| 16:28:51 | <Inst> | drink beer |
| 16:28:55 | <Inst> | watch TV, go on with your everyday life |
| 16:29:04 | <EvanR> | yes the monad tutorial fallacy |
| 16:29:06 | <Inst> | eventually that someone will drop dead of hopefully natural causes |
| 16:29:12 | <Lycurgus> | i c |
| 16:29:18 | <Inst> | you're in their light cone |
| 16:29:25 | <Inst> | technically you're a causative actor in the most minimal way possible |
| 16:29:31 | × | max22- quits (~maxime@lfbn-ren-1-762-224.w81-53.abo.wanadoo.fr) (Remote host closed the connection) |
| 16:29:32 | <Inst> | so no, doing nothing is not illogical |
| 16:29:39 | <Lycurgus> | and the death will be attributed to covid prolly |
| 16:29:54 | <Inst> | 无为 |
| 16:30:06 | <EvanR> | Inst I think you're on the right track |
| 16:30:10 | <monochrom> | It is OK to learn and use IO without bringing up the monad generality. |
| 16:30:13 | × | lyxia quits (~lyxia@poisson.chat) (Quit: WeeChat 3.2) |
| 16:30:18 | <EvanR> | ^ |
| 16:30:27 | → | lyxia joins (~lyxia@poisson.chat) |
| 16:30:35 | <Inst> | whitington does something similar, i.e, he teaches how to use either, maybe, and io |
| 16:30:39 | <Inst> | without going into monads |
| 16:31:02 | <monochrom> | People have already learned and are using numbers without ring field generality. Heck most of them haven't even heard of Peano axioms. |
| 16:31:03 | <Inst> | he says it's for another book, but i feel sufficiently functional (small f) without it |
| 16:31:09 | <EvanR> | if they're a complete beginner, then they won't even want to get into monad memes with you |
| 16:31:18 | Lycurgus | abhors all mysticism and religion, taoism and quietism are no exceptions |
| 16:31:18 | <Inst> | I just feel hungry for burritos |
| 16:31:29 | <Inst> | Taoism -> philosophical and religious elements |
| 16:31:31 | <Inst> | but offtopic |
| 16:31:37 | → | yauhsien joins (~yauhsien@118-167-41-229.dynamic-ip.hinet.net) |
| 16:31:43 | → | burnsidesLlama joins (~burnsides@dhcp168-023.wadham.ox.ac.uk) |
| 16:31:44 | <maerwald> | best way to get into monads is to see what you can't do with applicative |
| 16:32:12 | <EvanR> | and applicative requires first explaining or demonstrating Functor, which is a lot more useful anyway xD |
| 16:32:34 | <Lycurgus> | or be super reductionist and say it's just a damn datastruce hs weenies use to get referential transparency |
| 16:32:35 | → | aqua0210 joins (~user@101.85.11.168) |
| 16:32:46 | <EvanR> | no don't |
| 16:32:51 | <monochrom> | That is false. |
| 16:32:53 | <Lycurgus> | *data structure |
| 16:33:08 | <Lycurgus> | yeah it's a lil more than just reductionist |
| 16:33:22 | <monochrom> | Unless you decide to classify the X->Y type as a data structure too. |
| 16:33:40 | <Lycurgus> | but only wrong by a detail |
| 16:34:18 | <EvanR> | since X->Y is a negative type, perhaps you could classify it as a negative data structure xD |
| 16:35:17 | → | eggplantade joins (~Eggplanta@108-201-191-115.lightspeed.sntcca.sbcglobal.net) |
| 16:35:21 | <maerwald> | what do monads have to do with referential transparency? |
| 16:35:41 | <hpc> | here's a fun math game: combine related concepts to create the most confused terminology possible |
| 16:35:51 | <hpc> | X is negative in X -> Y, but also X -> Y = Y ** X |
| 16:35:58 | <hpc> | so in exponentiation, the value on the right is negative |
| 16:36:24 | → | mrkrktsn1ctcrpt joins (~mrkrktsnd@50.228.44.6) |
| 16:36:30 | <hpc> | @let negate x = (** x) |
| 16:36:31 | <lambdabot> | Defined. |
| 16:37:25 | <geekosaur> | isn't that going to collide with Prelude negate? |
| 16:37:30 | <hpc> | :P |
| 16:38:53 | × | mrkrktsndctcrpt quits (~mrkrktsnd@50.228.44.6) (Ping timeout: 256 seconds) |
| 16:39:24 | <EvanR> | when two negates collide, the result is a positive |
| 16:39:46 | × | eggplantade quits (~Eggplanta@108-201-191-115.lightspeed.sntcca.sbcglobal.net) (Ping timeout: 260 seconds) |
| 16:43:59 | × | mrkrktsn1ctcrpt quits (~mrkrktsnd@50.228.44.6) (Ping timeout: 256 seconds) |
| 16:46:08 | → | tfeb joins (~tfb@88.98.95.237) |
| 16:48:05 | <xerox> | > negate it |
| 16:48:07 | <lambdabot> | error: |
| 16:48:07 | <lambdabot> | • Variable not in scope: it |
| 16:48:07 | <lambdabot> | • Perhaps you meant one of these: |
| 16:49:32 | <Lycurgus> | lambdabot doesn't have prelude? |
| 16:50:00 | <Lycurgus> | or the same error processing as ghci igess |
| 16:51:21 | × | zaquest quits (~notzaques@5.128.210.178) (Quit: Leaving) |
| 16:53:26 | × | bitdex quits (~bitdex@gateway/tor-sasl/bitdex) (Remote host closed the connection) |
| 16:54:41 | → | whatsupdoc joins (uid509081@id-509081.hampstead.irccloud.com) |
| 16:54:58 | → | bitdex joins (~bitdex@gateway/tor-sasl/bitdex) |
| 16:55:46 | → | zaquest joins (~notzaques@5.128.210.178) |
| 16:56:12 | × | fendor quits (~fendor@178.165.196.101.wireless.dyn.drei.com) (Remote host closed the connection) |
| 16:58:27 | → | merijn joins (~merijn@83-160-49-249.ip.xs4all.nl) |
| 17:00:05 | × | Lord_of_Life quits (~Lord@user/lord-of-life/x-2819915) (Excess Flood) |
| 17:00:48 | → | fendor joins (~fendor@178.165.196.101.wireless.dyn.drei.com) |
| 17:00:54 | × | pavonia quits (~user@user/siracusa) (Quit: Bye!) |
| 17:01:26 | → | Lord_of_Life joins (~Lord@user/lord-of-life/x-2819915) |
| 17:04:49 | × | tfeb quits (~tfb@88.98.95.237) (Quit: died) |
| 17:05:11 | × | merijn quits (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 264 seconds) |
| 17:07:28 | → | mrkrktsndctcrpt joins (~mrkrktsnd@mobile-166-171-248-94.mycingular.net) |
| 17:11:46 | <geekosaur> | Lycurgus, it's not ghci, no. it used to expose a variable that worked not quite like "it" but it got abused |
| 17:12:45 | <hpc> | yahb is ghci |
| 17:12:47 | <hpc> | % it |
| 17:12:48 | <yahb> | hpc: () |
| 17:13:09 | <hpc> | you even get to execute IO |
| 17:13:56 | → | mastarija joins (~mastarija@2a05:4f46:e06:ff00:18c4:3126:ef80:d743) |
| 17:16:30 | × | burnsidesLlama quits (~burnsides@dhcp168-023.wadham.ox.ac.uk) (Remote host closed the connection) |
| 17:16:52 | <Lycurgus> | % negate it |
| 17:16:52 | <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 |
| 17:17:18 | <Lycurgus> | whatever repl i have stacked suggests id from prelude |
| 17:18:14 | <Lycurgus> | 'foolish consistency is the hobgoblin of small minds' |
| 17:20:34 | → | v01d4lph4 joins (~v01d4lph4@122.177.85.95) |
| 17:20:34 | × | v01d4lph4 quits (~v01d4lph4@122.177.85.95) (Changing host) |
| 17:20:34 | → | v01d4lph4 joins (~v01d4lph4@user/v01d4lph4) |
| 17:20:42 | → | max22- joins (~maxime@lfbn-ren-1-762-224.w81-53.abo.wanadoo.fr) |
| 17:20:46 | <hpc> | i prefer consistent foolishness |
| 17:21:18 | <monochrom> | I don't see a foolish consistency there. |
| 17:21:24 | <monochrom> | Foolish spell-checking, maybe. |
| 17:22:18 | <Lycurgus> | no here it would be a foolish expectation of consistency |
| 17:22:37 | → | aleator joins (~aleator@87-93-222-114.bb.dnainternet.fi) |
| 17:23:10 | × | aqua0210 quits (~user@101.85.11.168) (Ping timeout: 260 seconds) |
| 17:23:23 | → | econo joins (uid147250@user/econo) |
| 17:23:33 | <monochrom> | I guess I have a foolish expectation of accurate wording, too. |
| 17:24:31 | <monochrom> | Now Inst is going to breathe "the accuracy that can be accurated is not the real accuracy" down my throat :) |
| 17:24:48 | <Inst> | um, what, it's just noumenon vs phenomenon |
| 17:25:06 | <Inst> | we try to get as close as we can to the actual reality, but the actual reality is unreachable |
| 17:25:30 | <Inst> | good enough, back to work, have a beer after you're done |
| 17:25:32 | × | v01d4lph4 quits (~v01d4lph4@user/v01d4lph4) (Ping timeout: 268 seconds) |
| 17:25:34 | <Inst> | don't be a pedant |
| 17:25:42 | → | fuzzypixelz joins (~fuzzypixe@eth-west-pareq2-46-193-4-100.wb.wifirst.net) |
| 17:26:38 | → | lavaman joins (~lavaman@98.38.249.169) |
| 17:28:10 | <Lycurgus> | copilot suggests "= "/" ++ it |
| 17:28:42 | <Lycurgus> | " |
| 17:30:31 | → | burnsidesLlama joins (~burnsides@dhcp168-023.wadham.ox.ac.uk) |
| 17:31:06 | × | lavaman quits (~lavaman@98.38.249.169) (Ping timeout: 260 seconds) |
| 17:31:34 | → | tzh joins (~tzh@c-24-21-73-154.hsd1.wa.comcast.net) |
| 17:32:05 | × | robertfry quits (~robertfry@cosh-19-b2-v4wan-161499-cust683.vm10.cable.virginm.net) (Quit: Konversation terminated!) |
| 17:32:34 | × | mrkrktsndctcrpt quits (~mrkrktsnd@mobile-166-171-248-94.mycingular.net) (Ping timeout: 260 seconds) |
| 17:33:27 | × | ulvarrefr quits (~user@185.24.53.152) (Read error: Connection reset by peer) |
| 17:33:34 | → | ulvarrefr joins (~user@185.24.53.152) |
| 17:35:51 | → | merijn joins (~merijn@83-160-49-249.ip.xs4all.nl) |
| 17:38:19 | × | aleator quits (~aleator@87-93-222-114.bb.dnainternet.fi) (Ping timeout: 260 seconds) |
| 17:40:09 | → | random-jellyfish joins (~random-je@user/random-jellyfish) |
| 17:40:58 | × | merijn quits (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 268 seconds) |
| 17:43:05 | × | Lycurgus quits (~juan@98.4.112.204) (Quit: Exeunt) |
| 17:43:36 | → | Pickchea joins (~private@user/pickchea) |
| 17:45:23 | × | hiruji quits (~hiruji@user/hiruji) (Ping timeout: 264 seconds) |
| 17:48:30 | × | hgolden quits (~hgolden2@cpe-172-114-81-123.socal.res.rr.com) (Remote host closed the connection) |
| 17:48:53 | → | aqua0210 joins (~user@101.85.11.168) |
| 17:49:48 | → | hgolden joins (~hgolden2@cpe-172-114-81-123.socal.res.rr.com) |
| 17:50:13 | → | Guest|10 joins (~Guest|10@70-36-136-248.dsl.dynamic.fusionbroadband.com) |
| 17:51:05 | × | Guest|10 quits (~Guest|10@70-36-136-248.dsl.dynamic.fusionbroadband.com) (Client Quit) |
| 17:51:15 | → | hiruji joins (~hiruji@user/hiruji) |
| 17:54:15 | × | aqua0210 quits (~user@101.85.11.168) (Ping timeout: 256 seconds) |
| 17:55:57 | × | hiruji quits (~hiruji@user/hiruji) (Ping timeout: 256 seconds) |
| 17:59:00 | → | eggplantade joins (~Eggplanta@108-201-191-115.lightspeed.sntcca.sbcglobal.net) |
| 17:59:07 | <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 |
| 18:01:40 | × | random-jellyfish quits (~random-je@user/random-jellyfish) (Ping timeout: 256 seconds) |
| 18:05:14 | → | aqua0210 joins (~user@101.85.11.168) |
| 18:06:27 | × | jess quits (~jess@libera/staff/jess) () |
| 18:09:43 | → | ees joins (~user@pool-108-18-30-46.washdc.fios.verizon.net) |
| 18:11:47 | × | aqua0210 quits (~user@101.85.11.168) (Ping timeout: 268 seconds) |
| 18:13:18 | → | merijn joins (~merijn@83-160-49-249.ip.xs4all.nl) |
| 18:13:35 | × | ees quits (~user@pool-108-18-30-46.washdc.fios.verizon.net) (Read error: Connection reset by peer) |
| 18:14:40 | → | ees joins (~user@pool-108-18-30-46.washdc.fios.verizon.net) |
| 18:23:28 | × | msmhnd^ quits (~msmhnd@h50.174.139.63.static.ip.windstream.net) (Remote host closed the connection) |
| 18:24:43 | → | aqua0210 joins (~user@101.85.11.168) |
| 18:30:06 | × | aqua0210 quits (~user@101.85.11.168) (Ping timeout: 245 seconds) |
| 18:34:19 | × | eggplantade quits (~Eggplanta@108-201-191-115.lightspeed.sntcca.sbcglobal.net) (Remote host closed the connection) |
| 18:36:24 | × | hololeap quits (~hololeap@user/hololeap) (Ping timeout: 276 seconds) |
| 18:36:48 | → | hololeap joins (~hololeap@user/hololeap) |
| 18:38:02 | × | yauhsien quits (~yauhsien@118-167-41-229.dynamic-ip.hinet.net) (Remote host closed the connection) |
| 18:38:39 | → | yauhsien joins (~yauhsien@118-167-41-229.dynamic-ip.hinet.net) |
| 18:40:14 | × | burnsidesLlama quits (~burnsides@dhcp168-023.wadham.ox.ac.uk) (Remote host closed the connection) |
| 18:41:18 | → | justsomeguy joins (~justsomeg@user/justsomeguy) |
| 18:42:01 | → | kawzeg joins (kawzeg@2a01:7e01::f03c:92ff:fee2:ec34) |
| 18:43:02 | → | aqua0210 joins (~user@101.85.11.168) |
| 18:44:40 | → | hiruji joins (~hiruji@user/hiruji) |
| 18:46:10 | <hololeap> | anyone know of a library for normalizing inequalities? |
| 18:46:30 | <awpr> | type-level Nat inequalities? |
| 18:46:43 | <hololeap> | no, just any Ord |
| 18:47:31 | × | merijn quits (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 256 seconds) |
| 18:47:52 | <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] |
| 18:48:09 | → | eruditass joins (uid248673@id-248673.uxbridge.irccloud.com) |
| 18:48:10 | × | aqua0210 quits (~user@101.85.11.168) (Ping timeout: 260 seconds) |
| 18:48:33 | <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 |
| 18:49:33 | × | yauhsien quits (~yauhsien@118-167-41-229.dynamic-ip.hinet.net) (Remote host closed the connection) |
| 18:50:05 | → | yauhsien joins (~yauhsien@118-167-41-229.dynamic-ip.hinet.net) |
| 18:52:00 | ← | ees parts (~user@pool-108-18-30-46.washdc.fios.verizon.net) (ERC 5.4 (IRC client for GNU Emacs 28.0.60)) |
| 18:52:42 | → | ees joins (~ees@pool-108-18-30-46.washdc.fios.verizon.net) |
| 18:54:42 | <hololeap> | this doesn't really match what I'm asking for, but seems interesting: https://hackage.haskell.org/package/speculate |
| 18:55:10 | × | dsrt^ quits (~dsrt@h50.174.139.63.static.ip.windstream.net) (Ping timeout: 260 seconds) |
| 18:57:34 | <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. |
| 18:58:31 | → | chisui joins (~chisui@dyndsl-095-033-149-191.ewe-ip-backbone.de) |
| 18:58:38 | <EvanR> | so you want to merge all the half open intervals to get a two sided interval, but also track the difference between < and <= |
| 18:58:41 | <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 |
| 19:00:02 | <EvanR> | if it's integers you could simplify to only <='s |
| 19:00:12 | <geekosaur> | and then translate back to comparisons |
| 19:00:46 | ← | ees parts (~ees@pool-108-18-30-46.washdc.fios.verizon.net) (Killed buffer) |
| 19:01:20 | × | chisui quits (~chisui@dyndsl-095-033-149-191.ewe-ip-backbone.de) (Client Quit) |
| 19:01:28 | <hololeap> | ok |
| 19:02:37 | <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 |
| 19:03:07 | × | kawzeg quits (kawzeg@2a01:7e01::f03c:92ff:fee2:ec34) (Quit: WeeChat 3.3) |
| 19:03:55 | <hololeap> | but that makes sense, smallest bounding interval |
| 19:05:27 | → | kawzeg joins (kawzeg@2a01:7e01::f03c:92ff:fee2:ec34) |
| 19:07:14 | <hololeap> | hm, I might also want to normalize versions, for instance 5.0.0 = 5 (for this purpose) |
| 19:08:09 | × | yauhsien quits (~yauhsien@118-167-41-229.dynamic-ip.hinet.net) (Remote host closed the connection) |
| 19:08:14 | <geekosaur> | that might not work so well in the presence of a version like 5.0.12 |
| 19:08:42 | → | yauhsien joins (~yauhsien@118-167-41-229.dynamic-ip.hinet.net) |
| 19:09:15 | <hololeap> | this is going to be for normalizing version range dependencies |
| 19:09:23 | <hololeap> | so >5.0.0 = >5 |
| 19:09:32 | → | ees joins (~user@pool-108-18-30-46.washdc.fios.verizon.net) |
| 19:10:32 | <hololeap> | >5.0.12 /= >5 |
| 19:10:49 | → | neurocyte0132889 joins (~neurocyte@45.10.61.172) |
| 19:10:49 | × | neurocyte0132889 quits (~neurocyte@45.10.61.172) (Changing host) |
| 19:10:49 | → | neurocyte0132889 joins (~neurocyte@user/neurocyte) |
| 19:13:47 | → | zzz joins (~z@user/zero) |
| 19:13:50 | × | yauhsien quits (~yauhsien@118-167-41-229.dynamic-ip.hinet.net) (Ping timeout: 260 seconds) |
| 19:15:35 | → | eggplantade joins (~Eggplanta@108-201-191-115.lightspeed.sntcca.sbcglobal.net) |
| 19:15:48 | → | mrkrktsndctcrpt joins (~mrkrktsnd@c-24-6-12-87.hsd1.ca.comcast.net) |
| 19:17:53 | → | lavaman joins (~lavaman@98.38.249.169) |
| 19:20:34 | → | burnsidesLlama joins (~burnsides@dhcp168-023.wadham.ox.ac.uk) |
| 19:21:04 | × | whatsupdoc quits (uid509081@id-509081.hampstead.irccloud.com) (Quit: Connection closed for inactivity) |
| 19:24:23 | <zzz> | @def newtype N = N Int |
| 19:24:24 | <lambdabot> | Defined. |
| 19:24:29 | <zzz> | @def sup (N x) = ("sup",x) |
| 19:24:30 | <lambdabot> | Defined. |
| 19:24:34 | <zzz> | > fst $ sup undefined |
| 19:24:35 | <lambdabot> | "sup" |
| 19:25:10 | <zzz> | this patternmatches because the newtype "doesn't really exist" right? |
| 19:25:37 | <dolio> | Something like that. |
| 19:26:54 | × | burnsidesLlama quits (~burnsides@dhcp168-023.wadham.ox.ac.uk) (Ping timeout: 260 seconds) |
| 19:27:03 | <zzz> | somehow i feel like there's something more to say |
| 19:27:09 | <tomjaguarpaw> | zzz: No, why? If you defined it as data you'd get the same behaviour |
| 19:27:28 | <dolio> | No, with data you'd get undefined. |
| 19:27:46 | <hololeap> | "sup" is a literal so it doesn't need the value of x |
| 19:27:47 | <tomjaguarpaw> | Oh yes, so you would |
| 19:28:28 | <dolio> | You can also imagine that ~ is the default mode for newtype patterns. |
| 19:28:30 | <tomjaguarpaw> | Right, so the N pattern doesn't actually force anything whereas the D pattern would |
| 19:29:08 | <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. |
| 19:30:02 | <zzz> | right |
| 19:30:44 | <dolio> | zzz: Sometimes you can observe incidental consequences of wrapping things in a newtype. |
| 19:31:09 | <dolio> | Like, if you have polymorphic stuff in a newtype, it might cause an eta expansion that makes something non-bottom. |
| 19:31:35 | × | zmt00 quits (~zmt00@user/zmt00) (Ping timeout: 264 seconds) |
| 19:31:38 | <zzz> | can you provide an example of that? |
| 19:31:46 | <dolio> | No, I don't remember an example. :) |
| 19:32:44 | <hololeap> | I don't understand either, dolio |
| 19:32:57 | × | max22- quits (~maxime@lfbn-ren-1-762-224.w81-53.abo.wanadoo.fr) (Remote host closed the connection) |
| 19:33:45 | → | zmt00 joins (~zmt00@user/zmt00) |
| 19:34:42 | → | aqua0210 joins (~user@101.85.11.168) |
| 19:35:06 | <c_wraith> | @let newtype F = F (forall f. Functor f => () -> f ()) |
| 19:35:07 | <lambdabot> | Defined. |
| 19:35:10 | <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`. |
| 19:35:15 | <c_wraith> | > seq (F undefined) () |
| 19:35:16 | <lambdabot> | () |
| 19:35:22 | <c_wraith> | just like that |
| 19:35:26 | <dolio> | Oh, nice. |
| 19:35:37 | × | FragByte quits (~christian@user/fragbyte) (Quit: Quit) |
| 19:36:03 | → | max22- joins (~maxime@2a01cb0883359800ab19ff1ba7c64c00.ipv6.abo.wanadoo.fr) |
| 19:36:05 | <tomjaguarpaw> | Interesting |
| 19:36:09 | <c_wraith> | and yeah, that's eta expansion biting |
| 19:36:36 | <dolio> | Yeah, the newtype still 'doesn't exist', but the generality of the type it corresponds to might have semantic consequences. |
| 19:37:10 | <dolio> | And might force generalizing something that wouldn't otherwise be generalized. |
| 19:37:24 | → | FragByte joins (~christian@user/fragbyte) |
| 19:37:33 | <c_wraith> | It requires the class constraint |
| 19:37:47 | <c_wraith> | So it has something to do with dictionary passing in the internal representation |
| 19:37:52 | <tomjaguarpaw> | newtype F = F (forall f. f ()) shows the same behaviour |
| 19:37:54 | <hololeap> | what _should_ happen in that example, c_wraith? |
| 19:38:08 | <tomjaguarpaw> | Err sorry, I mean newtype F = F (forall f. Functor f => f ()) |
| 19:38:08 | <c_wraith> | tomjaguarpaw: huh, not for me. ghc 9.2.1 on my side |
| 19:38:26 | <c_wraith> | tomjaguarpaw: wait, no. That's not a function, so it doesn't get eta expanded. |
| 19:38:36 | <c_wraith> | I tested with (forall f. () -> f ()) |
| 19:38:47 | <c_wraith> | that gives an exception |
| 19:38:58 | <tomjaguarpaw> | Not sure if you've seen my correction |
| 19:39:01 | <c_wraith> | ah, right. |
| 19:39:11 | <c_wraith> | definitely has to do with the dictionary-passing in core |
| 19:39:14 | <tomjaguarpaw> | and indeed newtype F = F (forall a. Num a => a) |
| 19:39:16 | <tomjaguarpaw> | Yes I agree |
| 19:39:19 | <c_wraith> | that must cause eta expansion |
| 19:39:32 | <c_wraith> | hololeap: naively, you'd expect to get an exception from evaluating undefined |
| 19:39:59 | × | aqua0210 quits (~user@101.85.11.168) (Ping timeout: 268 seconds) |
| 19:40:09 | <hololeap> | so the compiler has no idea that (forall f. Functor f => () -> f ()) doesn't make sense |
| 19:40:53 | <c_wraith> | nope. that's irrelevant |
| 19:40:57 | <hololeap> | I suppose it wouldn't, since that's a result of what Functor means semantically, vs Applicative |
| 19:42:08 | <hololeap> | e.g. there is no pure defined for Functor, so no function could satisfy that type, unless it was also an Applicative |
| 19:42:19 | <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) . |
| 19:42:22 | → | zmt01 joins (~zmt00@user/zmt00) |
| 19:43:30 | <c_wraith> | huh. I didn't expect that. |
| 19:43:31 | → | burnsidesLlama joins (~burnsides@dhcp168-023.wadham.ox.ac.uk) |
| 19:44:27 | <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 |
| 19:44:50 | <hpc> | what if there isn't a class constraint? |
| 19:44:53 | <c_wraith> | that doesn't explain the last thing tomjaguarpaw mentioned. At least, not completely |
| 19:44:59 | <awpr> | yeah, getting to that |
| 19:45:31 | × | zmt00 quits (~zmt00@user/zmt00) (Ping timeout: 245 seconds) |
| 19:45:31 | <awpr> | GHC wouldn't instantiate `F` impredicatively, so the former one is just `F a` for some `a`, and not constrained |
| 19:45:47 | <awpr> | probably defaults it to `Integer` |
| 19:46:15 | <awpr> | in the latter, the contents of the newtype are actually a type with a constraint, no need to infer impredicativity |
| 19:46:57 | <hololeap> | what was the library that was termed "a better ListT" |
| 19:47:03 | <tomjaguarpaw> | streaming? |
| 19:47:03 | <geekosaur> | logict? |
| 19:47:11 | × | zmt01 quits (~zmt00@user/zmt00) (Ping timeout: 245 seconds) |
| 19:47:17 | <hololeap> | logict |
| 19:47:45 | <[exa]> | परोलोग |
| 19:48:06 | <[exa]> | whoops what happened there. I wanted to write "prolog". |
| 19:48:33 | <hololeap> | sanskrit? |
| 19:48:36 | × | burnsidesLlama quits (~burnsides@dhcp168-023.wadham.ox.ac.uk) (Ping timeout: 268 seconds) |
| 19:49:08 | → | zmt00 joins (~zmt00@user/zmt00) |
| 19:51:06 | × | ees quits (~user@pool-108-18-30-46.washdc.fios.verizon.net) (Ping timeout: 260 seconds) |
| 19:53:07 | × | eggplantade quits (~Eggplanta@108-201-191-115.lightspeed.sntcca.sbcglobal.net) (Remote host closed the connection) |
| 19:53:27 | → | gehmehgeh joins (~user@user/gehmehgeh) |
| 19:53:49 | → | euandreh joins (~euandreh@2804:14c:65c9:5161:4d0f:6b02:d329:b5d2) |
| 19:56:24 | → | Codaraxis joins (~Codaraxis@user/codaraxis) |
| 19:56:46 | → | yauhsien joins (~yauhsien@118-167-41-229.dynamic-ip.hinet.net) |
| 19:58:00 | <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 |
| 19:58:19 | <hololeap> | so this looks like a depth-first search with backtracking. how can I use logict here? |
| 19:58:38 | × | pgib quits (~textual@173.38.117.89) (Ping timeout: 260 seconds) |
| 19:58:55 | <dolio> | If you just use it normally like a list, it'll be depth-first. |
| 19:59:17 | × | LiaoTao quits (~LiaoTao@gateway/tor-sasl/liaotao) (Quit: ZNC 1.8.2 - https://znc.in) |
| 19:59:30 | <dolio> | For the same reason that list is depth first. LogicT is essentially an encoded list. |
| 19:59:35 | <hololeap> | I haven't ever used it, normally or not, because I haven't had a use-case since I discovered it |
| 19:59:41 | → | LiaoTao joins (~LiaoTao@gateway/tor-sasl/liaotao) |
| 20:00:16 | <dolio> | The only way it'll do things out of order is if you use the additional combinators in the package, like `interleave` or >>-. |
| 20:00:52 | <dolio> | What I mean is that if you use it the way you'd use list monad stuff for DFS. |
| 20:01:11 | × | yauhsien quits (~yauhsien@118-167-41-229.dynamic-ip.hinet.net) (Ping timeout: 256 seconds) |
| 20:01:28 | <hololeap> | ok, so what I don't understand is what is how it is used for "backtracking" |
| 20:02:03 | <hololeap> | s/is what is how/is how/ |
| 20:02:54 | <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. |
| 20:03:25 | × | hendursaga quits (~weechat@user/hendursaga) (Remote host closed the connection) |
| 20:03:48 | → | hendursaga joins (~weechat@user/hendursaga) |
| 20:04:02 | <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 |
| 20:05:10 | × | juhp quits (~juhp@128.106.188.220) (Ping timeout: 260 seconds) |
| 20:05:15 | <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? |
| 20:05:20 | → | retro_ joins (~retro@2e41e9c8.skybroadband.com) |
| 20:05:26 | <geekosaur> | mhh, if logs were still running I'd point you to ski's discussion last night my time |
| 20:05:57 | <geekosaur> | you don't need to do caching, the list monad (or, here, LogicT) does it automatically |
| 20:06:44 | → | juhp joins (~juhp@128.106.188.220) |
| 20:07:00 | × | harveypwca quits (~harveypwc@2601:246:c180:a570:3828:d8:e523:3f67) (Quit: Leaving) |
| 20:07:11 | <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. |
| 20:07:20 | → | mrkrktsn1ctcrpt joins (~mrkrktsnd@c-24-6-12-87.hsd1.ca.comcast.net) |
| 20:07:31 | <dolio> | Becasue there will be 0 results from that branch, so to get any result, you must use another branch. |
| 20:08:32 | <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. |
| 20:08:57 | × | retroid_ quits (~retro@2e41e9c8.skybroadband.com) (Ping timeout: 268 seconds) |
| 20:09:18 | <hololeap> | ok, so we're specifically talking about the list monad, ([a] -> (a -> [b]) -> [b]), here? |
| 20:09:47 | <dolio> | That and LogicT both work essentially the same way. |
| 20:10:12 | <dolio> | Except LogicT uses a better behaved implementation for certain uses. |
| 20:10:21 | <hololeap> | so when the function `f :: a -> [b]` returns [], it naturally falls back to the previous element? |
| 20:10:50 | → | [itchyjunk] joins (~itchyjunk@user/itchyjunk/x-7353470) |
| 20:11:06 | <hololeap> | because something else after it is still looking for a `b`? |
| 20:11:45 | <dolio> | Right, because it's concatMap. [1,2,3] >>= f = f 1 ++ f 2 ++ f 3. |
| 20:11:48 | → | LiaoTao_ joins (~LiaoTao@gateway/tor-sasl/liaotao) |
| 20:12:15 | <geekosaur> | "backtracking" is actually a mischaracterization. it produces all possible values, but it does so lazily at all levels, so it *looks* like backtracking |
| 20:12:17 | <hololeap> | I'm still lost on how any of this is backtracking |
| 20:12:31 | <hololeap> | oh |
| 20:13:15 | <dolio> | Yeah, lazy evaluation makes lists act like backtracking computationally. |
| 20:13:15 | × | LiaoTao quits (~LiaoTao@gateway/tor-sasl/liaotao) (Ping timeout: 276 seconds) |
| 20:13:21 | <dolio> | LogicT does it with continuation passing. |
| 20:13:26 | <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 |
| 20:13:41 | LiaoTao_ | is now known as LiaoTao |
| 20:14:00 | <ski> | geekosaur : what's the difference ? |
| 20:15:22 | → | wootehfoot joins (~wootehfoo@user/wootehfoot) |
| 20:15:31 | <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 |
| 20:15:50 | → | burnsidesLlama joins (~burnsides@dhcp168-023.wadham.ox.ac.uk) |
| 20:16:07 | <geekosaur> | and laziness means if you ask for only one result, it'll just stop and discard the whole computation after producing it |
| 20:16:16 | <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 |
| 20:18:36 | <geekosaur> | I could see this as different from backtracking, or as a "laziness implementation" of backtracking, or as semantic fiddling to no point |
| 20:19:19 | × | lavaman quits (~lavaman@98.38.249.169) (Ping timeout: 256 seconds) |
| 20:21:15 | → | pavonia joins (~user@user/siracusa) |
| 20:22:01 | <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 |
| 20:22:59 | <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 |
| 20:23:29 | <geekosaur> | yeh, but I think a "conventional" view of backtracking expects that some information is propagated backwards to resume the previous level |
| 20:23:43 | <geekosaur> | whereas here it's just the natural behavior of a lazy list |
| 20:24:50 | <dolio> | Prolog does something better than depth-first backtracking search, right? |
| 20:26:41 | <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. |
| 20:30:10 | × | favonia quits (~favonia@user/favonia) (Quit: Leaving) |
| 20:31:18 | × | mei3 quits (~mei@user/mei) (Ping timeout: 260 seconds) |
| 20:32:42 | × | pretty_dumm_guy quits (trottel@gateway/vpn/protonvpn/prettydummguy/x-88029655) (Ping timeout: 260 seconds) |
| 20:34:34 | <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) |
| 20:35:06 | <ski> | geekosaur : what kind of information ? |
| 20:35:29 | → | aqua0210 joins (~user@101.85.11.168) |
| 20:36:42 | <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 |
| 20:37:47 | <dolio> | Oh, I meant that I thought it was typical for some 'better' strategy than depth first to be used. |
| 20:38:09 | <dolio> | But I'm not that well read on implementing Prolog. |
| 20:38:26 | <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) |
| 20:38:51 | <ski> | no, i think normally plain depth-first is what is used |
| 20:39:05 | <dolio> | Oh, huh. |
| 20:39:16 | <ski> | one reason is that people sometimes depend on the specific ordering that they get with the naïve depth-first |
| 20:39:50 | <ski> | and so implementations don't want to mess with that, unasked, in ways that's not obvious |
| 20:40:35 | × | aqua0210 quits (~user@101.85.11.168) (Ping timeout: 264 seconds) |
| 20:43:12 | <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) |
| 20:44:03 | → | merijn joins (~merijn@83-160-49-249.ip.xs4all.nl) |
| 20:45:51 | <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. |
| 20:46:13 | <ski> | > [[x,y] | x <- "ab" ++ "cd",y <- "ef"] |
| 20:46:14 | <lambdabot> | ["ae","af","be","bf","ce","cf","de","df"] |
| 20:46:15 | <ski> | [[x,y] | x <- "ab",y <- "ef"] ++ [[x,y] | x <- "cd",y <- "ef"] |
| 20:46:18 | <ski> | > [[x,y] | x <- "ab",y <- "ef"] ++ [[x,y] | x <- "cd",y <- "ef"] |
| 20:46:19 | <lambdabot> | ["ae","af","be","bf","ce","cf","de","df"] |
| 20:46:39 | <ski> | > [[x,y] | x <- "ab",y <- "cd" ++ "ef"] |
| 20:46:41 | <lambdabot> | ["ac","ad","ae","af","bc","bd","be","bf"] |
| 20:46:42 | <ski> | > [[x,y] | x <- "ab",y <- "cd"] ++ [[x,y] | x <- "ab",y <- "ef"] |
| 20:46:43 | <lambdabot> | ["ac","ad","bc","bd","ae","af","be","bf"] |
| 20:47:10 | → | pretty_dumm_guy joins (trottel@gateway/vpn/protonvpn/prettydummguy/x-88029655) |
| 20:47:44 | <ski> | dolio : yea, but that'd require analysis of that, and that there's no side-effects happening |
| 20:48:01 | <geekosaur> | ski, like in your discussion last night where success of a consequent is treated as a failure by the Antecedent |
| 20:48:10 | <ski> | Mercury is more free to reorder and refactor stuff, because it doesn't allow side-effects |
| 20:48:56 | <ski> | (although, it's possible to run Mercury in a "strict" mode where it doesn't reorder solutions) |
| 20:49:06 | <ski> | (or deduplicate) |
| 20:49:26 | <geekosaur> | whereas with laziness the "antecedent" just keeps going without considering what happened with the "consequent" |
| 20:50:23 | <ski> | well, what i talked about last night was not the behaviour of `(>>=)', but of another combinator |
| 20:53:44 | → | eggplantade joins (~Eggplanta@108-201-191-115.lightspeed.sntcca.sbcglobal.net) |
| 20:54:16 | → | kupi joins (uid212005@id-212005.hampstead.irccloud.com) |
| 20:54:56 | <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 |
| 20:55:14 | → | michalz joins (~michalz@185.246.204.58) |
| 20:55:54 | <geekosaur> | and neither knows nor cares whether any value(s) have already been produced |
| 20:58:22 | × | eggplantade quits (~Eggplanta@108-201-191-115.lightspeed.sntcca.sbcglobal.net) (Ping timeout: 260 seconds) |
| 21:01:56 | <ski> | @let infixl 1 ==>; (==>) :: [a] -> (a -> [b]) -> [[b]]; (==>) = for |
| 21:01:57 | <lambdabot> | Defined. |
| 21:02:00 | <ski> | > [1,4,2,9] ==> \x -> guard (x < 10) |
| 21:02:02 | <lambdabot> | error: |
| 21:02:02 | <lambdabot> | Ambiguous occurrence ‘==>’ |
| 21:02:02 | <lambdabot> | It could refer to |
| 21:02:08 | <ski> | oh |
| 21:02:16 | <ski> | @let infixl 1 ===>; (===>) :: [a] -> (a -> [b]) -> [[b]]; (===>) = for |
| 21:02:17 | <lambdabot> | Defined. |
| 21:02:21 | <ski> | > [1,4,2,9] ===> \x -> guard (x < 10) |
| 21:02:22 | <lambdabot> | [[(),(),(),()]] |
| 21:02:25 | <ski> | > [1,4,2,9] ===> \x -> guard (x < 5) |
| 21:02:27 | <lambdabot> | [] |
| 21:02:51 | <ski> | > [1,4,2,9] ===> \x -> return (x*x) |
| 21:02:52 | <lambdabot> | [[1,16,4,81]] |
| 21:03:12 | <ski> | > [1,4,2,9] ==> \x -> do guard (x >= 0); let {y = floor (sqrt (fromIntegral x))}; guard (x == y * y); return y <|> return (-y) |
| 21:03:13 | <lambdabot> | error: |
| 21:03:14 | <lambdabot> | Ambiguous occurrence ‘==>’ |
| 21:03:14 | <lambdabot> | It could refer to |
| 21:03:25 | <ski> | > [1,4,2,9] ===> \x -> do guard (x >= 0); let {y = floor (sqrt (fromIntegral x))}; guard (x == y * y); return y <|> return (-y) |
| 21:03:27 | <lambdabot> | [] |
| 21:03:29 | <ski> | > [1,4,9] ===> \x -> do guard (x >= 0); let {y = floor (sqrt (fromIntegral x))}; guard (x == y * y); return y <|> return (-y) |
| 21:03:30 | <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]] |
| 21:04:07 | <ski> | that's basically what i implemented, except using continuations, and also supporting logic variables (implemented using mutation) |
| 21:05:10 | → | acidjnk joins (~acidjnk@p200300d0c72635825cb0fefbc648f0e4.dip0.t-ipconnect.de) |
| 21:05:39 | <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) |
| 21:07:16 | <ski> | geekosaur : well, fwiw, what you just said i'd argue is more or less what Prolog systems do, as well .. |
| 21:08:10 | × | pretty_dumm_guy quits (trottel@gateway/vpn/protonvpn/prettydummguy/x-88029655) (Ping timeout: 260 seconds) |
| 21:08:20 | <geekosaur> | yes, but see hololeap's confusion about it |
| 21:08:30 | <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 |
| 21:09:13 | <geekosaur> | not seeing how this corresponded to "backtracking" |
| 21:09:37 | <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) |
| 21:10:21 | → | pretty_dumm_guy joins (trottel@gateway/vpn/protonvpn/prettydummguy/x-88029655) |
| 21:11:22 | <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 |
| 21:11:43 | × | retro_ quits (~retro@2e41e9c8.skybroadband.com) (Read error: Connection reset by peer) |
| 21:11:59 | <geekosaur> | (also last time I got to seriously use Prolog was 1992ish, sigh) |
| 21:12:04 | <ski> | acrual implementations record where the last choice-point was, and just jumps back to it |
| 21:12:25 | → | retroid_ joins (~retro@2e41e9c8.skybroadband.com) |
| 21:12:56 | <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 |
| 21:13:12 | <geekosaur> | confused the heck out of my boss when I used it to model a complex pricing system :) |
| 21:13:40 | <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) |
| 21:13:49 | × | darkstardevx quits (~darkstard@50.39.114.152) (Read error: Connection reset by peer) |
| 21:16:41 | → | aqua0210 joins (~user@101.85.11.168) |
| 21:17:32 | × | mrkrktsn1ctcrpt quits (~mrkrktsnd@c-24-6-12-87.hsd1.ca.comcast.net) (Quit: Lost terminal) |
| 21:18:22 | × | mrkrktsndctcrpt quits (~mrkrktsnd@c-24-6-12-87.hsd1.ca.comcast.net) (Quit: Lost terminal) |
| 21:18:23 | <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) |
| 21:18:26 | × | merijn quits (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 260 seconds) |
| 21:19:23 | <ski> | geekosaur : i guess they'd never seen it before ? |
| 21:19:34 | <geekosaur> | nope |
| 21:20:14 | <geekosaur> | my boss was a database dev turned salesman, had not much clue about languages beyond C |
| 21:21:20 | <geekosaur> | so I got thrown at the stuff with more "exotic" languages including a business cobol and a custom embedded-programming basic dialect |
| 21:21:36 | × | _ht quits (~quassel@82-169-194-8.biz.kpn.net) (Remote host closed the connection) |
| 21:21:42 | × | aqua0210 quits (~user@101.85.11.168) (Ping timeout: 260 seconds) |
| 21:22:11 | <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 |
| 21:22:22 | <geekosaur> | then I rewrote it for speed when we had it firmed down |
| 21:22:25 | <ski> | well, a general cursory knowledge of different paradigms and approaches to programming (both general, and sometimes more specific), is unfortunately commonly lacking .. |
| 21:22:29 | ski | nods |
| 21:22:32 | → | darkstardevx joins (~darkstard@50.39.114.152) |
| 21:23:07 | <ski> | (Basic for embedded programming ?) |
| 21:23:28 | × | darkstardevx quits (~darkstard@50.39.114.152) (Remote host closed the connection) |
| 21:23:52 | → | darkstardevx joins (~darkstard@50.39.114.152) |
| 21:24:13 | → | eggplantade joins (~Eggplanta@108-201-191-115.lightspeed.sntcca.sbcglobal.net) |
| 21:24:14 | <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 |
| 21:24:28 | <geekosaur> | all this stuff was around 20 years ago |
| 21:24:53 | × | LiaoTao quits (~LiaoTao@gateway/tor-sasl/liaotao) (Remote host closed the connection) |
| 21:25:14 | → | LiaoTao joins (~LiaoTao@gateway/tor-sasl/liaotao) |
| 21:25:24 | <geekosaur> | mm, actually the hrt thing would have been 1987 |
| 21:25:41 | <ski> | hm, sounds curious |
| 21:26:26 | ski | was recently toying around with a Prolog implementation for the Commodore 64 |
| 21:26:56 | <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 |
| 21:28:06 | <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)) |
| 21:29:06 | → | aeke joins (~a@p200300ef973db1af4086f0a6a24fc4dd.dip0.t-ipconnect.de) |
| 21:29:59 | <aeke> | Hi, is beta reduction the same as function application in lambda calculus? |
| 21:30:08 | <ski> | no |
| 21:30:59 | <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 |
| 21:31:43 | <ski> | (\x. x * x) (2 + 3) --> (2 + 3) * (2 + 3) |
| 21:31:51 | <ski> | is an example of beta-reduction |
| 21:32:37 | <aeke> | So is function application just the juxtaposition of two lambda terms? |
| 21:33:16 | <aeke> | And the left term does not need to be a lambda abstraction? |
| 21:33:21 | <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 |
| 21:34:15 | <ski> | function application is usually written as just juxtaposition (left-associative), in lambda calculus, yes. occasionally you'll see an explicit infix operator, like `@' |
| 21:34:46 | <ski> | aeke : yes, the left term could be a variable, or another application, e.g. |
| 21:35:06 | <ski> | e.g. `f x y' is normally parsed as `(f x) y' |
| 21:36:04 | <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)? |
| 21:36:32 | <ski> | so .. beta-reduction removes both an application, and an abstaction, from the AST. they "react", so to speak |
| 21:36:46 | <ski> | aeke : yes |
| 21:37:22 | → | zmt01 joins (~zmt00@user/zmt00) |
| 21:38:01 | × | zmt00 quits (~zmt00@user/zmt00) (Ping timeout: 245 seconds) |
| 21:38:50 | → | wonko joins (~wjc@user/wonko) |
| 21:43:35 | × | zmt01 quits (~zmt00@user/zmt00) (Ping timeout: 264 seconds) |
| 21:44:39 | → | aqua0210 joins (~user@101.85.11.168) |
| 21:44:40 | × | emf quits (~emf@c-73-97-137-43.hsd1.wa.comcast.net) (Remote host closed the connection) |
| 21:45:46 | → | emf joins (~emf@163.114.132.5) |
| 21:46:52 | ← | ulvarrefr parts (~user@185.24.53.152) (ERC (IRC client for Emacs 27.2)) |
| 21:49:42 | × | aqua0210 quits (~user@101.85.11.168) (Ping timeout: 260 seconds) |
| 21:54:29 | × | chexum quits (~quassel@gateway/tor-sasl/chexum) (Remote host closed the connection) |
| 21:55:46 | → | chexum joins (~quassel@gateway/tor-sasl/chexum) |
| 21:57:30 | × | werneta quits (~werneta@70-142-214-115.lightspeed.irvnca.sbcglobal.net) (Ping timeout: 268 seconds) |
| 21:58:50 | × | jpds1 quits (~jpds@gateway/tor-sasl/jpds) (Remote host closed the connection) |
| 21:59:32 | → | jpds1 joins (~jpds@gateway/tor-sasl/jpds) |
| 22:00:28 | × | basti_ quits (~basti@ip-84-119-8-195.unity-media.net) (Quit: leaving) |
| 22:02:02 | → | v01d4lph4 joins (~v01d4lph4@user/v01d4lph4) |
| 22:05:54 | × | qwedfg quits (~qwedfg@user/qwedfg) (Remote host closed the connection) |
| 22:06:58 | × | v01d4lph4 quits (~v01d4lph4@user/v01d4lph4) (Ping timeout: 260 seconds) |
| 22:08:23 | → | qwedfg joins (~qwedfg@user/qwedfg) |
| 22:10:05 | × | fendor quits (~fendor@178.165.196.101.wireless.dyn.drei.com) (Read error: Connection reset by peer) |
| 22:11:16 | → | zmt00 joins (~zmt00@user/zmt00) |
| 22:11:26 | <EvanR> | often times (beta) reducing something greatly increases its size xD |
| 22:12:43 | → | werneta joins (~werneta@70-142-214-115.lightspeed.irvnca.sbcglobal.net) |
| 22:14:45 | × | ubert quits (~Thunderbi@p200300ecdf4fca30e019fddc82d0353e.dip0.t-ipconnect.de) (Ping timeout: 268 seconds) |
| 22:24:36 | × | gehmehgeh quits (~user@user/gehmehgeh) (Quit: Leaving) |
| 22:29:05 | × | wonko quits (~wjc@user/wonko) (Ping timeout: 256 seconds) |
| 22:30:08 | → | fluffyballoon joins (~user@131.93.208.196) |
| 22:30:41 | → | unit73e joins (~emanuel@2001:818:e8dd:7c00:32b5:c2ff:fe6b:5291) |
| 22:32:23 | × | pavonia quits (~user@user/siracusa) (Read error: Connection reset by peer) |
| 22:33:03 | → | Sgeo_ joins (~Sgeo@user/sgeo) |
| 22:33:06 | × | cheater quits (~Username@user/cheater) (Ping timeout: 260 seconds) |
| 22:33:26 | × | Sgeo quits (~Sgeo@user/sgeo) (Ping timeout: 245 seconds) |
| 22:33:27 | → | cheater joins (~Username@user/cheater) |
| 22:37:05 | → | lavaman joins (~lavaman@98.38.249.169) |
| 22:37:34 | → | pavonia joins (~user@user/siracusa) |
| 22:45:27 | → | aqua0210 joins (~user@101.85.11.168) |
| 22:46:54 | → | yauhsien joins (~yauhsien@118-167-41-229.dynamic-ip.hinet.net) |
| 22:49:56 | → | slack1256 joins (~slack1256@191.125.227.73) |
| 22:50:01 | × | cosimone quits (~user@93-47-229-157.ip115.fastwebnet.it) (Quit: ERC (IRC client for Emacs 27.1)) |
| 22:51:45 | × | yauhsien quits (~yauhsien@118-167-41-229.dynamic-ip.hinet.net) (Ping timeout: 256 seconds) |
| 22:57:18 | × | unit73e quits (~emanuel@2001:818:e8dd:7c00:32b5:c2ff:fe6b:5291) (Ping timeout: 268 seconds) |
| 22:57:26 | × | mastarija quits (~mastarija@2a05:4f46:e06:ff00:18c4:3126:ef80:d743) (Quit: Leaving) |
| 22:59:01 | → | ubert joins (~Thunderbi@p200300ecdf4fca30e019fddc82d0353e.dip0.t-ipconnect.de) |
| 22:59:09 | × | machinedgod quits (~machinedg@24.105.81.50) (Ping timeout: 268 seconds) |
| 23:00:08 | <gentauro> | does anybody in here have a `macOS` with a M1-CPU? |
| 23:00:16 | <gentauro> | and uses `stack`? |
| 23:02:46 | <gentauro> | it's like `stack install` doesn't care about the `arch: aarch64` value in the `.stack/global-project/stack.yaml` file |
| 23:04:10 | <gentauro> | `ld: warning: ignoring file /Users/.../.stack/programs/x86_64-osx-nix/ghc-8.10.7/lib/ghc-8.10.7/Cabal-3.2.1.0/libHSCabal-3.2.1.0.a, building for macOS-arm64 but attempting to link with file built for macOS-x86_64` |
| 23:04:14 | <gentauro> | :-\ |
| 23:04:30 | × | ubert quits (~Thunderbi@p200300ecdf4fca30e019fddc82d0353e.dip0.t-ipconnect.de) (Read error: Connection reset by peer) |
| 23:04:34 | <sclv> | thats a shame |
| 23:06:27 | <maerwald> | gentauro: afaik there's no M1 stack binary |
| 23:06:37 | <gentauro> | maerwald: I know |
| 23:06:40 | <maerwald> | so you're probably running via rosetta, which means it picks x86 toolchain |
| 23:07:28 | <gentauro> | but if you specify in your projects `stack.yaml` -> `arch: aarch64`, then it builts a binary for ARM (which is nice) |
| 23:08:07 | <maerwald> | there's some magic going on with rosetta afaik, so if your invoking binary is x86, then you it picks x86 toolchain |
| 23:08:08 | <gentauro> | but it seems that it only works for local `stack.yaml` files, but not for the global (I'm trying to install the haskell-language-server) |
| 23:08:32 | <Franciman> | good luck to SPJ |
| 23:08:49 | <Franciman> | can't wait for his new language |
| 23:08:49 | <maerwald> | and I wasn't able to build a native stack binary |
| 23:09:04 | <maerwald> | haskell-tls is broken on M1 afair |
| 23:09:11 | <gentauro> | maerwald: :o |
| 23:09:22 | <maerwald> | the `security` binary is missing I think |
| 23:09:56 | × | alzgh quits (~alzgh@user/alzgh) (Ping timeout: 256 seconds) |
| 23:10:19 | <gentauro> | maerwald: hmmm, what does that mean? |
| 23:10:43 | <gentauro> | Franciman: link? |
| 23:10:55 | <Franciman> | https://discourse.haskell.org/t/an-epic-future-for-spj/3573 |
| 23:11:23 | <maerwald> | gentauro: https://gitlab.haskell.org/maerwald/stack/-/jobs/756968#L3070 |
| 23:11:27 | <gentauro> | thx |
| 23:12:02 | <gentauro> | :o |
| 23:12:10 | <gentauro> | is he going to work on Fortnite? :o |
| 23:12:22 | <Rembane_> | Dang! That's odd. |
| 23:12:43 | <maerwald> | https://github.com/vincenthz/hs-certificate/blob/a899bda3d7666d25143be7be8f3105fc076703d9/x509-system/System/X509/MacOS.hs#L22 |
| 23:12:49 | × | slack1256 quits (~slack1256@191.125.227.73) (Remote host closed the connection) |
| 23:12:58 | <maerwald> | also, terrible code |
| 23:13:23 | <maerwald> | one of the reasons I stay away from all of cryptonite and friends :p |
| 23:13:47 | <maerwald> | `pems <- either error id . pemParseLBS <$> LBS.hGetContents hout` |
| 23:14:43 | <gentauro> | maerwald: :o |
| 23:14:51 | <gentauro> | indeed, that is some pretty bad code .. |
| 23:14:59 | → | merijn joins (~merijn@83-160-49-249.ip.xs4all.nl) |
| 23:15:18 | <maerwald> | do you have `security` binary on your M1? |
| 23:15:20 | <gentauro> | btw, is `vincenthz` the only person in the world that can write TLS libs? He also worked on the ones for OCaml |
| 23:16:05 | <gentauro> | maerwald: si -> `/usr/bin/security` |
| 23:16:09 | <maerwald> | odd |
| 23:16:19 | <maerwald> | they are not on the darwin builders |
| 23:16:51 | <gentauro> | `darwin` = Intel CPU? |
| 23:16:57 | <maerwald> | no, aarch64 |
| 23:17:14 | <maerwald> | maybe it's this nix nonsense |
| 23:17:23 | <gentauro> | maerwald: in order to install `stack` I had to enable roseta |
| 23:17:26 | <gentauro> | could it be that? |
| 23:17:45 | <gentauro> | with regard of `nix`. I'm just relying on `home-manager` to deal with stuff |
| 23:18:20 | <maerwald> | I don't know, maybe I'll try again |
| 23:18:32 | <gentauro> | but the creator of `home-manager` told me that I should be looking into `niv` -> https://github.com/nmattia/niv |
| 23:18:47 | <maerwald> | also nix |
| 23:18:52 | <gentauro> | to hanlde dependencies in a `declarative` way |
| 23:18:55 | <maerwald> | lol |
| 23:19:21 | <maerwald> | if nix is declarative, then C is functional |
| 23:19:32 | <gentauro> | maerwald: xD |
| 23:19:46 | × | johnny_sitar quits (~artur@078088015209.bialystok.vectranet.pl) (Ping timeout: 260 seconds) |
| 23:19:52 | × | Pickchea quits (~private@user/pickchea) (Quit: Leaving) |
| 23:20:24 | × | aqua0210 quits (~user@101.85.11.168) (Read error: Connection reset by peer) |
| 23:20:43 | → | aqua0210 joins (~user@101.85.11.168) |
| 23:23:09 | <maerwald> | since there's no public CI that supports aarch64, the only way for stack to build the binaries would be gitlab.haskell.org |
| 23:23:25 | → | ees joins (~user@pool-108-18-30-46.washdc.fios.verizon.net) |
| 23:23:51 | → | alzgh joins (alzgh@user/alzgh) |
| 23:23:55 | ← | ees parts (~user@pool-108-18-30-46.washdc.fios.verizon.net) () |
| 23:24:02 | <maerwald> | I've had a lot of trouble getting the test suite to work there |
| 23:24:23 | → | ees joins (~user@pool-108-18-30-46.washdc.fios.verizon.net) |
| 23:25:03 | × | acidjnk quits (~acidjnk@p200300d0c72635825cb0fefbc648f0e4.dip0.t-ipconnect.de) (Ping timeout: 268 seconds) |
| 23:25:17 | <gentauro> | maerwald: have you tried this? https://ghc.dev/ |
| 23:25:33 | <gentauro> | I will give it a try :) |
| 23:25:57 | <maerwald> | gentauro: huh? |
| 23:26:02 | <maerwald> | I can't follow |
| 23:26:18 | × | fluffyballoon quits (~user@131.93.208.196) (Ping timeout: 260 seconds) |
| 23:26:20 | <gentauro> | just build GHC from scratch |
| 23:26:25 | <gentauro> | as described there |
| 23:26:28 | <maerwald> | I'm talking about stack |
| 23:26:35 | <gentauro> | ahhhh |
| 23:26:42 | <maerwald> | the integration tests |
| 23:26:46 | → | zmt01 joins (~zmt00@user/zmt00) |
| 23:27:27 | × | Kaiepi quits (~Kaiepi@156.34.44.192) (Ping timeout: 256 seconds) |
| 23:28:05 | <gentauro> | it's getting to late (been going on with the `mac` since 04:00 AM and it's almost 00:30 AM ...) |
| 23:28:12 | <gentauro> | I guess I need some rest + food :) |
| 23:28:54 | × | zmt01 quits (~zmt00@user/zmt00) (Client Quit) |
| 23:29:13 | → | zmt01 joins (~zmt00@user/zmt00) |
| 23:29:41 | × | zmt00 quits (~zmt00@user/zmt00) (Ping timeout: 245 seconds) |
| 23:30:26 | <maerwald> | I'm trying with brew: https://gitlab.haskell.org/maerwald/stack/-/jobs/848842 |
| 23:31:09 | × | michalz quits (~michalz@185.246.204.58) (Remote host closed the connection) |
| 23:31:32 | × | geekosaur quits (~geekosaur@xmonad/geekosaur) (Remote host closed the connection) |
| 23:32:27 | → | Kaiepi joins (~Kaiepi@156.34.44.192) |
| 23:33:13 | → | geekosaur joins (~geekosaur@xmonad/geekosaur) |
| 23:34:02 | × | __monty__ quits (~toonn@user/toonn) (Quit: leaving) |
| 23:35:00 | ← | ees parts (~user@pool-108-18-30-46.washdc.fios.verizon.net) (ERC 5.4 (IRC client for GNU Emacs 28.0.60)) |
| 23:35:06 | × | vysn quits (~vysn@user/vysn) (Ping timeout: 260 seconds) |
| 23:35:24 | → | darkstarx joins (~darkstard@185.226.144.76) |
| 23:37:58 | × | darkstardevx quits (~darkstard@50.39.114.152) (Ping timeout: 260 seconds) |
| 23:39:23 | × | alzgh quits (alzgh@user/alzgh) (Ping timeout: 256 seconds) |
| 23:40:25 | → | darkstardev13 joins (~darkstard@176.113.72.221) |
| 23:42:03 | × | max22- quits (~maxime@2a01cb0883359800ab19ff1ba7c64c00.ipv6.abo.wanadoo.fr) (Remote host closed the connection) |
| 23:43:02 | × | darkstarx quits (~darkstard@185.226.144.76) (Ping timeout: 260 seconds) |
| 23:43:42 | → | alzgh joins (~alzgh@user/alzgh) |
| 23:45:38 | × | Tuplanolla quits (~Tuplanoll@91-159-69-50.elisa-laajakaista.fi) (Quit: Leaving.) |
| 23:48:23 | × | merijn quits (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 264 seconds) |
| 23:48:24 | → | darkstarx joins (~darkstard@50.39.114.152) |
| 23:50:56 | × | darkstardev13 quits (~darkstard@176.113.72.221) (Ping timeout: 245 seconds) |
| 23:55:54 | → | jess joins (~jess@libera/staff/jess) |
All times are in UTC on 2021-11-06.