Newest at the top
| 2024-10-13 06:14:41 +0200 | <haskellbridge> | <Bowuigi> Also note that parametricity only works at the term level. Type families break it |
| 2024-10-13 06:11:30 +0200 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2024-10-13 06:11:20 +0200 | bh34e5 | (~bh34e5@user/bh34e5) (Ping timeout: 252 seconds) |
| 2024-10-13 06:09:34 +0200 | Lord_of_Life | (~Lord@user/lord-of-life/x-2819915) (Client Quit) |
| 2024-10-13 06:08:15 +0200 | <haskellbridge> | <Bowuigi> Inst/Lears parametricity and "Reason Isomorphically!" to the rescue! |
| 2024-10-13 06:04:51 +0200 | Lord_of_Life | (~Lord@user/lord-of-life/x-2819915) Lord_of_Life |
| 2024-10-13 06:03:59 +0200 | Lord_of_Life | (~Lord@user/lord-of-life/x-2819915) (Quit: Laa shay'a waqi'un moutlaq bale kouloun moumkine) |
| 2024-10-13 06:03:44 +0200 | <Inst> | after I foolishly thought I got one over Hutton by claiming that there's more than one possible functor instance |
| 2024-10-13 06:03:27 +0200 | <Inst> | i'm trying to remember someone telling me that you can break derive functor by adding type lambdas |
| 2024-10-13 06:00:21 +0200 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 244 seconds) |
| 2024-10-13 05:57:59 +0200 | Lord_of_Life | (~Lord@user/lord-of-life/x-2819915) Lord_of_Life |
| 2024-10-13 05:56:24 +0200 | raehik | (~raehik@rdng-25-b2-v4wan-169990-cust1344.vm39.cable.virginm.net) (Ping timeout: 252 seconds) |
| 2024-10-13 05:55:43 +0200 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2024-10-13 05:55:33 +0200 | Lord_of_Life | (~Lord@user/lord-of-life/x-2819915) (Client Quit) |
| 2024-10-13 05:52:24 +0200 | Lord_of_Life | (~Lord@user/lord-of-life/x-2819915) Lord_of_Life |
| 2024-10-13 05:49:48 +0200 | Lord_of_Life | (~Lord@user/lord-of-life/x-2819915) (Ping timeout: 252 seconds) |
| 2024-10-13 05:49:27 +0200 | <yin> | but i guess i recognize their utility |
| 2024-10-13 05:49:03 +0200 | <yin> | i don't use type families much if at all |
| 2024-10-13 05:45:52 +0200 | <geekosaur> | type families, OTOH, are the only way to create type functions since you can't make type functions the way you make value level functions |
| 2024-10-13 05:45:22 +0200 | <geekosaur> | I don't see them get used much if at all |
| 2024-10-13 05:45:06 +0200 | comonad | (~comonad@p200300d02711e6001d93b8c5b2241d7f.dip0.t-ipconnect.de) (Ping timeout: 246 seconds) |
| 2024-10-13 05:44:50 +0200 | <geekosaur> | or declarations |
| 2024-10-13 05:44:43 +0200 | <geekosaur> | my feel is that data families are just function definitions spread over multiple source files |
| 2024-10-13 05:44:33 +0200 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 245 seconds) |
| 2024-10-13 05:43:24 +0200 | <yin> | can't remember if i ever got to understand them |
| 2024-10-13 05:43:02 +0200 | tcard_ | (~tcard@2400:4051:5801:7500:cf17:befc:ff82:5303) (Read error: Connection reset by peer) |
| 2024-10-13 05:42:59 +0200 | tcard__ | (~tcard@2400:4051:5801:7500:cf17:befc:ff82:5303) |
| 2024-10-13 05:42:58 +0200 | <yin> | i never got into data families. i'm not sure if i like them |
| 2024-10-13 05:42:13 +0200 | <Inst> | also, is it me, but is data families just "i miss OOP class declarations"? |
| 2024-10-13 05:39:55 +0200 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2024-10-13 05:39:11 +0200 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) peterbecich |
| 2024-10-13 05:35:31 +0200 | <Inst> | b there is constrained by its usage in that function, also, hi (&) |
| 2024-10-13 05:35:12 +0200 | <Inst> | i guess i should be more precise when I say constrained |
| 2024-10-13 05:32:59 +0200 | <probie> | Inst: I don't think that last bit is true (depending on what you mean by "unconstrained"). `a -> (a -> b) -> b` is not restricted to `Void` |
| 2024-10-13 05:31:48 +0200 | aforemny | (~aforemny@2001:9e8:6ce0:3e00:98ec:934c:3b0e:2930) (Ping timeout: 246 seconds) |
| 2024-10-13 05:31:00 +0200 | aforemny_ | (~aforemny@i577BEEEB.versanet.de) aforemny |
| 2024-10-13 05:29:48 +0200 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 276 seconds) |
| 2024-10-13 05:29:04 +0200 | bh34e5 | (~bh34e5@user/bh34e5) bh34e5 |
| 2024-10-13 05:24:08 +0200 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2024-10-13 05:22:03 +0200 | <Inst> | also, it implies that any function whose signature ends in an unconstrained type variable, is equivalent to trying to produce a value of type Void |
| 2024-10-13 05:21:14 +0200 | <Inst> | geekosaur: but a -> Void is defined, on the term level, exactly the same as a -> b |
| 2024-10-13 05:21:11 +0200 | Inst_ | Inst |
| 2024-10-13 05:21:08 +0200 | Inst | (~Inst@user/Inst) (Killed (NickServ (GHOST command used by Inst_))) |
| 2024-10-13 05:20:55 +0200 | Inst_ | (~Inst@user/Inst) Inst |
| 2024-10-13 05:15:30 +0200 | ephilalethes | (~noumenon@113.51-175-156.customer.lyse.net) (Quit: Leaving) |
| 2024-10-13 05:14:45 +0200 | <geekosaur> | sorry, I mean the only value possible of type `b` |
| 2024-10-13 05:14:41 +0200 | <Lears> | All isomorphic. |
| 2024-10-13 05:14:38 +0200 | <Lears> | `forall a b. a -> b` ~ `forall a. a -> forall b. b` ~ `forall a. a -> Void` ~ `(exists a. a) -> Void` ~ `() -> Void` ~ `Void` |
| 2024-10-13 05:13:59 +0200 | <geekosaur> | in the same way that a -> a must be `id` |
| 2024-10-13 05:13:46 +0200 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 252 seconds) |