Logs: freenode/#haskell
| 2020-11-18 20:41:05 | × | rekahsoft quits (~rekahsoft@cpe0008a20f982f-cm64777d666260.cpe.net.cable.rogers.com) (Ping timeout: 240 seconds) |
| 2020-11-18 20:41:08 | × | nuncanada quits (~dude@179.235.160.168) (Ping timeout: 260 seconds) |
| 2020-11-18 20:41:14 | <dolio> | Instead they use loops they borrowed from C. |
| 2020-11-18 20:41:15 | → | knupfer joins (~Thunderbi@200116b8244bd600690e470b1c9f0b95.dip.versatel-1u1.de) |
| 2020-11-18 20:42:11 | <ski> | `exists a. Counter a *> a' expresses "bundling methods with object state". but in Haskell, we can also express e.g. `exists a. (Ord a,Widget a) *> [a]' where we bundle not an individual object with methods, but rather attach them to a whole collection of objects |
| 2020-11-18 20:44:09 | <ski> | (in the case of `exists a. (a,a -> IO Int,a -> IO ())', a shorter way (normally implemented by closures) to express this is `(IO Int,IO ())' .. but this method of removing the existential doesn't always work, e.g. if some method take multiple `a's as input (so-called "binary methods", like a comparision. also see "clone methods")) |
| 2020-11-18 20:45:05 | <unfixpoint> | Why *> instead of =>? Never used the singletons but in this case is it not the same? |
| 2020-11-18 20:45:19 | <ski> | not at all the same, rather the "opposite" |
| 2020-11-18 20:46:20 | <boxscape> | does it actually have to do with singletons? |
| 2020-11-18 20:46:21 | <unfixpoint> | So given [a] we can Ord and Widget it? Instead of Given that we can Ord, Widget an a we have [a]? Wat? |
| 2020-11-18 20:47:01 | <unfixpoint> | Idk, I didn't know (*>) as type operator so I looked it up on Hoogle |
| 2020-11-18 20:47:09 | <dminuoso> | unfixpoint: It's not, it's pseudo haskell |
| 2020-11-18 20:47:26 | <ski> | if you have `foo :: Blah => ...', then the caller/consumer/user of `foo' must provide evidence of `Blah', before being able to call/use `foo' (with type `...'). and the callee/implementor/producer of `foo' can simply take the evidence of `Blah' for granted, can e.g. call methods (and other operations relying on those methods) from `Blah' |
| 2020-11-18 20:47:30 | <boxscape> | (the singletons version is just the lifted version of Applicative's *>) |
| 2020-11-18 20:47:37 | <dminuoso> | If we had exists in addition to forall, then it'd make sense to have a *> variant of => instead |
| 2020-11-18 20:48:05 | <dminuoso> | Not even sure who introduced the syntax of *>, but I wouldn't be surprised if it was ski themselves. :) |
| 2020-11-18 20:48:17 | <monochrom> | It's related to: "for all positive x, P(x)" = "for all x, positive x implies P(x)", but "for some positive x, P(x)" = "for some x, positive x and P(x)" |
| 2020-11-18 20:48:44 | <monochrom> | You simply don't use "implies" in the existential version. |
| 2020-11-18 20:48:45 | → | conal joins (~conal@64.71.133.70) |
| 2020-11-18 20:49:22 | <ski> | if you have `foo :: Blah *> ...', then the callee/producer/implementor of `foo' can simply take the evidence of `Blah' for granted (and also use the value of type `...'). but the caller/user/consumer of `foo' must produce evidence of `Blah' (together with constructing a value of type `...') |
| 2020-11-18 20:49:27 | <ski> | dminuoso : yes |
| 2020-11-18 20:49:50 | × | falafel quits (~falafel@2601:547:1303:b30:7811:313f:d0f3:f9f4) (Ping timeout: 264 seconds) |
| 2020-11-18 20:50:18 | <monochrom> | So given that "and" is somewhat analogous to multiplication, and it would be nice to keep the ">" part, some of us chose the pseudocode *> notation. |
| 2020-11-18 20:50:30 | × | Franciman quits (~francesco@host-82-56-223-169.retail.telecomitalia.it) (Quit: Leaving) |
| 2020-11-18 20:50:43 | <ski> | the distinction `Blah => ...' vs. `Blah *> ...' is similar to the distinction `T -> U' vs. `(T,U)', and the distinction `forall a. ..a..' vs. `exists a. ..a..' |
| 2020-11-18 20:51:06 | <boxscape> | can you encode *> analogously to how you can encode exists? |
| 2020-11-18 20:51:20 | <ski> | and yes, this `*>' is just pseudo-code that some of us sometimes use to express this "dual" concept to `=>' |
| 2020-11-18 20:51:31 | hackage | phonetic-languages-examples 0.6.1.0 - A generalization of the uniqueness-periods-vector-examples functionality. https://hackage.haskell.org/package/phonetic-languages-examples-0.6.1.0 (OleksandrZhabenko) |
| 2020-11-18 20:51:55 | <dminuoso> | boxscape: Sure, as we can encode exists with forall. |
| 2020-11-18 20:52:06 | <boxscape> | okay, neat |
| 2020-11-18 20:52:07 | <dminuoso> | boxscape: So in that encoding => takes the role of *> |
| 2020-11-18 20:52:16 | <boxscape> | oh, that's pretty straightforward |
| 2020-11-18 20:52:21 | → | dragestil joins (~quassel@fsf/member/dragestil) |
| 2020-11-18 20:53:07 | <ski> | yes, you can write `data cxt *> a = cxt => Provide a' alternatively `data cxt *> a where Provide :: cxt => a -> cxt *> a' |
| 2020-11-18 20:53:12 | <monochrom> | Like this? "data X = forall a. Show a => X [a]" becomes "forall a. Show a => ([a] -> c) -> c" |
| 2020-11-18 20:53:22 | <ski> | (compare `Provide' with `(,) :: a -> b -> (a,b)') |
| 2020-11-18 20:53:26 | × | crdrost quits (~crdrost@c-98-207-102-156.hsd1.ca.comcast.net) (Quit: This computer has gone to sleep) |
| 2020-11-18 20:53:32 | <monochrom> | Now, allow me to replace => by ->. Hell, there was a GHC version that did this by mistake. >:) |
| 2020-11-18 20:53:55 | <monochrom> | "forall a. Show a -> ([a] -> c) -> c |
| 2020-11-18 20:54:14 | <monochrom> | "forall a. (Show a, [a] -> c) -> c" |
| 2020-11-18 20:54:28 | <ski> | a value of type `cxt *> a' is like a pair of evidence for (a "dictrionary"/"vtable" for) `cxt', together (bundled) with a value of type `a' |
| 2020-11-18 20:55:19 | → | pavonia joins (~user@unaffiliated/siracusa) |
| 2020-11-18 20:55:27 | <boxscape> | monochrom do you mean this (timestamped) video rae uploaded a few days ago where it happened or a much older ghc version? https://youtu.be/l5veKgGxXd4?t=262 |
| 2020-11-18 20:55:45 | <boxscape> | or, let's say, the bug in this video or a bug from an older ghc version |
| 2020-11-18 20:55:46 | <dminuoso> | boxscape: Note, the above things are mashed into the library `constraints` with slightly altered ergonomics |
| 2020-11-18 20:55:52 | <geekosaur> | much older version |
| 2020-11-18 20:55:55 | <ski> | unfixpoint : makes any sense ? |
| 2020-11-18 20:55:55 | <boxscape> | ah, that library keeps coming up |
| 2020-11-18 20:56:09 | <boxscape> | geekosaur I see |
| 2020-11-18 20:56:33 | <unfixpoint> | Not yet |
| 2020-11-18 20:56:36 | <monochrom> | Yeah, a few years ago. |
| 2020-11-18 20:56:41 | <unfixpoint> | I'll re-read |
| 2020-11-18 20:56:59 | × | Aquazi quits (uid312403@gateway/web/irccloud.com/x-dkkwvspwitpqcrse) (Quit: Connection closed for inactivity) |
| 2020-11-18 20:57:14 | <monochrom> | I don't know whether that video uses the GHC version I have in mind. Too lazy to check. |
| 2020-11-18 20:57:31 | <dminuoso> | boxscape: Roughly, constraints just gives you a bare data: Dict :: Constraint -> * where Dict :: a => Dict a |
| 2020-11-18 20:57:39 | <boxscape> | monochrom it uses something pretty close to HEAD so you've answered the question with your previous comment :) |
| 2020-11-18 20:57:42 | <monochrom> | But certainly not >= 8.6 when I noticed it. |
| 2020-11-18 20:57:51 | <dminuoso> | (So it comes with *just* the constraint, not the value ski used above) |
| 2020-11-18 20:58:12 | <boxscape> | dminuoso I see |
| 2020-11-18 20:58:31 | <dminuoso> | And it turns out GHC has this cool behavior that when you pattern match on that, the dictionary is brought into scope and it can be used to discharge obligations for it |
| 2020-11-18 20:58:58 | <boxscape> | right, that's what we talked about earlier today when I wasn't able to do it in a type class :) |
| 2020-11-18 20:59:04 | <boxscape> | type family |
| 2020-11-18 20:59:04 | <boxscape> | rather |
| 2020-11-18 20:59:16 | <ski> | unfixpoint : `forall' vs. `exists' flips the rôle of caller/user/consumer and the rôle of callee/implementor/producer. with `forall a. ..a..', the caller picks the type to use in place of `a', while the callee have to make do with whatever choise was made (can't even know, in general, which choice was made). with `exists a. ..a..' the callee picks the concrete type that is forgotten, hidden by `a', |
| 2020-11-18 20:59:22 | <ski> | and the caller has to be prepared for any choice (and can't know which was chosen, in general) |
| 2020-11-18 21:00:23 | <dminuoso> | boxscape: The old version has this cool and mindboggingly simple implementation of: |
| 2020-11-18 21:00:32 | <dminuoso> | withDict :: Dict a -> (a => r) -> r; withDict d r = case d of Dict -> r |
| 2020-11-18 21:00:33 | <unfixpoint> | It makes sense but why does one end up needing a library like `constraints` |
| 2020-11-18 21:00:55 | <dminuoso> | Which might look like magic at first glance. :) |
| 2020-11-18 21:01:14 | <boxscape> | does look fairly strange, yeah |
| 2020-11-18 21:01:42 | <boxscape> | but I think it makes sense to me |
| 2020-11-18 21:02:01 | <ski> | unfixpoint : similarly, `cxt => a' vs. `cxt *> a' also flips that rôle, wrt how `cxt' is treated. with `=>', the caller has to provide evidence of `cxt', and the callee can just assume the evidence will be provided to it. with `*>', the callee has to provide the evidence for `cxt', while the caller can rely on it being given / handed to it, along with the value |
| 2020-11-18 21:02:27 | <unfixpoint> | I imagine these are ad-hoc solutions to the crappy module system? |
| 2020-11-18 21:03:20 | <dminuoso> | It's quite surprising that constraints has *that* many downloads.. |
| 2020-11-18 21:03:47 | <ski> | @where on-understanding-revisited |
| 2020-11-18 21:03:47 | <lambdabot> | "On Understanding Data Abstraction, Revisited" by William R. Cook in 2009-10 at <http://www.cs.utexas.edu/~wcook/Drafts/2009/essay.pdf> |
| 2020-11-18 21:04:15 | <ski> | has a discussion on OO vs. Abstract Data Types (and mentions relation of both to existentials), iirc |
| 2020-11-18 21:05:52 | → | moth joins (~moth@s91904426.blix.com) |
| 2020-11-18 21:06:12 | <p0a> | I was told to look into ExceptT |
| 2020-11-18 21:06:14 | <ski> | unfixpoint : "So given [a] we can Ord and Widget it? Instead of Given that we can Ord, Widget an a we have [a]? Wat?" -- having a value of type `exists a. (Ord a,Widget a) *> [a]' means that you have a list of values of some (common) unknown/forgotten/hidden type `a', about which you only know that it's an instance of `Ord' and `Widget' (so you can only really process the values in the list, by passing them |
| 2020-11-18 21:06:20 | <ski> | to the methods of those two type classes) |
| 2020-11-18 21:06:26 | <p0a> | is it from mtl or transformers? |
| 2020-11-18 21:07:16 | <dminuoso> | p0a: mtl provides Monad* typeclasses, transformers provides *T type constructors. |
| 2020-11-18 21:07:21 | <dminuoso> | Though mtl re-exports some of transformers. |
| 2020-11-18 21:07:25 | <ski> | unfixpoint : otoh, `exists a. (Ord a,Widget a) => [a]' would be very different. you'd still have a list of values of a (common) unknown type, but now, to be able to access them, you must now magically somehow conjure up `Ord' and `Widget' instances (for this type `a' that you know nothing about) .. i hope you can see that this is fairly useless |
| 2020-11-18 21:07:36 | <p0a> | dminuoso: got it, thank you |
| 2020-11-18 21:08:07 | → | crdrost joins (~crdrost@c-98-207-102-156.hsd1.ca.comcast.net) |
| 2020-11-18 21:08:29 | → | boxscape59 joins (54a35f37@gateway/web/cgi-irc/kiwiirc.com/ip.84.163.95.55) |
| 2020-11-18 21:09:09 | <hekkaidekapus> | idnar: Now that I got a real machine handy, take a look at this: <https://paste.tomsmeding.com/llmymcm4>. |
| 2020-11-18 21:10:06 | → | Franciman joins (~francesco@host-82-56-223-169.retail.telecomitalia.it) |
| 2020-11-18 21:10:14 | × | Klobbinger quits (543b08ef@dslb-084-059-008-239.084.059.pools.vodafone-ip.de) (Remote host closed the connection) |
| 2020-11-18 21:10:30 | <unfixpoint> | Yeah, I wouldn't know when I'd need that |
| 2020-11-18 21:11:50 | <ski> | `*>' typically goes with `exists', like `=>' typically goes with `forall' |
| 2020-11-18 21:12:46 | <unfixpoint> | By typically you mean freenode#haskell or in general (eg. research)? |
| 2020-11-18 21:12:49 | × | boxscape quits (54a35f37@gateway/web/cgi-irc/kiwiirc.com/ip.84.163.95.55) (Ping timeout: 264 seconds) |
| 2020-11-18 21:13:01 | × | crdrost quits (~crdrost@c-98-207-102-156.hsd1.ca.comcast.net) (Quit: This computer has gone to sleep) |
| 2020-11-18 21:13:18 | <dminuoso> | Mmm, how many other languages have type systems involving quantification and constraints? |
| 2020-11-18 21:13:56 | <ski> | Clean,Mercury |
| 2020-11-18 21:14:40 | <dminuoso> | unfixpoint: Note, this exists and *> is not even Haskell. It's just a pseudo haskell some of us pretend existed. |
| 2020-11-18 21:15:08 | <ski> | unfixpoint : by "typically", i mean that, in practice, most of the times you'd want to express `*>', is in direct conjunction with expressing `exists'; and most of the times you want `=>', it's in direct conjunction with `forall' |
All times are in UTC.