Newest at the top
| 2025-01-17 18:52:24 +0100 | simplystuart | (~simplystu@c-75-75-152-164.hsd1.pa.comcast.net) (Ping timeout: 260 seconds) |
| 2025-01-17 18:51:28 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2025-01-17 18:49:02 +0100 | gorignak | (~gorignak@user/gorignak) gorignak |
| 2025-01-17 18:47:38 +0100 | simplystuart | (~simplystu@c-75-75-152-164.hsd1.pa.comcast.net) |
| 2025-01-17 18:43:00 +0100 | Feuermagier_ | Feuermagier |
| 2025-01-17 18:43:00 +0100 | Feuermagier_ | (~Feuermagi@user/feuermagier) Feuermagier |
| 2025-01-17 18:41:30 +0100 | Guest4267 | (~Feuermagi@user/feuermagier) (Killed (molybdenum.libera.chat (Nickname regained by services))) |
| 2025-01-17 18:41:30 +0100 | Feuermagier | Guest4267 |
| 2025-01-17 18:41:21 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 276 seconds) |
| 2025-01-17 18:41:09 +0100 | vanishingideal | (~vanishing@user/vanishingideal) (Ping timeout: 248 seconds) |
| 2025-01-17 18:36:04 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2025-01-17 18:35:22 +0100 | <haskellbridge> | <Bowuigi> Huh, maybe some type wrapper over arrows works then |
| 2025-01-17 18:34:11 +0100 | <haskellbridge> | <thirdofmay18081814goya> returning "t" on the last line will make a valid function |
| 2025-01-17 18:33:40 +0100 | <haskellbridge> | <thirdofmay18081814goya> it's haskell, see this piece of code for the definition of "Vec" |
| 2025-01-17 18:33:06 +0100 | <haskellbridge> | <Bowuigi> I assume that's not Haskell because you're working with Type on a normal function |
| 2025-01-17 18:31:43 +0100 | euphores | (~SASL_euph@user/euphores) euphores |
| 2025-01-17 18:30:33 +0100 | <haskellbridge> | <thirdofmay18081814goya> the last line will fail to parse "->" |
| 2025-01-17 18:30:26 +0100 | <haskellbridge> | ... long message truncated: https://kf8nh.com/_heisenbridge/media/kf8nh.com/GivjAOUJRTejXEzvgiSSvzqy/32228VJtd_8 (4 lines) |
| 2025-01-17 18:30:26 +0100 | <haskellbridge> | <thirdofmay18081814goya> is the following function possible at all? |
| 2025-01-17 18:30:16 +0100 | <haskellbridge> | <thirdofmay18081814goya> hm |
| 2025-01-17 18:28:50 +0100 | euleritian | (~euleritia@77.23.250.232) |
| 2025-01-17 18:28:38 +0100 | euleritian | (~euleritia@ip4d17fae8.dynamic.kabel-deutschland.de) (Ping timeout: 265 seconds) |
| 2025-01-17 18:28:21 +0100 | ubert | (~Thunderbi@2a02:8109:ab8a:5a00:90fa:a109:5301:a5a3) (Ping timeout: 276 seconds) |
| 2025-01-17 18:26:41 +0100 | agent314 | (~quassel@37.19.210.25) agent314 |
| 2025-01-17 18:26:19 +0100 | euphores | (~SASL_euph@user/euphores) (Quit: Leaving.) |
| 2025-01-17 18:25:59 +0100 | agent314 | (~quassel@c-24-17-1-67.hsd1.wa.comcast.net) (Ping timeout: 244 seconds) |
| 2025-01-17 18:24:57 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) (Ping timeout: 244 seconds) |
| 2025-01-17 18:24:53 +0100 | <haskellbridge> | <thirdofmay18081814goya> oooo neat! |
| 2025-01-17 18:23:52 +0100 | <Leary> | You can get this function for free as a field, BTW: `Cons :: { vHead :: a, vTail :: Vec a n } -> Vec a (Succ n)` |
| 2025-01-17 18:23:19 +0100 | alecs | (~alecs@61.pool85-58-154.dynamic.orange.es) (Ping timeout: 265 seconds) |
| 2025-01-17 18:22:09 +0100 | lxsameer | (~lxsameer@Serene/lxsameer) (Ping timeout: 252 seconds) |
| 2025-01-17 18:21:29 +0100 | <haskellbridge> | <thirdofmay18081814goya> very cool, thanks a lot! |
| 2025-01-17 18:21:09 +0100 | ColinRobinson | JuanDaugherty |
| 2025-01-17 18:20:58 +0100 | <Leary> | `vTail :: forall (a :: Type) (n :: Nat). ...` |
| 2025-01-17 18:20:43 +0100 | merijn | (~merijn@128-137-045-062.dynamic.caiway.nl) merijn |
| 2025-01-17 18:19:33 +0100 | <haskellbridge> | <thirdofmay18081814goya> the work of "a :: Type" is usually done by "forall a" I think |
| 2025-01-17 18:19:28 +0100 | euleritian | (~euleritia@ip4d17fae8.dynamic.kabel-deutschland.de) |
| 2025-01-17 18:19:17 +0100 | <haskellbridge> | <thirdofmay18081814goya> is there a way to explicitly annotate the type of "vTail" with "a :: Type" and "n :: Nat"? |
| 2025-01-17 18:19:09 +0100 | euleritian | (~euleritia@dynamic-176-006-139-088.176.6.pool.telefonica.de) (Read error: Connection reset by peer) |
| 2025-01-17 18:18:37 +0100 | alecs | (~alecs@61.pool85-58-154.dynamic.orange.es) alecs |
| 2025-01-17 18:17:55 +0100 | <haskellbridge> | <thirdofmay18081814goya> ty!@ |
| 2025-01-17 18:17:55 +0100 | <haskellbridge> | <thirdofmay18081814goya> no way to pass "Nil" because we require "Succ n" |
| 2025-01-17 18:17:43 +0100 | <haskellbridge> | <thirdofmay18081814goya> right nevermind, I misunderstood |
| 2025-01-17 18:16:24 +0100 | <Leary> | That case is excluded by the type of the argument; just drop it? |
| 2025-01-17 18:15:55 +0100 | <haskellbridge> | <thirdofmay18081814goya> ah the problem is a bit more serious |
| 2025-01-17 18:14:27 +0100 | <haskellbridge> | <thirdofmay18081814goya> how could I explicitly annotate the last match of "vTail" to make a "Nil" value of "Vec a n" |
| 2025-01-17 18:14:02 +0100 | <haskellbridge> | ... long message truncated: https://kf8nh.com/_heisenbridge/media/kf8nh.com/SLhYEhHTJnvdxEpqFwluIqDU/4YBZpIuH0YU (12 lines) |
| 2025-01-17 18:14:02 +0100 | <haskellbridge> | <thirdofmay18081814goya> {-# LANGUAGE GADTs, DataKinds, NoStarIsType, KindSignatures #-} |
| 2025-01-17 18:13:16 +0100 | target_i | (~target_i@user/target-i/x-6023099) target_i |
| 2025-01-17 18:13:11 +0100 | machinedgod | (~machinedg@d108-173-18-100.abhsia.telus.net) (Ping timeout: 265 seconds) |