Newest at the top
| 2024-05-10 21:28:35 +0200 | justsomeguy | goes off to google GADTs |
| 2024-05-10 21:27:00 +0200 | mankanor | (~mankanor@210.185.176.242) |
| 2024-05-10 21:25:58 +0200 | mankanor | (~mankanor@210.185.176.242) (Remote host closed the connection) |
| 2024-05-10 21:25:58 +0200 | mankanor | (~mankanor@210.185.176.242) |
| 2024-05-10 21:25:57 +0200 | <probie> | You only need GADTs if you want to include the depth in the type |
| 2024-05-10 21:25:09 +0200 | <int-e> | ncf: You don't need GADT powers for that; Haskell 98 data types would allow that. |
| 2024-05-10 21:25:00 +0200 | <ncf> | right, it's not an actual GADT |
| 2024-05-10 21:25:00 +0200 | <ski> | you can separate it into a singleton, and an indexed type, if you want to .. |
| 2024-05-10 21:24:33 +0200 | <ski> | that's just `GADTSyntax' |
| 2024-05-10 21:24:15 +0200 | <ncf> | Z :: a -> Powers f a; S :: Powers f (f a) -> Powers f a |
| 2024-05-10 21:23:58 +0200 | <ski> | (requires polymorphic recursion) |
| 2024-05-10 21:23:56 +0200 | <ncf> | you can encode it as a GADT right? |
| 2024-05-10 21:23:55 +0200 | mankanor | (~mankanor@210.185.176.242) (Remote host closed the connection) |
| 2024-05-10 21:23:54 +0200 | mankanor | (~mankanor@210.185.176.242) |
| 2024-05-10 21:23:48 +0200 | <ncf> | yes yes |
| 2024-05-10 21:23:43 +0200 | <ski> | (and this is a nonregular data type, not a GADT) |
| 2024-05-10 21:23:25 +0200 | mankanor | (~mankanor@210.185.176.242) (Remote host closed the connection) |
| 2024-05-10 21:23:23 +0200 | <ncf> | oh yeah |
| 2024-05-10 21:23:20 +0200 | <probie> | Assuming f is `[]`, do you mean something that's equivalent to `data Lists a = F0 a | F1 [a] | F2 [[a]] | F3 [[[a]]] ...` or have I misinterpreted? |
| 2024-05-10 21:23:08 +0200 | <ski> | s/Z/Z a/ |
| 2024-05-10 21:23:01 +0200 | <ncf> | EvanR: lol |
| 2024-05-10 21:22:53 +0200 | <ncf> | no wait |
| 2024-05-10 21:22:48 +0200 | <EvanR> | 1 / (1 - f) |
| 2024-05-10 21:22:37 +0200 | <ncf> | Powers f a = Z | S (Powers f (f a)) ? |
| 2024-05-10 21:22:11 +0200 | mankanor | (~mankanor@210.185.176.242) |
| 2024-05-10 21:21:43 +0200 | <ncf> | 1 + f + f² + ... |
| 2024-05-10 21:21:36 +0200 | <ncf> | is there a GADT that builds the sum of powers of a functor |
| 2024-05-10 21:20:37 +0200 | raehik | (~raehik@rdng-25-b2-v4wan-169990-cust1344.vm39.cable.virginm.net) |
| 2024-05-10 21:19:33 +0200 | <int-e> | you can't reasily do that... you'll have to play some nasty type class tricks. |
| 2024-05-10 21:19:21 +0200 | <justsomeguy> | ...I finally feel like I'm learning something... |
| 2024-05-10 21:18:57 +0200 | <int-e> | justsomeguy: right |
| 2024-05-10 21:18:57 +0200 | <justsomeguy> | But the goal is to not have to specify the depth. |
| 2024-05-10 21:18:38 +0200 | <justsomeguy> | To get what I want (a 2-dimensional [] from a 2-dimensional List), I have to use toList $ fmap toList nested. |
| 2024-05-10 21:18:35 +0200 | <mauke> | that only does one level |
| 2024-05-10 21:17:40 +0200 | <int-e> | (Not exported by Prelude. Too many other modules define toList functions.) |
| 2024-05-10 21:17:06 +0200 | <int-e> | (It even exists there already) |
| 2024-05-10 21:16:57 +0200 | <lambdabot> | Foldable t => t a -> [a] |
| 2024-05-10 21:16:56 +0200 | <int-e> | :t Data.Foldable.toList |
| 2024-05-10 21:16:46 +0200 | <ncf> | you could wrap the dimension in an existential |
| 2024-05-10 21:16:29 +0200 | <int-e> | justsomeguy: since you already have Foldable |
| 2024-05-10 21:16:20 +0200 | <int-e> | justsomeguy: yes, foldr (:) [] |
| 2024-05-10 21:16:19 +0200 | <justsomeguy> | I think it's probably not, because the type system wants to know the dimension of the list beforehand... |
| 2024-05-10 21:16:00 +0200 | <justsomeguy> | int-e: Is it possible to write a toList function that will convert a List of arbitrary depth to []? |
| 2024-05-10 21:15:06 +0200 | <Henson> | probie, ncf: thank you for your help. I'll give your suggestions a try. |
| 2024-05-10 21:13:27 +0200 | <ncf> | i guess (.: "foo") >=> (.: "bar") |
| 2024-05-10 21:13:05 +0200 | zetef | (~quassel@2a02:2f00:5202:1200:df0b:9c52:7feb:3551) |
| 2024-05-10 21:12:13 +0200 | zetef | (~quassel@2a02:2f00:5202:1200:df0b:9c52:7feb:3551) (Remote host closed the connection) |
| 2024-05-10 21:12:03 +0200 | raehik | (~raehik@rdng-25-b2-v4wan-169990-cust1344.vm39.cable.virginm.net) (Ping timeout: 256 seconds) |
| 2024-05-10 21:10:04 +0200 | <Henson> | ncf: can you give an example of how I'd do the chaining? |
| 2024-05-10 21:09:48 +0200 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) |