Newest at the top
| 2024-05-14 21:51:53 +0200 | <tomsmeding> | raehik: I re-ran all commands that could possibly be relevant in yahb2's history in a ghci shell and it still doesn't work |
| 2024-05-14 21:51:07 +0200 | waleee | (~waleee@h-176-10-144-38.NA.cust.bahnhof.se) |
| 2024-05-14 21:47:21 +0200 | <raehik> | XD |
| 2024-05-14 21:47:01 +0200 | <tomsmeding> | but the state is gone now :D |
| 2024-05-14 21:46:54 +0200 | <tomsmeding> | there was some state that made it work somehow |
| 2024-05-14 21:46:53 +0200 | euleritian | (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) |
| 2024-05-14 21:46:44 +0200 | <tomsmeding> | I :q'd and did it again |
| 2024-05-14 21:46:41 +0200 | euleritian | (~euleritia@ip4d16fc38.dynamic.kabel-deutschland.de) (Read error: Connection reset by peer) |
| 2024-05-14 21:46:38 +0200 | <yahb2> | Id (TypeError (Text "test")) :: k ; = (TypeError ...) |
| 2024-05-14 21:46:38 +0200 | <tomsmeding> | % :k! Id (TypeError (Text "test")) |
| 2024-05-14 21:45:55 +0200 | <raehik> | I can work around this by reifying, but it means I can't do super simple type-level evaluation failure examples :( |
| 2024-05-14 21:45:22 +0200 | <tomsmeding> | (why does ghci not have a :version command or something) |
| 2024-05-14 21:44:06 +0200 | <tomsmeding> | hm it does |
| 2024-05-14 21:43:29 +0200 | <raehik> | tomsmeding: my 9.4.8 still prints `= (TypeError ...)` :'( |
| 2024-05-14 21:43:12 +0200 | <ph88> | yes it's enough, i can study it |
| 2024-05-14 21:43:03 +0200 | <ski> | ph88 : .. i could go on, but perhaps this is enough, for the time being |
| 2024-05-14 21:42:41 +0200 | <ph88> | thank you ski :) |
| 2024-05-14 21:42:34 +0200 | <tomsmeding> | maybe it regressed! |
| 2024-05-14 21:42:27 +0200 | <tomsmeding> | if I'm not mistaken yahb2 is on 9.4.8 |
| 2024-05-14 21:42:12 +0200 | <raehik> | hmm I simply don't get the same output on GHC 9.6 or 9.8 |
| 2024-05-14 21:41:11 +0200 | <[exa]> | dmj`: for the evaluator I meant basically this https://gitea.blesmrt.net/exa/uskel/ |
| 2024-05-14 21:41:04 +0200 | <raehik> | thanks! interesting maybe it changed in GHC 9.8 (I know they constantly fiddle with :k and :k!) |
| 2024-05-14 21:40:35 +0200 | <yahb2> | <interactive>:1:1: error: test |
| 2024-05-14 21:40:35 +0200 | <tomsmeding> | % :k! Id (TypeError (Text "test")) |
| 2024-05-14 21:40:35 +0200 | <ski> | (this is *one* way to express/encode an existential. there is also another common way, which is sometimes preferable, which is based on a logical equivalence between `T' and `forall o. (T -> o) -> o') |
| 2024-05-14 21:40:26 +0200 | <yahb2> | <no output> |
| 2024-05-14 21:40:26 +0200 | <tomsmeding> | % type family Id a where Id a = a |
| 2024-05-14 21:40:19 +0200 | <yahb2> | <no output> |
| 2024-05-14 21:40:19 +0200 | <tomsmeding> | % :set -XTypeFamilies |
| 2024-05-14 21:40:02 +0200 | <raehik> | (by fail I mean doesn't print the type error properly) |
| 2024-05-14 21:39:55 +0200 | ocra8 | (ocra8@user/ocra8) |
| 2024-05-14 21:39:44 +0200 | <raehik> | oh well I can't show you what I mean xd but if you now wrap the above :k! invocation in Id, it fails |
| 2024-05-14 21:39:25 +0200 | <yahb2> | <interactive>:79:1: error: ; • Illegal family declaration for ‘Id’ ; Enable TypeFamilies to allow indexed type families ; • In the type family declaration for ‘Id’ |
| 2024-05-14 21:39:25 +0200 | <raehik> | % type family Id a where Id a = a |
| 2024-05-14 21:39:14 +0200 | <raehik> | tomsmeding: aha ty |
| 2024-05-14 21:37:51 +0200 | ent | (entgod@kapsi.fi) |
| 2024-05-14 21:37:41 +0200 | ent | (entgod@kapsi.fi) (Ping timeout: 240 seconds) |
| 2024-05-14 21:37:13 +0200 | <ski> | meaning that a value of type `Box c' amounts to ("wraps") a value of type `exists a. c a *> a' |
| 2024-05-14 21:36:48 +0200 | <ski> | MkBox :: (exists a. (c a *> a)) -> Box c |
| 2024-05-14 21:36:35 +0200 | <yahb2> | <interactive>:1:1: error: test |
| 2024-05-14 21:36:35 +0200 | <tomsmeding> | % :k! TypeError (Text "test") -- raehik |
| 2024-05-14 21:36:29 +0200 | <ski> | which is equivalent to |
| 2024-05-14 21:36:24 +0200 | <ski> | MkBox :: forall a. ((c a *> a) -> Box c) |
| 2024-05-14 21:36:13 +0200 | <ski> | to be explicit, which is equivalent to |
| 2024-05-14 21:36:04 +0200 | <ski> | MkBox :: forall a. (c a => (a -> Box c)) |
| 2024-05-14 21:35:54 +0200 | <ski> | or |
| 2024-05-14 21:35:52 +0200 | <ski> | MkBox :: forall a. c a => a -> Box c |
| 2024-05-14 21:35:37 +0200 | <ski> | means that we have |
| 2024-05-14 21:35:33 +0200 | <ski> | data Box c = forall a. (c a) => MkBox a |
| 2024-05-14 21:34:59 +0200 | <ski> | er, right, ty |