Newest at the top
| 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' |
| 2024-05-14 21:26:04 +0200 | <ph88> | i'm interested in those details :p |
| 2024-05-14 21:25:46 +0200 | <ski> | (before getting into the details of how to actually effect the desired semantics with current-day Haskell) |
| 2024-05-14 21:25:16 +0200 | <ski> | it's (imho) a useful way to talk about these matters |
| 2024-05-14 21:25:00 +0200 | <EvanR> | it's skiskell |
| 2024-05-14 21:24:59 +0200 | <ski> | it's not in the manual, it's pseudo-Haskell |
| 2024-05-14 21:24:47 +0200 | <ph88> | can't find it in the manual |
| 2024-05-14 21:24:42 +0200 | <ski> | ("provide", as opposed to "expect") |
| 2024-05-14 21:24:13 +0200 | <ski> | "provide this constraint along with a value of this other type" |
| 2024-05-14 21:23:53 +0200 | <ph88> | ski, what does *> mean in a type ? |
| 2024-05-14 21:22:05 +0200 | <ski> | ph88 : "i'm trying to have a function that given a data which implements a typeclass can return another data that implements the same type class" -- sounds like you want `getSomething :: a -> Maybe (exists b. Something b *> b)', not `getSomething :: forall b. Something b => a -> Maybe b', then |
| 2024-05-14 21:18:24 +0200 | sord937 | (~sord937@gateway/tor-sasl/sord937) |
| 2024-05-14 21:17:02 +0200 | sord937 | (~sord937@gateway/tor-sasl/sord937) (Ping timeout: 260 seconds) |
| 2024-05-14 21:16:53 +0200 | greenflower | (~greenflow@103.191.25.63) |
| 2024-05-14 21:07:46 +0200 | <mauke> | blame the original rust code :-) |
| 2024-05-14 21:07:32 +0200 | <yin> | have you considered 0.37 ? |
| 2024-05-14 21:06:34 +0200 | <yin> | mauke: 0.234 doesn't seem random at all |
| 2024-05-14 21:01:34 +0200 | <raehik> | understandable |