Newest at the top
| 2024-04-24 17:12:07 +0200 | tromp | (~textual@92-110-219-57.cable.dynamic.v4.ziggo.nl) (Quit: My iMac has gone to sleep. ZZZzzz…) |
| 2024-04-24 17:10:15 +0200 | zwrv | hides |
| 2024-04-24 17:10:06 +0200 | <danse-nr3> | well... |
| 2024-04-24 17:09:53 +0200 | <zwrv> | the Report is not proper Haskell |
| 2024-04-24 17:09:32 +0200 | p3n | (~p3n@2a00:19a0:3:7c:0:d9c6:7cf6:1) |
| 2024-04-24 17:09:22 +0200 | <EvanR> | it's in the Report |
| 2024-04-24 17:09:05 +0200 | <zwrv> | undefined is not proper Haskell |
| 2024-04-24 17:07:20 +0200 | euleritian | (~euleritia@dynamic-176-000-165-138.176.0.pool.telefonica.de) |
| 2024-04-24 17:06:52 +0200 | euleritian | (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Ping timeout: 268 seconds) |
| 2024-04-24 17:05:26 +0200 | Guest13 | (~Guest13@cpc93370-hers8-2-0-cust590.6-3.cable.virginm.net) |
| 2024-04-24 16:59:55 +0200 | tri | (~tri@ool-18bbef1a.static.optonline.net) (Ping timeout: 245 seconds) |
| 2024-04-24 16:59:10 +0200 | average | (uid473595@user/average) |
| 2024-04-24 16:58:39 +0200 | shapr | (~user@c-24-218-186-89.hsd1.ma.comcast.net) (Ping timeout: 252 seconds) |
| 2024-04-24 16:55:37 +0200 | tri | (~tri@ool-18bbef1a.static.optonline.net) |
| 2024-04-24 16:50:36 +0200 | waleee | (~waleee@h-176-10-144-38.NA.cust.bahnhof.se) (Client Quit) |
| 2024-04-24 16:49:05 +0200 | waleee | (~waleee@h-176-10-144-38.NA.cust.bahnhof.se) |
| 2024-04-24 16:47:16 +0200 | euleritian | (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) |
| 2024-04-24 16:46:48 +0200 | euleritian | (~euleritia@dynamic-176-000-165-138.176.0.pool.telefonica.de) (Read error: Connection reset by peer) |
| 2024-04-24 16:41:02 +0200 | Raito_Bezarius | (~Raito@wireguard/tunneler/raito-bezarius) |
| 2024-04-24 16:31:39 +0200 | cods | (~fred@tuxee.net) (Ping timeout: 272 seconds) |
| 2024-04-24 16:30:56 +0200 | <EvanR> | never a good sign |
| 2024-04-24 16:30:30 +0200 | <EvanR> | contradiction |
| 2024-04-24 16:30:26 +0200 | <EvanR> | Void is a type with no values. Yet we found one anyway xD |
| 2024-04-24 16:27:44 +0200 | <danse-nr3> | :/ |
| 2024-04-24 16:27:21 +0200 | <danse-nr3> | oh i see, void is supposed to be void ... |
| 2024-04-24 16:26:59 +0200 | <danse-nr3> | i don't get your example ncf. undefined is any type, therefore also Void |
| 2024-04-24 16:25:32 +0200 | <EvanR> | type system is already inconsistent, but I vaguely recall additional separate reasoning about it |
| 2024-04-24 16:23:51 +0200 | <ncf> | looks pretty inconsistent to me already |
| 2024-04-24 16:23:45 +0200 | <lambdabot> | Void |
| 2024-04-24 16:23:44 +0200 | <ncf> | :t undefined :: Void |
| 2024-04-24 16:23:37 +0200 | <lambdabot> | a |
| 2024-04-24 16:23:36 +0200 | <ncf> | :t undefined |
| 2024-04-24 16:22:58 +0200 | <zwrv> | dependent haskell makes the type system inconsistent? |
| 2024-04-24 16:22:14 +0200 | zwrv | (~yin@user/zero) |
| 2024-04-24 16:20:36 +0200 | zwrv | (~yin@user/zero) (Ping timeout: 256 seconds) |
| 2024-04-24 16:17:38 +0200 | gmg | (~user@user/gehmehgeh) |
| 2024-04-24 16:17:19 +0200 | gmg | (~user@user/gehmehgeh) (Remote host closed the connection) |
| 2024-04-24 16:13:52 +0200 | notzmv | (~daniel@user/notzmv) |
| 2024-04-24 16:10:50 +0200 | <EvanR> | which is what dependent haskell does |
| 2024-04-24 16:10:45 +0200 | xff0x | (~xff0x@2405:6580:b080:900:a709:5227:95bf:dd51) |
| 2024-04-24 16:10:30 +0200 | <EvanR> | you can also ignore the issue and do Type : Type, if stuff like girard's paradox doesn't bother you |
| 2024-04-24 16:09:39 +0200 | <haskellbridge> | <irregularsphere> s/yes/sure |
| 2024-04-24 16:09:30 +0200 | <haskellbridge> | <irregularsphere> EvanR: yes, but I guess it's better to live off an already infinite tower |
| 2024-04-24 16:09:02 +0200 | raehik | (~raehik@rdng-25-b2-v4wan-169990-cust1344.vm39.cable.virginm.net) |
| 2024-04-24 16:06:43 +0200 | <EvanR> | a dependently typed system doesn't necessarily need an infinite hierarchy of Type, it could provide like 5 levels and say screw you if you end up needing more. Similar to GHC's tuple sizes |
| 2024-04-24 16:03:21 +0200 | <zwrv> | __monty__: i know i know |
| 2024-04-24 16:02:37 +0200 | <__monty__> | zwrv: I wouldn't take anyone's word for it for one thing. |
| 2024-04-24 16:02:03 +0200 | hueso | (~root@user/hueso) |
| 2024-04-24 16:02:02 +0200 | <ph88> | is haskell on the way to be dependently typed ? |
| 2024-04-24 15:59:37 +0200 | <zwrv> | if i write a medium sized project in both simple, idiomatic haskell and simple, idiomatic chez scheme, which one would you bet to perform the best speedwise? |