| 2024-06-27 00:07:58 +0200 | safinaskar | (~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 +0200 | Sgeo | (~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 +0200 | acidjnk_new3 | (~acidjnk@p200300d6e714dc96bd88011075acd305.dip0.t-ipconnect.de) (Ping timeout: 246 seconds) |
| 2024-06-27 00:24:04 +0200 | tromp | (~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 +0200 | michalz | (~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 +0200 | CiaoSen | (~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 +0200 | waleee | (~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 +0200 | waleee | (~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 +0200 | JimL | (~quassel@89.162.16.26) (Ping timeout: 268 seconds) |
| 2024-06-27 00:51:09 +0200 | waleee | (~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 +0200 | waleee | (~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 +0200 | gmg | (~user@user/gehmehgeh) (Quit: Leaving) |
| 2024-06-27 01:25:39 +0200 | Garbanzo | (~Garbanzo@2602:304:6eac:dc10::46) (Remote host closed the connection) |
| 2024-06-27 01:39:24 +0200 | emmanuelux | (~emmanuelu@user/emmanuelux) |
| 2024-06-27 01:43:11 +0200 | zzz | (~yin@user/zero) (Ping timeout: 264 seconds) |
| 2024-06-27 01:50:04 +0200 | zzz | (~yin@user/zero) |
| 2024-06-27 01:50:24 +0200 | xsarnik | (xsarnik@lounge.fi.muni.cz) (Quit: Ping timeout (120 seconds)) |
| 2024-06-27 01:50:24 +0200 | xstill_ | (xstill@fimu/xstill) (Quit: Ping timeout (120 seconds)) |
| 2024-06-27 01:50:58 +0200 | malte | (~malte@mal.tc) (Read error: Connection reset by peer) |
| 2024-06-27 01:51:12 +0200 | malte | (~malte@mal.tc) |
| 2024-06-27 01:51:38 +0200 | rvalue | (~rvalue@user/rvalue) (Quit: ZNC - https://znc.in) |
| 2024-06-27 01:51:51 +0200 | it_ | (~quassel@v2202212189510211193.supersrv.de) (Quit: No Ping reply in 180 seconds.) |
| 2024-06-27 01:52:00 +0200 | rvalue | (~rvalue@user/rvalue) |
| 2024-06-27 01:52:56 +0200 | xstill_ | (xstill@fimu/xstill) |
| 2024-06-27 01:53:15 +0200 | it_ | (~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 +0200 | xsarnik | (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 +0200 | sawilagar | (~sawilagar@user/sawilagar) (Ping timeout: 268 seconds) |
| 2024-06-27 02:02:55 +0200 | acarrico | (~acarrico@dhcp-68-142-57-215.greenmountainaccess.net) (Quit: Leaving.) |
| 2024-06-27 02:05:05 +0200 | SoF | (~skius@user/skius) (Remote host closed the connection) |
| 2024-06-27 02:08:40 +0200 | waleee | (~waleee@h-176-10-144-38.NA.cust.bahnhof.se) (Ping timeout: 246 seconds) |
| 2024-06-27 02:13:48 +0200 | waleee | (~waleee@h-176-10-144-38.NA.cust.bahnhof.se) |
| 2024-06-27 02:14:39 +0200 | ryanbooker | (uid4340@id-4340.hampstead.irccloud.com) |
| 2024-06-27 02:20:15 +0200 | waleee | (~waleee@h-176-10-144-38.NA.cust.bahnhof.se) (Ping timeout: 255 seconds) |
| 2024-06-27 02:24:13 +0200 | CrunchyFlakes | (~CrunchyFl@ip92348280.dynamic.kabel-deutschland.de) (Read error: Connection reset by peer) |
| 2024-06-27 02:26:51 +0200 | CrunchyFlakes | (~CrunchyFl@ip92348280.dynamic.kabel-deutschland.de) |
| 2024-06-27 02:33:46 +0200 | henry40408 | (~henry4040@175.182.111.183) (Quit: Ping timeout (120 seconds)) |
| 2024-06-27 02:34:12 +0200 | henry40408 | (~henry4040@175.182.111.183) |
| 2024-06-27 02:36:13 +0200 | hgolden | (~hgolden@2603:8000:9d00:3ed1:2678:8497:aa5c:7fa9) (Remote host closed the connection) |
| 2024-06-27 02:38:06 +0200 | hgolden | (~hgolden@2603:8000:9d00:3ed1:2678:8497:aa5c:7fa9) |
| 2024-06-27 02:40:11 +0200 | philopsos1 | (~caecilius@user/philopsos) (Ping timeout: 264 seconds) |
| 2024-06-27 03:02:15 +0200 | aforemny | (~aforemny@i59F516D5.versanet.de) (Ping timeout: 268 seconds) |
| 2024-06-27 03:02:37 +0200 | aforemny | (~aforemny@i59F516D5.versanet.de) |
| 2024-06-27 03:06:45 +0200 | joeyadams | (~joeyadams@2603:6010:5100:2ed:93a8:3ab0:fdc9:ca35) (Quit: Leaving) |
| 2024-06-27 03:16:15 +0200 | xff0x | (~xff0x@2405:6580:b080:900:374:70e:871e:8e7b) (Ping timeout: 256 seconds) |
| 2024-06-27 03:25:13 +0200 | safinaskar | (~quassel@212.73.77.104) () |
| 2024-06-27 03:25:44 +0200 | xstill_ | (xstill@fimu/xstill) (Quit: Ping timeout (120 seconds)) |
| 2024-06-27 03:25:56 +0200 | xsarnik | (xsarnik@lounge.fi.muni.cz) (Quit: Ping timeout (120 seconds)) |
| 2024-06-27 03:26:04 +0200 | xstill_ | (xstill@fimu/xstill) |
| 2024-06-27 03:26:29 +0200 | xsarnik | (xsarnik@lounge.fi.muni.cz) |
| 2024-06-27 03:27:16 +0200 | it_ | (~quassel@v2202212189510211193.supersrv.de) (Quit: No Ping reply in 180 seconds.) |
| 2024-06-27 03:28:25 +0200 | it_ | (~quassel@v2202212189510211193.supersrv.de) |
| 2024-06-27 03:46:55 +0200 | phma | (phma@2001:5b0:210f:1ad8:36db:ca4e:16e7:7eb) (Read error: Connection reset by peer) |
| 2024-06-27 03:47:04 +0200 | rosco | (~rosco@175.136.155.137) |
| 2024-06-27 03:47:21 +0200 | phma | (~phma@host-67-44-208-96.hnremote.net) |
| 2024-06-27 03:47:23 +0200 | machinedgod | (~machinedg@d173-183-246-216.abhsia.telus.net) (Ping timeout: 264 seconds) |
| 2024-06-27 04:00:50 +0200 | xff0x | (~xff0x@125x103x176x34.ap125.ftth.ucom.ne.jp) |
| 2024-06-27 04:07:05 +0200 | soverysour | (~soverysou@81.196.150.219) |
| 2024-06-27 04:07:05 +0200 | soverysour | (~soverysou@81.196.150.219) (Changing host) |
| 2024-06-27 04:07:05 +0200 | soverysour | (~soverysou@user/soverysour) |
| 2024-06-27 04:07:11 +0200 | xff0x | (~xff0x@125x103x176x34.ap125.ftth.ucom.ne.jp) (Ping timeout: 252 seconds) |
| 2024-06-27 04:08:05 +0200 | dequbed | (~dequbed@banana-new.kilobyte22.de) (Ping timeout: 240 seconds) |
| 2024-06-27 04:08:30 +0200 | nadja | (~dequbed@banana-new.kilobyte22.de) |
| 2024-06-27 04:09:10 +0200 | xff0x | (~xff0x@125x103x176x34.ap125.ftth.ucom.ne.jp) |
| 2024-06-27 04:11:24 +0200 | soverysour | (~soverysou@user/soverysour) (Ping timeout: 255 seconds) |
| 2024-06-27 04:48:15 +0200 | td_ | (~td@i53870920.versanet.de) (Ping timeout: 264 seconds) |
| 2024-06-27 04:49:52 +0200 | td_ | (~td@i53870923.versanet.de) |
| 2024-06-27 05:01:50 +0200 | Unicorn_Princess | (~Unicorn_P@user/Unicorn-Princess/x-3540542) (Remote host closed the connection) |
| 2024-06-27 05:05:17 +0200 | aaronv | (~aaronv@user/aaronv) |
| 2024-06-27 05:16:39 +0200 | aaronv | (~aaronv@user/aaronv) (Remote host closed the connection) |
| 2024-06-27 05:17:03 +0200 | aaronv | (~aaronv@user/aaronv) |
| 2024-06-27 05:22:32 +0200 | MrFox | (~MrFox___@216-151-184-162.lon.as62651.net) |
| 2024-06-27 05:23:42 +0200 | MrFox | darmario |
| 2024-06-27 05:23:46 +0200 | darmario | (~MrFox___@216-151-184-162.lon.as62651.net) (Changing host) |
| 2024-06-27 05:23:46 +0200 | darmario | (~MrFox___@user/darmario) |
| 2024-06-27 05:37:01 +0200 | aforemny_ | (~aforemny@i59F516E5.versanet.de) |
| 2024-06-27 05:38:35 +0200 | aforemny | (~aforemny@i59F516D5.versanet.de) (Ping timeout: 268 seconds) |
| 2024-06-27 05:40:21 +0200 | madhavanmiui | (~madhavanm@2409:40f4:3047:1afd:8000::) |
| 2024-06-27 05:46:39 +0200 | madhavanmiui | (~madhavanm@2409:40f4:3047:1afd:8000::) (Read error: Connection reset by peer) |
| 2024-06-27 05:46:47 +0200 | zzz | (~yin@user/zero) (Ping timeout: 264 seconds) |
| 2024-06-27 05:46:55 +0200 | madhavanmiui | (~madhavanm@2409:40f4:3047:1afd:8000::) |
| 2024-06-27 05:48:40 +0200 | zzz | (~yin@user/zero) |
| 2024-06-27 05:48:53 +0200 | madhavanmiui | (~madhavanm@2409:40f4:3047:1afd:8000::) (Read error: Connection reset by peer) |
| 2024-06-27 05:49:06 +0200 | madhavanmiui | (~madhavanm@152.58.250.215) |
| 2024-06-27 05:51:21 +0200 | madhavanmiui | (~madhavanm@152.58.250.215) (Client Quit) |
| 2024-06-27 06:03:33 +0200 | zzz | (~yin@user/zero) (Ping timeout: 268 seconds) |
| 2024-06-27 06:04:04 +0200 | philopsos1 | (~caecilius@user/philopsos) |
| 2024-06-27 06:04:11 +0200 | xff0x | (~xff0x@125x103x176x34.ap125.ftth.ucom.ne.jp) (Ping timeout: 264 seconds) |
| 2024-06-27 06:05:46 +0200 | xff0x | (~xff0x@125x103x176x34.ap125.ftth.ucom.ne.jp) |
| 2024-06-27 06:16:11 +0200 | philopsos1 | (~caecilius@user/philopsos) (Ping timeout: 264 seconds) |
| 2024-06-27 06:16:28 +0200 | darmario | (~MrFox___@user/darmario) (Leaving) |
| 2024-06-27 06:24:23 +0200 | ryanbooker | (uid4340@id-4340.hampstead.irccloud.com) (Quit: Connection closed for inactivity) |
| 2024-06-27 06:34:17 +0200 | philopsos1 | (~caecilius@user/philopsos) |
| 2024-06-27 06:34:58 +0200 | wbooze | (~wbooze@2a02:908:1244:9a20:3d84:fc89:d93b:3334) (Remote host closed the connection) |
| 2024-06-27 06:58:31 +0200 | sroso | (~sroso@user/SrOso) |
| 2024-06-27 07:08:18 +0200 | xff0x | (~xff0x@125x103x176x34.ap125.ftth.ucom.ne.jp) (Ping timeout: 268 seconds) |
| 2024-06-27 07:16:02 +0200 | monochrom | (trebla@216.138.220.146) (Quit: ZNC 1.9.0+deb2build3 - https://znc.in) |
| 2024-06-27 07:23:55 +0200 | monochrom | (trebla@216.138.220.146) |
| 2024-06-27 07:24:57 +0200 | takuan | (~takuan@178-116-218-225.access.telenet.be) |
| 2024-06-27 07:30:11 +0200 | Sgeo | (~Sgeo@user/sgeo) (Read error: Connection reset by peer) |
| 2024-06-27 07:35:59 +0200 | philopsos1 | (~caecilius@user/philopsos) (Ping timeout: 264 seconds) |
| 2024-06-27 07:39:33 +0200 | causal | (~eric@50.35.88.207) (Quit: WeeChat 4.3.1) |
| 2024-06-27 07:40:24 +0200 | xff0x | (~xff0x@125x103x176x34.ap125.ftth.ucom.ne.jp) |
| 2024-06-27 07:42:53 +0200 | michalz | (~michalz@185.246.207.215) |
| 2024-06-27 07:46:53 +0200 | acidjnk_new3 | (~acidjnk@p200300d6e714dc25e45fde1d7555be75.dip0.t-ipconnect.de) |
| 2024-06-27 07:48:14 +0200 | danse-nr3 | (~danse-nr3@151.44.219.215) |
| 2024-06-27 07:49:17 +0200 | danse-nr3 | (~danse-nr3@151.44.219.215) (Remote host closed the connection) |
| 2024-06-27 07:49:42 +0200 | danse-nr3 | (~danse-nr3@151.44.219.215) |
| 2024-06-27 07:55:39 +0200 | philopsos1 | (~caecilius@user/philopsos) |
| 2024-06-27 07:58:50 +0200 | dcoutts_ | (~duncan@2a00:23c6:1c8d:901:b94:4566:9d63:4848) |
| 2024-06-27 08:00:55 +0200 | rosco | (~rosco@175.136.155.137) (Quit: Lost terminal) |
| 2024-06-27 08:02:23 +0200 | forell | (~forell@user/forell) (Ping timeout: 264 seconds) |
| 2024-06-27 08:03:48 +0200 | aaronv | (~aaronv@user/aaronv) (Ping timeout: 268 seconds) |
| 2024-06-27 08:05:23 +0200 | machinedgod | (~machinedg@d173-183-246-216.abhsia.telus.net) |
| 2024-06-27 08:06:43 +0200 | xff0x | (~xff0x@125x103x176x34.ap125.ftth.ucom.ne.jp) (Quit: xff0x) |
| 2024-06-27 08:09:31 +0200 | pavonia | (~user@user/siracusa) (Quit: Bye!) |
| 2024-06-27 08:13:39 +0200 | tv | (~tv@user/tv) (Ping timeout: 260 seconds) |
| 2024-06-27 08:22:38 +0200 | rosco | (~rosco@175.136.155.137) |
| 2024-06-27 08:29:14 +0200 | sord937 | (~sord937@gateway/tor-sasl/sord937) |
| 2024-06-27 08:53:03 +0200 | ft | (~ft@p4fc2ab80.dip0.t-ipconnect.de) (Ping timeout: 264 seconds) |
| 2024-06-27 08:53:32 +0200 | m1dnight | (~christoph@82.146.125.185) (Quit: WeeChat 4.2.2) |
| 2024-06-27 08:54:17 +0200 | m1dnight | (~christoph@82.146.125.185) |
| 2024-06-27 08:57:47 +0200 | echoreply | (~echoreply@45.32.163.16) (Quit: WeeChat 2.8) |
| 2024-06-27 08:58:20 +0200 | echoreply | (~echoreply@45.32.163.16) |
| 2024-06-27 09:11:59 +0200 | jle` | (~jle`@2603:8001:3b02:84d4:89e:9b05:41f1:3af8) (Ping timeout: 256 seconds) |
| 2024-06-27 09:12:41 +0200 | jle` | (~jle`@2603:8001:3b02:84d4:143f:9778:ef77:7e4) |
| 2024-06-27 09:17:24 +0200 | lortabac | (~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) |
| 2024-06-27 09:20:37 +0200 | philopsos1 | (~caecilius@user/philopsos) (Ping timeout: 256 seconds) |
| 2024-06-27 09:21:45 +0200 | madhavanmiui | (~madhavanm@2409:40f4:10fe:dc03:8000::) |
| 2024-06-27 09:24:17 +0200 | emmanuelux_ | (~emmanuelu@user/emmanuelux) |
| 2024-06-27 09:24:18 +0200 | madhavanmiui | (~madhavanm@2409:40f4:10fe:dc03:8000::) (Client Quit) |
| 2024-06-27 09:24:48 +0200 | wbooze | (~wbooze@2a02:908:1244:9a20:9512:47b7:c73:ce1d) |
| 2024-06-27 09:27:35 +0200 | emmanuelux | (~emmanuelu@user/emmanuelux) (Ping timeout: 264 seconds) |
| 2024-06-27 09:36:30 +0200 | lxsameer | (~lxsameer@Serene/lxsameer) |
| 2024-06-27 09:47:51 +0200 | tv | (~tv@user/tv) |
| 2024-06-27 09:47:52 +0200 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 2024-06-27 10:03:37 +0200 | rvalue- | (~rvalue@user/rvalue) |
| 2024-06-27 10:04:47 +0200 | rvalue | (~rvalue@user/rvalue) (Ping timeout: 264 seconds) |
| 2024-06-27 10:06:04 +0200 | cfricke | (~cfricke@user/cfricke) |
| 2024-06-27 10:07:37 +0200 | rvalue- | rvalue |
| 2024-06-27 10:15:27 +0200 | chele | (~chele@user/chele) |
| 2024-06-27 10:44:27 +0200 | danse-nr3 | (~danse-nr3@151.44.219.215) (Ping timeout: 268 seconds) |
| 2024-06-27 10:47:44 +0200 | tzh | (~tzh@c-76-115-131-146.hsd1.or.comcast.net) (Quit: zzz) |
| 2024-06-27 10:48:21 +0200 | dysthesis | (~dysthesis@user/dysthesis) |
| 2024-06-27 10:52:55 +0200 | danse-nr3 | (~danse-nr3@151.57.38.73) |
| 2024-06-27 10:55:03 +0200 | dsrt^ | (~cd@c-98-242-74-66.hsd1.ga.comcast.net) (Ping timeout: 255 seconds) |
| 2024-06-27 11:00:14 +0200 | rosco | (~rosco@175.136.155.137) (Quit: Lost terminal) |
| 2024-06-27 11:06:38 +0200 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 2024-06-27 11:10:29 +0200 | gabriel_sevecek | (~gabriel@188-167-229-200.dynamic.chello.sk) (Ping timeout: 240 seconds) |
| 2024-06-27 11:13:04 +0200 | tt123109783 | (~tt1231@syn-075-185-104-199.res.spectrum.com) |
| 2024-06-27 11:14:51 +0200 | gehmehgeh | (~user@user/gehmehgeh) |
| 2024-06-27 11:15:17 +0200 | tt12310978 | (~tt1231@2603:6010:8700:4a81:219f:50d3:618a:a6ee) (Ping timeout: 240 seconds) |
| 2024-06-27 11:15:18 +0200 | tt123109783 | tt12310978 |
| 2024-06-27 11:15:45 +0200 | zzz | (~yin@user/zero) |
| 2024-06-27 11:16:45 +0200 | gabriel_sevecek | (~gabriel@188-167-229-200.dynamic.chello.sk) |
| 2024-06-27 11:24:10 +0200 | gehmehgeh | gmg |
| 2024-06-27 11:24:55 +0200 | __monty__ | (~toonn@user/toonn) |
| 2024-06-27 11:41:35 +0200 | destituion | (~destituio@2a02:2121:6cb:fbc3:3c0f:94ae:6844:a1fa) (Ping timeout: 256 seconds) |
| 2024-06-27 11:42:33 +0200 | destituion | (~destituio@85.221.111.174) |
| 2024-06-27 11:50:46 +0200 | econo_ | (uid147250@id-147250.tinside.irccloud.com) (Quit: Connection closed for inactivity) |
| 2024-06-27 11:51:13 +0200 | rosco | (~rosco@175.136.155.137) |
| 2024-06-27 12:01:34 +0200 | lortabac | (~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) (Ping timeout: 246 seconds) |
| 2024-06-27 12:03:41 +0200 | notzmv | (~daniel@user/notzmv) (Ping timeout: 268 seconds) |
| 2024-06-27 12:05:23 +0200 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 2024-06-27 12:12:27 +0200 | tv | (~tv@user/tv) (Ping timeout: 255 seconds) |
| 2024-06-27 12:14:14 +0200 | cheater_ | (~Username@user/cheater) |
| 2024-06-27 12:18:11 +0200 | cheater | (~Username@user/cheater) (Ping timeout: 268 seconds) |
| 2024-06-27 12:18:11 +0200 | cheater_ | cheater |
| 2024-06-27 12:19:08 +0200 | CiaoSen | (~Jura@2a05:5800:2b1:7a00:e6b9:7aff:fe80:3d03) |
| 2024-06-27 12:20:05 +0200 | soverysour | (~soverysou@user/soverysour) |
| 2024-06-27 12:20:23 +0200 | xff0x | (~xff0x@2405:6580:b080:900:a4df:4a3a:94ab:11e4) |
| 2024-06-27 12:24:42 +0200 | soverysour | (~soverysou@user/soverysour) (Ping timeout: 256 seconds) |
| 2024-06-27 12:24:59 +0200 | ubert | (~Thunderbi@2a02:8109:ab8a:5a00:eae9:52ec:67d4:506b) |
| 2024-06-27 12:25:26 +0200 | tv | (~tv@user/tv) |
| 2024-06-27 12:32:53 +0200 | tabaqui | (~root@91.74.190.107) (Quit: WeeChat 4.2.2) |
| 2024-06-27 12:35:56 +0200 | tabaqui | (~root@91.74.190.107) |
| 2024-06-27 12:36:58 +0200 | rosco | (~rosco@175.136.155.137) (Quit: Lost terminal) |
| 2024-06-27 12:37:18 +0200 | tabaqui | (~root@91.74.190.107) (Client Quit) |
| 2024-06-27 12:38:48 +0200 | tabaqui | (~root@91.74.190.107) |
| 2024-06-27 12:48:41 +0200 | lortabac | (~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) |
| 2024-06-27 12:49:41 +0200 | gabriel_sevecek | (~gabriel@188-167-229-200.dynamic.chello.sk) (Ping timeout: 240 seconds) |
| 2024-06-27 12:56:03 +0200 | danse-nr3 | (~danse-nr3@151.57.38.73) (Ping timeout: 264 seconds) |
| 2024-06-27 13:07:10 +0200 | gabriel_sevecek | (~gabriel@188-167-229-200.dynamic.chello.sk) |
| 2024-06-27 13:14:51 +0200 | sroso | (~sroso@user/SrOso) (Quit: Leaving :)) |
| 2024-06-27 13:15:53 +0200 | notzmv | (~daniel@user/notzmv) |
| 2024-06-27 13:22:07 +0200 | Miroboru | (~myrvoll@178-164-114.82.3p.ntebredband.no) |
| 2024-06-27 13:22:57 +0200 | dsrt^ | (~cd@c-98-242-74-66.hsd1.ga.comcast.net) |
| 2024-06-27 13:25:42 +0200 | notzmv | (~daniel@user/notzmv) (Ping timeout: 268 seconds) |
| 2024-06-27 13:26:23 +0200 | zzz | (~yin@user/zero) (Ping timeout: 264 seconds) |
| 2024-06-27 13:33:24 +0200 | zzz | (~yin@user/zero) |
| 2024-06-27 13:36:03 +0200 | acidjnk_new3 | (~acidjnk@p200300d6e714dc25e45fde1d7555be75.dip0.t-ipconnect.de) (Ping timeout: 256 seconds) |
| 2024-06-27 13:41:02 +0200 | forell | (~forell@user/forell) |
| 2024-06-27 13:45:06 +0200 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 2024-06-27 13:45:43 +0200 | meritamen | (~user@user/meritamen) |
| 2024-06-27 13:48:46 +0200 | mreh | (~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 +0200 | dysthesis | (~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 +0200 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 2024-06-27 14:24:33 +0200 | kuribas | (~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 +0200 | kimiamania | (~65804703@user/kimiamania) (Quit: PegeLinux) |
| 2024-06-27 14:33:13 +0200 | acidjnk_new3 | (~acidjnk@p200300d6e714dc25e45fde1d7555be75.dip0.t-ipconnect.de) |
| 2024-06-27 14:34:10 +0200 | kimiamania | (~65804703@user/kimiamania) |
| 2024-06-27 14:44:54 +0200 | wbooze | (~wbooze@2a02:908:1244:9a20:9512:47b7:c73:ce1d) (Remote host closed the connection) |
| 2024-06-27 15:03:00 +0200 | mreh | (~matthew@host86-160-168-12.range86-160.btcentralplus.com) (Ping timeout: 255 seconds) |
| 2024-06-27 15:04:02 +0200 | sawilagar | (~sawilagar@user/sawilagar) |
| 2024-06-27 15:05:39 +0200 | euleritian | (~euleritia@77.22.252.56) (Ping timeout: 264 seconds) |
| 2024-06-27 15:09:45 +0200 | euleritian | (~euleritia@dynamic-176-001-208-051.176.1.pool.telefonica.de) |
| 2024-06-27 15:09:51 +0200 | meritamen | (~user@user/meritamen) (Ping timeout: 264 seconds) |
| 2024-06-27 15:15:56 +0200 | bitdex | (~bitdex@gateway/tor-sasl/bitdex) (Quit: = "") |
| 2024-06-27 15:19:58 +0200 | hc | (~hc@mail.hce.li) (Remote host closed the connection) |
| 2024-06-27 15:22:32 +0200 | hc | (~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 +0200 | cfricke | (~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 +0200 | Sgeo | (~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 +0200 | comonad | (~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 +0200 | TMA | (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 +0200 | wbooze | (~wbooze@2a02:908:1244:9a20:d426:d0e1:e498:10ea) |
| 2024-06-27 16:03:04 +0200 | zzz | (~yin@user/zero) (Ping timeout: 246 seconds) |
| 2024-06-27 16:04:52 +0200 | TMA | (tma@twin.jikos.cz) |
| 2024-06-27 16:12:12 +0200 | lortabac | (~lortabac@2a01:e0a:541:b8f0:55ab:e185:7f81:54a4) (Quit: WeeChat 4.2.2) |
| 2024-06-27 16:12:15 +0200 | EvanR | eyes sum type with field names with suspicion |
| 2024-06-27 16:14:03 +0200 | michalz | (~michalz@185.246.207.215) (Ping timeout: 264 seconds) |
| 2024-06-27 16:16:40 +0200 | euleritian | (~euleritia@dynamic-176-001-208-051.176.1.pool.telefonica.de) (Read error: Connection reset by peer) |
| 2024-06-27 16:18:54 +0200 | euleritian | (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) |
| 2024-06-27 16:29:33 +0200 | zzz | (~yin@user/zero) |
| 2024-06-27 16:31:41 +0200 | lxsameer | (~lxsameer@Serene/lxsameer) (Ping timeout: 240 seconds) |
| 2024-06-27 16:38:16 +0200 | noscript | (~noscript@user/earldouglas) (WeeChat 4.2.1) |
| 2024-06-27 16:48:55 +0200 | pavonia | (~user@user/siracusa) |
| 2024-06-27 16:52:36 +0200 | dsrt^ | (~cd@c-98-242-74-66.hsd1.ga.comcast.net) (Ping timeout: 268 seconds) |
| 2024-06-27 16:54:25 +0200 | lxsameer | (~lxsameer@Serene/lxsameer) |
| 2024-06-27 17:02:23 +0200 | ocra8 | (~ocra8@user/ocra8) (Ping timeout: 260 seconds) |
| 2024-06-27 17:04:23 +0200 | ocra8 | (ocra8@user/ocra8) |
| 2024-06-27 17:07:27 +0200 | destituion | (~destituio@85.221.111.174) (Ping timeout: 264 seconds) |
| 2024-06-27 17:07:32 +0200 | mreh | (~matthew@host86-160-168-12.range86-160.btcentralplus.com) |
| 2024-06-27 17:10:08 +0200 | ocra8 | (ocra8@user/ocra8) (Excess Flood) |
| 2024-06-27 17:15:42 +0200 | euphores | (~SASL_euph@user/euphores) (Quit: Leaving.) |
| 2024-06-27 17:19:11 +0200 | destituion | (~destituio@2a02:2121:6cb:fbc3:ec2c:8d1b:640f:1406) |
| 2024-06-27 17:21:37 +0200 | euphores | (~SASL_euph@user/euphores) |
| 2024-06-27 17:36:04 +0200 | zmt00 | (~zmt00@user/zmt00) (Ping timeout: 268 seconds) |
| 2024-06-27 17:36:23 +0200 | zmt00 | (~zmt00@user/zmt00) |
| 2024-06-27 17:45:49 +0200 | causal | (~eric@50.35.88.207) |
| 2024-06-27 17:54:23 +0200 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 2024-06-27 18:06:41 +0200 | chele | (~chele@user/chele) (Remote host closed the connection) |
| 2024-06-27 18:10:22 +0200 | CiaoSen | (~Jura@2a05:5800:2b1:7a00:e6b9:7aff:fe80:3d03) (Ping timeout: 256 seconds) |
| 2024-06-27 18:11:29 +0200 | irfan | (~irfan@user/irfan) |
| 2024-06-27 18:12:05 +0200 | Tuplanolla | (~Tuplanoll@91-159-69-59.elisa-laajakaista.fi) |
| 2024-06-27 18:12:31 +0200 | econo_ | (uid147250@id-147250.tinside.irccloud.com) |
| 2024-06-27 18:14:55 +0200 | dsrt^ | (~cd@c-98-242-74-66.hsd1.ga.comcast.net) |
| 2024-06-27 18:15:49 +0200 | irfan | (~irfan@user/irfan) (Quit: leaving) |
| 2024-06-27 18:16:36 +0200 | irfan | (~irfan@user/irfan) |
| 2024-06-27 18:17:16 +0200 | zmt01 | (~zmt00@user/zmt00) |
| 2024-06-27 18:17:54 +0200 | irfan | flareon |
| 2024-06-27 18:18:00 +0200 | zmt00 | (~zmt00@user/zmt00) (Ping timeout: 268 seconds) |
| 2024-06-27 18:18:35 +0200 | euleritian | (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Ping timeout: 264 seconds) |
| 2024-06-27 18:18:45 +0200 | flareon | (~irfan@user/irfan) (Client Quit) |
| 2024-06-27 18:19:11 +0200 | euleritian | (~euleritia@dynamic-176-001-208-051.176.1.pool.telefonica.de) |
| 2024-06-27 18:22:36 +0200 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 2024-06-27 18:23:05 +0200 | sord937 | (~sord937@gateway/tor-sasl/sord937) (Remote host closed the connection) |
| 2024-06-27 18:24:07 +0200 | sord937 | (~sord937@gateway/tor-sasl/sord937) |
| 2024-06-27 18:28:47 +0200 | kuribas | (~user@ip-188-118-57-242.reverse.destiny.be) (Ping timeout: 264 seconds) |
| 2024-06-27 18:32:07 +0200 | glguy | (g@libera/staff/glguy) (Remote host closed the connection) |
| 2024-06-27 18:33:14 +0200 | glguy | (g@libera/staff/glguy) |
| 2024-06-27 18:36:23 +0200 | ocra8 | (ocra8@user/ocra8) |
| 2024-06-27 18:37:27 +0200 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 2024-06-27 18:50:58 +0200 | sprout_ | (~quassel@2a02-a448-3a80-0-d123-5da7-9ae5-44be.fixed6.kpn.net) |
| 2024-06-27 18:51:35 +0200 | soverysour | (~soverysou@81.196.150.219) |
| 2024-06-27 18:51:35 +0200 | soverysour | (~soverysou@81.196.150.219) (Changing host) |
| 2024-06-27 18:51:35 +0200 | soverysour | (~soverysou@user/soverysour) |
| 2024-06-27 18:51:49 +0200 | ocra8 | (ocra8@user/ocra8) (Ping timeout: 256 seconds) |
| 2024-06-27 18:51:55 +0200 | sprout | (~quassel@2a02-a448-3a80-0-3430-92e6-1565-73f9.fixed6.kpn.net) (Ping timeout: 268 seconds) |
| 2024-06-27 18:53:43 +0200 | ocra8 | (~ocra8@user/ocra8) |
| 2024-06-27 19:05:58 +0200 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |
| 2024-06-27 19:06:00 +0200 | mreh | (~matthew@host86-160-168-12.range86-160.btcentralplus.com) (Ping timeout: 255 seconds) |
| 2024-06-27 19:07:12 +0200 | sprout_ | sprout |
| 2024-06-27 19:11:53 +0200 | ubert | (~Thunderbi@2a02:8109:ab8a:5a00:eae9:52ec:67d4:506b) (Remote host closed the connection) |
| 2024-06-27 19:13:27 +0200 | qqq | (~qqq@92.43.167.61) |
| 2024-06-27 19:16:47 +0200 | soverysour | (~soverysou@user/soverysour) (Ping timeout: 260 seconds) |
| 2024-06-27 19:18:32 +0200 | wz1000 | (~zubin@static.11.113.47.78.clients.your-server.de) (Ping timeout: 252 seconds) |
| 2024-06-27 19:30:55 +0200 | wz1000 | (~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 +0200 | soverysour | (~soverysou@81.196.150.219) |
| 2024-06-27 19:42:50 +0200 | soverysour | (~soverysou@81.196.150.219) (Changing host) |
| 2024-06-27 19:42:50 +0200 | soverysour | (~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 +0200 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 2024-06-27 19:56:35 +0200 | tzh | (~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 |