Logs: freenode/#haskell
| 2021-04-13 18:17:24 | <ski> | "unknown" (as a noun) is certainly not a bad term for it |
| 2021-04-13 18:17:42 | <ski> | wroathe : e.g. `Const' certainly does not have kind `*' |
| 2021-04-13 18:17:54 | <[exa]> | wroathe: perhaps best contrast it with monomorphic |
| 2021-04-13 18:17:59 | <ski> | @kind Const :: * |
| 2021-04-13 18:18:01 | <lambdabot> | error: |
| 2021-04-13 18:18:01 | <lambdabot> | • Expecting two more arguments to ‘Const’ |
| 2021-04-13 18:18:01 | <lambdabot> | Expected a type, but ‘Const’ has kind ‘* -> k0 -> *’ |
| 2021-04-13 18:18:02 | <ski> | @kind Const :: * -> * -> * |
| 2021-04-13 18:18:03 | <lambdabot> | * -> * -> * |
| 2021-04-13 18:18:06 | <ski> | @kind Const :: * -> (* -> *) -> * |
| 2021-04-13 18:18:07 | <lambdabot> | * -> (* -> *) -> * |
| 2021-04-13 18:18:08 | <[exa]> | ski: nitpicking/curiosity: is `Const` polymorphic? |
| 2021-04-13 18:18:16 | <ski> | @kind Const |
| 2021-04-13 18:18:18 | <lambdabot> | * -> k -> * |
| 2021-04-13 18:18:28 | <ski> | [exa] : yes (as i said above) |
| 2021-04-13 18:18:57 | <[exa]> | ah it clicked now, I was thinking at a wrong level. |
| 2021-04-13 18:19:00 | <[exa]> | :] |
| 2021-04-13 18:19:41 | <ski> | (for short, instead of "universally quantified type", i guess one could say `forall'-type) |
| 2021-04-13 18:20:01 | <wroathe> | What would be the simplest possible example where an explicit forall would be required to achieve behavior that's different than what haskell's default behavior is? |
| 2021-04-13 18:21:00 | <ski> | monochrom : "meta variable" make some kind of sense to me. but i agree it's not that great a name, a bit clunky .. and "logic variable" (basically the same thing, in a logic programming context) is more ad hoc a term |
| 2021-04-13 18:21:05 | <[exa]> | wroathe: guessing: `f x = x x` called as `f id` |
| 2021-04-13 18:21:19 | <monochrom> | You'll need rank-2 for that. forall b. (forall a. a -> a -> a) -> b -> b -> b isn't expressible in Haskell 2010. |
| 2021-04-13 18:21:25 | → | tsandstr joins (~user@nat-130-132-173-221.central.yale.edu) |
| 2021-04-13 18:22:12 | <monochrom> | Then gain I goofed it. You can argue that it's just forall b. Bool -> b -> b -> b >:) |
| 2021-04-13 18:22:52 | × | merijn quits (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 240 seconds) |
| 2021-04-13 18:23:04 | <wroathe> | [exa]: Right, so in this example it's about breaking the assumption that x would have a type of kind * |
| 2021-04-13 18:23:38 | <wroathe> | [exa]: ? I meant to add |
| 2021-04-13 18:24:44 | <wroathe> | monochrom: Was that an answer to my question? |
| 2021-04-13 18:24:51 | <monochrom> | Yes. |
| 2021-04-13 18:24:56 | <wroathe> | monochrom: And if so, why is forall required there? |
| 2021-04-13 18:25:03 | <[exa]> | wroathe: x has to have kind *, it's used as a value-level term, right? |
| 2021-04-13 18:25:07 | <wroathe> | monochrom: (sorry if I'm being dense) |
| 2021-04-13 18:25:09 | → | curlybangs joins (185a6b4e@cpe-24-90-107-78.nyc.res.rr.com) |
| 2021-04-13 18:25:13 | <monochrom> | The inner "forall a" cannot be deleted. |
| 2021-04-13 18:25:36 | <monochrom> | The outer "forall b", I don't care either way. |
| 2021-04-13 18:26:30 | <monochrom> | Here. xxx :: (forall a. a->a->a) -> Int; xxx f = f 10 20 |
| 2021-04-13 18:26:42 | <ski> | bah .. i know John Baez has a TWF issue talking about stuff like `2 = forall a. a -> a -> a', but i can't find it atm .. :/ |
| 2021-04-13 18:27:39 | <wroathe> | monochrom: So without the forall, the first paramater's type would have to be a -> a -> Int, right? |
| 2021-04-13 18:28:12 | <monochrom> | Without the forall, you have (a->a->a)->Int. That's very different. |
| 2021-04-13 18:28:27 | → | ddellaco_ joins (~ddellacos@ool-44c73afa.dyn.optonline.net) |
| 2021-04-13 18:28:40 | <monochrom> | yyy :: (a->a->a) -> Int; yyy f = f 10 20 = type error |
| 2021-04-13 18:28:45 | <ski> | > let frob f = f (map f ["foo","bar","baz","quux"]) in frob reverse |
| 2021-04-13 18:28:47 | <lambdabot> | error: |
| 2021-04-13 18:28:47 | <lambdabot> | • Couldn't match type ‘[Char]’ with ‘Char’ |
| 2021-04-13 18:28:47 | <lambdabot> | Expected type: [Char] -> Char |
| 2021-04-13 18:28:57 | <ski> | > let frob :: (forall a. [a] -> [a]) -> [String]; frob f = f (map f ["foo","bar","baz","quux"]) in frob reverse |
| 2021-04-13 18:28:59 | <lambdabot> | ["xuuq","zab","rab","oof"] |
| 2021-04-13 18:29:01 | <ski> | > let frob :: (forall a. [a] -> [a]) -> [String]; frob f = f (map f ["foo","bar","baz","quux"]) in frob (take 2) |
| 2021-04-13 18:29:04 | <lambdabot> | ["fo","ba"] |
| 2021-04-13 18:29:17 | <ski> | wroathe : ^ that's another rank-2 example |
| 2021-04-13 18:29:55 | <monochrom> | "for every person p, (if p drinks, then I drink)" vs "if (for every person p, p drinks), then I drink". |
| 2021-04-13 18:30:34 | × | jaykru quits (~user@unaffiliated/jaykru) (Remote host closed the connection) |
| 2021-04-13 18:30:55 | <[exa]> | wroathe: anyway the previous example is basically a play on ω=λx.xx, it's a usual (anti)example in almost all type textbooks |
| 2021-04-13 18:31:04 | <wroathe> | ski: So in that first line, f is being applied to both an array of strings, and individual strings themselves, right? |
| 2021-04-13 18:31:39 | ski | . o O ( <https://en.wikipedia.org/wiki/Drinker_paradox> ; "Searchable Sets, Dubuc-Penon Compactness, Omniscience Principles, and the Drinker Paradox" by Martín Hötzel Escardó,Paulo Oliva in 2010 at <http://www.cs.bham.ac.uk/~mhe/papers/dp.pdf>,<http://www.cs.bham.ac.uk/~mhe/papers/DP/> ) |
| 2021-04-13 18:31:56 | <ski> | wroathe : yes (lists, not arrays) |
| 2021-04-13 18:32:11 | <wroathe> | ski: Sorry, I still have one foot in C land :P |
| 2021-04-13 18:32:13 | <wroathe> | ski: Yes, lists |
| 2021-04-13 18:32:19 | <ski> | wroathe : or, to take a simpler example, `let frob f = (f False,f "True") in f id' |
| 2021-04-13 18:32:28 | <wroathe> | ski: Perfect! |
| 2021-04-13 18:32:32 | <ski> | er, s/f id/frob id/ |
| 2021-04-13 18:33:04 | <wroathe> | ski: So without forall you couldn't express that f is both a Bool -> Bool and a String -> String |
| 2021-04-13 18:33:22 | ski | . o O ( <https://en.wikipedia.org/wiki/Donkey_sentence> ) |
| 2021-04-13 18:33:24 | <ski> | right |
| 2021-04-13 18:33:40 | <ski> | (with intersection types, you could. but Haskell doesn't have those) |
| 2021-04-13 18:34:07 | <wroathe> | ski: That example helps a lot. Thanks. |
| 2021-04-13 18:34:55 | <wroathe> | ski: What does this donkey sentence thing have to do with this conversation :P? |
| 2021-04-13 18:35:14 | <ski> | rank-2 isn't that commonly useful .. but when it what one wants to do, it can be hard to work around in another way |
| 2021-04-13 18:35:37 | → | rom1504 joins (rom1504@rom1504.fr) |
| 2021-04-13 18:36:02 | <ski> | rank-2 can also be used for information hiding, separation of concerns. prohibiting a callback, passed to you, from reaching into your implementation innards |
| 2021-04-13 18:36:02 | <wroathe> | I noticed another article mentioning ScopedTypeVariables. Is it the case that forall has been overloaded with meanings that it doesn't traditionally have in Haskell? |
| 2021-04-13 18:36:18 | <ski> | not really |
| 2021-04-13 18:36:41 | <ski> | (although, `ScopedTypeVariables' is, imho, backwards ..) |
| 2021-04-13 18:36:49 | <wroathe> | I.e. shouldn't there be some other form of syntax indicating that a variable is "scoped"? And if not, why does it make sense ot use forall. to designate that? |
| 2021-04-13 18:37:00 | <wroathe> | a type variable* |
| 2021-04-13 18:38:22 | → | coot joins (~coot@37.30.50.130.nat.umts.dynamic.t-mobile.pl) |
| 2021-04-13 18:38:30 | <geekosaur> | forall (a) to minimize stealing syntax (b) it's kinda the reverse of what it normally means, in the sense of it normally restricts the scope of a type variable but in STV expands it instead |
| 2021-04-13 18:38:37 | <ski> | oh, the "if (for every person p, p drinks), then I drink" reminded me of anaphora. like e.g. "Every farmer who owns a donkey beats it.". or "If there exists a prime ⌜p⌝ such that ⌜P(p)⌝, then ⌜Q(q)⌝ also holds." .. does this mean ⌜(∃p. P(p)) ⇒ Q(p)⌝ ? what is the scope of ⌜p⌝ there ?? |
| 2021-04-13 18:39:31 | <monochrom> | Hey, may I reduce the referential transparency problem to the donkey sentence problem? "The King of France is bald" is short for "Every time there is a King of France, he's bald", now it's "just" a donkey sentence. |
| 2021-04-13 18:39:40 | → | falafel joins (~falafel@pool-96-255-70-50.washdc.fios.verizon.net) |
| 2021-04-13 18:39:43 | × | curlybangs quits (185a6b4e@cpe-24-90-107-78.nyc.res.rr.com) (Quit: Connection closed) |
| 2021-04-13 18:40:01 | <wroathe> | This is some high brow hazing going on |
| 2021-04-13 18:40:08 | × | grimpeux quits (~textual@modemcable153.12-178-173.mc.videotron.ca) (Quit: My MacBook has gone to sleep. ZZZzzz…) |
| 2021-04-13 18:40:23 | <wroathe> | https://www.youtube.com/watch?v=LlfSAGucPZc live action footage of ski and monochrom |
| 2021-04-13 18:40:29 | × | usr25 quits (~usr25@unaffiliated/usr25) (Quit: Leaving) |
| 2021-04-13 18:41:27 | <wroathe> | ski: monochrom: [exa]: Well, thanks for the examples. Heading out for now. |
| 2021-04-13 18:43:24 | <monochrom> | "if there is an even prime, it's even" is clearly a forall sentence. |
| 2021-04-13 18:43:31 | <monochrom> | This is what's wrong with English. |
| 2021-04-13 18:44:01 | → | Sornaensis joins (~Sornaensi@85.203.36.21) |
| 2021-04-13 18:44:08 | → | horatiohb joins (~horatiohb@104.236.81.226) |
| 2021-04-13 18:44:17 | <ski> | i think there was some issue on GHC, talking about possibly having a language extension that "does `ScopedTypeVariables' right" (in the above sense) .. but i can't find it, atm. at least it mentioned this perception |
| 2021-04-13 18:44:43 | <[exa]> | wroathe: btw highly suggest getting how the STLC and Hindley-Milner "inference algorithms" work before you jump to haskell, if you didn't do that already |
| 2021-04-13 18:44:55 | <ski> | monochrom : Russell preferred to use an existential quantifier |
| 2021-04-13 18:45:01 | <monochrom> | But people don't use that idiom unless it's on the order of "if there is an odd perfect number, it's odd". |
| 2021-04-13 18:45:22 | <ski> | now, is "The King of France is not bald." the negation of "The King of France is bald." ? |
| 2021-04-13 18:45:36 | <ski> | wroathe : yw |
| 2021-04-13 18:45:48 | <monochrom> | the "there is" there is really poetic emphasis on "I really doubt that there is an odd perfect number. Fat chance." |
| 2021-04-13 18:46:49 | × | Sorny quits (~Sornaensi@79.142.232.102) (Ping timeout: 252 seconds) |
| 2021-04-13 18:47:21 | × | wroathe quits (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) (Ping timeout: 260 seconds) |
| 2021-04-13 18:48:03 | <monochrom> | Pig Latin and Donkey English. |
All times are in UTC.