| 2024-09-05 00:06:40 +0200 | justsomeguy | (~justsomeg@user/justsomeguy) |
| 2024-09-05 00:06:57 +0200 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 246 seconds) |
| 2024-09-05 00:08:13 +0200 | Tuplanolla | (~Tuplanoll@91-159-69-59.elisa-laajakaista.fi) (Quit: Leaving.) |
| 2024-09-05 00:08:36 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 2024-09-05 00:09:23 +0200 | <haskellbridge> | <thirdofmay18081814goya> is the following a correct statement? Consider the type "\forall t -> t". There exist values inhabiting this type whose type is "Bool -> Bool", "Nat -> Nat", "Int -> Int". |
| 2024-09-05 00:10:55 +0200 | <haskellbridge> | <thirdofmay18081814goya> whoops didn't mean to put a backslash |
| 2024-09-05 00:10:56 +0200 | <monochrom> | Do you mean "\forall t. t -> t"? |
| 2024-09-05 00:11:14 +0200 | <haskellbridge> | <thirdofmay18081814goya> ah, right |
| 2024-09-05 00:11:15 +0200 | <haskellbridge> | <thirdofmay18081814goya> yeah |
| 2024-09-05 00:12:39 +0200 | <haskellbridge> | <thirdofmay18081814goya> so, reformulating |
| 2024-09-05 00:13:08 +0200 | <monochrom> | On second thought, I don't actually know how to interpret the statement. |
| 2024-09-05 00:13:36 +0200 | <haskellbridge> | <thirdofmay18081814goya> yeah am somewhat confused here |
| 2024-09-05 00:13:49 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 260 seconds) |
| 2024-09-05 00:13:50 +0200 | <haskellbridge> | <thirdofmay18081814goya> "Bool -> Bool", "Nat -> Nat", "Int -> Int" are some types inhabited by values inhabiting "forall t. t -> t"? |
| 2024-09-05 00:15:33 +0200 | <monochrom> | System F is not an interesction type system (or a union type system, for that matter). So the type "Bool->Bool" and the type "forall t. t->t" are disjoint. |
| 2024-09-05 00:15:34 +0200 | <EvanR> | did you explicitly explain the syntax of your language yet |
| 2024-09-05 00:15:48 +0200 | <EvanR> | "a model of" system F is... I'm not sure |
| 2024-09-05 00:16:13 +0200 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) |
| 2024-09-05 00:16:14 +0200 | <monochrom> | (or a subtyping system) |
| 2024-09-05 00:17:47 +0200 | <monochrom> | You need at least one of {subtyping, intersection} to talk about one term having two types and so the two types have some overlap. |
| 2024-09-05 00:17:48 +0200 | <haskellbridge> | <thirdofmay18081814goya> monochrom: i.e. they do not have any common values? |
| 2024-09-05 00:17:48 +0200 | <EvanR> | a specific term can get assigned specific typings. Your question kind of sounds like we're talking about platonic values out in space being in one or more sets |
| 2024-09-05 00:18:09 +0200 | paddymahoney | (~paddymaho@pool-99-250-10-137.cpe.net.cable.rogers.com) (Ping timeout: 246 seconds) |
| 2024-09-05 00:18:28 +0200 | <haskellbridge> | <thirdofmay18081814goya> EvanR: sorry I'm not really unconfused enough to be able to state a syntax lol |
| 2024-09-05 00:18:47 +0200 | <EvanR> | you don't have system F spelled out in front of you? xD |
| 2024-09-05 00:18:50 +0200 | <monochrom> | The Platonic Plane is untyped set theory in the first place. :) |
| 2024-09-05 00:19:16 +0200 | <haskellbridge> | <thirdofmay18081814goya> EvanR: yeah tapl's, but am slowly working through its meaning |
| 2024-09-05 00:19:55 +0200 | <haskellbridge> | <Bowuigi> thirdofmay18081814goya re:single-lambda Henk Barendegt's (might have mispelled that) lambda cube has a single lambda that works as both type application and abstraction, tho you might need type annotations or some way to disambiguate between them (upper/lower case variables could work) |
| 2024-09-05 00:20:05 +0200 | <EvanR> | the "values" you ask about need to be sentences in the allowed language |
| 2024-09-05 00:20:09 +0200 | pavonia | (~user@user/siracusa) |
| 2024-09-05 00:20:25 +0200 | <EvanR> | like lambda (x:Int) . x, or something |
| 2024-09-05 00:20:26 +0200 | <haskellbridge> | <thirdofmay18081814goya> EvanR: hm this might be my problem, i might be confusing values and terms |
| 2024-09-05 00:20:57 +0200 | <haskellbridge> | <thirdofmay18081814goya> Bowuigi: ah I see! |
| 2024-09-05 00:21:30 +0200 | <haskellbridge> | <thirdofmay18081814goya> oh, i think I found the issue |
| 2024-09-05 00:21:35 +0200 | <haskellbridge> | <thirdofmay18081814goya> terms unify, values inhabit |
| 2024-09-05 00:21:36 +0200 | <EvanR> | dependent types are at the pinnacle of the lambda cube and have one lambda |
| 2024-09-05 00:23:05 +0200 | <EvanR> | in one sense values are expressions which are fully evaluated. In another sense values are semantic, like \x -> x and \y -> y being "really the same value" |
| 2024-09-05 00:23:24 +0200 | <monochrom> | terms inhabit types too. I haven't heard of "terms unify". |
| 2024-09-05 00:24:12 +0200 | <EvanR> | stick to terms |
| 2024-09-05 00:24:27 +0200 | <EvanR> | void where prohibited |
| 2024-09-05 00:27:27 +0200 | sprout | (~sprout@84-80-106-227.fixed.kpn.net) (Ping timeout: 244 seconds) |
| 2024-09-05 00:27:52 +0200 | <ski> | dependently typed languages may've term reconstruction, as well |
| 2024-09-05 00:28:06 +0200 | <monochrom> | You can treat ∀ as an epic intersection; then your questions have meaning. But System F does not require it, it allows me to, alternatively, treat ∀ as waiting for instantiation; then your questions are meaningless, two types are disjoint, there is no "my term inhabits two types", a term inhabits only one type. |
| 2024-09-05 00:28:41 +0200 | <EvanR> | that's a theorem of system F, terms have at most 1 typing? |
| 2024-09-05 00:29:06 +0200 | <haskellbridge> | <thirdofmay18081814goya> monochrom: I'll focus on this, thank you |
| 2024-09-05 00:29:20 +0200 | <haskellbridge> | <thirdofmay18081814goya> a term inhabits only a single type (in system F) |
| 2024-09-05 00:29:49 +0200 | <ski> | (Henk Barendregt) |
| 2024-09-05 00:29:55 +0200 | <monochrom> | E.g., "clearly", (Λt. λx:t. x) does not inhabit Nat->Nat, and (λx:Nat. x) does not inhabit ∀t. t->t. |
| 2024-09-05 00:30:22 +0200 | <monochrom> | (λx. |
| 2024-09-05 00:31:16 +0200 | <monochrom> | (λx. x) is illegal in System F. In an intersection type system, it could inhabit both Nat->Nat and ∀t. t->t, but then that's not System F. |
| 2024-09-05 00:31:37 +0200 | ski | idly ponders monic unions |
| 2024-09-05 00:31:38 +0200 | <dolio> | No, it isn't illegal in System F. It's illegal in a particular presentation of System F. |
| 2024-09-05 00:32:37 +0200 | <EvanR> | back to asking for the specific language and typing rules |
| 2024-09-05 00:32:59 +0200 | <monochrom> | Would that require a heavy dose of type inference? |
| 2024-09-05 00:36:07 +0200 | <dolio> | Well, you can't do type inference in general. But you can require people to give you full derivations for terms. |
| 2024-09-05 00:36:20 +0200 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 252 seconds) |
| 2024-09-05 00:36:35 +0200 | <haskellbridge> | <thirdofmay18081814goya> so dumb question but what is the type of the identity function, with explicit forall and parentheses? |
| 2024-09-05 00:37:00 +0200 | <EvanR> | "the identity function", the platonic entity out in mathemagic land xD |
| 2024-09-05 00:37:18 +0200 | <monochrom> | ∀t. t->t |
| 2024-09-05 00:38:02 +0200 | <monochrom> | Parametricity says that it has only one inhabitant, so "the" is OK for this. :) |
| 2024-09-05 00:38:03 +0200 | <EvanR> | what term has that type and has that behavior, with explicit forall and parentheses |
| 2024-09-05 00:38:16 +0200 | <monochrom> | (Λt. λx:t. x) |
| 2024-09-05 00:38:28 +0200 | <EvanR> | \o/ |
| 2024-09-05 00:38:39 +0200 | <monochrom> | I have been using that for running examples for 3 times already. |
| 2024-09-05 00:39:09 +0200 | sawilagar | (~sawilagar@user/sawilagar) (Ping timeout: 246 seconds) |
| 2024-09-05 00:39:12 +0200 | <haskellbridge> | <thirdofmay18081814goya> am profoundly meditating on it thank you sorry for repeat |
| 2024-09-05 00:39:26 +0200 | paddymahoney | (~paddymaho@pool-99-250-10-137.cpe.net.cable.rogers.com) |
| 2024-09-05 00:40:10 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 2024-09-05 00:40:11 +0200 | szkl | (uid110435@id-110435.uxbridge.irccloud.com) |
| 2024-09-05 00:41:01 +0200 | ChaiTRex | (~ChaiTRex@user/chaitrex) |
| 2024-09-05 00:41:22 +0200 | acidjnk_new | (~acidjnk@p200300d6e72cfb17e4f43f2fc0c04a46.dip0.t-ipconnect.de) (Ping timeout: 248 seconds) |
| 2024-09-05 00:41:31 +0200 | ski | . o O ( `snd : (t : Type) * t -> t' ) |
| 2024-09-05 00:42:23 +0200 | <haskellbridge> | <Bowuigi> That looks odd |
| 2024-09-05 00:42:44 +0200 | <dolio> | It doesn't, actually. |
| 2024-09-05 00:42:52 +0200 | <haskellbridge> | <Bowuigi> Isn't it "snd : (t t' : Type) -> t * t' -> t'"? |
| 2024-09-05 00:43:17 +0200 | <EvanR> | lol |
| 2024-09-05 00:43:21 +0200 | <monochrom> | (t : Type) * t -> t |
| 2024-09-05 00:43:29 +0200 | <monochrom> | The ' is just to close the ` |
| 2024-09-05 00:43:30 +0200 | <EvanR> | unknown type variable t' |
| 2024-09-05 00:43:58 +0200 | <monochrom> | This is why I just use " |
| 2024-09-05 00:44:12 +0200 | <monochrom> | We need html over irc. |
| 2024-09-05 00:44:31 +0200 | <EvanR> | Isn't it t' |
| 2024-09-05 00:44:38 +0200 | ski | sprinkles some anaphora, chases donkeys |
| 2024-09-05 00:45:08 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 265 seconds) |
| 2024-09-05 00:45:23 +0200 | <monochrom> | So that I can write <code>t -> t</code> >:) |
| 2024-09-05 00:47:03 +0200 | <ski> | some people use Qt -> tQ |
| 2024-09-05 00:47:21 +0200 | <EvanR> | o_O |
| 2024-09-05 00:48:43 +0200 | srazkvt | (~sarah@user/srazkvt) (Quit: Konversation terminated!) |
| 2024-09-05 00:49:19 +0200 | <haskellbridge> | <thirdofmay18081814goya> the only thing "Λt. λx:t. x" can take, in System F, is a type, right? including a function type? |
| 2024-09-05 00:49:39 +0200 | <ski> | "can take" ? |
| 2024-09-05 00:50:17 +0200 | <monochrom> | Yeah the first lambda is to be instantiated to a type. "type-level lambda" |
| 2024-09-05 00:50:53 +0200 | <monochrom> | actually just "type lambda". GHC may get it soon. |
| 2024-09-05 00:50:54 +0200 | <haskellbridge> | <thirdofmay18081814goya> ski: i.e. the only step that is defined to reduce this expression is the one of substituting t for any type |
| 2024-09-05 00:51:15 +0200 | <ski> | when applying it to a type, yes |
| 2024-09-05 00:51:29 +0200 | <haskellbridge> | <thirdofmay18081814goya> ski: can you apply it to anything else? |
| 2024-09-05 00:51:35 +0200 | <ski> | no |
| 2024-09-05 00:51:44 +0200 | <haskellbridge> | <thirdofmay18081814goya> ok i see, ty |
| 2024-09-05 00:51:51 +0200 | <ski> | (but you didn't mention anything about application) |
| 2024-09-05 00:52:03 +0200 | <ski> | (just substitution) |
| 2024-09-05 00:53:29 +0200 | sprout | (~sprout@84-80-106-227.fixed.kpn.net) |
| 2024-09-05 00:55:06 +0200 | <ski> | it's |
| 2024-09-05 00:55:50 +0200 | <EvanR> | (Λt. λx:t. x) Nat could reduce |
| 2024-09-05 00:55:53 +0200 | <ski> | (Λt. λx:t. x) u ⟿ λx:u. x |
| 2024-09-05 00:55:54 +0200 | <ski> | not |
| 2024-09-05 00:55:58 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 2024-09-05 00:56:00 +0200 | <ski> | Λt. λx:t. x ⟿ λx:u. x |
| 2024-09-05 00:56:22 +0200 | ddb1 | ddb |
| 2024-09-05 00:57:03 +0200 | <ski> | (sometimes with a syntactic difference for applying a term to a type) |
| 2024-09-05 00:57:11 +0200 | <EvanR> | because t is a bound variable, substituting seems problematic |
| 2024-09-05 00:57:31 +0200 | <ski> | in the body |
| 2024-09-05 00:58:17 +0200 | <EvanR> | substituting stuff for free variables always works |
| 2024-09-05 00:58:33 +0200 | <EvanR> | where stuff doesn't capture bound variables |
| 2024-09-05 00:58:54 +0200 | <EvanR> | or you void your warranty |
| 2024-09-05 01:01:31 +0200 | <ski> | you can substitute for code variables, when meta-programming, not avoiding variable capture |
| 2024-09-05 01:03:24 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 260 seconds) |
| 2024-09-05 01:06:07 +0200 | ZharMeny | (~ZharMeny@user/ZharMeny) (Quit: ERC 5.5.0.29.1 (IRC client for GNU Emacs 29.4)) |
| 2024-09-05 01:06:22 +0200 | <haskellbridge> | <thirdofmay18081814goya> hm "λx:t. x : t -> t" is somewhat ambiguous outside of context right? we could mean either "Λt. λx:t. x : ∀t. t -> t" or "[y ↦ t] λx:y. x : y -> y", right? |
| 2024-09-05 01:07:40 +0200 | <EvanR> | hence the syntax rules of your language needing to exist |
| 2024-09-05 01:08:16 +0200 | <haskellbridge> | <thirdofmay18081814goya> nice, i think i've got it, thanks a lot |
| 2024-09-05 01:09:33 +0200 | CiaoSen | (~Jura@2a05:5800:24b:5c00:ca4b:d6ff:fec1:99da) (Ping timeout: 276 seconds) |
| 2024-09-05 01:12:42 +0200 | gmg | (~user@user/gehmehgeh) (Remote host closed the connection) |
| 2024-09-05 01:13:58 +0200 | gmg | (~user@user/gehmehgeh) |
| 2024-09-05 01:14:43 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 2024-09-05 01:15:59 +0200 | spew | (~spew@201.141.99.170) |
| 2024-09-05 01:19:43 +0200 | Batzy | (~quassel@user/batzy) |
| 2024-09-05 01:19:49 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 248 seconds) |
| 2024-09-05 01:20:09 +0200 | CAT_S | (apic@brezn3.muc.ccc.de) (Ping timeout: 244 seconds) |
| 2024-09-05 01:30:29 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 2024-09-05 01:31:19 +0200 | spew | (~spew@201.141.99.170) (Quit: spew) |
| 2024-09-05 01:32:16 +0200 | xff0x | (~xff0x@2405:6580:b080:900:ccef:b4d3:d1ad:38b8) (Quit: xff0x) |
| 2024-09-05 01:35:22 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 2024-09-05 01:36:38 +0200 | Sciencentistguy | (~sciencent@hacksoc/ordinary-member) (Ping timeout: 245 seconds) |
| 2024-09-05 01:46:16 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 2024-09-05 01:46:34 +0200 | <haskellbridge> | <GunpowderGuy> Hello i am computer science interested in functional programming. I think by the end of the year i will be skilled enough to work on a high performance compiler |
| 2024-09-05 01:46:50 +0200 | <haskellbridge> | <GunpowderGuy> like grin : https://www.reddit.com/r/haskell/comments/ku1zsm/nextgen_haskell_compilation_techniques/ |
| 2024-09-05 01:47:07 +0200 | <haskellbridge> | <GunpowderGuy> Anyone else is interested in working with me? |
| 2024-09-05 01:47:21 +0200 | <haskellbridge> | <GunpowderGuy> -is |
| 2024-09-05 01:47:40 +0200 | <haskellbridge> | <GunpowderGuy> Hello i am computer science student researching functional programming. I think by the end of the year i will be skilled enough to work on a high performance compiler |
| 2024-09-05 01:48:34 +0200 | <monochrom> | I can consider "λx:t. x : t -> t" to mean that "t" is specified from the surrounding context but I don't need to know. |
| 2024-09-05 01:49:35 +0200 | Sciencentistguy | (~sciencent@hacksoc/ordinary-member) |
| 2024-09-05 01:49:38 +0200 | <monochrom> | Am I allowed to mock? I have a PhD in computer science, I think by the end of the year I will solve P vs NP. |
| 2024-09-05 01:49:57 +0200 | Square2 | (~Square4@user/square) |
| 2024-09-05 01:50:58 +0200 | <monochrom> | OK this channel isn't very interested in P vs NP. I will finish Dependent Linear Haskell instead. >:) |
| 2024-09-05 01:52:53 +0200 | emmanuelux | (~emmanuelu@user/emmanuelux) |
| 2024-09-05 01:53:08 +0200 | <haskellbridge> | <thirdofmay18081814goya> monochrom: pls do |
| 2024-09-05 01:53:41 +0200 | <monochrom> | :) |
| 2024-09-05 01:54:22 +0200 | <monochrom> | I don't actually even know where to start. Don't hold your breath. |
| 2024-09-05 01:56:09 +0200 | Sciencentistguy | (~sciencent@hacksoc/ordinary-member) (Ping timeout: 246 seconds) |
| 2024-09-05 01:57:21 +0200 | <haskellbridge> | <GunpowderGuy> monochrom: so idris2? |
| 2024-09-05 01:57:38 +0200 | <haskellbridge> | <GunpowderGuy> idrsi2 is dependent linear haskell |
| 2024-09-05 01:57:39 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 260 seconds) |
| 2024-09-05 01:57:50 +0200 | <haskellbridge> | <GunpowderGuy> * idris2 |
| 2024-09-05 02:03:56 +0200 | motherfsck | (~motherfsc@user/motherfsck) |
| 2024-09-05 02:04:09 +0200 | Sciencentistguy | (~sciencent@hacksoc/ordinary-member) |
| 2024-09-05 02:04:28 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 2024-09-05 02:04:36 +0200 | neuroevolutus | (~neuroevol@146.70.211.24) |
| 2024-09-05 02:05:18 +0200 | weary-traveler | (~user@user/user363627) |
| 2024-09-05 02:16:19 +0200 | <EvanR> | dependent linear haskell is something else |
| 2024-09-05 02:16:53 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 248 seconds) |
| 2024-09-05 02:16:59 +0200 | <EvanR> | idris diverges from haskellness heavily in the area of type classes |
| 2024-09-05 02:17:19 +0200 | <EvanR> | see "type classes vs the world" |
| 2024-09-05 02:17:41 +0200 | weary-traveler | (~user@user/user363627) (Remote host closed the connection) |
| 2024-09-05 02:18:23 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 2024-09-05 02:22:00 +0200 | weary-traveler | (~user@user/user363627) |
| 2024-09-05 02:23:06 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 246 seconds) |
| 2024-09-05 02:33:50 +0200 | <haskellbridge> | <thirdofmay18081814goya> can system f\omega model haskell? |
| 2024-09-05 02:34:07 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 2024-09-05 02:34:54 +0200 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) |
| 2024-09-05 02:37:16 +0200 | <justsomeguy> | ! |
| 2024-09-05 02:39:17 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 255 seconds) |
| 2024-09-05 02:41:58 +0200 | weary-traveler | (~user@user/user363627) (Quit: Konversation terminated!) |
| 2024-09-05 02:42:14 +0200 | weary-traveler | (~user@user/user363627) |
| 2024-09-05 02:44:11 +0200 | athan_ | (~athan@syn-098-153-145-140.biz.spectrum.com) (Quit: Konversation terminated!) |
| 2024-09-05 02:47:18 +0200 | weary-traveler | (~user@user/user363627) (Quit: Konversation terminated!) |
| 2024-09-05 02:47:38 +0200 | weary-traveler | (~user@user/user363627) |
| 2024-09-05 02:48:19 +0200 | szkl | (uid110435@id-110435.uxbridge.irccloud.com) (Quit: Connection closed for inactivity) |
| 2024-09-05 02:48:32 +0200 | <d34df00d> | EvanR: oh that's funny, I'm writing a post for my blog about idris interfaces vs haskell classes. |
| 2024-09-05 02:48:51 +0200 | <d34df00d> | Idris' interfaces are basically a syntactic sugar for `auto` implicit arguments. |
| 2024-09-05 02:49:23 +0200 | <d34df00d> | That is, a function/interface constraint is this sugar. |
| 2024-09-05 02:49:42 +0200 | <d34df00d> | The interface itself is just a type [constructor], which makes lots of Haskell extensions ranging from ConstraintKinds to QuantifiedConstraints redundant. |
| 2024-09-05 02:49:54 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 2024-09-05 02:50:05 +0200 | <d34df00d> | The cost is that Idris has no coherence of interfaces, and even the usage of (==) in a context like (Eq a, Ord a) => ... is ambiguous. |
| 2024-09-05 02:50:27 +0200 | troydm | (~troydm@user/troydm) |
| 2024-09-05 02:50:58 +0200 | <d34df00d> | That is, because there are actually two `Eq a` in scope — the explicit one and the Ord's superclass one. |
| 2024-09-05 02:51:55 +0200 | <d34df00d> | Also, `C1 a => C2 a => t` and `(C1 a, C2 a) => t` and `C2 a => C1 a => t` are three distinct types that don't unify. |
| 2024-09-05 02:52:38 +0200 | weary-traveler | (~user@user/user363627) (Quit: Konversation terminated!) |
| 2024-09-05 02:52:54 +0200 | weary-traveler | (~user@user/user363627) |
| 2024-09-05 02:53:06 +0200 | <d34df00d> | Also, re linear types, it kinda sucks that linear-base doesn't have unboxed linear mutable vectors. Boxed ones are slooooow. |
| 2024-09-05 02:54:36 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 246 seconds) |
| 2024-09-05 03:00:16 +0200 | <justsomeguy> | As a beginner with Haskell I've had a hard time working with arrays in general. |
| 2024-09-05 03:03:06 +0200 | <haskellbridge> | <Bowuigi> thirdofmay18081814goya F omega is a superset of Haskell (Core is system FC, an extension of system F), tho it lacks many of the familiar features (typeclasses and type families, mainly) |
| 2024-09-05 03:04:47 +0200 | <haskellbridge> | <thirdofmay18081814goya> Bowuigi: thanks a lot! |
| 2024-09-05 03:04:59 +0200 | lockywolf | (~lockywolf@public.lockywolf.net) (Quit: ZNC 1.8.2 - https://znc.in) |
| 2024-09-05 03:05:27 +0200 | neuroevolutus | (~neuroevol@146.70.211.24) (Ping timeout: 256 seconds) |
| 2024-09-05 03:05:42 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 2024-09-05 03:06:05 +0200 | <Axman6> | justsomeguy: what are you trying to do with them? They're not a particularly common structure in most Haskell programs, unless you need a) random access and b) don't need to update them much (though we have a lot of good support for mutable arrays too) |
| 2024-09-05 03:06:49 +0200 | lockywolf | (~lockywolf@public.lockywolf.net) |
| 2024-09-05 03:07:58 +0200 | weary-traveler | (~user@user/user363627) (Quit: Konversation terminated!) |
| 2024-09-05 03:08:14 +0200 | weary-traveler | (~user@user/user363627) |
| 2024-09-05 03:08:40 +0200 | <d34df00d> | I'm also curious if the instances of the form `MArray (STUArray s) Ty (ST s)` should better be replaced by `s ~ s' => MArray (STUArray s') Int16 (ST s)` to guide type inference in contexts like `foo <- unsafeNewArray_ @(STUArray _) ...` |
| 2024-09-05 03:09:24 +0200 | justsomeguy | (~justsomeg@user/justsomeguy) (Ping timeout: 260 seconds) |
| 2024-09-05 03:09:28 +0200 | <d34df00d> | (read that Int16 as Ty, of course) |
| 2024-09-05 03:10:21 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 246 seconds) |
| 2024-09-05 03:13:18 +0200 | weary-traveler | (~user@user/user363627) (Quit: Konversation terminated!) |
| 2024-09-05 03:13:36 +0200 | weary-traveler | (~user@user/user363627) |
| 2024-09-05 03:15:49 +0200 | machinedgod | (~machinedg@d50-99-47-73.abhsia.telus.net) (Ping timeout: 260 seconds) |
| 2024-09-05 03:18:38 +0200 | weary-traveler | (~user@user/user363627) (Quit: Konversation terminated!) |
| 2024-09-05 03:18:54 +0200 | weary-traveler | (~user@user/user363627) |
| 2024-09-05 03:21:28 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 2024-09-05 03:23:58 +0200 | weary-traveler | (~user@user/user363627) (Quit: Konversation terminated!) |
| 2024-09-05 03:24:14 +0200 | weary-traveler | (~user@user/user363627) |
| 2024-09-05 03:26:12 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 2024-09-05 03:28:22 +0200 | <monochrom> | BTW what does System FC add to System F? |
| 2024-09-05 03:29:11 +0200 | <haskellbridge> | <thirdofmay18081814goya> monochrom: "type equalities and coercions", am trying to understand what this means |
| 2024-09-05 03:29:19 +0200 | weary-traveler | (~user@user/user363627) (Quit: Konversation terminated!) |
| 2024-09-05 03:29:34 +0200 | weary-traveler | (~user@user/user363627) |
| 2024-09-05 03:29:55 +0200 | <haskellbridge> | <thirdofmay18081814goya> "coercions serve as evidence for type equalities" |
| 2024-09-05 03:31:41 +0200 | <probie> | monochrom: C |
| 2024-09-05 03:32:17 +0200 | <Axman6> | nah clearly they're multiplied, that'd be F+C |
| 2024-09-05 03:32:53 +0200 | <Axman6> | it adds FC-F |
| 2024-09-05 03:33:19 +0200 | vglfr | (~vglfr@2601:14d:4e01:1370:919a:c941:4142:9778) (Ping timeout: 260 seconds) |
| 2024-09-05 03:33:28 +0200 | vglfr | (~vglfr@c-73-163-164-68.hsd1.md.comcast.net) |
| 2024-09-05 03:34:38 +0200 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 255 seconds) |
| 2024-09-05 03:34:38 +0200 | weary-traveler | (~user@user/user363627) (Quit: Konversation terminated!) |
| 2024-09-05 03:34:54 +0200 | weary-traveler | (~user@user/user363627) |
| 2024-09-05 03:37:16 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 2024-09-05 03:39:58 +0200 | weary-traveler | (~user@user/user363627) (Quit: Konversation terminated!) |
| 2024-09-05 03:40:15 +0200 | weary-traveler | (~user@user/user363627) |
| 2024-09-05 03:42:12 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 246 seconds) |
| 2024-09-05 03:45:18 +0200 | weary-traveler | (~user@user/user363627) (Quit: Konversation terminated!) |
| 2024-09-05 03:45:35 +0200 | weary-traveler | (~user@user/user363627) |
| 2024-09-05 03:53:04 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 2024-09-05 03:55:09 +0200 | waleee | (~waleee@h-176-10-144-38.NA.cust.bahnhof.se) (Ping timeout: 246 seconds) |
| 2024-09-05 03:55:44 +0200 | <monochrom> | :( :) |
| 2024-09-05 03:58:31 +0200 | <d34df00d> | FC really stands for Football Club. |
| 2024-09-05 03:58:33 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 276 seconds) |
| 2024-09-05 03:58:37 +0200 | <monochrom> | If https://www.systemf.com.au/ wants to form a football team, what would they call the team? Answer: System FC. >:) |
| 2024-09-05 04:00:38 +0200 | weary-traveler | (~user@user/user363627) (Quit: Konversation terminated!) |
| 2024-09-05 04:00:54 +0200 | weary-traveler | (~user@user/user363627) |
| 2024-09-05 04:01:21 +0200 | cross | (~cross@spitfire.i.gajendra.net) (Ping timeout: 244 seconds) |
| 2024-09-05 04:05:58 +0200 | weary-traveler | (~user@user/user363627) (Quit: Konversation terminated!) |
| 2024-09-05 04:06:14 +0200 | weary-traveler | (~user@user/user363627) |
| 2024-09-05 04:08:50 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 2024-09-05 04:11:19 +0200 | weary-traveler | (~user@user/user363627) (Quit: Konversation terminated!) |
| 2024-09-05 04:11:40 +0200 | weary-traveler | (~user@user/user363627) |
| 2024-09-05 04:13:41 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 248 seconds) |
| 2024-09-05 04:16:21 +0200 | czy | (~user@2a00:23c6:54a8:6301:5024:a70a:b7d6:6a68) (Ping timeout: 265 seconds) |
| 2024-09-05 04:16:38 +0200 | weary-traveler | (~user@user/user363627) (Quit: Konversation terminated!) |
| 2024-09-05 04:16:45 +0200 | emmanuelux | (~emmanuelu@user/emmanuelux) (Quit: au revoir) |
| 2024-09-05 04:16:54 +0200 | weary-traveler | (~user@user/user363627) |
| 2024-09-05 04:17:31 +0200 | cross | (~cross@spitfire.i.gajendra.net) |
| 2024-09-05 04:21:58 +0200 | weary-traveler | (~user@user/user363627) (Quit: Konversation terminated!) |
| 2024-09-05 04:22:14 +0200 | weary-traveler | (~user@user/user363627) |
| 2024-09-05 04:24:37 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 2024-09-05 04:27:18 +0200 | weary-traveler | (~user@user/user363627) (Quit: Konversation terminated!) |
| 2024-09-05 04:27:34 +0200 | weary-traveler | (~user@user/user363627) |
| 2024-09-05 04:28:33 +0200 | uli-fem | (~user@user/uli-fem) |
| 2024-09-05 04:32:21 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 244 seconds) |
| 2024-09-05 04:32:38 +0200 | weary-traveler | (~user@user/user363627) (Quit: Konversation terminated!) |
| 2024-09-05 04:32:54 +0200 | weary-traveler | (~user@user/user363627) |
| 2024-09-05 04:33:25 +0200 | Axman6 | (~Axman6@user/axman6) (Ping timeout: 246 seconds) |
| 2024-09-05 04:33:42 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 2024-09-05 04:35:45 +0200 | uli-fem | (~user@user/uli-fem) (Read error: Connection reset by peer) |
| 2024-09-05 04:37:58 +0200 | weary-traveler | (~user@user/user363627) (Quit: Konversation terminated!) |
| 2024-09-05 04:38:14 +0200 | weary-traveler | (~user@user/user363627) |
| 2024-09-05 04:38:33 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 244 seconds) |
| 2024-09-05 04:43:19 +0200 | weary-traveler | (~user@user/user363627) (Quit: Konversation terminated!) |
| 2024-09-05 04:43:34 +0200 | weary-traveler | (~user@user/user363627) |
| 2024-09-05 04:48:38 +0200 | weary-traveler | (~user@user/user363627) (Quit: Konversation terminated!) |
| 2024-09-05 04:48:57 +0200 | weary-traveler | (~user@user/user363627) |
| 2024-09-05 04:49:25 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 2024-09-05 04:54:06 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 2024-09-05 04:54:24 +0200 | td_ | (~td@i5387092A.versanet.de) (Ping timeout: 260 seconds) |
| 2024-09-05 04:56:16 +0200 | td_ | (~td@i53870939.versanet.de) |
| 2024-09-05 04:58:58 +0200 | weary-traveler | (~user@user/user363627) (Quit: Konversation terminated!) |
| 2024-09-05 04:59:14 +0200 | weary-traveler | (~user@user/user363627) |
| 2024-09-05 05:04:18 +0200 | weary-traveler | (~user@user/user363627) (Quit: Konversation terminated!) |
| 2024-09-05 05:04:34 +0200 | weary-traveler | (~user@user/user363627) |
| 2024-09-05 05:05:11 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 2024-09-05 05:09:38 +0200 | weary-traveler | (~user@user/user363627) (Quit: Konversation terminated!) |
| 2024-09-05 05:09:54 +0200 | weary-traveler | (~user@user/user363627) |
| 2024-09-05 05:10:14 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |
| 2024-09-05 05:14:58 +0200 | weary-traveler | (~user@user/user363627) (Quit: Konversation terminated!) |
| 2024-09-05 05:15:14 +0200 | weary-traveler | (~user@user/user363627) |
| 2024-09-05 05:18:37 +0200 | Axman6 | (~Axman6@user/axman6) |
| 2024-09-05 05:19:02 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 2024-09-05 05:20:18 +0200 | weary-traveler | (~user@user/user363627) (Quit: Konversation terminated!) |
| 2024-09-05 05:20:34 +0200 | weary-traveler | (~user@user/user363627) |
| 2024-09-05 05:24:05 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 248 seconds) |
| 2024-09-05 05:25:38 +0200 | weary-traveler | (~user@user/user363627) (Quit: Konversation terminated!) |
| 2024-09-05 05:25:54 +0200 | weary-traveler | (~user@user/user363627) |
| 2024-09-05 05:27:13 +0200 | Lord_of_Life | (~Lord@user/lord-of-life/x-2819915) (Ping timeout: 248 seconds) |
| 2024-09-05 05:27:56 +0200 | youthlic | (~Thunderbi@user/youthlic) |
| 2024-09-05 05:28:15 +0200 | Lord_of_Life | (~Lord@user/lord-of-life/x-2819915) |
| 2024-09-05 05:30:16 +0200 | Axma92047 | (~Axman6@user/axman6) |
| 2024-09-05 05:30:59 +0200 | weary-traveler | (~user@user/user363627) (Quit: Konversation terminated!) |
| 2024-09-05 05:31:14 +0200 | weary-traveler | (~user@user/user363627) |
| 2024-09-05 05:32:09 +0200 | Axman6 | (~Axman6@user/axman6) (Ping timeout: 240 seconds) |
| 2024-09-05 05:34:50 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 2024-09-05 05:36:48 +0200 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) |
| 2024-09-05 05:40:05 +0200 | aforemny | (~aforemny@i59F516D7.versanet.de) (Ping timeout: 248 seconds) |
| 2024-09-05 05:40:20 +0200 | aforemny_ | (~aforemny@i59F516F7.versanet.de) |
| 2024-09-05 05:40:38 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 255 seconds) |
| 2024-09-05 05:45:35 +0200 | Axma92047 | Axman6 |
| 2024-09-05 05:46:18 +0200 | weary-traveler | (~user@user/user363627) (Quit: Konversation terminated!) |
| 2024-09-05 05:46:34 +0200 | weary-traveler | (~user@user/user363627) |
| 2024-09-05 05:51:38 +0200 | weary-traveler | (~user@user/user363627) (Quit: Konversation terminated!) |
| 2024-09-05 05:51:39 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 2024-09-05 05:51:54 +0200 | weary-traveler | (~user@user/user363627) |
| 2024-09-05 05:56:34 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 248 seconds) |
| 2024-09-05 05:56:58 +0200 | weary-traveler | (~user@user/user363627) (Quit: Konversation terminated!) |
| 2024-09-05 05:57:14 +0200 | weary-traveler | (~user@user/user363627) |
| 2024-09-05 06:02:11 +0200 | Lord_of_Life | (~Lord@user/lord-of-life/x-2819915) (Quit: Laa shay'a waqi'un moutlaq bale kouloun moumkine) |
| 2024-09-05 06:02:19 +0200 | weary-traveler | (~user@user/user363627) (Quit: Konversation terminated!) |
| 2024-09-05 06:02:34 +0200 | weary-traveler | (~user@user/user363627) |
| 2024-09-05 06:06:54 +0200 | rosco | (~rosco@175.136.158.234) |
| 2024-09-05 06:07:27 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 2024-09-05 06:07:39 +0200 | weary-traveler | (~user@user/user363627) (Quit: Konversation terminated!) |
| 2024-09-05 06:07:54 +0200 | weary-traveler | (~user@user/user363627) |
| 2024-09-05 06:08:32 +0200 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 252 seconds) |
| 2024-09-05 06:12:21 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 246 seconds) |
| 2024-09-05 06:12:58 +0200 | weary-traveler | (~user@user/user363627) (Quit: Konversation terminated!) |
| 2024-09-05 06:13:14 +0200 | weary-traveler | (~user@user/user363627) |
| 2024-09-05 06:18:19 +0200 | weary-traveler | (~user@user/user363627) (Quit: Konversation terminated!) |
| 2024-09-05 06:18:34 +0200 | weary-traveler | (~user@user/user363627) |
| 2024-09-05 06:21:38 +0200 | pounce | (~pounce@user/cute/pounce) (Ping timeout: 248 seconds) |
| 2024-09-05 06:23:13 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 2024-09-05 06:23:38 +0200 | weary-traveler | (~user@user/user363627) (Quit: Konversation terminated!) |
| 2024-09-05 06:23:54 +0200 | weary-traveler | (~user@user/user363627) |
| 2024-09-05 06:28:59 +0200 | weary-traveler | (~user@user/user363627) (Quit: Konversation terminated!) |
| 2024-09-05 06:29:14 +0200 | weary-traveler | (~user@user/user363627) |
| 2024-09-05 06:32:21 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 248 seconds) |
| 2024-09-05 06:34:17 +0200 | uli-fem | (~uli-fem@120.18.170.208) |
| 2024-09-05 06:34:18 +0200 | weary-traveler | (~user@user/user363627) (Quit: Konversation terminated!) |
| 2024-09-05 06:34:36 +0200 | weary-traveler | (~user@user/user363627) |
| 2024-09-05 06:34:50 +0200 | uli-fem | (~uli-fem@120.18.170.208) (Changing host) |
| 2024-09-05 06:34:50 +0200 | uli-fem | (~uli-fem@user/uli-fem) |
| 2024-09-05 06:35:51 +0200 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) |
| 2024-09-05 06:36:43 +0200 | weary-traveler | (~user@user/user363627) (Remote host closed the connection) |
| 2024-09-05 06:40:52 +0200 | sp1ff | (~user@c-73-11-70-111.hsd1.wa.comcast.net) (Write error: Connection reset by peer) |
| 2024-09-05 06:41:06 +0200 | sp1ff | (~user@c-73-11-70-111.hsd1.wa.comcast.net) |
| 2024-09-05 06:43:41 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 2024-09-05 06:47:57 +0200 | takuan | (~takuan@178-116-218-225.access.telenet.be) |
| 2024-09-05 06:48:24 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 246 seconds) |
| 2024-09-05 06:58:21 +0200 | michalz | (~michalz@185.246.207.205) |
| 2024-09-05 06:59:28 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 2024-09-05 07:04:20 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 255 seconds) |
| 2024-09-05 07:06:56 +0200 | zlqrvx | (~zlqrvx@user/zlqrvx) (Quit: %quit%) |
| 2024-09-05 07:07:19 +0200 | zlqrvx | (~zlqrvx@user/zlqrvx) |
| 2024-09-05 07:09:34 +0200 | uli-fem | (~uli-fem@user/uli-fem) (Quit: uli-fem) |
| 2024-09-05 07:11:57 +0200 | berberman | (~berberman@user/berberman) (Quit: ZNC 1.8.2 - https://znc.in) |
| 2024-09-05 07:12:34 +0200 | berberman | (~berberman@user/berberman) |
| 2024-09-05 07:15:16 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 2024-09-05 07:17:23 +0200 | euphores | (~SASL_euph@user/euphores) (Ping timeout: 255 seconds) |
| 2024-09-05 07:21:18 +0200 | mud | (~mud@user/kadoban) (Quit: quit) |
| 2024-09-05 07:22:28 +0200 | jle` | (~jle`@2603:8001:3b02:84d4:cf52:aad8:ec6d:eddd) (Ping timeout: 245 seconds) |
| 2024-09-05 07:23:47 +0200 | jle` | (~jle`@2603:8001:3b02:84d4:2fca:bfe0:41f4:4c2b) |
| 2024-09-05 07:24:17 +0200 | rosco | (~rosco@175.136.158.234) (Quit: Lost terminal) |
| 2024-09-05 07:24:19 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 260 seconds) |
| 2024-09-05 07:24:29 +0200 | euphores | (~SASL_euph@user/euphores) |
| 2024-09-05 07:25:03 +0200 | mud | (~mud@user/kadoban) |
| 2024-09-05 07:25:32 +0200 | crvs | (~crvs@c-a03ae555.016-99-73746f5.bbcust.telenor.se) |
| 2024-09-05 07:25:40 +0200 | euleritian | (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Read error: Connection reset by peer) |
| 2024-09-05 07:26:22 +0200 | euleritian | (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) |
| 2024-09-05 07:30:09 +0200 | Sgeo | (~Sgeo@user/sgeo) (Read error: Connection reset by peer) |
| 2024-09-05 07:33:09 +0200 | euleritian | (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Ping timeout: 248 seconds) |
| 2024-09-05 07:34:57 +0200 | misterfish | (~misterfis@84.53.85.146) (Ping timeout: 246 seconds) |
| 2024-09-05 07:35:51 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 2024-09-05 07:35:56 +0200 | euleritian | (~euleritia@dynamic-176-006-145-211.176.6.pool.telefonica.de) |
| 2024-09-05 07:41:43 +0200 | BA_Dragon | A_Dragon |
| 2024-09-05 07:42:06 +0200 | Artea | (~Lufia@2001:41d0:404:200::2d7) (Remote host closed the connection) |
| 2024-09-05 07:44:24 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 246 seconds) |
| 2024-09-05 07:56:01 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 2024-09-05 08:01:06 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 265 seconds) |
| 2024-09-05 08:02:09 +0200 | Axman6 | (~Axman6@user/axman6) (Ping timeout: 240 seconds) |
| 2024-09-05 08:03:14 +0200 | sord937 | (~sord937@gateway/tor-sasl/sord937) |
| 2024-09-05 08:07:46 +0200 | pounce | (~pounce@user/cute/pounce) |
| 2024-09-05 08:10:31 +0200 | rosco | (~rosco@175.136.158.234) |
| 2024-09-05 08:11:49 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 2024-09-05 08:16:35 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 244 seconds) |
| 2024-09-05 08:18:54 +0200 | acidjnk_new | (~acidjnk@p200300d6e72cfb86616a3f2ff56a8996.dip0.t-ipconnect.de) |
| 2024-09-05 08:21:03 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 2024-09-05 08:25:53 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 244 seconds) |
| 2024-09-05 08:26:15 +0200 | ubert | (~Thunderbi@178.165.175.79.wireless.dyn.drei.com) |
| 2024-09-05 08:30:36 +0200 | ubert | (~Thunderbi@178.165.175.79.wireless.dyn.drei.com) (Ping timeout: 246 seconds) |
| 2024-09-05 08:31:35 +0200 | hsw | (~hsw@2001-b030-2303-0104-0172-0025-0012-0132.hinet-ip6.hinet.net) |
| 2024-09-05 08:32:38 +0200 | ubert | (~Thunderbi@178.165.175.79.wireless.dyn.drei.com) |
| 2024-09-05 08:36:49 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 2024-09-05 08:36:54 +0200 | ubert | (~Thunderbi@178.165.175.79.wireless.dyn.drei.com) (Ping timeout: 246 seconds) |
| 2024-09-05 08:37:52 +0200 | Axman6 | (~Axman6@user/axman6) |
| 2024-09-05 08:39:23 +0200 | euleritian | (~euleritia@dynamic-176-006-145-211.176.6.pool.telefonica.de) (Read error: Connection reset by peer) |
| 2024-09-05 08:39:41 +0200 | euleritian | (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) |
| 2024-09-05 08:41:27 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 246 seconds) |
| 2024-09-05 08:43:35 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 2024-09-05 08:45:51 +0200 | mikess | (~mikess@user/mikess) (Ping timeout: 276 seconds) |
| 2024-09-05 08:46:14 +0200 | lortabac | (~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) |
| 2024-09-05 08:48:21 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 248 seconds) |
| 2024-09-05 08:52:31 +0200 | Axman3650 | (~Axman6@user/axman6) |
| 2024-09-05 08:54:31 +0200 | Axman6 | (~Axman6@user/axman6) (Ping timeout: 246 seconds) |
| 2024-09-05 08:57:41 +0200 | misterfish | (~misterfis@87.215.131.102) |
| 2024-09-05 08:57:54 +0200 | ft | (~ft@p4fc2a393.dip0.t-ipconnect.de) (Quit: leaving) |
| 2024-09-05 08:58:59 +0200 | euleritian | (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Ping timeout: 260 seconds) |
| 2024-09-05 08:59:18 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 2024-09-05 09:00:42 +0200 | euleritian | (~euleritia@dynamic-176-006-145-211.176.6.pool.telefonica.de) |
| 2024-09-05 09:04:42 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 276 seconds) |
| 2024-09-05 09:09:09 +0200 | ash3en | (~Thunderbi@2a01:c23:8c51:9600:3168:7de0:ad26:7330) |
| 2024-09-05 09:10:51 +0200 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 246 seconds) |
| 2024-09-05 09:15:05 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 2024-09-05 09:18:09 +0200 | riatre | (~quassel@2001:310:6000:f::5198:1) (Ping timeout: 248 seconds) |
| 2024-09-05 09:20:22 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 272 seconds) |
| 2024-09-05 09:30:12 +0200 | ash3en | (~Thunderbi@2a01:c23:8c51:9600:3168:7de0:ad26:7330) (Quit: ash3en) |
| 2024-09-05 09:34:42 +0200 | ash3en | (~Thunderbi@2a01:c23:8c51:9600:3168:7de0:ad26:7330) |
| 2024-09-05 09:39:45 +0200 | Guest84 | (~Guest37@159.146.64.69) |
| 2024-09-05 09:42:25 +0200 | Guest84 | (~Guest37@159.146.64.69) (Client Quit) |
| 2024-09-05 09:48:59 +0200 | fn_lumi | (3d621153a5@2a03:6000:1812:100::df7) (Ping timeout: 260 seconds) |
| 2024-09-05 09:49:34 +0200 | flukiluke | (~m-7humut@2603:c023:c000:6c7e:8945:ad24:9113:a962) (Ping timeout: 260 seconds) |
| 2024-09-05 09:49:34 +0200 | shawwwn | (sid6132@id-6132.helmsley.irccloud.com) (Ping timeout: 260 seconds) |
| 2024-09-05 09:49:34 +0200 | edwardk | (sid47016@haskell/developer/edwardk) (Ping timeout: 260 seconds) |
| 2024-09-05 09:49:56 +0200 | flukiluke | (~m-7humut@2603:c023:c000:6c7e:8945:ad24:9113:a962) |
| 2024-09-05 09:50:09 +0200 | [exa] | (~exa@user/exa/x-3587197) (Ping timeout: 260 seconds) |
| 2024-09-05 09:50:09 +0200 | rembo10 | (~rembo10@main.remulis.com) (Ping timeout: 260 seconds) |
| 2024-09-05 09:50:09 +0200 | liskin | (~liskin@xmonad/liskin) (Ping timeout: 260 seconds) |
| 2024-09-05 09:50:31 +0200 | [exa] | (~exa@2001:15e8:110:7d00::117) |
| 2024-09-05 09:50:35 +0200 | rembo10 | (~rembo10@main.remulis.com) |
| 2024-09-05 09:50:44 +0200 | degraafk | (sid71464@id-71464.lymington.irccloud.com) (Ping timeout: 260 seconds) |
| 2024-09-05 09:50:44 +0200 | delyan_ | (sid523379@id-523379.hampstead.irccloud.com) (Ping timeout: 260 seconds) |
| 2024-09-05 09:50:44 +0200 | kitaleth | (23bd17ddc6@sourcehut/user/alethkit) (Ping timeout: 260 seconds) |
| 2024-09-05 09:50:44 +0200 | aniketd | (32aa4844cd@2a03:6000:1812:100::dcb) (Ping timeout: 260 seconds) |
| 2024-09-05 09:50:44 +0200 | caasih | (sid13241@id-13241.ilkley.irccloud.com) (Ping timeout: 260 seconds) |
| 2024-09-05 09:50:44 +0200 | bjs | (sid190364@user/bjs) (Ping timeout: 260 seconds) |
| 2024-09-05 09:50:44 +0200 | jackdk | (sid373013@cssa/jackdk) (Ping timeout: 260 seconds) |
| 2024-09-05 09:51:43 +0200 | liskin | (~liskin@xmonad/liskin) |
| 2024-09-05 09:51:53 +0200 | aniketd | (32aa4844cd@2a03:6000:1812:100::dcb) |
| 2024-09-05 09:52:27 +0200 | edwardk | (sid47016@haskell/developer/edwardk) |
| 2024-09-05 09:52:32 +0200 | shawwwn | (sid6132@helmsley.irccloud.com) |
| 2024-09-05 09:52:54 +0200 | jackdk | (sid373013@cssa/jackdk) |
| 2024-09-05 09:53:19 +0200 | caasih | (sid13241@id-13241.ilkley.irccloud.com) |
| 2024-09-05 09:53:40 +0200 | gmg | (~user@user/gehmehgeh) (Quit: Leaving) |
| 2024-09-05 09:53:52 +0200 | delyan_ | (sid523379@id-523379.hampstead.irccloud.com) |
| 2024-09-05 09:53:56 +0200 | degraafk | (sid71464@id-71464.lymington.irccloud.com) |
| 2024-09-05 09:54:38 +0200 | bjs | (sid190364@user/bjs) |
| 2024-09-05 09:55:11 +0200 | sourcetarius | (~sourcetar@user/sourcetarius) |
| 2024-09-05 09:55:24 +0200 | kuribas | (~user@ip-188-118-57-242.reverse.destiny.be) |
| 2024-09-05 09:55:40 +0200 | [exa] | (~exa@2001:15e8:110:7d00::117) (Changing host) |
| 2024-09-05 09:55:40 +0200 | [exa] | (~exa@user/exa/x-3587197) |
| 2024-09-05 09:57:48 +0200 | machinedgod | (~machinedg@d50-99-47-73.abhsia.telus.net) |
| 2024-09-05 09:58:14 +0200 | ubert | (~Thunderbi@2001:871:263:9b13:379:6815:ba4a:300c) |
| 2024-09-05 10:00:58 +0200 | merijn | (~merijn@77.242.116.146) |
| 2024-09-05 10:03:16 +0200 | kitaleth | (23bd17ddc6@sourcehut/user/alethkit) |
| 2024-09-05 10:06:37 +0200 | uli-fem | (~lambdapin@user/uli-fem) |
| 2024-09-05 10:07:42 +0200 | fn_lumi | (3d621153a5@2a03:6000:1812:100::df7) |
| 2024-09-05 10:09:04 +0200 | Artea | (~Lufia@vps.artea.ovh) |
| 2024-09-05 10:13:08 +0200 | benjaminl_ | (~benjaminl@c-76-144-12-233.hsd1.or.comcast.net) |
| 2024-09-05 10:14:04 +0200 | benjaminl | (~benjaminl@user/benjaminl) (Ping timeout: 260 seconds) |
| 2024-09-05 10:17:43 +0200 | gmg | (~user@user/gehmehgeh) |
| 2024-09-05 10:22:16 +0200 | gmg | (~user@user/gehmehgeh) (Client Quit) |
| 2024-09-05 10:24:12 +0200 | euleritian | (~euleritia@dynamic-176-006-145-211.176.6.pool.telefonica.de) (Read error: Connection reset by peer) |
| 2024-09-05 10:24:29 +0200 | euleritian | (~euleritia@77.22.252.56) |
| 2024-09-05 10:30:22 +0200 | mesaoptimizer | (~mesaoptim@user/PapuaHardyNet) (Quit: mesaoptimizer) |
| 2024-09-05 10:30:30 +0200 | mesaoptimizer | (~mesaoptim@user/PapuaHardyNet) |
| 2024-09-05 10:42:49 +0200 | gmg | (~user@user/gehmehgeh) |
| 2024-09-05 10:46:32 +0200 | Luj9 | (~Luj@2a01:e0a:de4:a0e1:be24:11ff:febc:b5b5) (Quit: The Lounge - https://thelounge.chat) |
| 2024-09-05 10:47:10 +0200 | __monty__ | (~toonn@user/toonn) |
| 2024-09-05 10:47:14 +0200 | tzh | (~tzh@c-76-115-131-146.hsd1.or.comcast.net) (Quit: zzz) |
| 2024-09-05 10:47:17 +0200 | Luj9 | (~Luj@2a01:e0a:de4:a0e1:be24:11ff:febc:b5b5) |
| 2024-09-05 10:51:53 +0200 | chele | (~chele@user/chele) |
| 2024-09-05 10:51:58 +0200 | merijn | (~merijn@77.242.116.146) (Ping timeout: 252 seconds) |
| 2024-09-05 10:52:35 +0200 | merijn | (~merijn@77.242.116.146) |
| 2024-09-05 10:57:36 +0200 | Square2 | (~Square4@user/square) (Ping timeout: 246 seconds) |
| 2024-09-05 11:07:00 +0200 | merijn | (~merijn@77.242.116.146) (Ping timeout: 252 seconds) |
| 2024-09-05 11:11:16 +0200 | srazkvt | (~sarah@user/srazkvt) |
| 2024-09-05 11:12:11 +0200 | merijn | (~merijn@77.242.116.146) |
| 2024-09-05 11:18:49 +0200 | euleritian | (~euleritia@77.22.252.56) (Ping timeout: 260 seconds) |
| 2024-09-05 11:21:19 +0200 | euleritian | (~euleritia@dynamic-176-006-145-211.176.6.pool.telefonica.de) |
| 2024-09-05 11:23:45 +0200 | euleritian | (~euleritia@dynamic-176-006-145-211.176.6.pool.telefonica.de) (Read error: Connection reset by peer) |
| 2024-09-05 11:24:02 +0200 | euleritian | (~euleritia@77.22.252.56) |
| 2024-09-05 11:44:24 +0200 | <yin> | SSFFC - Sport System F Football Club |
| 2024-09-05 11:45:02 +0200 | ZharMeny | (~ZharMeny@user/ZharMeny) |
| 2024-09-05 11:45:17 +0200 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 2024-09-05 11:46:25 +0200 | ash3en | (~Thunderbi@2a01:c23:8c51:9600:3168:7de0:ad26:7330) (Ping timeout: 248 seconds) |
| 2024-09-05 11:48:36 +0200 | sawilagar | (~sawilagar@user/sawilagar) |
| 2024-09-05 11:59:06 +0200 | comerijn | (~merijn@77.242.116.146) |
| 2024-09-05 12:01:14 +0200 | ubert | (~Thunderbi@2001:871:263:9b13:379:6815:ba4a:300c) (Ping timeout: 272 seconds) |
| 2024-09-05 12:01:59 +0200 | merijn | (~merijn@77.242.116.146) (Ping timeout: 260 seconds) |
| 2024-09-05 12:04:44 +0200 | sourcetarius | (~sourcetar@user/sourcetarius) (Quit: nyaa~) |
| 2024-09-05 12:07:49 +0200 | troydm | (~troydm@user/troydm) (Ping timeout: 248 seconds) |
| 2024-09-05 12:14:30 +0200 | comerijn | (~merijn@77.242.116.146) (Ping timeout: 276 seconds) |
| 2024-09-05 12:20:44 +0200 | EarlPitts | (~EarlPitts@2E8B7DD6.catv.pool.telekom.hu) |
| 2024-09-05 12:21:15 +0200 | ZharMeny | (~ZharMeny@user/ZharMeny) (Ping timeout: 246 seconds) |
| 2024-09-05 12:21:40 +0200 | ubert | (~Thunderbi@2001:871:263:9b13:239d:e071:1867:e9a4) |
| 2024-09-05 12:25:51 +0200 | merijn | (~merijn@77.242.116.146) |
| 2024-09-05 12:30:21 +0200 | merijn | (~merijn@77.242.116.146) (Ping timeout: 246 seconds) |
| 2024-09-05 12:33:21 +0200 | alexherbo2 | (~alexherbo@2a02-8440-321a-7a79-610a-a4c2-c600-890e.rev.sfr.net) |
| 2024-09-05 12:36:58 +0200 | merijn | (~merijn@77.242.116.146) |
| 2024-09-05 12:38:48 +0200 | Smiles | (uid551636@id-551636.lymington.irccloud.com) |
| 2024-09-05 12:43:35 +0200 | <apache2> | 40 |
| 2024-09-05 12:46:08 +0200 | <ski> | 65 |
| 2024-09-05 12:46:39 +0200 | <Rembane> | 90 |
| 2024-09-05 12:51:31 +0200 | <Maxdamantus> | That's numberwang. |
| 2024-09-05 12:54:44 +0200 | laxmik | (~laxmik@85-193-3-200.rib.o2.cz) |
| 2024-09-05 12:57:21 +0200 | laxmik | (~laxmik@85-193-3-200.rib.o2.cz) (Client Quit) |
| 2024-09-05 12:57:44 +0200 | uli-fem | (~lambdapin@user/uli-fem) (Ping timeout: 252 seconds) |
| 2024-09-05 13:04:33 +0200 | poscat0x04 | (~poscat@user/poscat) (Quit: Bye) |
| 2024-09-05 13:08:51 +0200 | poscat | (~poscat@user/poscat) |
| 2024-09-05 13:42:53 +0200 | CrunchyFlakes | (~CrunchyFl@31.18.102.35) (Quit: ZNC 1.8.2 - https://znc.in) |
| 2024-09-05 13:47:00 +0200 | CrunchyFlakes | (~CrunchyFl@31.18.102.35) |
| 2024-09-05 14:06:36 +0200 | ubert | (~Thunderbi@2001:871:263:9b13:239d:e071:1867:e9a4) (Ping timeout: 246 seconds) |
| 2024-09-05 14:06:37 +0200 | alexherbo2 | (~alexherbo@2a02-8440-321a-7a79-610a-a4c2-c600-890e.rev.sfr.net) (Remote host closed the connection) |
| 2024-09-05 14:06:57 +0200 | alexherbo2 | (~alexherbo@2a02-8440-321a-7a79-610a-a4c2-c600-890e.rev.sfr.net) |
| 2024-09-05 14:12:19 +0200 | <albet70> | is there a function can get the most matched item from a list, like f [1,2,5] [[1,3,6], [1,7], [1,2,3,5]] == [1,2,3,5]? |
| 2024-09-05 14:18:40 +0200 | <Leary> | > (find . isSubsequenceOf) [1,2,5] [[1,3,6], [1,7], [1,2,3,5]] |
| 2024-09-05 14:18:41 +0200 | <lambdabot> | Just [1,2,3,5] |
| 2024-09-05 14:18:56 +0200 | <mauke> | define "most matched"? |
| 2024-09-05 14:20:05 +0200 | <albet70> | have the most common elements |
| 2024-09-05 14:20:18 +0200 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 2024-09-05 14:20:52 +0200 | <albet70> | find the sublist within a list of sublists that has the most elements in common with a given list |
| 2024-09-05 14:21:26 +0200 | <mauke> | are all sublists sorted? |
| 2024-09-05 14:21:37 +0200 | <albet70> | no |
| 2024-09-05 14:22:36 +0200 | <Rembane> | It sounds a bit like this problem: https://en.wikipedia.org/wiki/Longest_common_substring |
| 2024-09-05 14:22:52 +0200 | <mauke> | oh, does the order of elements matter? |
| 2024-09-05 14:24:33 +0200 | <albet70> | no |
| 2024-09-05 14:25:35 +0200 | <mauke> | then it might be easiest to just convert everything to sets |
| 2024-09-05 14:26:39 +0200 | solution | (~Solution@78-131-74-26.pool.digikabel.hu) (Ping timeout: 260 seconds) |
| 2024-09-05 14:27:38 +0200 | ash3en | (~Thunderbi@2a01:c23:8c51:9600:3168:7de0:ad26:7330) |
| 2024-09-05 14:27:58 +0200 | solution | (~Solution@78-131-74-9.pool.digikabel.hu) |
| 2024-09-05 14:29:25 +0200 | <mauke> | > let set = Data.Set.fromList; foo (set -> p) = maximumBy (comparing (Data.Set.size . Data.Set.intersection p . set)) in foo [1,2,5] [[1,3,6], [1,7], [1,2,3,5]] |
| 2024-09-05 14:29:26 +0200 | <lambdabot> | [1,2,3,5] |
| 2024-09-05 14:30:13 +0200 | <mauke> | > let set = Data.Set.fromList; foo (set -> p) = maximumBy (comparing (Data.Set.size . Data.Set.intersection p . set)) in "celery" (words "the quick brown fox jumps over the lazy dog") |
| 2024-09-05 14:30:15 +0200 | <lambdabot> | error: |
| 2024-09-05 14:30:15 +0200 | <lambdabot> | • Couldn't match expected type ‘[String] -> t’ |
| 2024-09-05 14:30:15 +0200 | <lambdabot> | with actual type ‘[Char]’ |
| 2024-09-05 14:30:23 +0200 | <mauke> | > let set = Data.Set.fromList; foo (set -> p) = maximumBy (comparing (Data.Set.size . Data.Set.intersection p . set)) in foo "celery" (words "the quick brown fox jumps over the lazy dog") |
| 2024-09-05 14:30:24 +0200 | <lambdabot> | "lazy" |
| 2024-09-05 14:39:28 +0200 | sawilagar | (~sawilagar@user/sawilagar) (Remote host closed the connection) |
| 2024-09-05 14:39:50 +0200 | sawilagar | (~sawilagar@user/sawilagar) |
| 2024-09-05 14:41:03 +0200 | ZharMeny | (~ZharMeny@user/ZharMeny) |
| 2024-09-05 14:43:24 +0200 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 2024-09-05 14:57:34 +0200 | sawilagar | (~sawilagar@user/sawilagar) (Ping timeout: 260 seconds) |
| 2024-09-05 14:57:55 +0200 | Smiles | (uid551636@id-551636.lymington.irccloud.com) (Quit: Connection closed for inactivity) |
| 2024-09-05 15:03:19 +0200 | sawilagar | (~sawilagar@user/sawilagar) |
| 2024-09-05 15:12:27 +0200 | quack | (~quack@209.60-130-109.adsl-dyn.isp.belgacom.be) |
| 2024-09-05 15:13:55 +0200 | weary-traveler | (~user@user/user363627) |
| 2024-09-05 15:14:32 +0200 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Read error: Connection reset by peer) |
| 2024-09-05 15:15:16 +0200 | <quack> | Hello, I'm trying to understand better what the exact rules are for evaluating thunks, e.g. consider: |
| 2024-09-05 15:15:17 +0200 | <quack> | f (0, 1) = 0 |
| 2024-09-05 15:15:18 +0200 | <quack> | f (x, 2) = 1 |
| 2024-09-05 15:15:38 +0200 | <quack> | If you then evaluate f (undefined, 2) you get an exception |
| 2024-09-05 15:15:51 +0200 | <quack> | but if you have: |
| 2024-09-05 15:15:53 +0200 | <quack> | g (1, 0) = 0 |
| 2024-09-05 15:15:54 +0200 | <quack> | g (2, x) = 1 |
| 2024-09-05 15:16:28 +0200 | <quack> | Then g (2, undefined) gives 2, which implies that pattern matching runs from left to right, but I'm not sure if that is accurate? |
| 2024-09-05 15:17:25 +0200 | lortabac | (~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) (Quit: WeeChat 4.2.2) |
| 2024-09-05 15:21:00 +0200 | <EvanR> | > let f (x, 2) = 1 in f (undefined, 2) |
| 2024-09-05 15:21:02 +0200 | <lambdabot> | 1 |
| 2024-09-05 15:21:05 +0200 | <EvanR> | no exception |
| 2024-09-05 15:21:45 +0200 | <EvanR> | you might be thinking of |
| 2024-09-05 15:22:02 +0200 | athan | (~athan@syn-098-153-145-140.biz.spectrum.com) |
| 2024-09-05 15:22:25 +0200 | <EvanR> | > let f (False, False) = 2 in f (error "A", error "B") |
| 2024-09-05 15:22:27 +0200 | <lambdabot> | *Exception: A |
| 2024-09-05 15:22:28 +0200 | <ski> | matching `undefied' with `0' doesn't succeed |
| 2024-09-05 15:22:32 +0200 | <ncf> | > let f (0, 1) = 0; f (x, 2) = 1 in f (undefined, 2) |
| 2024-09-05 15:22:34 +0200 | <lambdabot> | *Exception: Prelude.undefined |
| 2024-09-05 15:22:40 +0200 | <ncf> | you need both lines |
| 2024-09-05 15:22:49 +0200 | <ski> | and yes, matching constructor components from left to right |
| 2024-09-05 15:22:53 +0200 | <EvanR> | in this case, the error you get is technically arbitrary, not left to right |
| 2024-09-05 15:22:54 +0200 | ash3en | (~Thunderbi@2a01:c23:8c51:9600:3168:7de0:ad26:7330) (Ping timeout: 246 seconds) |
| 2024-09-05 15:23:14 +0200 | <quack> | ski: matching left from right is guaranteed? |
| 2024-09-05 15:23:22 +0200 | <EvanR> | no? |
| 2024-09-05 15:23:41 +0200 | <EvanR> | in the absence of competing exceptions, you can't tell |
| 2024-09-05 15:23:41 +0200 | <ncf> | > The matching process itself occurs "top-down, left-to-right." |
| 2024-09-05 15:23:43 +0200 | <lambdabot> | error: |
| 2024-09-05 15:23:43 +0200 | <lambdabot> | Data constructor not in scope: |
| 2024-09-05 15:23:43 +0200 | <lambdabot> | The |
| 2024-09-05 15:23:43 +0200 | <ncf> | seems like it |
| 2024-09-05 15:23:53 +0200 | <quack> | > let g (1, 0) = 0; g (2, x) = 1 in g (2, undefined) |
| 2024-09-05 15:23:54 +0200 | <lambdabot> | 1 |
| 2024-09-05 15:24:08 +0200 | ncf | (~n@monade.li) (Fairfarren.) |
| 2024-09-05 15:24:09 +0200 | <ski> | pretty sure you get the appearance of that. the implementation may decide to do a different order in actuality, if it can show it gives the same result |
| 2024-09-05 15:24:12 +0200 | ncf | (~n@monade.li) |
| 2024-09-05 15:24:17 +0200 | <ncf> | ≫ For example, if [1,2] is matched against [0,bot], then 1 fails to match 0, so the result is a failed match. (Recall that bot, defined earlier, is a variable bound to _|_.) But if [1,2] is matched against [bot,0], then matching 1 against bot causes divergence (i.e. _|_). |
| 2024-09-05 15:24:21 +0200 | <EvanR> | the compiler will rearrange your high level code into something hard to recognize, and it can choose which order to match in as long as the semantics are respected |
| 2024-09-05 15:25:00 +0200 | <[exa]> | quack: this might be an interesting read, IIRC the order is specified there: https://www.haskell.org/onlinereport/haskell2010/haskellch3.html#x8-580003.17 |
| 2024-09-05 15:25:18 +0200 | <dminuoso> | top-to-bottom, left-to-right is indeed a good first approximation of case-of expressions. |
| 2024-09-05 15:25:20 +0200 | <[exa]> | (section 3.17.2, list item 5, bullet 1) |
| 2024-09-05 15:26:02 +0200 | <dminuoso> | It of course becomes more complicated since it depends on whether patterns are refutable or not, lazy or not, strictness annotations |
| 2024-09-05 15:26:21 +0200 | <ncf> | EvanR: this sounds like the exact kind of thing the compiler isn't allowed to do if it changes the semantics |
| 2024-09-05 15:26:31 +0200 | ystael | (~ystael@user/ystael) |
| 2024-09-05 15:26:33 +0200 | <ncf> | do you have an example? |
| 2024-09-05 15:26:36 +0200 | <dminuoso> | (Note that case-of is valid since the haskell report specifies that multiple-function-definitions are equivalent/desugared into case-of |
| 2024-09-05 15:26:43 +0200 | <EvanR> | ncf, what semantics are being changed? |
| 2024-09-05 15:26:52 +0200 | <EvanR> | which competing exception wins? |
| 2024-09-05 15:26:55 +0200 | <EvanR> | that's undefined |
| 2024-09-05 15:27:04 +0200 | <ncf> | there are no competing exceptions here |
| 2024-09-05 15:27:05 +0200 | <dminuoso> | ncf: They explicitly said "as long as the semantics are respected" |
| 2024-09-05 15:27:05 +0200 | alexherbo2 | (~alexherbo@2a02-8440-321a-7a79-610a-a4c2-c600-890e.rev.sfr.net) (Remote host closed the connection) |
| 2024-09-05 15:27:22 +0200 | <dminuoso> | I mean compilers generally live under the as-if rule. If you cant tell differently, it does not matter. :p |
| 2024-09-05 15:27:23 +0200 | <ncf> | well changing the order of the pattern matching wouldn't respect the semantics! |
| 2024-09-05 15:27:24 +0200 | alexherbo2 | (~alexherbo@2a02-8440-321a-7a79-610a-a4c2-c600-890e.rev.sfr.net) |
| 2024-09-05 15:27:24 +0200 | <EvanR> | otherwise you can't observe the order that things are pattern matched in |
| 2024-09-05 15:27:32 +0200 | <dminuoso> | ncf: depends on whether you can tell or not. |
| 2024-09-05 15:27:35 +0200 | <ski> | having `True || _ = True; _ || True = True; _ || _ = False' give you both `True || undefined' and `undefined || True' evaluating to `True' is called "parallel OR", is a common non-sequential example in denotational semantics |
| 2024-09-05 15:28:21 +0200 | <quack> | [exa]: thanks, I missed that on my first skim |
| 2024-09-05 15:29:09 +0200 | <EvanR> | other than exceptions, the only reason you want to "know" the order (as if the code you wrote is literally being executed as written), is to game the performance. But that seems hard for a complex pattern |
| 2024-09-05 15:29:19 +0200 | <EvanR> | the answers come out the same |
| 2024-09-05 15:29:48 +0200 | zmt01 | (~zmt00@user/zmt00) |
| 2024-09-05 15:29:53 +0200 | <dminuoso> | EvanR: Not necessarily, given infinite data structures it may be necessary to understand evaluation order. |
| 2024-09-05 15:30:06 +0200 | <quack> | EvanR: it's not for performance but to know whether evaluation will throw an exception. Right now f throws and g succeeds, but if the order were right to left then f would succeed and g throw |
| 2024-09-05 15:30:09 +0200 | <dminuoso> | Especially with recursive structure. |
| 2024-09-05 15:30:36 +0200 | EarlPitts | (~EarlPitts@2E8B7DD6.catv.pool.telekom.hu) (Remote host closed the connection) |
| 2024-09-05 15:30:48 +0200 | <ski> | (or TyingTheKnot) |
| 2024-09-05 15:30:57 +0200 | EarlPitts | (~EarlPitts@2E8B7DD6.catv.pool.telekom.hu) |
| 2024-09-05 15:31:12 +0200 | <EvanR> | how do you have an infinite pattern |
| 2024-09-05 15:31:39 +0200 | <EvanR> | quack, yes so back to your original question, you were mistaken about f throwing an exception at all |
| 2024-09-05 15:31:45 +0200 | <EvanR> | it doesn't |
| 2024-09-05 15:32:02 +0200 | <quack> | It does? ncf showed it |
| 2024-09-05 15:32:03 +0200 | <quack> | > let f (0, 1) = 0; f (x, 2) = 1 in f (undefined, 2) |
| 2024-09-05 15:32:05 +0200 | <lambdabot> | *Exception: Prelude.undefined |
| 2024-09-05 15:32:14 +0200 | <EvanR> | oh |
| 2024-09-05 15:32:23 +0200 | <EvanR> | yes the first definition will be pattern matched first, that's true |
| 2024-09-05 15:32:29 +0200 | <ncf> | ...yes |
| 2024-09-05 15:32:42 +0200 | <EvanR> | I was arguing about whether x or 2 is matched first |
| 2024-09-05 15:32:49 +0200 | <ski> | (strictly speaking, the argument `undefined' is to be blamed for throwing, not `f' itself) |
| 2024-09-05 15:33:24 +0200 | zmt00 | (~zmt00@user/zmt00) (Ping timeout: 276 seconds) |
| 2024-09-05 15:33:55 +0200 | <ski> | (Racket has a blame-tracking system, with contracts, to determine who's to blame, especially re higher-order procedures (so accepting callbacks), when a contract is broken) |
| 2024-09-05 15:37:52 +0200 | <fr33domlover> | o/ I defined a type named Schema, and now I'd like to write a typeclass @Message@, where for a given @m@ there's a type family @FromSchema (s :: Schema) :: m@ and a type family @ToSchema (x :: m) :: (Maybe Schema)@ |
| 2024-09-05 15:38:17 +0200 | <fr33domlover> | How do I do that? It seems like I need type-level type-families, which don't exist (yet)? |
| 2024-09-05 15:39:34 +0200 | quack | (~quack@209.60-130-109.adsl-dyn.isp.belgacom.be) (Quit: Client closed) |
| 2024-09-05 15:40:32 +0200 | <EvanR> | fromSchema :: Schema -> m, toSchema :: m -> Maybe Schema, as methods on the type class? |
| 2024-09-05 15:41:17 +0200 | <fr33domlover> | But that's value level :) I have an idea for a workaround /me tries in GHCi 1 sec |
| 2024-09-05 15:45:07 +0200 | ubert | (~Thunderbi@2001:871:263:9b13:c5fe:c84e:4781:2c20) |
| 2024-09-05 15:46:23 +0200 | <fr33domlover> | Here's code and error from GHC: http://paste.debian.net/1328521/ |
| 2024-09-05 15:46:43 +0200 | <fr33domlover> | Workaround is failing :p |
| 2024-09-05 15:47:44 +0200 | benjaminl_ | (~benjaminl@c-76-144-12-233.hsd1.or.comcast.net) (Ping timeout: 260 seconds) |
| 2024-09-05 15:48:54 +0200 | Smiles | (uid551636@id-551636.lymington.irccloud.com) |
| 2024-09-05 15:48:55 +0200 | benjaminl | (~benjaminl@user/benjaminl) |
| 2024-09-05 15:49:37 +0200 | <EvanR> | type Msg c just by itself with no annotation or definition? |
| 2024-09-05 15:50:40 +0200 | <ski> | fr33domlover : wondering whether breaking into a super- and sub- class would help |
| 2024-09-05 15:58:24 +0200 | <fr33domlover> | ski: It helped but there's a new error http://paste.debian.net/1328524/ |
| 2024-09-05 15:58:30 +0200 | athan | (~athan@syn-098-153-145-140.biz.spectrum.com) (Ping timeout: 252 seconds) |
| 2024-09-05 16:00:08 +0200 | <fr33domlover> | I tried adding (Msg X ~ Msgx) as a constraint to the instance, but got same errors |
| 2024-09-05 16:05:02 +0200 | <ski> | fr33domlover : tried injectivity on `Msg' ? |
| 2024-09-05 16:06:05 +0200 | <ski> | (dunno if it's what it's complaining about, but it's what i could think to try) |
| 2024-09-05 16:12:00 +0200 | <fr33domlover> | Yes, it didn't help. But I just tried moving the FromPat case-handling into an external type family and the code builds now ^_^ |
| 2024-09-05 16:17:12 +0200 | alexherbo2 | (~alexherbo@2a02-8440-321a-7a79-610a-a4c2-c600-890e.rev.sfr.net) (Remote host closed the connection) |
| 2024-09-05 16:17:28 +0200 | <fr33domlover> | It's sooo weird, moving just FromPat is enough for GHCi to accept the code; but if FromPat and ToPat are in different typeclasses, they both need to use helper standalone families |
| 2024-09-05 16:17:39 +0200 | <fr33domlover> | Oh well at least I found a way to make it work |
| 2024-09-05 16:18:23 +0200 | alexherbo2 | (~alexherbo@2a02-8440-321a-7a79-241e-13ab-7d87-53f9.rev.sfr.net) |
| 2024-09-05 16:18:57 +0200 | lol_ | (~lol@2603:3016:1e01:b960:4840:2ad9:7736:e7f5) |
| 2024-09-05 16:21:51 +0200 | alexherbo2 | (~alexherbo@2a02-8440-321a-7a79-241e-13ab-7d87-53f9.rev.sfr.net) (Remote host closed the connection) |
| 2024-09-05 16:22:54 +0200 | jcarpenter2 | (~lol@2603:3016:1e01:b960:f4ac:a003:2d11:ead1) (Ping timeout: 260 seconds) |
| 2024-09-05 16:22:56 +0200 | ash3en | (~Thunderbi@2a01:c23:8c51:9600:3168:7de0:ad26:7330) |
| 2024-09-05 16:30:56 +0200 | justsomeguy | (~justsomeg@user/justsomeguy) |
| 2024-09-05 16:32:39 +0200 | Sgeo | (~Sgeo@user/sgeo) |
| 2024-09-05 16:36:22 +0200 | lol_ | jcarpenter2 |
| 2024-09-05 16:40:28 +0200 | athan | (~athan@2600:382:2d15:de3c:7342:aa0b:1e24:3f2d) |
| 2024-09-05 16:42:18 +0200 | Tuplanolla | (~Tuplanoll@91-159-69-59.elisa-laajakaista.fi) |
| 2024-09-05 16:45:04 +0200 | <haskellbridge> | <thirdofmay18081814goya> "data NatOrBool = Nat | Bool" |
| 2024-09-05 16:45:25 +0200 | <haskellbridge> | <thirdofmay18081814goya> system F can't model this, wasn't a model able to model this? |
| 2024-09-05 16:45:35 +0200 | <haskellbridge> | <thirdofmay18081814goya> what's a model able to model this* |
| 2024-09-05 16:47:14 +0200 | <ski> | presumably you're looking for some kind of subtyping |
| 2024-09-05 16:52:38 +0200 | ubert | (~Thunderbi@2001:871:263:9b13:c5fe:c84e:4781:2c20) (Quit: ubert) |
| 2024-09-05 16:56:00 +0200 | misterfish | (~misterfis@87.215.131.102) (Ping timeout: 246 seconds) |
| 2024-09-05 16:57:56 +0200 | <tomsmeding> | typescript has union types |
| 2024-09-05 16:58:06 +0200 | <tomsmeding> | python also does |
| 2024-09-05 16:58:14 +0200 | <tomsmeding> | to the extent that python "has types" |
| 2024-09-05 17:00:50 +0200 | <dminuoso> | tomsmeding: The one part that always makes me smile, is that python has "types" but comes with no type checker. |
| 2024-09-05 17:01:15 +0200 | <tomsmeding> | and multiple exist, and they are incompatible :) |
| 2024-09-05 17:01:34 +0200 | <dminuoso> | tomsmeding: At least that makes then true syntactic constructs in the sense of TaPL! |
| 2024-09-05 17:04:30 +0200 | <EvanR> | thirdofmay: an enum type? |
| 2024-09-05 17:05:48 +0200 | comerijn | (~merijn@77.242.116.146) |
| 2024-09-05 17:07:25 +0200 | <tomsmeding> | fr33domlover: odd, it works if Msg is a closed type family but not if it's an open one (and an associated type family is always open) |
| 2024-09-05 17:08:06 +0200 | <tomsmeding> | https://play.haskell.org/saved/pSxMC6lR |
| 2024-09-05 17:08:15 +0200 | merijn | (~merijn@77.242.116.146) (Ping timeout: 246 seconds) |
| 2024-09-05 17:09:10 +0200 | EarlPitts | (~EarlPitts@2E8B7DD6.catv.pool.telekom.hu) (Remote host closed the connection) |
| 2024-09-05 17:09:24 +0200 | <tomsmeding> | _wat_ |
| 2024-09-05 17:09:38 +0200 | <tomsmeding> | ok this is a ghc bug |
| 2024-09-05 17:09:56 +0200 | <EvanR> | vlad_, I swear by this, https://www.haskell.org/tutorial/ |
| 2024-09-05 17:10:50 +0200 | mikess | (~mikess@user/mikess) |
| 2024-09-05 17:11:12 +0200 | <tomsmeding> | fr33domlover: https://play.haskell.org/saved/ruULajDX |
| 2024-09-05 17:11:15 +0200 | <weary-traveler> | when multiple exist, they're usually not compatible. see also erlang type checkers |
| 2024-09-05 17:12:28 +0200 | <haskellbridge> | <thirdofmay18081814goya> hm typescript and python have them but they're really different to system F and derivatives |
| 2024-09-05 17:12:54 +0200 | <haskellbridge> | <thirdofmay18081814goya> I'm looking for something that could approximate the behaviour of "data NatOrBool = Nat | Bool" in haskell |
| 2024-09-05 17:13:01 +0200 | <haskellbridge> | <thirdofmay18081814goya> formally |
| 2024-09-05 17:13:08 +0200 | <EvanR> | that is just an enum type |
| 2024-09-05 17:13:18 +0200 | <EvanR> | equivalent to data Bool = True | False |
| 2024-09-05 17:13:33 +0200 | <EvanR> | which you can emulate using church encoding |
| 2024-09-05 17:13:50 +0200 | <[exa]> | I think it was more of `type NatOrBool = Bool | Nat` with some magickal | |
| 2024-09-05 17:14:11 +0200 | <haskellbridge> | <thirdofmay18081814goya> EvanR: wow i had totally misunderstood how that worked in haskell |
| 2024-09-05 17:14:17 +0200 | <haskellbridge> | <thirdofmay18081814goya> right ok, ty |
| 2024-09-05 17:14:18 +0200 | <EvanR> | \o/ |
| 2024-09-05 17:14:47 +0200 | <glguy> | tomsmeding: (yes, it's still a bug) You can define type Id a = a; and then Id (Msg X) works |
| 2024-09-05 17:15:39 +0200 | <tomsmeding> | glguy: where precisely? |
| 2024-09-05 17:15:49 +0200 | <tomsmeding> | my latest reduction is https://play.haskell.org/saved/VibtX2ah |
| 2024-09-05 17:16:10 +0200 | <tomsmeding> | surely the _location_ of the definition of X should not matter? |
| 2024-09-05 17:16:17 +0200 | <tomsmeding> | there's no TH here |
| 2024-09-05 17:17:39 +0200 | <glguy> | tomsmeding: Id (Msg X) in the type ascription - seemed to trick GHC into evaluating the expression |
| 2024-09-05 17:17:47 +0200 | <glguy> | yeah, location shouldn't matter |
| 2024-09-05 17:18:09 +0200 | Axman3650 | (~Axman6@user/axman6) (Ping timeout: 240 seconds) |
| 2024-09-05 17:18:24 +0200 | <tomsmeding> | oh I see |
| 2024-09-05 17:18:39 +0200 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 2024-09-05 17:18:44 +0200 | <tomsmeding> | glguy: do you happen to know if there's already an open issue about this? |
| 2024-09-05 17:19:10 +0200 | <glguy> | I don't |
| 2024-09-05 17:20:38 +0200 | <fr33domlover> | Feels like the boundaries where normal rules of physics cease to exist... :p |
| 2024-09-05 17:20:43 +0200 | srazkvt | (~sarah@user/srazkvt) (Remote host closed the connection) |
| 2024-09-05 17:21:02 +0200 | srazkvt | (~sarah@user/srazkvt) |
| 2024-09-05 17:22:36 +0200 | Axman6 | (~Axman6@user/axman6) |
| 2024-09-05 17:23:34 +0200 | <tomsmeding> | fr33domlover: mind if I mention your IRC nick in the GHC issue? |
| 2024-09-05 17:27:13 +0200 | comerijn | (~merijn@77.242.116.146) (Ping timeout: 252 seconds) |
| 2024-09-05 17:27:29 +0200 | justsomeguy | (~justsomeg@user/justsomeguy) (Ping timeout: 260 seconds) |
| 2024-09-05 17:28:55 +0200 | srazkvt | (~sarah@user/srazkvt) (Quit: Konversation terminated!) |
| 2024-09-05 17:29:03 +0200 | <fr33domlover> | tomsmeding: Go ahead (and of course feel free to paste my code too! So that if anyone has questions it will remind me what I was trying to do :P) |
| 2024-09-05 17:29:15 +0200 | <tomsmeding> | I did change some of the names |
| 2024-09-05 17:29:21 +0200 | <tomsmeding> | (in the code) |
| 2024-09-05 17:30:38 +0200 | <fr33domlover> | Cool. Soon I'll probably have the actual working code with more meaningful names (I'm implementing a type-level schema for parsing and encoding Preserves, a data model a bit like json/protobuf/etc. https://preserves.dev/ |
| 2024-09-05 17:30:39 +0200 | merijn | (~merijn@77.242.116.146) |
| 2024-09-05 17:33:04 +0200 | <tomsmeding> | fr33domlover glguy: https://gitlab.haskell.org/ghc/ghc/-/issues/25238 |
| 2024-09-05 17:34:08 +0200 | <vlad_> | ooh :help works in ghci |
| 2024-09-05 17:34:27 +0200 | <tomsmeding> | vlad_: https://downloads.haskell.org/ghc/latest/docs/users_guide/ghci.html#ghci-commands :p |
| 2024-09-05 17:35:40 +0200 | merijn | (~merijn@77.242.116.146) (Ping timeout: 252 seconds) |
| 2024-09-05 17:36:28 +0200 | <vlad_> | how do i examine a variable? |
| 2024-09-05 17:36:37 +0200 | <tomsmeding> | examine in what way? |
| 2024-09-05 17:36:42 +0200 | <vlad_> | like its type |
| 2024-09-05 17:36:45 +0200 | <tomsmeding> | :t |
| 2024-09-05 17:36:48 +0200 | <tomsmeding> | :t print |
| 2024-09-05 17:36:49 +0200 | <lambdabot> | Show a => a -> IO () |
| 2024-09-05 17:37:26 +0200 | <tomsmeding> | vlad_: there is also :i, which shows more info |
| 2024-09-05 17:37:49 +0200 | <tomsmeding> | (but :i works on individual names only, while :t takes an expression) |
| 2024-09-05 17:39:06 +0200 | L29Ah | (~L29Ah@wikipedia/L29Ah) () |
| 2024-09-05 17:40:55 +0200 | Guest38 | (~Guest38@194.183.191.121) |
| 2024-09-05 17:41:37 +0200 | Guest38 | (~Guest38@194.183.191.121) (Client Quit) |
| 2024-09-05 17:46:22 +0200 | rosco | (~rosco@175.136.158.234) (Quit: Lost terminal) |
| 2024-09-05 17:53:11 +0200 | justsomeguy | (~justsomeg@user/justsomeguy) |
| 2024-09-05 17:53:24 +0200 | nadja | (~dequbed@banana-new.kilobyte22.de) (Quit: bye!) |
| 2024-09-05 17:55:53 +0200 | <EvanR> | information on an arbitrary expression would be interesting ngl |
| 2024-09-05 17:58:33 +0200 | nadja | (~dequbed@banana-new.kilobyte22.de) |
| 2024-09-05 18:00:44 +0200 | EarlPitts | (~EarlPitts@20014C4C1C6E6700B93D810C58171531.catv.pool.telekom.hu) |
| 2024-09-05 18:00:58 +0200 | son0p | (~ff@191.104.26.195) (Ping timeout: 252 seconds) |
| 2024-09-05 18:04:08 +0200 | kuribas | (~user@ip-188-118-57-242.reverse.destiny.be) (Remote host closed the connection) |
| 2024-09-05 18:05:02 +0200 | <tomsmeding> | EvanR: what kind of info would you like :p |
| 2024-09-05 18:05:19 +0200 | EarlPitts | (~EarlPitts@20014C4C1C6E6700B93D810C58171531.catv.pool.telekom.hu) (Ping timeout: 256 seconds) |
| 2024-09-05 18:06:53 +0200 | <EvanR> | the structure diagram with highlighted pieces showing the type or something |
| 2024-09-05 18:09:01 +0200 | Square | (~Square@user/square) |
| 2024-09-05 18:10:18 +0200 | weary-traveler | (~user@user/user363627) (Remote host closed the connection) |
| 2024-09-05 18:18:27 +0200 | EarlPitts | (~EarlPitts@20014C4C1C6E6700B93D810C58171531.catv.pool.telekom.hu) |
| 2024-09-05 18:18:49 +0200 | machinedgod | (~machinedg@d50-99-47-73.abhsia.telus.net) (Ping timeout: 260 seconds) |
| 2024-09-05 18:19:06 +0200 | ft | (~ft@p4fc2a393.dip0.t-ipconnect.de) |
| 2024-09-05 18:21:53 +0200 | tzh | (~tzh@c-76-115-131-146.hsd1.or.comcast.net) |
| 2024-09-05 18:22:03 +0200 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 2024-09-05 18:22:53 +0200 | EarlPitts | (~EarlPitts@20014C4C1C6E6700B93D810C58171531.catv.pool.telekom.hu) (Ping timeout: 256 seconds) |
| 2024-09-05 18:28:28 +0200 | misterfish | (~misterfis@84.53.85.146) |
| 2024-09-05 18:28:40 +0200 | srazkvt | (~sarah@user/srazkvt) |
| 2024-09-05 18:29:17 +0200 | chele | (~chele@user/chele) (Remote host closed the connection) |
| 2024-09-05 18:35:26 +0200 | EarlPitts | (~EarlPitts@20014C4C1C6E6700B93D810C58171531.catv.pool.telekom.hu) |
| 2024-09-05 18:39:53 +0200 | EarlPitts | (~EarlPitts@20014C4C1C6E6700B93D810C58171531.catv.pool.telekom.hu) (Ping timeout: 256 seconds) |
| 2024-09-05 18:44:58 +0200 | alanz | (sid110616@uxbridge.irccloud.com) (Ping timeout: 252 seconds) |
| 2024-09-05 18:48:45 +0200 | alanz | (sid110616@id-110616.uxbridge.irccloud.com) |
| 2024-09-05 18:58:10 +0200 | NemesisD | (sid24071@lymington.irccloud.com) (Ping timeout: 252 seconds) |
| 2024-09-05 18:59:16 +0200 | SrPx | (sid108780@uxbridge.irccloud.com) (Ping timeout: 252 seconds) |
| 2024-09-05 19:00:29 +0200 | NemesisD | (sid24071@id-24071.lymington.irccloud.com) |
| 2024-09-05 19:02:34 +0200 | Pent | (sid313808@lymington.irccloud.com) (Ping timeout: 252 seconds) |
| 2024-09-05 19:02:38 +0200 | SrPx | (sid108780@id-108780.uxbridge.irccloud.com) |
| 2024-09-05 19:02:56 +0200 | <haskellbridge> | <thirdofmay18081814goya> woah we have explicit big lambda in ghc 9.10 now |
| 2024-09-05 19:02:58 +0200 | <haskellbridge> | <thirdofmay18081814goya> neato |
| 2024-09-05 19:03:24 +0200 | <haskellbridge> | <thirdofmay18081814goya> TypeAbstractions |
| 2024-09-05 19:05:13 +0200 | Pent | (sid313808@id-313808.lymington.irccloud.com) |
| 2024-09-05 19:05:49 +0200 | EarlPitts | (~EarlPitts@20014C4C1C6E6700B93D810C58171531.catv.pool.telekom.hu) |
| 2024-09-05 19:05:52 +0200 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 2024-09-05 19:09:21 +0200 | vglfr | (~vglfr@c-73-163-164-68.hsd1.md.comcast.net) (Ping timeout: 246 seconds) |
| 2024-09-05 19:09:32 +0200 | vglfr | (~vglfr@2607:fb91:1420:4418:ac39:6af1:e1c8:8bec) |
| 2024-09-05 19:10:16 +0200 | poscat | (~poscat@user/poscat) (Ping timeout: 252 seconds) |
| 2024-09-05 19:12:26 +0200 | <haskellbridge> | <thirdofmay18081814goya> what are some possible semantics for typeclasses? |
| 2024-09-05 19:13:48 +0200 | <ncf> | do you mean instance search? typeclasses themselves are just record types (cf dictionary passing implementations) |
| 2024-09-05 19:14:27 +0200 | EarlPitts | (~EarlPitts@20014C4C1C6E6700B93D810C58171531.catv.pool.telekom.hu) (Ping timeout: 256 seconds) |
| 2024-09-05 19:14:31 +0200 | oo_miguel1 | (~Thunderbi@78.10.207.45) |
| 2024-09-05 19:14:39 +0200 | <justsomeguy> | What is the purpose of the Reader monad? Why not just use a closure? |
| 2024-09-05 19:15:04 +0200 | <haskellbridge> | <thirdofmay18081814goya> ncf: will look these up, thank you! |
| 2024-09-05 19:15:42 +0200 | <haskellbridge> | <thirdofmay18081814goya> by instance search do you mean typeclass inference? |
| 2024-09-05 19:15:44 +0200 | <ncf> | justsomeguy: closures are implementation details that are mostly irrelevant to haskell. do you mean what's the point of the Reader newtype as opposed to just using the native ((->) r) instance? |
| 2024-09-05 19:16:04 +0200 | <ncf> | goya: yes, sorry, that's what Agda calls it |
| 2024-09-05 19:16:17 +0200 | <justsomeguy> | I mean, conceptually, what problem is the reader monad intended to solve? |
| 2024-09-05 19:16:18 +0200 | <ncf> | (and it's a better name IMO) |
| 2024-09-05 19:16:29 +0200 | oo_miguel | (~Thunderbi@78.10.207.45) (Ping timeout: 255 seconds) |
| 2024-09-05 19:16:29 +0200 | oo_miguel1 | oo_miguel |
| 2024-09-05 19:16:41 +0200 | <ncf> | justsomeguy: repeatedly applying functions to global arguments |
| 2024-09-05 19:16:47 +0200 | poscat | (~poscat@user/poscat) |
| 2024-09-05 19:16:49 +0200 | <haskellbridge> | <thirdofmay18081814goya> ncf: ty! |
| 2024-09-05 19:17:23 +0200 | <ncf> | try to implement a basic type checker and when you're done you should wish you had a reader monad to stuff your environment into |
| 2024-09-05 19:17:58 +0200 | <EvanR> | reader monad = passing the environment around to anything that needs it, only it's implicit so you don't have to |
| 2024-09-05 19:18:06 +0200 | <EvanR> | while also being type safe |
| 2024-09-05 19:18:22 +0200 | <EvanR> | that being said you might just want to pass the environment around anyway |
| 2024-09-05 19:18:52 +0200 | <EvanR> | also the asks function is pretty nifty |
| 2024-09-05 19:18:53 +0200 | <EvanR> | :t asks |
| 2024-09-05 19:18:55 +0200 | <lambdabot> | MonadReader r m => (r -> a) -> m a |
| 2024-09-05 19:19:17 +0200 | <ncf> | :t local |
| 2024-09-05 19:19:18 +0200 | <lambdabot> | MonadReader r m => (r -> r) -> m a -> m a |
| 2024-09-05 19:20:00 +0200 | <EvanR> | also cool |
| 2024-09-05 19:20:23 +0200 | <ncf> | local is a very useful abstraction that lets you say "run this part of the computation in a modified context". for example, if your typechecker encounters something like λx.e, you'll probably want to go on typechecking e in an extended context where x is a bound variable |
| 2024-09-05 19:21:07 +0200 | <monochrom> | I wrote my type checker with the reader monad. Then I wished I just used "Env ->". |
| 2024-09-05 19:21:17 +0200 | <ncf> | eh, that's a reader monad :p |
| 2024-09-05 19:21:24 +0200 | <ncf> | just not the Reader monad |
| 2024-09-05 19:21:27 +0200 | <EvanR> | just pass the environment around |
| 2024-09-05 19:21:53 +0200 | <monochrom> | But it also means I don't bother with "local" and the other method I forgot the name of. |
| 2024-09-05 19:23:00 +0200 | <justsomeguy> | So when does the record (environment) get defined? As part of the instance declaration? |
| 2024-09-05 19:23:20 +0200 | <monochrom> | I'm bivalent about this. I have done both ways. Each way has something to like and something to dislike. At the end, I wish something else writes the code for me. :) |
| 2024-09-05 19:24:57 +0200 | <ncf> | justsomeguy: yeah, `class Foo where` is basically `data Foo = ...` and `instance Foo where` is basically `foo :: Foo; foo = ...` |
| 2024-09-05 19:25:22 +0200 | <monochrom> | I recognize that if I'm writing "infer env foo" five times in a row, then Reader[T] reduces that repetition of "env". |
| 2024-09-05 19:26:50 +0200 | <monochrom> | But "env <- ask; local (f env) (infer bar)" is noisier than "infer (f env) bar" |
| 2024-09-05 19:27:36 +0200 | <EvanR> | justsomeguy, it is passed in to runReader |
| 2024-09-05 19:27:36 +0200 | <ncf> | i mean in a serious typechecker you'd have a whole stack of effects and "accessing and updating the environment" would only be one of them. so then the question becomes "why do you use reader for that instead of state or something else" |
| 2024-09-05 19:27:42 +0200 | <EvanR> | :t runReader |
| 2024-09-05 19:27:42 +0200 | <mauke> | did you mean: local f (infer bar) |
| 2024-09-05 19:27:43 +0200 | <lambdabot> | Reader r a -> r -> a |
| 2024-09-05 19:28:07 +0200 | <monochrom> | Ah yeah, local f (infer bar) |
| 2024-09-05 19:28:08 +0200 | <ncf> | EvanR: wrong conversation |
| 2024-09-05 19:28:24 +0200 | <EvanR> | huh |
| 2024-09-05 19:28:26 +0200 | <ncf> | oh wait no it's me who am confused |
| 2024-09-05 19:31:01 +0200 | <monochrom> | I actually teach my answer to that, albeit for an interpreter (or semantic model) rather than a checker. https://www.cs.utoronto.ca/~trebla/CSCC24-2024-Summer/10-semantics-2.html#model |
| 2024-09-05 19:33:01 +0200 | <justsomeguy> | Sometimes I feel like these abstractions are just obstacles in my way, instead of a useful tool to address a problem. |
| 2024-09-05 19:33:19 +0200 | <monochrom> | I used to have a longer, much expanded version of that, completely fleshed out with "lets make it all state" and coded up, to show what would go wrong, or at least hard to fix and error-prone. But eventually, "in the interest of saving time", I deleted it. |
| 2024-09-05 19:33:39 +0200 | sawilagar | (~sawilagar@user/sawilagar) (Ping timeout: 252 seconds) |
| 2024-09-05 19:34:21 +0200 | <ncf> | justsomeguy: if you feel like that, then probably don't use them |
| 2024-09-05 19:35:14 +0200 | vglfr | (~vglfr@2607:fb91:1420:4418:ac39:6af1:e1c8:8bec) (Ping timeout: 260 seconds) |
| 2024-09-05 19:35:29 +0200 | <EvanR> | justsomeguy, don't fall into the trap of seeing a feature that exists, and assuming you have to use to for something, or go looking for some reason to use it |
| 2024-09-05 19:35:32 +0200 | vglfr | (~vglfr@2607:fb90:eaac:5d4:ad3:f757:81b5:4809) |
| 2024-09-05 19:35:38 +0200 | <EvanR> | use it* |
| 2024-09-05 19:36:00 +0200 | <EvanR> | wait until a good reason to use it comes up (if ever) |
| 2024-09-05 19:36:54 +0200 | <EvanR> | Reader's scope is so narrow it's easy to judge if you need it |
| 2024-09-05 19:36:54 +0200 | <justsomeguy> | For context, I'm going through a book in order, and this is the next chapter. I think if I wasn't commited to finishing this thing I probably wouldn't come across Reader until I had a good use case for it. |
| 2024-09-05 19:37:40 +0200 | srazkvt | (~sarah@user/srazkvt) (Quit: Konversation terminated!) |
| 2024-09-05 19:37:49 +0200 | <EvanR> | ok then finish the chapter and return to reasonable afterward |
| 2024-09-05 19:38:09 +0200 | Square | (~Square@user/square) (Ping timeout: 260 seconds) |
| 2024-09-05 19:38:26 +0200 | <justsomeguy> | :D |
| 2024-09-05 19:38:54 +0200 | justsomeguy | has a little post-it note on his mirror that says "Finsih HPFP before you dit" |
| 2024-09-05 19:39:02 +0200 | <justsomeguy> | *die |
| 2024-09-05 19:40:49 +0200 | EarlPitts | (~EarlPitts@20014C4C1C6E6700B93D810C58171531.catv.pool.telekom.hu) |
| 2024-09-05 19:40:57 +0200 | <int-e> | tomsmeding: re: #25238 ...the difference appears to be that the later `data X` pulls the FromPat and Msg type families into the same group, and that causes the Msg X = MsgDef type instance to be added to the environment (addLocalFamInst) much later, *after* `Msg X` has been subjected to its first simplification. And it looks like that is never retried. That doesn't explain why `Id (Msg X)` works... |
| 2024-09-05 19:41:03 +0200 | <int-e> | ...of course. But at least it's an observable difference in --ddump-tc-trace. |
| 2024-09-05 19:42:17 +0200 | <tomsmeding> | int-e: interesting! |
| 2024-09-05 19:42:24 +0200 | <tomsmeding> | I know very little about how the type checker actually works :) |
| 2024-09-05 19:42:42 +0200 | <tomsmeding> | I just found it funny that apparently this issue has existed since at least 8.4 |
| 2024-09-05 19:43:07 +0200 | <tomsmeding> | it does explain how ordering gets into the problem, though |
| 2024-09-05 19:43:27 +0200 | <tomsmeding> | int-e: though that does beg the question: why are these "groups" a thing in the first place? |
| 2024-09-05 19:44:04 +0200 | <tomsmeding> | I know that mutually recursive groups have to be handled specially in the case of functions (I recall that from the haskell report), and I expect the same holds for type families, for analogous reasons |
| 2024-09-05 19:44:21 +0200 | <tomsmeding> | but whether things are mutually recursive has little to do with whether they are lexically adjacent in the source file |
| 2024-09-05 19:45:03 +0200 | EarlPitts | (~EarlPitts@20014C4C1C6E6700B93D810C58171531.catv.pool.telekom.hu) (Ping timeout: 256 seconds) |
| 2024-09-05 19:45:59 +0200 | <int-e> | I'd guess that adding instances early makes simplification more efficient. But I don't know. I suspect I don't know more about the type checker than you do. Something constraint handling rules something. It has also changed a lot over time. |
| 2024-09-05 19:46:58 +0200 | <tomsmeding> | but then why not add everything early? :p |
| 2024-09-05 19:47:16 +0200 | <int-e> | because it might fail to typecheck |
| 2024-09-05 19:47:53 +0200 | <tomsmeding> | and it's less efficient to through everything in one group to be typechecked simultaneously? |
| 2024-09-05 19:47:57 +0200 | <tomsmeding> | *to throw |
| 2024-09-05 19:52:56 +0200 | <int-e> | It's a guess; I don't know. Rewriting feels cheaper than tracking additional constraints. |
| 2024-09-05 19:54:32 +0200 | <int-e> | The reference to "addLocalFamInst" above is there not because I looked at any code but because it's a label that comes up in the type-checker trace. (I did look at code but I can't say that I understood any of it :P) |
| 2024-09-05 19:54:41 +0200 | <tomsmeding> | :) |
| 2024-09-05 19:57:46 +0200 | Fijxu | (~Fijxu@user/fijxu) (Quit: XD!!) |
| 2024-09-05 19:57:47 +0200 | EarlPitts | (~EarlPitts@20014C4C1C6E6700B93D810C58171531.catv.pool.telekom.hu) |
| 2024-09-05 20:01:45 +0200 | Fijxu | (~Fijxu@user/fijxu) |
| 2024-09-05 20:02:03 +0200 | EarlPitts | (~EarlPitts@20014C4C1C6E6700B93D810C58171531.catv.pool.telekom.hu) (Ping timeout: 256 seconds) |
| 2024-09-05 20:02:30 +0200 | <dmj`> | tomsmeding: the HM(x) paper is a good place to start |
| 2024-09-05 20:03:11 +0200 | <dmj`> | this sdiehl implementation is a good micro implementation of HM(x), HM w/o any extensions. https://github.com/sdiehl/write-you-a-haskell/blob/master/chapter7/poly_constraints/src/Infer.hs |
| 2024-09-05 20:03:32 +0200 | <dmj`> | but once you add type classes it just explodes in complexity |
| 2024-09-05 20:04:24 +0200 | <tomsmeding> | dmj`: is that the same as "OutsideIn(X)", that I vaguely recall hearing of? |
| 2024-09-05 20:04:42 +0200 | <tomsmeding> | ah seems to be different |
| 2024-09-05 20:06:04 +0200 | <tomsmeding> | apparently OutsideIn(X) is an extension of HM(X?) |
| 2024-09-05 20:06:24 +0200 | athan | (~athan@2600:382:2d15:de3c:7342:aa0b:1e24:3f2d) (Ping timeout: 276 seconds) |
| 2024-09-05 20:06:44 +0200 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 2024-09-05 20:07:46 +0200 | <dmj`> | tomsmeding: yea, OutsideIn(x) is how they refactored the type checker to be a constraint solver, like HM(x), but why they had to sacrifice let generalization to do so |
| 2024-09-05 20:08:04 +0200 | <tomsmeding> | HM(X) is not from the GHC people? |
| 2024-09-05 20:08:08 +0200 | <dmj`> | HM(x) is just a general framework for doing type checking as constraint solving |
| 2024-09-05 20:08:44 +0200 | <dmj`> | tomsmeding: I don't think so, I think its Remy and Pottier (could be wrong), but its the "French approach", because they are two french guys |
| 2024-09-05 20:08:47 +0200 | <tomsmeding> | I should read that OutsideIn(x) paper at some point |
| 2024-09-05 20:08:50 +0200 | <tomsmeding> | ah I see |
| 2024-09-05 20:10:02 +0200 | <dmj`> | yea I'm trying to figure out how to recover the entailment property when doing type inference w/ classes using the HM(x) approach |
| 2024-09-05 20:10:34 +0200 | son0p | (~ff@186.121.49.191) |
| 2024-09-05 20:11:00 +0200 | EarlPitts | (~EarlPitts@20014C4C1C6E6700B93D810C58171531.catv.pool.telekom.hu) |
| 2024-09-05 20:11:45 +0200 | <mauke> | https://www.krook.dev/papers/partitioningHaskell2024.pdf - disappointed that the second co-author's name is Hammersberg, not Hooke |
| 2024-09-05 20:12:31 +0200 | rvalue- | (~rvalue@user/rvalue) |
| 2024-09-05 20:13:08 +0200 | <mauke> | then I could say it is a paper by Hooke and by Krook |
| 2024-09-05 20:13:21 +0200 | rvalue | (~rvalue@user/rvalue) (Ping timeout: 265 seconds) |
| 2024-09-05 20:15:39 +0200 | EarlPitts | (~EarlPitts@20014C4C1C6E6700B93D810C58171531.catv.pool.telekom.hu) (Ping timeout: 256 seconds) |
| 2024-09-05 20:16:36 +0200 | rvalue- | rvalue |
| 2024-09-05 20:17:04 +0200 | <monochrom> | heh |
| 2024-09-05 20:22:23 +0200 | pavonia | (~user@user/siracusa) (Quit: Bye!) |
| 2024-09-05 20:23:36 +0200 | justsomeguy | (~justsomeg@user/justsomeguy) (Ping timeout: 252 seconds) |
| 2024-09-05 20:26:28 +0200 | Fijxu | (~Fijxu@user/fijxu) (Quit: XD!!) |
| 2024-09-05 20:26:30 +0200 | EarlPitts | (~EarlPitts@20014C4C1C6E6700B93D810C58171531.catv.pool.telekom.hu) |
| 2024-09-05 20:28:02 +0200 | CiaoSen | (~Jura@2a05:5800:2e8:9e00:ca4b:d6ff:fec1:99da) |
| 2024-09-05 20:30:57 +0200 | EarlPitts | (~EarlPitts@20014C4C1C6E6700B93D810C58171531.catv.pool.telekom.hu) (Ping timeout: 256 seconds) |
| 2024-09-05 20:34:22 +0200 | athan | (~athan@syn-098-153-145-140.biz.spectrum.com) |
| 2024-09-05 20:40:51 +0200 | gawen | (~gawen@user/gawen) (Quit: cya) |
| 2024-09-05 20:42:13 +0200 | sord937 | (~sord937@gateway/tor-sasl/sord937) (Quit: sord937) |
| 2024-09-05 20:42:14 +0200 | gawen | (~gawen@user/gawen) |
| 2024-09-05 20:44:11 +0200 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) |
| 2024-09-05 20:47:04 +0200 | ash3en | (~Thunderbi@2a01:c23:8c51:9600:3168:7de0:ad26:7330) (Quit: ash3en) |
| 2024-09-05 20:52:50 +0200 | CAT_S | (~apic@ppp-46-244-252-175.dynamic.mnet-online.de) |
| 2024-09-05 20:53:34 +0200 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) (Ping timeout: 260 seconds) |
| 2024-09-05 20:58:02 +0200 | Smiles | (uid551636@id-551636.lymington.irccloud.com) (Quit: Connection closed for inactivity) |
| 2024-09-05 20:58:24 +0200 | vglfr | (~vglfr@2607:fb90:eaac:5d4:ad3:f757:81b5:4809) (Ping timeout: 276 seconds) |
| 2024-09-05 20:58:27 +0200 | EarlPitts | (~EarlPitts@20014C4C1C6E6700B93D810C58171531.catv.pool.telekom.hu) |
| 2024-09-05 20:58:48 +0200 | vglfr | (~vglfr@2601:14d:4e01:1370:71d6:bfd8:becf:12cb) |
| 2024-09-05 21:01:30 +0200 | Square2 | (~Square4@user/square) |
| 2024-09-05 21:02:41 +0200 | EarlPitts | (~EarlPitts@20014C4C1C6E6700B93D810C58171531.catv.pool.telekom.hu) (Ping timeout: 256 seconds) |
| 2024-09-05 21:02:51 +0200 | Square | (~Square@user/square) |
| 2024-09-05 21:05:22 +0200 | gawen | (~gawen@user/gawen) (Read error: error:0A000119:SSL routines::decryption failed or bad record mac) |
| 2024-09-05 21:06:15 +0200 | Square2 | (~Square4@user/square) (Ping timeout: 246 seconds) |
| 2024-09-05 21:07:36 +0200 | gawen | (~gawen@user/gawen) |
| 2024-09-05 21:11:19 +0200 | RedFlamingos | (~RedFlamin@user/RedFlamingos) |
| 2024-09-05 21:15:10 +0200 | EarlPitts | (~EarlPitts@20014C4C1C6E6700B93D810C58171531.catv.pool.telekom.hu) |
| 2024-09-05 21:18:11 +0200 | Fijxu | (~Fijxu@user/fijxu) |
| 2024-09-05 21:19:41 +0200 | EarlPitts | (~EarlPitts@20014C4C1C6E6700B93D810C58171531.catv.pool.telekom.hu) (Ping timeout: 256 seconds) |
| 2024-09-05 21:25:25 +0200 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 2024-09-05 21:26:33 +0200 | CAT_S | (~apic@ppp-46-244-252-175.dynamic.mnet-online.de) (Ping timeout: 246 seconds) |
| 2024-09-05 21:32:48 +0200 | EarlPitts | (~EarlPitts@20014C4C1C6E6700B93D810C58171531.catv.pool.telekom.hu) |
| 2024-09-05 21:34:06 +0200 | youthlic | (~Thunderbi@user/youthlic) (Quit: youthlic) |
| 2024-09-05 21:37:15 +0200 | EarlPitts | (~EarlPitts@20014C4C1C6E6700B93D810C58171531.catv.pool.telekom.hu) (Ping timeout: 256 seconds) |
| 2024-09-05 21:39:42 +0200 | hugo | (~hugo@quicksilver.lysator.liu.se) |
| 2024-09-05 21:39:45 +0200 | CAT_S | (~apic@ppp-46-244-252-202.dynamic.mnet-online.de) |
| 2024-09-05 21:43:14 +0200 | Smiles | (uid551636@id-551636.lymington.irccloud.com) |
| 2024-09-05 21:45:00 +0200 | athan | (~athan@syn-098-153-145-140.biz.spectrum.com) (Ping timeout: 252 seconds) |
| 2024-09-05 21:46:40 +0200 | hugo | (~hugo@quicksilver.lysator.liu.se) (Quit: ZNC 1.8.2+deb3.1 - https://znc.in) |
| 2024-09-05 21:48:46 +0200 | gmg | (~user@user/gehmehgeh) (Ping timeout: 260 seconds) |
| 2024-09-05 21:51:21 +0200 | gmg | (~user@user/gehmehgeh) |
| 2024-09-05 21:56:16 +0200 | srazkvt | (~sarah@user/srazkvt) |
| 2024-09-05 22:00:16 +0200 | athan | (~athan@2600:382:3a29:3ae2:2541:beb:5d67:8d9c) |
| 2024-09-05 22:02:10 +0200 | ash3en | (~Thunderbi@2a01:c23:8c51:9600:3168:7de0:ad26:7330) |
| 2024-09-05 22:03:35 +0200 | machinedgod | (~machinedg@d50-99-47-73.abhsia.telus.net) |
| 2024-09-05 22:04:34 +0200 | euleritian | (~euleritia@77.22.252.56) (Ping timeout: 260 seconds) |
| 2024-09-05 22:06:05 +0200 | EarlPitts | (~EarlPitts@20014C4C1C6E6700B93D810C58171531.catv.pool.telekom.hu) |
| 2024-09-05 22:06:20 +0200 | euleritian | (~euleritia@dynamic-176-006-132-001.176.6.pool.telefonica.de) |
| 2024-09-05 22:10:41 +0200 | EarlPitts | (~EarlPitts@20014C4C1C6E6700B93D810C58171531.catv.pool.telekom.hu) (Ping timeout: 256 seconds) |
| 2024-09-05 22:18:15 +0200 | weary-traveler | (~user@user/user363627) |
| 2024-09-05 22:20:57 +0200 | sawilagar | (~sawilagar@user/sawilagar) |
| 2024-09-05 22:23:43 +0200 | justsomeguy | (~justsomeg@user/justsomeguy) |
| 2024-09-05 22:23:58 +0200 | EarlPitts | (~EarlPitts@20014C4C1C6E6700B93D810C58171531.catv.pool.telekom.hu) |
| 2024-09-05 22:25:12 +0200 | christiaanb | (uid84827@id-84827.lymington.irccloud.com) |
| 2024-09-05 22:28:15 +0200 | EarlPitts | (~EarlPitts@20014C4C1C6E6700B93D810C58171531.catv.pool.telekom.hu) (Ping timeout: 256 seconds) |
| 2024-09-05 22:38:52 +0200 | ash3en | (~Thunderbi@2a01:c23:8c51:9600:3168:7de0:ad26:7330) (Quit: ash3en) |
| 2024-09-05 22:39:14 +0200 | misterfish | (~misterfis@84.53.85.146) (Ping timeout: 248 seconds) |
| 2024-09-05 22:40:18 +0200 | EarlPitts | (~EarlPitts@20014C4C1C6E6700B93D810C58171531.catv.pool.telekom.hu) |
| 2024-09-05 22:44:41 +0200 | EarlPitts | (~EarlPitts@20014C4C1C6E6700B93D810C58171531.catv.pool.telekom.hu) (Ping timeout: 256 seconds) |
| 2024-09-05 22:55:38 +0200 | Inst | (~Inst@user/Inst) (Remote host closed the connection) |
| 2024-09-05 22:56:17 +0200 | Inst | (~Inst@user/Inst) |
| 2024-09-05 23:05:15 +0200 | takuan | (~takuan@178-116-218-225.access.telenet.be) (Ping timeout: 246 seconds) |
| 2024-09-05 23:05:48 +0200 | CiaoSen | (~Jura@2a05:5800:2e8:9e00:ca4b:d6ff:fec1:99da) (Ping timeout: 245 seconds) |
| 2024-09-05 23:07:06 +0200 | itaipu | (~itaipu@168.121.99.142) (Ping timeout: 276 seconds) |
| 2024-09-05 23:13:29 +0200 | EarlPitts | (~EarlPitts@20014C4C1C6E6700B93D810C58171531.catv.pool.telekom.hu) |
| 2024-09-05 23:18:07 +0200 | EarlPitts | (~EarlPitts@20014C4C1C6E6700B93D810C58171531.catv.pool.telekom.hu) (Ping timeout: 256 seconds) |
| 2024-09-05 23:19:14 +0200 | michalz | (~michalz@185.246.207.205) (Remote host closed the connection) |
| 2024-09-05 23:21:04 +0200 | itaipu | (~itaipu@168.121.99.143) |
| 2024-09-05 23:26:09 +0200 | justsomeguy | (~justsomeg@user/justsomeguy) (Ping timeout: 248 seconds) |
| 2024-09-05 23:28:59 +0200 | WarmHeart | (~WarmHeart@2605:6440:300a:5001:4a94:d13c:dbb0:ec9b) |
| 2024-09-05 23:30:55 +0200 | EarlPitts | (~EarlPitts@20014C4C1C6E6700B93D810C58171531.catv.pool.telekom.hu) |
| 2024-09-05 23:31:25 +0200 | __monty__ | (~toonn@user/toonn) (Quit: leaving) |
| 2024-09-05 23:35:07 +0200 | EarlPitts | (~EarlPitts@20014C4C1C6E6700B93D810C58171531.catv.pool.telekom.hu) (Ping timeout: 256 seconds) |
| 2024-09-05 23:36:28 +0200 | justsomeguy | (~justsomeg@user/justsomeguy) |
| 2024-09-05 23:36:38 +0200 | Square2 | (~Square4@user/square) |
| 2024-09-05 23:38:40 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 2024-09-05 23:39:12 +0200 | Square | (~Square@user/square) (Ping timeout: 246 seconds) |
| 2024-09-05 23:40:23 +0200 | CAT_S | (~apic@ppp-46-244-252-202.dynamic.mnet-online.de) (Ping timeout: 245 seconds) |
| 2024-09-05 23:42:13 +0200 | srazkvt | (~sarah@user/srazkvt) (Quit: Konversation terminated!) |
| 2024-09-05 23:43:24 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 246 seconds) |
| 2024-09-05 23:45:54 +0200 | WarmHeart | (~WarmHeart@2605:6440:300a:5001:4a94:d13c:dbb0:ec9b) (Quit: Client closed) |
| 2024-09-05 23:47:49 +0200 | justsomeguy | (~justsomeg@user/justsomeguy) (Ping timeout: 260 seconds) |
| 2024-09-05 23:47:49 +0200 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Ping timeout: 260 seconds) |
| 2024-09-05 23:48:24 +0200 | EarlPitts | (~EarlPitts@20014C4C1C6E6700B93D810C58171531.catv.pool.telekom.hu) |
| 2024-09-05 23:52:41 +0200 | EarlPitts | (~EarlPitts@20014C4C1C6E6700B93D810C58171531.catv.pool.telekom.hu) (Ping timeout: 256 seconds) |
| 2024-09-05 23:54:27 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) |
| 2024-09-05 23:55:22 +0200 | <haskellbridge> | <eldritchcookie> wow Linear types error messages suck, please point where i use more than once orif it is'nt used. |
| 2024-09-05 23:59:09 +0200 | merijn | (~merijn@204-220-045-062.dynamic.caiway.nl) (Ping timeout: 246 seconds) |