Newest at the top
| 2024-05-14 21:58:56 +0200 | <raehik> | thx for the help my docs will benefit from knowing this! |
| 2024-05-14 21:58:19 +0200 | jespada | (~jespada@cpc121308-nmal25-2-0-cust15.19-2.cable.virginm.net) (Quit: Textual IRC Client: www.textualapp.com) |
| 2024-05-14 21:57:31 +0200 | <tomsmeding> | -y |
| 2024-05-14 21:57:28 +0200 | <tomsmeding> | unfortunatelt |
| 2024-05-14 21:57:25 +0200 | <tomsmeding> | yeah I've always found :k! to be a bit unstable |
| 2024-05-14 21:57:16 +0200 | <tomsmeding> | ah :) |
| 2024-05-14 21:57:11 +0200 | <raehik> | tomsmeding: oh yep that works on 9.2. but my non-contrived example (that goes thru lots of type families) doesn't xd |
| 2024-05-14 21:56:50 +0200 | <ncf> | you barely missed it |
| 2024-05-14 21:56:37 +0200 | ski | looks around, confusedly |
| 2024-05-14 21:56:27 +0200 | <ncf> | right here! |
| 2024-05-14 21:56:21 +0200 | <ski> | where ? |
| 2024-05-14 21:56:07 +0200 | <ncf> | the ski existential lecture has taken place |
| 2024-05-14 21:55:23 +0200 | <tomsmeding> | ¯\_(ツ)_/¯ |
| 2024-05-14 21:55:21 +0200 | <tomsmeding> | raehik: https://paste.tomsmeding.com/QzNahvGW |
| 2024-05-14 21:54:14 +0200 | <raehik> | *but I'm not too worried |
| 2024-05-14 21:54:03 +0200 | <raehik> | alas my 9.2 doesn't work either bu |
| 2024-05-14 21:53:44 +0200 | thaliaa | (uid486183@id-486183.uxbridge.irccloud.com) |
| 2024-05-14 21:53:15 +0200 | <raehik> | ahhhh there it is |
| 2024-05-14 21:53:11 +0200 | <tomsmeding> | fails from 9.4 on |
| 2024-05-14 21:53:06 +0200 | <raehik> | hahahahahaha good stuff |
| 2024-05-14 21:53:05 +0200 | <tomsmeding> | raehik: works on ghc 9.0 and 9.2 xD |
| 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 |