2024/06/27

2024-06-27 00:07:58 +0200safinaskar(~quassel@212.73.77.104)
2024-06-27 00:08:54 +0200 <safinaskar> hi. i just proved in haskell that (0 + x = x) from (x + 0 = x) and induction https://godbolt.org/z/Tvqdaozoh
2024-06-27 00:09:09 +0200 <safinaskar> i did NOT implement prover in haskell, i used type system of haskell itself as a prover
2024-06-27 00:10:53 +0200 <safinaskar> unfortunately, i just understand that my proof is wrong. type application in haskell is injective, thus in my code (Add (N Z) Z ~ Add Z (N Z)) (this is true) implies (Z ~ N Z) (which is false)
2024-06-27 00:10:59 +0200 <safinaskar> is there a way to fix this?
2024-06-27 00:11:48 +0200 <safinaskar> maybe there is some experimental feature of haskell, which disables type application injectivity?
2024-06-27 00:14:46 +0200 <ncf> it's injective with respect to type equality (~) (in some cases), but it shouldn't be injective with respect to your custom Equal type, should it?
2024-06-27 00:15:16 +0200 <ncf> since you've gone with the weird axiomatic definition instead of the inductive definition with a refl constructor
2024-06-27 00:15:19 +0200 <safinaskar> ncf: hmm, seems correct. thank you!
2024-06-27 00:15:56 +0200 <ncf> i'm not even sure which type families are considered injective. https://ghc.gitlab.haskell.org/ghc/doc/users_guide/exts/type_families.html has some information
2024-06-27 00:15:57 +0200Sgeo(~Sgeo@user/sgeo)
2024-06-27 00:22:41 +0200 <zzz> are typefamilies worth it or can i just get by with "simple" haskell?
2024-06-27 00:24:00 +0200 <monochrom> I'm going to answer tautologically. Type families are worth it when you need type families. You can get by with simple Haskell when simple Haskell suffices.
2024-06-27 00:24:01 +0200acidjnk_new3(~acidjnk@p200300d6e714dc96bd88011075acd305.dip0.t-ipconnect.de) (Ping timeout: 246 seconds)
2024-06-27 00:24:04 +0200tromp(~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…)
2024-06-27 00:24:27 +0200 <monochrom> But I will add that I have only ever needed fairly simple Haskell most of the time.
2024-06-27 00:25:14 +0200 <monochrom> But there are times when I miss SML's parametrized modules, and I can use type families to do something similar.
2024-06-27 00:26:12 +0200 <monochrom> i.e., when I want to make some fairly general abstraction.
2024-06-27 00:27:05 +0200 <monochrom> Or IOW when I use type families, it's for general template-like things, not for dependent typing.
2024-06-27 00:27:27 +0200 <EvanR> type synonym family is a fairly simple way to reduce the verbosity of some type level shenanigans, they just expand to some other shenanigan
2024-06-27 00:27:56 +0200 <safinaskar> ncf: unfortunately, no. see: https://godbolt.org/z/xEa54v666 . see "oops1" and "oops2" in the end. unfortunately i was able to prove that my Equal is equivalent to standard haskell equality
2024-06-27 00:27:57 +0200 <EvanR> associated type synonym family in a class can sometimes save you from multi-parameter type classes
2024-06-27 00:28:08 +0200michalz(~michalz@185.246.207.205) (Quit: ZNC 1.9.0 - https://znc.in)
2024-06-27 00:28:27 +0200 <monochrom> Yeah that's what I use them for.
2024-06-27 00:28:30 +0200 <EvanR> for the sake of argument "simple haskell" doesn't have you doing any of those so those don't help
2024-06-27 00:28:53 +0200CiaoSen(~Jura@2a05:5800:2d8:3a00:e6b9:7aff:fe80:3d03) (Ping timeout: 240 seconds)
2024-06-27 00:28:59 +0200 <safinaskar> (and no, i cannot just remove "subst", i use it in proof of "subst2" and i use "subst2" in proof of (0 + x = x) )
2024-06-27 00:28:59 +0200 <ncf> safinaskar: good point
2024-06-27 00:29:11 +0200 <zzz> that was my suspicion
2024-06-27 00:29:29 +0200 <zzz> i barey do any type-level acrobatics
2024-06-27 00:29:51 +0200 <zzz> s/barey/barely
2024-06-27 00:31:31 +0200 <safinaskar> ncf: "i'm not even sure which type families are considered injective" - according to https://hackage.haskell.org/package/base-4.20.0.1/docs/Data-Type-Equality.html#v:inner (f a ~ g b) always implies (a ~ b). but this relies on the fact that we can substitute given type-level function to "f" and "g"
2024-06-27 00:32:04 +0200 <safinaskar> ncf: so the rule is here: all type-level functions, which can be substituted to type-level variables, are injective
2024-06-27 00:32:58 +0200 <safinaskar> ncf: in particular (i checked this using expirement) if we have "type Foo a = ...", then "Foo" cannot be substituted, so "Foo" is not injective. But "Foo a" can be substituted, and thus it is injective
2024-06-27 00:33:21 +0200 <dolio> inner does not say type families are injective, because `f` and `g` do not range over type families.
2024-06-27 00:34:49 +0200 <safinaskar> dolio: i did expirement, and result are so. if i have "type family Foo a :: Type -> Type", then "Foo" cannot be substituted and thus is not injective. but "Foo a" can be substituted and thus injective
2024-06-27 00:35:02 +0200 <safinaskar> dolio: so yes, type families are not injective
2024-06-27 00:35:13 +0200 <safinaskar> type level functions are
2024-06-27 00:35:59 +0200waleee(~waleee@h-176-10-144-38.NA.cust.bahnhof.se) (Ping timeout: 252 seconds)
2024-06-27 00:36:01 +0200 <safinaskar> it seems i found solution. i just need to define "type family Add a b :: Nat", not "type family Add :: Nat -> Nat -> Nat"
2024-06-27 00:36:06 +0200 <safinaskar> cool!
2024-06-27 00:37:47 +0200 <geekosaur> they are if you declare them right (https://downloads.haskell.org/ghc/9.10.1/docs/users_guide/exts/type_families.html#injective-type-f…)
2024-06-27 00:37:59 +0200waleee(~waleee@h-176-10-144-38.NA.cust.bahnhof.se)
2024-06-27 00:44:04 +0200 <safinaskar> zzz: "are typefamilies worth it or can i just get by with "simple" haskell?" - i never needed type families except for this very weird code
2024-06-27 00:47:49 +0200JimL(~quassel@89.162.16.26) (Ping timeout: 268 seconds)
2024-06-27 00:51:09 +0200waleee(~waleee@h-176-10-144-38.NA.cust.bahnhof.se) (Ping timeout: 255 seconds)
2024-06-27 00:53:40 +0200 <safinaskar> ncf: thanks for link. i just slightly have read it. and yes, now i know that type families can be injective if specially annotated. i. e. one can add more injectivity to a program if needed
2024-06-27 00:54:24 +0200 <safinaskar> ncf: but in my case i want less injectivity, not more. and i already know how to do this. "type family Add a b :: Nat" instead of "type family Add :: Nat -> Nat -> Nat"
2024-06-27 00:55:43 +0200 <ncf> (i have no idea why this works)
2024-06-27 01:04:14 +0200 <safinaskar> ncf: i think i know why this works. "type family Add a b :: Nat" is somewhat similar to usual type synonym "type Add a b = ....". they are not injective (because you can easily write "type Add a b = Char"). and thus you should always apply all arguments, i. e. you cannot write (f @Add), you should write (f @(Add a b)). otherwise you could prove injectivity using "Data.Type.Equality.inner"
2024-06-27 01:05:34 +0200 <safinaskar> ncf: and in "type family Add :: Nat -> Nat -> Nat" we have injectivity (because one cannot define non-injective "Add"), thus we can rely on it
2024-06-27 01:13:29 +0200waleee(~waleee@h-176-10-144-38.NA.cust.bahnhof.se)
2024-06-27 01:17:09 +0200 <safinaskar> i found a wrong statement at https://ghc.gitlab.haskell.org/ghc/doc/users_guide/exts/type_families.html
2024-06-27 01:17:23 +0200 <safinaskar> but i will not report bug, because your bug reporting process is too compilected
2024-06-27 01:17:30 +0200 <safinaskar> *complicated
2024-06-27 01:18:07 +0200 <safinaskar> the statement is: "We call the number of parameters in a type family declaration, the family’s arity, and all applications of a type family must be fully saturated with respect to that arity. This requirement is unlike ordinary type synonyms and it implies that the kind of a type family is not sufficient to determine a family’s arity, and hence in general, also insufficient to determine whether a type family application is well formed."
2024-06-27 01:18:31 +0200 <safinaskar> the statement is wrong, because ordinary type synonyms share this property, too (determined by expirement)
2024-06-27 01:19:13 +0200gmg(~user@user/gehmehgeh) (Quit: Leaving)
2024-06-27 01:25:39 +0200Garbanzo(~Garbanzo@2602:304:6eac:dc10::46) (Remote host closed the connection)
2024-06-27 01:39:24 +0200emmanuelux(~emmanuelu@user/emmanuelux)
2024-06-27 01:43:11 +0200zzz(~yin@user/zero) (Ping timeout: 264 seconds)
2024-06-27 01:50:04 +0200zzz(~yin@user/zero)
2024-06-27 01:50:24 +0200xsarnik(xsarnik@lounge.fi.muni.cz) (Quit: Ping timeout (120 seconds))
2024-06-27 01:50:24 +0200xstill_(xstill@fimu/xstill) (Quit: Ping timeout (120 seconds))
2024-06-27 01:50:58 +0200malte(~malte@mal.tc) (Read error: Connection reset by peer)
2024-06-27 01:51:12 +0200malte(~malte@mal.tc)
2024-06-27 01:51:38 +0200rvalue(~rvalue@user/rvalue) (Quit: ZNC - https://znc.in)
2024-06-27 01:51:51 +0200it_(~quassel@v2202212189510211193.supersrv.de) (Quit: No Ping reply in 180 seconds.)
2024-06-27 01:52:00 +0200rvalue(~rvalue@user/rvalue)
2024-06-27 01:52:56 +0200xstill_(xstill@fimu/xstill)
2024-06-27 01:53:15 +0200it_(~quassel@v2202212189510211193.supersrv.de)
2024-06-27 01:53:55 +0200 <davean> safinaskar: why do you think that is wrong? Pretty sure I've defined classes on type synonyms for example
2024-06-27 01:56:04 +0200xsarnik(xsarnik@lounge.fi.muni.cz)
2024-06-27 01:57:58 +0200 <dolio> I don't think you can define classes on synonyms unless it satisfies a similar arity condition to families.
2024-06-27 01:58:24 +0200 <dolio> But LiberalTypeSynonyms let you partially apply them as long as they become saturated, and doesn't allow the same thing to happen with families.
2024-06-27 02:02:45 +0200sawilagar(~sawilagar@user/sawilagar) (Ping timeout: 268 seconds)
2024-06-27 02:02:55 +0200acarrico(~acarrico@dhcp-68-142-57-215.greenmountainaccess.net) (Quit: Leaving.)
2024-06-27 02:05:05 +0200SoF(~skius@user/skius) (Remote host closed the connection)
2024-06-27 02:08:40 +0200waleee(~waleee@h-176-10-144-38.NA.cust.bahnhof.se) (Ping timeout: 246 seconds)
2024-06-27 02:13:48 +0200waleee(~waleee@h-176-10-144-38.NA.cust.bahnhof.se)
2024-06-27 02:14:39 +0200ryanbooker(uid4340@id-4340.hampstead.irccloud.com)
2024-06-27 02:20:15 +0200waleee(~waleee@h-176-10-144-38.NA.cust.bahnhof.se) (Ping timeout: 255 seconds)
2024-06-27 02:24:13 +0200CrunchyFlakes(~CrunchyFl@ip92348280.dynamic.kabel-deutschland.de) (Read error: Connection reset by peer)
2024-06-27 02:26:51 +0200CrunchyFlakes(~CrunchyFl@ip92348280.dynamic.kabel-deutschland.de)
2024-06-27 02:33:46 +0200henry40408(~henry4040@175.182.111.183) (Quit: Ping timeout (120 seconds))
2024-06-27 02:34:12 +0200henry40408(~henry4040@175.182.111.183)
2024-06-27 02:36:13 +0200hgolden(~hgolden@2603:8000:9d00:3ed1:2678:8497:aa5c:7fa9) (Remote host closed the connection)
2024-06-27 02:38:06 +0200hgolden(~hgolden@2603:8000:9d00:3ed1:2678:8497:aa5c:7fa9)
2024-06-27 02:40:11 +0200philopsos1(~caecilius@user/philopsos) (Ping timeout: 264 seconds)
2024-06-27 03:02:15 +0200aforemny(~aforemny@i59F516D5.versanet.de) (Ping timeout: 268 seconds)
2024-06-27 03:02:37 +0200aforemny(~aforemny@i59F516D5.versanet.de)
2024-06-27 03:06:45 +0200joeyadams(~joeyadams@2603:6010:5100:2ed:93a8:3ab0:fdc9:ca35) (Quit: Leaving)
2024-06-27 03:16:15 +0200xff0x(~xff0x@2405:6580:b080:900:374:70e:871e:8e7b) (Ping timeout: 256 seconds)
2024-06-27 03:25:13 +0200safinaskar(~quassel@212.73.77.104) ()
2024-06-27 03:25:44 +0200xstill_(xstill@fimu/xstill) (Quit: Ping timeout (120 seconds))
2024-06-27 03:25:56 +0200xsarnik(xsarnik@lounge.fi.muni.cz) (Quit: Ping timeout (120 seconds))
2024-06-27 03:26:04 +0200xstill_(xstill@fimu/xstill)
2024-06-27 03:26:29 +0200xsarnik(xsarnik@lounge.fi.muni.cz)
2024-06-27 03:27:16 +0200it_(~quassel@v2202212189510211193.supersrv.de) (Quit: No Ping reply in 180 seconds.)
2024-06-27 03:28:25 +0200it_(~quassel@v2202212189510211193.supersrv.de)
2024-06-27 03:46:55 +0200phma(phma@2001:5b0:210f:1ad8:36db:ca4e:16e7:7eb) (Read error: Connection reset by peer)
2024-06-27 03:47:04 +0200rosco(~rosco@175.136.155.137)
2024-06-27 03:47:21 +0200phma(~phma@host-67-44-208-96.hnremote.net)
2024-06-27 03:47:23 +0200machinedgod(~machinedg@d173-183-246-216.abhsia.telus.net) (Ping timeout: 264 seconds)
2024-06-27 04:00:50 +0200xff0x(~xff0x@125x103x176x34.ap125.ftth.ucom.ne.jp)
2024-06-27 04:07:05 +0200soverysour(~soverysou@81.196.150.219)
2024-06-27 04:07:05 +0200soverysour(~soverysou@81.196.150.219) (Changing host)
2024-06-27 04:07:05 +0200soverysour(~soverysou@user/soverysour)
2024-06-27 04:07:11 +0200xff0x(~xff0x@125x103x176x34.ap125.ftth.ucom.ne.jp) (Ping timeout: 252 seconds)
2024-06-27 04:08:05 +0200dequbed(~dequbed@banana-new.kilobyte22.de) (Ping timeout: 240 seconds)
2024-06-27 04:08:30 +0200nadja(~dequbed@banana-new.kilobyte22.de)
2024-06-27 04:09:10 +0200xff0x(~xff0x@125x103x176x34.ap125.ftth.ucom.ne.jp)
2024-06-27 04:11:24 +0200soverysour(~soverysou@user/soverysour) (Ping timeout: 255 seconds)
2024-06-27 04:48:15 +0200td_(~td@i53870920.versanet.de) (Ping timeout: 264 seconds)
2024-06-27 04:49:52 +0200td_(~td@i53870923.versanet.de)
2024-06-27 05:01:50 +0200Unicorn_Princess(~Unicorn_P@user/Unicorn-Princess/x-3540542) (Remote host closed the connection)
2024-06-27 05:05:17 +0200aaronv(~aaronv@user/aaronv)
2024-06-27 05:16:39 +0200aaronv(~aaronv@user/aaronv) (Remote host closed the connection)
2024-06-27 05:17:03 +0200aaronv(~aaronv@user/aaronv)
2024-06-27 05:22:32 +0200MrFox(~MrFox___@216-151-184-162.lon.as62651.net)
2024-06-27 05:23:42 +0200MrFoxdarmario
2024-06-27 05:23:46 +0200darmario(~MrFox___@216-151-184-162.lon.as62651.net) (Changing host)
2024-06-27 05:23:46 +0200darmario(~MrFox___@user/darmario)
2024-06-27 05:37:01 +0200aforemny_(~aforemny@i59F516E5.versanet.de)
2024-06-27 05:38:35 +0200aforemny(~aforemny@i59F516D5.versanet.de) (Ping timeout: 268 seconds)
2024-06-27 05:40:21 +0200madhavanmiui(~madhavanm@2409:40f4:3047:1afd:8000::)
2024-06-27 05:46:39 +0200madhavanmiui(~madhavanm@2409:40f4:3047:1afd:8000::) (Read error: Connection reset by peer)
2024-06-27 05:46:47 +0200zzz(~yin@user/zero) (Ping timeout: 264 seconds)
2024-06-27 05:46:55 +0200madhavanmiui(~madhavanm@2409:40f4:3047:1afd:8000::)
2024-06-27 05:48:40 +0200zzz(~yin@user/zero)
2024-06-27 05:48:53 +0200madhavanmiui(~madhavanm@2409:40f4:3047:1afd:8000::) (Read error: Connection reset by peer)
2024-06-27 05:49:06 +0200madhavanmiui(~madhavanm@152.58.250.215)
2024-06-27 05:51:21 +0200madhavanmiui(~madhavanm@152.58.250.215) (Client Quit)
2024-06-27 06:03:33 +0200zzz(~yin@user/zero) (Ping timeout: 268 seconds)
2024-06-27 06:04:04 +0200philopsos1(~caecilius@user/philopsos)
2024-06-27 06:04:11 +0200xff0x(~xff0x@125x103x176x34.ap125.ftth.ucom.ne.jp) (Ping timeout: 264 seconds)
2024-06-27 06:05:46 +0200xff0x(~xff0x@125x103x176x34.ap125.ftth.ucom.ne.jp)
2024-06-27 06:16:11 +0200philopsos1(~caecilius@user/philopsos) (Ping timeout: 264 seconds)
2024-06-27 06:16:28 +0200darmario(~MrFox___@user/darmario) (Leaving)
2024-06-27 06:24:23 +0200ryanbooker(uid4340@id-4340.hampstead.irccloud.com) (Quit: Connection closed for inactivity)
2024-06-27 06:34:17 +0200philopsos1(~caecilius@user/philopsos)
2024-06-27 06:34:58 +0200wbooze(~wbooze@2a02:908:1244:9a20:3d84:fc89:d93b:3334) (Remote host closed the connection)
2024-06-27 06:58:31 +0200sroso(~sroso@user/SrOso)
2024-06-27 07:08:18 +0200xff0x(~xff0x@125x103x176x34.ap125.ftth.ucom.ne.jp) (Ping timeout: 268 seconds)
2024-06-27 07:16:02 +0200monochrom(trebla@216.138.220.146) (Quit: ZNC 1.9.0+deb2build3 - https://znc.in)
2024-06-27 07:23:55 +0200monochrom(trebla@216.138.220.146)
2024-06-27 07:24:57 +0200takuan(~takuan@178-116-218-225.access.telenet.be)
2024-06-27 07:30:11 +0200Sgeo(~Sgeo@user/sgeo) (Read error: Connection reset by peer)
2024-06-27 07:35:59 +0200philopsos1(~caecilius@user/philopsos) (Ping timeout: 264 seconds)
2024-06-27 07:39:33 +0200causal(~eric@50.35.88.207) (Quit: WeeChat 4.3.1)
2024-06-27 07:40:24 +0200xff0x(~xff0x@125x103x176x34.ap125.ftth.ucom.ne.jp)
2024-06-27 07:42:53 +0200michalz(~michalz@185.246.207.215)
2024-06-27 07:46:53 +0200acidjnk_new3(~acidjnk@p200300d6e714dc25e45fde1d7555be75.dip0.t-ipconnect.de)
2024-06-27 07:48:14 +0200danse-nr3(~danse-nr3@151.44.219.215)
2024-06-27 07:49:17 +0200danse-nr3(~danse-nr3@151.44.219.215) (Remote host closed the connection)
2024-06-27 07:49:42 +0200danse-nr3(~danse-nr3@151.44.219.215)
2024-06-27 07:55:39 +0200philopsos1(~caecilius@user/philopsos)
2024-06-27 07:58:50 +0200dcoutts_(~duncan@2a00:23c6:1c8d:901:b94:4566:9d63:4848)
2024-06-27 08:00:55 +0200rosco(~rosco@175.136.155.137) (Quit: Lost terminal)
2024-06-27 08:02:23 +0200forell(~forell@user/forell) (Ping timeout: 264 seconds)
2024-06-27 08:03:48 +0200aaronv(~aaronv@user/aaronv) (Ping timeout: 268 seconds)
2024-06-27 08:05:23 +0200machinedgod(~machinedg@d173-183-246-216.abhsia.telus.net)
2024-06-27 08:06:43 +0200xff0x(~xff0x@125x103x176x34.ap125.ftth.ucom.ne.jp) (Quit: xff0x)
2024-06-27 08:09:31 +0200pavonia(~user@user/siracusa) (Quit: Bye!)
2024-06-27 08:13:39 +0200tv(~tv@user/tv) (Ping timeout: 260 seconds)
2024-06-27 08:22:38 +0200rosco(~rosco@175.136.155.137)
2024-06-27 08:29:14 +0200sord937(~sord937@gateway/tor-sasl/sord937)
2024-06-27 08:53:03 +0200ft(~ft@p4fc2ab80.dip0.t-ipconnect.de) (Ping timeout: 264 seconds)
2024-06-27 08:53:32 +0200m1dnight(~christoph@82.146.125.185) (Quit: WeeChat 4.2.2)
2024-06-27 08:54:17 +0200m1dnight(~christoph@82.146.125.185)
2024-06-27 08:57:47 +0200echoreply(~echoreply@45.32.163.16) (Quit: WeeChat 2.8)
2024-06-27 08:58:20 +0200echoreply(~echoreply@45.32.163.16)
2024-06-27 09:11:59 +0200jle`(~jle`@2603:8001:3b02:84d4:89e:9b05:41f1:3af8) (Ping timeout: 256 seconds)
2024-06-27 09:12:41 +0200jle`(~jle`@2603:8001:3b02:84d4:143f:9778:ef77:7e4)
2024-06-27 09:17:24 +0200lortabac(~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4)
2024-06-27 09:20:37 +0200philopsos1(~caecilius@user/philopsos) (Ping timeout: 256 seconds)
2024-06-27 09:21:45 +0200madhavanmiui(~madhavanm@2409:40f4:10fe:dc03:8000::)
2024-06-27 09:24:17 +0200emmanuelux_(~emmanuelu@user/emmanuelux)
2024-06-27 09:24:18 +0200madhavanmiui(~madhavanm@2409:40f4:10fe:dc03:8000::) (Client Quit)
2024-06-27 09:24:48 +0200wbooze(~wbooze@2a02:908:1244:9a20:9512:47b7:c73:ce1d)
2024-06-27 09:27:35 +0200emmanuelux(~emmanuelu@user/emmanuelux) (Ping timeout: 264 seconds)
2024-06-27 09:36:30 +0200lxsameer(~lxsameer@Serene/lxsameer)
2024-06-27 09:47:51 +0200tv(~tv@user/tv)
2024-06-27 09:47:52 +0200tromp(~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl)
2024-06-27 10:03:37 +0200rvalue-(~rvalue@user/rvalue)
2024-06-27 10:04:47 +0200rvalue(~rvalue@user/rvalue) (Ping timeout: 264 seconds)
2024-06-27 10:06:04 +0200cfricke(~cfricke@user/cfricke)
2024-06-27 10:07:37 +0200rvalue-rvalue
2024-06-27 10:15:27 +0200chele(~chele@user/chele)
2024-06-27 10:44:27 +0200danse-nr3(~danse-nr3@151.44.219.215) (Ping timeout: 268 seconds)
2024-06-27 10:47:44 +0200tzh(~tzh@c-76-115-131-146.hsd1.or.comcast.net) (Quit: zzz)
2024-06-27 10:48:21 +0200dysthesis(~dysthesis@user/dysthesis)
2024-06-27 10:52:55 +0200danse-nr3(~danse-nr3@151.57.38.73)
2024-06-27 10:55:03 +0200dsrt^(~cd@c-98-242-74-66.hsd1.ga.comcast.net) (Ping timeout: 255 seconds)
2024-06-27 11:00:14 +0200rosco(~rosco@175.136.155.137) (Quit: Lost terminal)
2024-06-27 11:06:38 +0200tromp(~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…)
2024-06-27 11:10:29 +0200gabriel_sevecek(~gabriel@188-167-229-200.dynamic.chello.sk) (Ping timeout: 240 seconds)
2024-06-27 11:13:04 +0200tt123109783(~tt1231@syn-075-185-104-199.res.spectrum.com)
2024-06-27 11:14:51 +0200gehmehgeh(~user@user/gehmehgeh)
2024-06-27 11:15:17 +0200tt12310978(~tt1231@2603:6010:8700:4a81:219f:50d3:618a:a6ee) (Ping timeout: 240 seconds)
2024-06-27 11:15:18 +0200tt123109783tt12310978
2024-06-27 11:15:45 +0200zzz(~yin@user/zero)
2024-06-27 11:16:45 +0200gabriel_sevecek(~gabriel@188-167-229-200.dynamic.chello.sk)
2024-06-27 11:24:10 +0200gehmehgehgmg
2024-06-27 11:24:55 +0200__monty__(~toonn@user/toonn)
2024-06-27 11:41:35 +0200destituion(~destituio@2a02:2121:6cb:fbc3:3c0f:94ae:6844:a1fa) (Ping timeout: 256 seconds)
2024-06-27 11:42:33 +0200destituion(~destituio@85.221.111.174)
2024-06-27 11:50:46 +0200econo_(uid147250@id-147250.tinside.irccloud.com) (Quit: Connection closed for inactivity)
2024-06-27 11:51:13 +0200rosco(~rosco@175.136.155.137)
2024-06-27 12:01:34 +0200lortabac(~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) (Ping timeout: 246 seconds)
2024-06-27 12:03:41 +0200notzmv(~daniel@user/notzmv) (Ping timeout: 268 seconds)
2024-06-27 12:05:23 +0200tromp(~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl)
2024-06-27 12:12:27 +0200tv(~tv@user/tv) (Ping timeout: 255 seconds)
2024-06-27 12:14:14 +0200cheater_(~Username@user/cheater)
2024-06-27 12:18:11 +0200cheater(~Username@user/cheater) (Ping timeout: 268 seconds)
2024-06-27 12:18:11 +0200cheater_cheater
2024-06-27 12:19:08 +0200CiaoSen(~Jura@2a05:5800:2b1:7a00:e6b9:7aff:fe80:3d03)
2024-06-27 12:20:05 +0200soverysour(~soverysou@user/soverysour)
2024-06-27 12:20:23 +0200xff0x(~xff0x@2405:6580:b080:900:a4df:4a3a:94ab:11e4)
2024-06-27 12:24:42 +0200soverysour(~soverysou@user/soverysour) (Ping timeout: 256 seconds)
2024-06-27 12:24:59 +0200ubert(~Thunderbi@2a02:8109:ab8a:5a00:eae9:52ec:67d4:506b)
2024-06-27 12:25:26 +0200tv(~tv@user/tv)
2024-06-27 12:32:53 +0200tabaqui(~root@91.74.190.107) (Quit: WeeChat 4.2.2)
2024-06-27 12:35:56 +0200tabaqui(~root@91.74.190.107)
2024-06-27 12:36:58 +0200rosco(~rosco@175.136.155.137) (Quit: Lost terminal)
2024-06-27 12:37:18 +0200tabaqui(~root@91.74.190.107) (Client Quit)
2024-06-27 12:38:48 +0200tabaqui(~root@91.74.190.107)
2024-06-27 12:48:41 +0200lortabac(~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4)
2024-06-27 12:49:41 +0200gabriel_sevecek(~gabriel@188-167-229-200.dynamic.chello.sk) (Ping timeout: 240 seconds)
2024-06-27 12:56:03 +0200danse-nr3(~danse-nr3@151.57.38.73) (Ping timeout: 264 seconds)
2024-06-27 13:07:10 +0200gabriel_sevecek(~gabriel@188-167-229-200.dynamic.chello.sk)
2024-06-27 13:14:51 +0200sroso(~sroso@user/SrOso) (Quit: Leaving :))
2024-06-27 13:15:53 +0200notzmv(~daniel@user/notzmv)
2024-06-27 13:22:07 +0200Miroboru(~myrvoll@178-164-114.82.3p.ntebredband.no)
2024-06-27 13:22:57 +0200dsrt^(~cd@c-98-242-74-66.hsd1.ga.comcast.net)
2024-06-27 13:25:42 +0200notzmv(~daniel@user/notzmv) (Ping timeout: 268 seconds)
2024-06-27 13:26:23 +0200zzz(~yin@user/zero) (Ping timeout: 264 seconds)
2024-06-27 13:33:24 +0200zzz(~yin@user/zero)
2024-06-27 13:36:03 +0200acidjnk_new3(~acidjnk@p200300d6e714dc25e45fde1d7555be75.dip0.t-ipconnect.de) (Ping timeout: 256 seconds)
2024-06-27 13:41:02 +0200forell(~forell@user/forell)
2024-06-27 13:45:06 +0200tromp(~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…)
2024-06-27 13:45:43 +0200meritamen(~user@user/meritamen)
2024-06-27 13:48:46 +0200mreh(~matthew@host86-160-168-12.range86-160.btcentralplus.com)
2024-06-27 13:49:55 +0200 <mreh> are there any functions other than `id` and `const <foo>` that have the type forall a. a -> r?
2024-06-27 13:50:46 +0200 <mreh> or functions in the form `const <foo>`, rather
2024-06-27 13:51:35 +0200dysthesis(~dysthesis@user/dysthesis) (Quit: dysthesis)
2024-06-27 13:53:44 +0200 <ncf> depends on what r is
2024-06-27 13:54:09 +0200 <probie> :t flip seq
2024-06-27 13:54:10 +0200 <lambdabot> c -> a -> c
2024-06-27 13:54:38 +0200 <ncf> also yeah, are you interested in laziness shenanigans
2024-06-27 13:55:23 +0200 <probie> > const "foo" (error "whoops")
2024-06-27 13:55:25 +0200 <lambdabot> "foo"
2024-06-27 13:55:34 +0200 <probie> > flip seq "foo" (error "whoops")
2024-06-27 13:55:35 +0200 <lambdabot> "*Exception: whoops
2024-06-27 13:57:05 +0200 <mreh> It's an exercise in this textbook about existential types. "Are functions of type forall a. a -> r interesting?
2024-06-27 13:57:29 +0200 <mreh> the textbook is about Type level programming "Thinking in Types"
2024-06-27 13:57:59 +0200 <ncf> and what is r?
2024-06-27 13:59:31 +0200 <mreh> Well, I'm coming at it from the other end. It can only be (forall a. a -> a) which is id, and the only other function I could come up with which satisfies it is `const`
2024-06-27 13:59:41 +0200 <mreh> so r can only be the r in `const r`
2024-06-27 13:59:56 +0200 <mreh> I think that's what they're getting at.
2024-06-27 14:01:10 +0200 <ncf> ok i think the point of the exercise is to say what functions forall a. a -> r are *for a fixed r*
2024-06-27 14:01:23 +0200 <ncf> in which case you don't even get id
2024-06-27 14:01:41 +0200 <ncf> i claim that forall r, (forall a. a -> r) ≃ r
2024-06-27 14:02:03 +0200 <mreh> isomorphic?
2024-06-27 14:02:06 +0200 <ncf> yes
2024-06-27 14:02:32 +0200 <ncf> proof hint: use the yoneda lemma with Const r
2024-06-27 14:04:58 +0200 <mreh> it makes sense ituitively, so if it's isomorphic to r then I guess it's not very interesting
2024-06-27 14:09:28 +0200 <mreh> I dont think my category theory is good enough to prove it
2024-06-27 14:22:20 +0200tromp(~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl)
2024-06-27 14:24:33 +0200kuribas(~user@ip-188-118-57-242.reverse.destiny.be)
2024-06-27 14:25:34 +0200 <arahael> Out of curiousity more than anything, with haskell shakespeare templates (yesod), how can I like, #include one templated file in another?
2024-06-27 14:28:50 +0200 <arahael> Looks like what I probably want are the "whamlets". So that answers my own question.
2024-06-27 14:33:10 +0200kimiamania(~65804703@user/kimiamania) (Quit: PegeLinux)
2024-06-27 14:33:13 +0200acidjnk_new3(~acidjnk@p200300d6e714dc25e45fde1d7555be75.dip0.t-ipconnect.de)
2024-06-27 14:34:10 +0200kimiamania(~65804703@user/kimiamania)
2024-06-27 14:44:54 +0200wbooze(~wbooze@2a02:908:1244:9a20:9512:47b7:c73:ce1d) (Remote host closed the connection)
2024-06-27 15:03:00 +0200mreh(~matthew@host86-160-168-12.range86-160.btcentralplus.com) (Ping timeout: 255 seconds)
2024-06-27 15:04:02 +0200sawilagar(~sawilagar@user/sawilagar)
2024-06-27 15:05:39 +0200euleritian(~euleritia@77.22.252.56) (Ping timeout: 264 seconds)
2024-06-27 15:09:45 +0200euleritian(~euleritia@dynamic-176-001-208-051.176.1.pool.telefonica.de)
2024-06-27 15:09:51 +0200meritamen(~user@user/meritamen) (Ping timeout: 264 seconds)
2024-06-27 15:15:56 +0200bitdex(~bitdex@gateway/tor-sasl/bitdex) (Quit: = "")
2024-06-27 15:19:58 +0200hc(~hc@mail.hce.li) (Remote host closed the connection)
2024-06-27 15:22:32 +0200hc(~hc@mail.hce.li)
2024-06-27 15:23:00 +0200 <absence> Is there a way to use record update on a sum type, or do you have to un/rewrap the constructor manually, e.g. \case A a -> A a{....}?
2024-06-27 15:26:03 +0200cfricke(~cfricke@user/cfricke) (Ping timeout: 264 seconds)
2024-06-27 15:36:57 +0200 <kaol> absence: It should be fine. You'll get a runtime exception if it's not an A, of course.
2024-06-27 15:41:54 +0200 <absence> kaol: That's ... not good. No way to provide separate updates for each of the constructors?
2024-06-27 15:43:53 +0200 <kaol> Sure there is, if you pattern match.
2024-06-27 15:45:18 +0200Sgeo(~Sgeo@user/sgeo)
2024-06-27 15:45:58 +0200 <kaol> And if fields have same names (and types of course) you can just use same record update for any of the sum values.
2024-06-27 15:47:27 +0200 <kaol> With something like "data SumType = A { foo :: Int, bar :: Int } | B { foo :: Int, abc :: Int }" you can use upd x = x { foo = 1 }.
2024-06-27 15:48:40 +0200comonad(~comonad@p200300d02713e4006c810324fa66ca70.dip0.t-ipconnect.de)
2024-06-27 15:49:50 +0200 <absence> Right, but if I pattern match I have to do the manual constructor rewrapping, so I guess there are no shortcuts.
2024-06-27 15:51:51 +0200TMA(tma@twin.jikos.cz) (Ping timeout: 268 seconds)
2024-06-27 15:52:24 +0200 <kaol> Not necessarily. \case x@A{..} -> x { foo = 1 } works.
2024-06-27 15:53:50 +0200 <kaol> Or rather \case x@A{} -> x { foo = 1 }. That was record wildcards and for this no need for it.
2024-06-27 16:00:26 +0200 <absence> Nice, thanks!
2024-06-27 16:01:05 +0200wbooze(~wbooze@2a02:908:1244:9a20:d426:d0e1:e498:10ea)
2024-06-27 16:03:04 +0200zzz(~yin@user/zero) (Ping timeout: 246 seconds)
2024-06-27 16:04:52 +0200TMA(tma@twin.jikos.cz)
2024-06-27 16:12:12 +0200lortabac(~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) (Quit: WeeChat 4.2.2)
2024-06-27 16:12:15 +0200EvanReyes sum type with field names with suspicion
2024-06-27 16:14:03 +0200michalz(~michalz@185.246.207.215) (Ping timeout: 264 seconds)
2024-06-27 16:16:40 +0200euleritian(~euleritia@dynamic-176-001-208-051.176.1.pool.telefonica.de) (Read error: Connection reset by peer)
2024-06-27 16:18:54 +0200euleritian(~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de)
2024-06-27 16:29:33 +0200zzz(~yin@user/zero)
2024-06-27 16:31:41 +0200lxsameer(~lxsameer@Serene/lxsameer) (Ping timeout: 240 seconds)
2024-06-27 16:38:16 +0200noscript(~noscript@user/earldouglas) (WeeChat 4.2.1)
2024-06-27 16:48:55 +0200pavonia(~user@user/siracusa)
2024-06-27 16:52:36 +0200dsrt^(~cd@c-98-242-74-66.hsd1.ga.comcast.net) (Ping timeout: 268 seconds)
2024-06-27 16:54:25 +0200lxsameer(~lxsameer@Serene/lxsameer)
2024-06-27 17:02:23 +0200ocra8(~ocra8@user/ocra8) (Ping timeout: 260 seconds)
2024-06-27 17:04:23 +0200ocra8(ocra8@user/ocra8)
2024-06-27 17:07:27 +0200destituion(~destituio@85.221.111.174) (Ping timeout: 264 seconds)
2024-06-27 17:07:32 +0200mreh(~matthew@host86-160-168-12.range86-160.btcentralplus.com)
2024-06-27 17:10:08 +0200ocra8(ocra8@user/ocra8) (Excess Flood)
2024-06-27 17:15:42 +0200euphores(~SASL_euph@user/euphores) (Quit: Leaving.)
2024-06-27 17:19:11 +0200destituion(~destituio@2a02:2121:6cb:fbc3:ec2c:8d1b:640f:1406)
2024-06-27 17:21:37 +0200euphores(~SASL_euph@user/euphores)
2024-06-27 17:36:04 +0200zmt00(~zmt00@user/zmt00) (Ping timeout: 268 seconds)
2024-06-27 17:36:23 +0200zmt00(~zmt00@user/zmt00)
2024-06-27 17:45:49 +0200causal(~eric@50.35.88.207)
2024-06-27 17:54:23 +0200tromp(~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…)
2024-06-27 18:06:41 +0200chele(~chele@user/chele) (Remote host closed the connection)
2024-06-27 18:10:22 +0200CiaoSen(~Jura@2a05:5800:2b1:7a00:e6b9:7aff:fe80:3d03) (Ping timeout: 256 seconds)
2024-06-27 18:11:29 +0200irfan(~irfan@user/irfan)
2024-06-27 18:12:05 +0200Tuplanolla(~Tuplanoll@91-159-69-59.elisa-laajakaista.fi)
2024-06-27 18:12:31 +0200econo_(uid147250@id-147250.tinside.irccloud.com)
2024-06-27 18:14:55 +0200dsrt^(~cd@c-98-242-74-66.hsd1.ga.comcast.net)
2024-06-27 18:15:49 +0200irfan(~irfan@user/irfan) (Quit: leaving)
2024-06-27 18:16:36 +0200irfan(~irfan@user/irfan)
2024-06-27 18:17:16 +0200zmt01(~zmt00@user/zmt00)
2024-06-27 18:17:54 +0200irfanflareon
2024-06-27 18:18:00 +0200zmt00(~zmt00@user/zmt00) (Ping timeout: 268 seconds)
2024-06-27 18:18:35 +0200euleritian(~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Ping timeout: 264 seconds)
2024-06-27 18:18:45 +0200flareon(~irfan@user/irfan) (Client Quit)
2024-06-27 18:19:11 +0200euleritian(~euleritia@dynamic-176-001-208-051.176.1.pool.telefonica.de)
2024-06-27 18:22:36 +0200tromp(~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl)
2024-06-27 18:23:05 +0200sord937(~sord937@gateway/tor-sasl/sord937) (Remote host closed the connection)
2024-06-27 18:24:07 +0200sord937(~sord937@gateway/tor-sasl/sord937)
2024-06-27 18:28:47 +0200kuribas(~user@ip-188-118-57-242.reverse.destiny.be) (Ping timeout: 264 seconds)
2024-06-27 18:32:07 +0200glguy(g@libera/staff/glguy) (Remote host closed the connection)
2024-06-27 18:33:14 +0200glguy(g@libera/staff/glguy)
2024-06-27 18:36:23 +0200ocra8(ocra8@user/ocra8)
2024-06-27 18:37:27 +0200tromp(~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…)
2024-06-27 18:50:58 +0200sprout_(~quassel@2a02-a448-3a80-0-d123-5da7-9ae5-44be.fixed6.kpn.net)
2024-06-27 18:51:35 +0200soverysour(~soverysou@81.196.150.219)
2024-06-27 18:51:35 +0200soverysour(~soverysou@81.196.150.219) (Changing host)
2024-06-27 18:51:35 +0200soverysour(~soverysou@user/soverysour)
2024-06-27 18:51:49 +0200ocra8(ocra8@user/ocra8) (Ping timeout: 256 seconds)
2024-06-27 18:51:55 +0200sprout(~quassel@2a02-a448-3a80-0-3430-92e6-1565-73f9.fixed6.kpn.net) (Ping timeout: 268 seconds)
2024-06-27 18:53:43 +0200ocra8(~ocra8@user/ocra8)
2024-06-27 19:05:58 +0200tromp(~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl)
2024-06-27 19:06:00 +0200mreh(~matthew@host86-160-168-12.range86-160.btcentralplus.com) (Ping timeout: 255 seconds)
2024-06-27 19:07:12 +0200sprout_sprout
2024-06-27 19:11:53 +0200ubert(~Thunderbi@2a02:8109:ab8a:5a00:eae9:52ec:67d4:506b) (Remote host closed the connection)
2024-06-27 19:13:27 +0200qqq(~qqq@92.43.167.61)
2024-06-27 19:16:47 +0200soverysour(~soverysou@user/soverysour) (Ping timeout: 260 seconds)
2024-06-27 19:18:32 +0200wz1000(~zubin@static.11.113.47.78.clients.your-server.de) (Ping timeout: 252 seconds)
2024-06-27 19:30:55 +0200wz1000(~zubin@static.11.113.47.78.clients.your-server.de)
2024-06-27 19:39:33 +0200 <lxsameer> Either I'm blind or too tired to notice it. but do you see any syntax error here? `newdata Backend = Backend {pool :: !DBPool}`
2024-06-27 19:41:10 +0200 <geekosaur> also check the immediately preceding code, sometimes you get an error because ghc is looking for a close paren or etc., or you have incorrect layout
2024-06-27 19:41:21 +0200 <Leary> "newdata"?
2024-06-27 19:41:43 +0200 <Leary> If that's meant to be a newtype, then the ! is an error too.
2024-06-27 19:42:01 +0200 <geekosaur> oh, whoops, yes, misread
2024-06-27 19:42:02 +0200 <lxsameer> jaysus, cheers
2024-06-27 19:42:09 +0200 <geekosaur> newdata isn't a word 🙂
2024-06-27 19:42:11 +0200 <lxsameer> so I'm blind then :)))
2024-06-27 19:42:34 +0200 <lxsameer> I was looking at this for like 2 hours
2024-06-27 19:42:50 +0200soverysour(~soverysou@81.196.150.219)
2024-06-27 19:42:50 +0200soverysour(~soverysou@81.196.150.219) (Changing host)
2024-06-27 19:42:50 +0200soverysour(~soverysou@user/soverysour)
2024-06-27 19:43:28 +0200 <Leary> Consider using syntax highlighting in your editor. It will make errors like this pretty obvious.
2024-06-27 19:44:43 +0200 <lxsameer> I do actually, funny enough I ignored the error as well :D
2024-06-27 19:45:33 +0200 <haskellbridge> <iqubic (she/her)> Wait... is it impossible to have strict data in a newtype wrapper?
2024-06-27 19:46:57 +0200 <zzz> {-# LANGUAGE NewDataDeclarations #-}
2024-06-27 19:47:08 +0200 <haskellbridge> <iqubic (she/her)> What's that do?
2024-06-27 19:47:49 +0200 <zzz> iqubic if you mean the pragma i just made up, probably throws an error
2024-06-27 19:50:53 +0200 <zzz> iqubic: you can't have strict annotations in newtypes
2024-06-27 19:51:09 +0200 <Leary> The newtype wrapper does not ultimately exist, so there's nothing meaningfully different to link the demand to. `Con !x` is essentially `\x -> x `seq` Con x`, but if `Con` is a newtype wrapper then that degenerates to `\x -> x `seq` x`.
2024-06-27 19:55:32 +0200tromp(~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…)
2024-06-27 19:56:35 +0200tzh(~tzh@c-76-115-131-146.hsd1.or.comcast.net)
2024-06-27 19:57:17 +0200 <zzz> f (MyNewtypeConstructor _) = () ; f undefined -- this pattern match won't fail because MyNewtypeWrapper doesn't actually exist
2024-06-27 19:58:16 +0200 <zzz> so it's the same as `f _ = ()`
2024-06-27 20:04:25 +0200 <zzz> f (_ :: MyNewType) = () -- to be precise
2024-06-27 20:05:11 +0200 <zzz> s/MyNewtypeWrapper/MyNewtypeConstructor
2024-06-27 20:07:43 +0200pavonia(~user@user/siracusa) (Quit: Bye!)
2024-06-27 20:11:51 +0200mikess(~mikess@user/mikess)
2024-06-27 20:12:19 +0200euphores(~SASL_euph@user/euphores) (Quit: Leaving.)
2024-06-27 20:12:42 +0200Lord_of_Life(~Lord@user/lord-of-life/x-2819915) (Ping timeout: 268 seconds)
2024-06-27 20:13:09 +0200ft(~ft@p4fc2ab80.dip0.t-ipconnect.de)
2024-06-27 20:14:59 +0200Lord_of_Life(~Lord@user/lord-of-life/x-2819915)
2024-06-27 20:17:20 +0200safinaskar(~quassel@212.73.77.104)
2024-06-27 20:17:30 +0200safinaskar(~quassel@212.73.77.104) ()
2024-06-27 20:18:56 +0200euphores(~SASL_euph@user/euphores)
2024-06-27 20:20:58 +0200philopsos1(~caecilius@user/philopsos)
2024-06-27 20:21:55 +0200 <lxsameer> is there any thread (os thread) local state in haskell's concurrency?
2024-06-27 20:24:11 +0200tromp(~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl)
2024-06-27 20:24:12 +0200 <EvanR> not normally, but if you're linking to a library that uses thread local state you can ask for a thread to be bound to one OS thread
2024-06-27 20:24:33 +0200 <lxsameer> got it, thank you
2024-06-27 20:26:16 +0200soverysour(~soverysou@user/soverysour) (Ping timeout: 268 seconds)
2024-06-27 20:27:10 +0200target_i(~target_i@user/target-i/x-6023099)
2024-06-27 20:33:56 +0200kuribas(~user@ptr-17d51ep8o8jltn94jrx.18120a2.ip6.access.telenet.be)
2024-06-27 20:40:22 +0200pierrot(~pi@user/pierrot) (Read error: Connection reset by peer)
2024-06-27 20:45:40 +0200pierrot(~pi@user/pierrot)
2024-06-27 20:51:35 +0200soverysour(~soverysou@81.196.150.219)
2024-06-27 20:51:36 +0200soverysour(~soverysou@81.196.150.219) (Changing host)
2024-06-27 20:51:36 +0200soverysour(~soverysou@user/soverysour)
2024-06-27 20:51:57 +0200tabemann__(~tabemann@2600:1700:7990:24e0:a80c:5b74:1624:82db) (Remote host closed the connection)
2024-06-27 20:51:59 +0200geekosaur(sid609282@xmonad/geekosaur) (Ping timeout: 260 seconds)
2024-06-27 20:51:59 +0200hamishmack(sid389057@id-389057.hampstead.irccloud.com) (Ping timeout: 260 seconds)
2024-06-27 20:52:10 +0200hamishmack(sid389057@id-389057.hampstead.irccloud.com)
2024-06-27 20:52:10 +0200geekosaur(sid609282@xmonad/geekosaur)
2024-06-27 20:52:11 +0200tabemann__(~tabemann@2600:1700:7990:24e0:fc27:3b97:9d0e:b091)
2024-06-27 20:56:26 +0200soverysour(~soverysou@user/soverysour) (Ping timeout: 252 seconds)
2024-06-27 21:00:52 +0200sord937(~sord937@gateway/tor-sasl/sord937) (Remote host closed the connection)
2024-06-27 21:01:43 +0200sord937(~sord937@gateway/tor-sasl/sord937)
2024-06-27 21:11:39 +0200kuribas(~user@ptr-17d51ep8o8jltn94jrx.18120a2.ip6.access.telenet.be) (Remote host closed the connection)
2024-06-27 21:14:15 +0200ocra8(~ocra8@user/ocra8) (Ping timeout: 272 seconds)
2024-06-27 21:26:05 +0200soverysour(~soverysou@user/soverysour)
2024-06-27 21:30:27 +0200soverysour(~soverysou@user/soverysour) (Ping timeout: 255 seconds)
2024-06-27 21:32:03 +0200Guest84(~Guest84@pool-174-112-127-99.cpe.net.cable.rogers.com)
2024-06-27 21:33:00 +0200tromp(~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…)
2024-06-27 21:35:12 +0200 <Guest84> Im working on a very small parser for my own usage, but i havent been able to properly encode parsing error messages. So, given some `newtype Parser s m a = Parser {runParser :: s -> m (a,s)}` how would you preserve the ease of monadic parsing with error messages? I've tried doing `m = Either String`, but I couldn't figure out how to use that with
2024-06-27 21:35:13 +0200 <Guest84> the monadic combinators. Any ideas on how I could do this?
2024-06-27 21:42:38 +0200machinedgod(~machinedg@d173-183-246-216.abhsia.telus.net) (Ping timeout: 252 seconds)
2024-06-27 21:44:41 +0200soverysour(~soverysou@81.196.150.219)
2024-06-27 21:44:41 +0200soverysour(~soverysou@81.196.150.219) (Changing host)
2024-06-27 21:44:41 +0200soverysour(~soverysou@user/soverysour)
2024-06-27 21:49:50 +0200soverysour(~soverysou@user/soverysour) (Ping timeout: 268 seconds)
2024-06-27 21:50:47 +0200 <Leary> Guest84: I would use transformers as building blocks and derive: `newtype ParserT s e m a = ParserT{ unParserT :: StateT s (ExceptT e m) a } deriving (Functor, Applicative, Alternative, Monad)`
2024-06-27 21:53:07 +0200tromp(~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl)
2024-06-27 21:53:08 +0200Miroboru(~myrvoll@178-164-114.82.3p.ntebredband.no) (Quit: Lost terminal)
2024-06-27 21:54:01 +0200pavonia(~user@user/siracusa)
2024-06-27 21:56:02 +0200sord937(~sord937@gateway/tor-sasl/sord937) (Ping timeout: 260 seconds)
2024-06-27 21:56:23 +0200lxsameer(~lxsameer@Serene/lxsameer) (Ping timeout: 264 seconds)
2024-06-27 21:58:11 +0200sord937(~sord937@gateway/tor-sasl/sord937)
2024-06-27 22:00:53 +0200michalz(~michalz@185.246.207.203)
2024-06-27 22:03:19 +0200 <Guest84> Leary: Thanks, that seems to solve my problem. Also, is there any specific reason to use StateT rather than writing `s -> ExceptT e m (a, s)`?
2024-06-27 22:04:41 +0200euleritian(~euleritia@dynamic-176-001-208-051.176.1.pool.telefonica.de) (Read error: Connection reset by peer)
2024-06-27 22:05:03 +0200euleritian(~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de)
2024-06-27 22:05:18 +0200 <EvanR> combining mtl classes gives you automagic lifting
2024-06-27 22:05:37 +0200 <ncf> it gives you a Monad instance...
2024-06-27 22:05:46 +0200 <EvanR> and that
2024-06-27 22:08:37 +0200Guest84(~Guest84@pool-174-112-127-99.cpe.net.cable.rogers.com) (Quit: Client closed)
2024-06-27 22:10:01 +0200Guest84(~Guest84@pool-174-112-127-99.cpe.net.cable.rogers.com)
2024-06-27 22:17:57 +0200dsrt^(~cd@c-98-242-74-66.hsd1.ga.comcast.net) (Ping timeout: 256 seconds)
2024-06-27 22:24:13 +0200philopsos1(~caecilius@user/philopsos) (Ping timeout: 246 seconds)
2024-06-27 22:29:54 +0200stiell(~stiell@gateway/tor-sasl/stiell) (Remote host closed the connection)
2024-06-27 22:30:45 +0200stiell(~stiell@gateway/tor-sasl/stiell)
2024-06-27 22:46:11 +0200gabriel_sevecek(~gabriel@188-167-229-200.dynamic.chello.sk) (Ping timeout: 264 seconds)
2024-06-27 22:50:46 +0200waleee(~waleee@h-176-10-144-38.NA.cust.bahnhof.se)
2024-06-27 22:54:08 +0200wbooze(~wbooze@2a02:908:1244:9a20:d426:d0e1:e498:10ea) (Remote host closed the connection)
2024-06-27 23:02:23 +0200AlexZenon(~alzenon@94.233.241.180) (Ping timeout: 252 seconds)
2024-06-27 23:02:32 +0200 <haskellbridge> <zwro> testing
2024-06-27 23:02:42 +0200mreh(~matthew@host86-160-168-12.range86-160.btcentralplus.com)
2024-06-27 23:02:54 +0200 <haskellbridge> <zwro> * test
2024-06-27 23:03:51 +0200 <haskellbridge> <magic_rb> Test back
2024-06-27 23:04:46 +0200 <geekosaur> you're here
2024-06-27 23:05:25 +0200gorignak(~gorignak@user/gorignak) (Quit: quit)
2024-06-27 23:05:32 +0200AlexZenon(~alzenon@94.233.241.180)
2024-06-27 23:06:26 +0200 <haskellbridge> <zwro> i wanted to see how edits translate to irc
2024-06-27 23:07:23 +0200gorignak(~gorignak@user/gorignak)
2024-06-27 23:08:15 +0200 <zzz> are there any current plans in the vein of Haskel Prime?
2024-06-27 23:08:36 +0200 <haskellbridge> <zwro> * edited messages
2024-06-27 23:08:45 +0200takuan(~takuan@178-116-218-225.access.telenet.be) (Remote host closed the connection)
2024-06-27 23:09:26 +0200 <haskellbridge> <zwro> * editing messages
2024-06-27 23:10:32 +0200 <haskellbridge> <zwro> testing completed [2 passed] [1 failed]
2024-06-27 23:11:15 +0200Guest84(~Guest84@pool-174-112-127-99.cpe.net.cable.rogers.com) (Quit: Client closed)
2024-06-27 23:13:17 +0200euleritian(~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Ping timeout: 240 seconds)
2024-06-27 23:18:33 +0200 <cheater> does anyone know if haskell works under nix on windows / WSL2?
2024-06-27 23:19:56 +0200euleritian(~euleritia@176.2.138.94)
2024-06-27 23:29:50 +0200gabriel_sevecek(~gabriel@188-167-229-200.dynamic.chello.sk)
2024-06-27 23:31:04 +0200euleritian(~euleritia@176.2.138.94) (Ping timeout: 246 seconds)
2024-06-27 23:32:47 +0200euleritian(~euleritia@dynamic-176-002-138-019.176.2.pool.telefonica.de)
2024-06-27 23:38:05 +0200 <dibblego> after `cabal install --lib --global lens` then build-depends: lens in a .cabal file, why does `cabal repl` then need to reinstall the lens library?
2024-06-27 23:46:04 +0200m5zs7k(aquares@web10.mydevil.net) (Ping timeout: 268 seconds)
2024-06-27 23:47:00 +0200target_i(~target_i@user/target-i/x-6023099) (Quit: leaving)
2024-06-27 23:47:22 +0200m5zs7k(aquares@web10.mydevil.net)
2024-06-27 23:47:57 +0200 <jackdk> the solver has likely decided that the version of lens in the global package db is not compatible with the other bounds on your package
2024-06-27 23:48:02 +0200euleritian(~euleritia@dynamic-176-002-138-019.176.2.pool.telefonica.de) (Ping timeout: 252 seconds)
2024-06-27 23:48:53 +0200euleritian(~euleritia@176.2.74.187)
2024-06-27 23:51:45 +0200 <dibblego> hmm, I'll use == and see if that works
2024-06-27 23:52:12 +0200michalz(~michalz@185.246.207.203) (Quit: ZNC 1.9.0 - https://znc.in)
2024-06-27 23:55:10 +0200 <dibblego> hmm, I ued == and it worked, even though I was using >= before, and it was compatible
2024-06-27 23:55:47 +0200 <jackdk> Did it change the versions of other libraries?