Newest at the top
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 |
2024-05-14 21:34:49 +0200 | <ski> | .. this is what justifies using the keyword `forall' above, in that `Box' datatype, to encode *existentials* |
2024-05-14 21:34:42 +0200 | <ncf> | (Cxt *> T) -> U |
2024-05-14 21:34:23 +0200 | peterbecich | (~Thunderbi@syn-047-229-123-186.res.spectrum.com) |
2024-05-14 21:34:05 +0200 | <ski> | in any case, it's useful to be aware that `(exists a. ..a..) -> ...' is logically equivalent to `forall a. (..a.. -> ...)', as well as `(Cxt *> T) => U' being equivalent to `Cxt => (T -> U)' (both of which are a kind of currying/uncurrying, kinda) |
2024-05-14 21:32:08 +0200 | <ski> | types don't exist at run-time, but one can imagine implementations that passes around evidence for types at run-time, e.g. to allow arbitrary unboxing, or for GC purposes) |
2024-05-14 21:32:02 +0200 | <ski> | (`forall a.' vs. `exists a.' is also conceptually similar. the first depends on the caller/user/consumer to specify the actual type to use in place of `a', while the second lets the callee/implementor/producer pick the type to use for `a'. so the former is kinda like a function that gets a type `a' at run-time, while the latter is kinda like a pair of a type `a' and a value. in a type-erasure implementation, |
2024-05-14 21:31:52 +0200 | gorignak | (~gorignak@user/gorignak) |
2024-05-14 21:29:29 +0200 | <ski> | while, in a dictionary-passing implementation, `Cxt *> T' would get translated to `(DictCxt,T)', a *pair* of the dictionary and the value |
2024-05-14 21:29:16 +0200 | <ph88> | is that dictionary visible in Core ? |
2024-05-14 21:28:56 +0200 | <ski> | in the dictionary-passing implementation of type classes, `Cxt => T' gets translated to `DictCxt -> T', a function that accepts a dictionary of method implementations, and computing a value of type `T' |
2024-05-14 21:28:07 +0200 | <ski> | a value of type `Cxt *> T' is a value that bundles evidence for a constraint `Cxt' together with a value `T', allowing the user/caller/consumer to both use the evidence, as well as the value |
2024-05-14 21:27:01 +0200 | <ski> | a value of type `Cxt => T' is a value such that, if the user/caller/consumer provides evidence of the constraint `Cxt' to it, it will give you back a value of type `T' |