Logs: liberachat/#haskell
| 2021-07-13 21:08:50 | → | Patternmaster joins (~georg@li1192-118.members.linode.com) |
| 2021-07-13 21:11:52 | × | Vajb quits (~Vajb@hag-jnsbng11-58c3a1-224.dhcp.inet.fi) (Remote host closed the connection) |
| 2021-07-13 21:12:49 | → | Vajb joins (~Vajb@hag-jnsbng11-58c3a1-224.dhcp.inet.fi) |
| 2021-07-13 21:12:55 | → | FixedPointDude joins (~FixedPoin@204.237.49.106) |
| 2021-07-13 21:13:11 | <FixedPointDude> | hello, i have a horrible conjecture |
| 2021-07-13 21:13:57 | <koz> | FixedPointDude: P vs NP is still undecided. |
| 2021-07-13 21:14:22 | <FixedPointDude> | abusing types, let f 0 = id, f k = f k-1 fmap |
| 2021-07-13 21:14:26 | <FixedPointDude> | (har) |
| 2021-07-13 21:14:40 | <FixedPointDude> | so that f k = fmap fmap ... fmap, with k terms |
| 2021-07-13 21:15:14 | <FixedPointDude> | then: f 4 is a fixed point of f k, for all k >= 6 |
| 2021-07-13 21:15:42 | <FixedPointDude> | i.e. (fmap ... fmap) 10 times = (fmap ... fmap) 6 times, etc |
| 2021-07-13 21:15:50 | <monochrom> | Is that "fmap (fmap (fmap ..."? Is that "(...(fmap fmap) fmap) ..."? |
| 2021-07-13 21:15:57 | <FixedPointDude> | left associate i believe |
| 2021-07-13 21:16:02 | <Hecate> | koz: :') |
| 2021-07-13 21:16:27 | <koz> | Hecate: What can I say? It's the source of many horrible conjectures. |
| 2021-07-13 21:16:55 | <FixedPointDude> | the basis of this conjecture is that ghc claims these have the same types, and no other combinations i've noticed do |
| 2021-07-13 21:17:22 | <monochrom> | @type ((fmap fmap) fmap) fmap |
| 2021-07-13 21:17:23 | <lambdabot> | (Functor f1, Functor f2, Functor f3) => f1 (f2 (a -> b)) -> f1 (f2 (f3 a -> f3 b)) |
| 2021-07-13 21:17:26 | <FixedPointDude> | inspired by the observation that fmap fmap fmap = (.).(.) |
| 2021-07-13 21:18:01 | → | neceve joins (~quassel@2a02:c7f:607e:d600:f762:20dd:304e:4b1f) |
| 2021-07-13 21:18:03 | → | o1lo01ol1o joins (~o1lo01ol1@bl7-89-228.dsl.telepac.pt) |
| 2021-07-13 21:18:22 | <hseg> | ah. you mean after a point, the types cycle between [(a -> b) -> f1 (f2 (f3 a)) -> f1 (f2 (f3 b))], [f1 (f2 (f3 (a -> b))) -> f1 (f2 (f3 (f4 a -> f4 b)))], [f1 (f2 (f3 (a -> b))) -> f1 (f2 (f3 (f4 a -> f4 b)))], [f1 (f2 (f3 (a -> b))) -> f1 (f2 (f3 (f4 a -> f4 b)))] |
| 2021-07-13 21:18:32 | <hseg> | .... that was unreadable |
| 2021-07-13 21:18:35 | <FixedPointDude> | not that i can parse what you wrote, but probably |
| 2021-07-13 21:18:49 | <FixedPointDude> | haha |
| 2021-07-13 21:19:07 | <Hecate> | hahaha |
| 2021-07-13 21:19:14 | <FixedPointDude> | the idea of proving this makes my palms sweaty |
| 2021-07-13 21:19:25 | <FixedPointDude> | i want to practice these kinds of things, but not actually this |
| 2021-07-13 21:19:43 | <hseg> | not too bad -- it's just four unifications |
| 2021-07-13 21:19:58 | <FixedPointDude> | (i don't know what a unification is) |
| 2021-07-13 21:20:42 | <FixedPointDude> | https://github.com/jozefg/higher-order-unification/blob/master/explanation.md |
| 2021-07-13 21:20:44 | <hseg> | when you apply f :: a -> b to a value c :: t, ghc checks a ~ c |
| 2021-07-13 21:20:46 | <FixedPointDude> | this looks abstract |
| 2021-07-13 21:21:24 | <hseg> | sorry, a ~t |
| 2021-07-13 21:21:26 | → | merijn joins (~merijn@83-160-49-249.ip.xs4all.nl) |
| 2021-07-13 21:22:01 | <hseg> | and to do that, it *unifies* the two types -- tries applying known equalities to show they are also equal |
| 2021-07-13 21:22:25 | × | o1lo01ol1o quits (~o1lo01ol1@bl7-89-228.dsl.telepac.pt) (Ping timeout: 246 seconds) |
| 2021-07-13 21:24:03 | <FixedPointDude> | so like, e.g. given two parametric types, what's the biggest parametric type which is a subtype both? |
| 2021-07-13 21:24:16 | × | raehik quits (~raehik@cpc95906-rdng25-2-0-cust156.15-3.cable.virginm.net) (Ping timeout: 272 seconds) |
| 2021-07-13 21:24:21 | <FixedPointDude> | the meet of parametric types |
| 2021-07-13 21:24:21 | <hseg> | yup |
| 2021-07-13 21:25:21 | <hseg> | e.g. x :: (Int, a), f :: (b,Bool) -> Char is legal since there is a unification (~ assignment of variables) s.t. (Int, a) ~ (b, Bool) |
| 2021-07-13 21:26:34 | × | amahl quits (~amahl@dsl-jklbng12-54fbca-64.dhcp.inet.fi) (Ping timeout: 272 seconds) |
| 2021-07-13 21:27:00 | <FixedPointDude> | it seems to me that things like this can only show that a term is well-typed, so that two functions *might* be equal |
| 2021-07-13 21:27:34 | <FixedPointDude> | but given two functions f,g : a -> b, i don't see how this technique can show that they are equal |
| 2021-07-13 21:27:46 | <FixedPointDude> | extentionally, on all possible values |
| 2021-07-13 21:28:16 | <FixedPointDude> | is this particular to some special universal property of fmap? |
| 2021-07-13 21:28:26 | → | warnz joins (~warnz@2600:1700:77c0:5610:9856:f279:a598:9845) |
| 2021-07-13 21:28:27 | <hseg> | don't _think_ so? |
| 2021-07-13 21:28:34 | × | warnz quits (~warnz@2600:1700:77c0:5610:9856:f279:a598:9845) (Remote host closed the connection) |
| 2021-07-13 21:28:56 | → | warnz joins (~warnz@2600:1700:77c0:5610:9856:f279:a598:9845) |
| 2021-07-13 21:30:45 | <hseg> | btw, note this depends on you applying left-associatively |
| 2021-07-13 21:31:29 | <hseg> | right-associatively, fmap (fmap (...) :: f1 (f2 (f3 ... (a -> b) -> f1 (f2 (f3 ... (g a -> g b) |
| 2021-07-13 21:33:04 | → | Lycurgus joins (~juan@cpe-45-46-140-49.buffalo.res.rr.com) |
| 2021-07-13 21:34:42 | <hseg> | ah, I see where the fixpoint comes from -- recall we have a Functor ((->) a) instance |
| 2021-07-13 21:38:11 | → | eggplantade joins (~Eggplanta@108-201-191-115.lightspeed.sntcca.sbcglobal.net) |
| 2021-07-13 21:41:52 | → | o1lo01ol1o joins (~o1lo01ol1@bl7-89-228.dsl.telepac.pt) |
| 2021-07-13 21:42:54 | × | eggplantade quits (~Eggplanta@108-201-191-115.lightspeed.sntcca.sbcglobal.net) (Ping timeout: 255 seconds) |
| 2021-07-13 21:43:09 | <FixedPointDude> | i went and got a snack and i actually think the "fixed point" formulation is wrong |
| 2021-07-13 21:43:23 | → | o1lo01ol_ joins (~o1lo01ol1@bl11-109-140.dsl.telepac.pt) |
| 2021-07-13 21:43:32 | <FixedPointDude> | for the simple reason that (f f)(f f) is different from ((f f) f) f |
| 2021-07-13 21:43:47 | <FixedPointDude> | so the re-stated conjecture is instead: |
| 2021-07-13 21:44:00 | <hseg> | yes, but it's a fixed point of \k -> k fmap |
| 2021-07-13 21:44:03 | <FixedPointDude> | f k+4 = f k, for all k >= 6 |
| 2021-07-13 21:44:15 | <FixedPointDude> | aaaah re: k as the variable |
| 2021-07-13 21:44:29 | <hseg> | (well, it enters a cycle of period 4 |
| 2021-07-13 21:44:48 | <hseg> | so actually you want "is a fixed point of \k -> k fmap fmap fmap fmap" |
| 2021-07-13 21:44:50 | <hseg> | ) |
| 2021-07-13 21:44:56 | → | Guest6135 joins (~Guest61@2001:ac8:27:20::a01e) |
| 2021-07-13 21:45:04 | <FixedPointDude> | yes, that'll do it |
| 2021-07-13 21:45:45 | <hololeap> | koz: MonadTrans is one of the examples in the docs. see the second example under "Motiviation" |
| 2021-07-13 21:45:50 | <hololeap> | *Motivation |
| 2021-07-13 21:46:05 | <koz> | hololeap: The docs for QuantifiedConstraints I'm guessing? |
| 2021-07-13 21:46:17 | × | warnz quits (~warnz@2600:1700:77c0:5610:9856:f279:a598:9845) (Remote host closed the connection) |
| 2021-07-13 21:46:17 | <hololeap> | yeah |
| 2021-07-13 21:46:32 | <hololeap> | GHC user's guide |
| 2021-07-13 21:46:35 | <hseg> | yeah, so the first couple steps are tiresome |
| 2021-07-13 21:46:50 | × | o1lo01ol1o quits (~o1lo01ol1@bl7-89-228.dsl.telepac.pt) (Ping timeout: 272 seconds) |
| 2021-07-13 21:47:59 | × | hexfive quits (~eric@50.35.83.177) (Quit: WeeChat 3.0) |
| 2021-07-13 21:48:22 | <hololeap> | (this is actually the first time I've read about this extension...) |
| 2021-07-13 21:49:23 | → | eggplantade joins (~Eggplanta@108-201-191-115.lightspeed.sntcca.sbcglobal.net) |
| 2021-07-13 21:49:51 | <hololeap> | so, would this allow us to make Set a real haskell Functor? |
| 2021-07-13 21:50:32 | <hseg> | don't think so -- to make set into a Functor you'd need to be able to restrict the types at which it is applied |
| 2021-07-13 21:50:54 | → | justsomeguy joins (~justsomeg@user/justsomeguy) |
| 2021-07-13 21:51:28 | × | drd quits (~drd@93-39-151-19.ip76.fastwebnet.it) (Ping timeout: 246 seconds) |
| 2021-07-13 21:52:40 | → | jneira_ joins (~jneira_@28.red-80-28-169.staticip.rima-tde.net) |
| 2021-07-13 21:52:51 | → | mariohesles joins (~user@172.58.97.195) |
| 2021-07-13 21:53:43 | × | wallymathieu quits (~wallymath@81-234-151-21-no94.tbcn.telia.com) (Quit: My MacBook has gone to sleep. ZZZzzz…) |
| 2021-07-13 21:55:19 | × | merijn quits (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 246 seconds) |
| 2021-07-13 21:55:24 | <hseg> | FixedPointDude: http://ix.io/3sUI |
| 2021-07-13 21:55:39 | × | fendor quits (~fendor@178.115.59.187.wireless.dyn.drei.com) (Read error: Connection reset by peer) |
| 2021-07-13 21:55:40 | × | falafel quits (~falafel@pool-96-255-70-50.washdc.fios.verizon.net) (Ping timeout: 246 seconds) |
| 2021-07-13 21:55:51 | <hseg> | note the heavy use made of the Functor ((->) a) instance to supply enough arguments |
| 2021-07-13 21:56:49 | × | ph88 quits (~ph88@2a02:8109:9e00:7e5c:146a:5c4b:109:2ce4) (Ping timeout: 268 seconds) |
| 2021-07-13 21:57:10 | <FixedPointDude> | this is interesting |
| 2021-07-13 21:57:15 | <FixedPointDude> | i don't know how to read it though |
| 2021-07-13 21:57:40 | <hseg> | the existence of such an instance means that a bare fmap can be fed any number of arguments, as can be checked by asking GHC for the types of fmap, fmap _, fmap _ _, ... |
| 2021-07-13 21:58:35 | <hseg> | ok, so lines outside {} are the types of various iterations of fmap |
| 2021-07-13 21:59:02 | <hseg> | one then applies the term of that type to fmap :: (α -> β) -> (φ α -> φ β) |
| 2021-07-13 21:59:35 | <hseg> | in order for this to be legal, the type of the parameter of the term must unify with this type |
All times are in UTC.