Logs: freenode/#haskell
| 2021-02-28 02:59:33 | <koz_> | I read that as 'one value of each data type'. |
| 2021-02-28 02:59:49 | → | mrchampion joins (~mrchampio@38.18.109.23) |
| 2021-02-28 02:59:52 | <koz_> | So you basically have a closed set of values, one of each type. |
| 2021-02-28 02:59:57 | <zq> | koz_: what reductions should i be applying? |
| 2021-02-28 03:00:10 | <koz_> | zq: Like, evaluations? |
| 2021-02-28 03:00:16 | <koz_> | Or equivalences from laws. |
| 2021-02-28 03:00:31 | <koz_> | Look at how we demonstrate things like type class laws for examples if you need to see this in action. |
| 2021-02-28 03:00:33 | × | m0rphism1 quits (~m0rphism@HSI-KBW-085-216-104-059.hsi.kabelbw.de) (Ping timeout: 264 seconds) |
| 2021-02-28 03:00:33 | → | ddellacosta joins (~ddellacos@86.106.143.32) |
| 2021-02-28 03:00:37 | → | conal joins (~conal@192.145.118.103) |
| 2021-02-28 03:00:44 | <zq> | that's pretty much my question. i'm not clear on which equivalences i should be using |
| 2021-02-28 03:00:52 | <koz_> | zq: There isn't a magic formula. |
| 2021-02-28 03:01:00 | <koz_> | It's like solving an equation. |
| 2021-02-28 03:01:02 | × | slack1256 quits (~slack1256@45.4.2.52) (Remote host closed the connection) |
| 2021-02-28 03:01:15 | <koz_> | You need to see what transformations are available and work towards making the two sides the same. |
| 2021-02-28 03:01:21 | <koz_> | It's different every time. |
| 2021-02-28 03:01:37 | <koz_> | Proofs are not automatable in general. If they were, mathematics would cease to be a science. |
| 2021-02-28 03:01:44 | <koz_> | Try some and see what happens? |
| 2021-02-28 03:01:53 | <zq> | so, foldl f ys (x:xs) = foldl f (x:ys) xs where f = reverse (:) -- where do i go from here? |
| 2021-02-28 03:02:19 | <koz_> | zq: You apply reductions to the whole equality you want to prove. |
| 2021-02-28 03:02:22 | <koz_> | it's a substitution. |
| 2021-02-28 03:02:29 | → | Mrbuck joins (~Mrbuck@gateway/tor-sasl/mrbuck) |
| 2021-02-28 03:02:29 | <koz_> | You're not substituting. |
| 2021-02-28 03:02:38 | <zq> | what wasnt substituted? |
| 2021-02-28 03:02:53 | × | xff0x quits (~xff0x@2001:1a81:5311:f400:9a7d:6852:57d4:8353) (Ping timeout: 272 seconds) |
| 2021-02-28 03:03:05 | <zq> | it's trivial when xs == [] so i've assumed that it isn't |
| 2021-02-28 03:03:24 | <koz_> | Your goal is 'prove that 'foldl (:) ys xs == reverse xs ++ ys' |
| 2021-02-28 03:03:37 | <koz_> | So first, replace the entire LHS with the definition of foldl, renaming parameters as appropriate. |
| 2021-02-28 03:03:40 | <koz_> | Ditto reverse. |
| 2021-02-28 03:03:43 | <koz_> | (except RHS) |
| 2021-02-28 03:03:57 | <koz_> | Maintain the ==, maintain variable names, ensure the == stays intact through each trnasformation. |
| 2021-02-28 03:04:00 | <koz_> | Then see what you get. |
| 2021-02-28 03:04:09 | <zq> | isn't that exactly what i've done on the lhs? |
| 2021-02-28 03:04:27 | <koz_> | Except I don't see 'reverse xs ++ ys' anywhere in the thing you just posted. |
| 2021-02-28 03:04:30 | <zq> | the definition of foldl is recursive |
| 2021-02-28 03:04:38 | → | xff0x joins (~xff0x@2001:1a81:5349:9200:4bab:e866:1730:4463) |
| 2021-02-28 03:04:38 | × | ddellacosta quits (~ddellacos@86.106.143.32) (Ping timeout: 245 seconds) |
| 2021-02-28 03:04:39 | <koz_> | So do one step, keep the recursive part. |
| 2021-02-28 03:04:53 | <koz_> | (also, is this homework?) |
| 2021-02-28 03:04:54 | <zq> | that's what the above is? |
| 2021-02-28 03:05:00 | <zq> | no, it's weekend fun |
| 2021-02-28 03:05:07 | <koz_> | OK, let me try. |
| 2021-02-28 03:05:22 | <zq> | i know i should be proving some side property of (++) but it's unclear to me which |
| 2021-02-28 03:05:45 | <zq> | for reference, this is the haskellified version of ex 4f in https://www.fstar-lang.org/tutorial/ |
| 2021-02-28 03:07:56 | × | darjeeling_ quits (~darjeelin@122.245.218.150) (Ping timeout: 240 seconds) |
| 2021-02-28 03:08:29 | → | banyanRob joins (49f11cfb@c-73-241-28-251.hsd1.ca.comcast.net) |
| 2021-02-28 03:08:44 | <minoru_shiraeesh> | how about proving by induction? |
| 2021-02-28 03:10:08 | <minoru_shiraeesh> | prove for empty list, then prove that if it holds for some list, then it holds for incremented (consed) list |
| 2021-02-28 03:10:30 | × | lawid quits (~quassel@dslb-090-186-099-002.090.186.pools.vodafone-ip.de) (Ping timeout: 246 seconds) |
| 2021-02-28 03:10:47 | <koz_> | I don't think it even compiles, as foldl (:) ys xs won't work when ys is a list, because the args are in the wrong order. |
| 2021-02-28 03:11:21 | <zq> | koz_: yeah, that was the second mistake in my original question. should isntead be `reverse (:)` |
| 2021-02-28 03:11:29 | → | lawid joins (~quassel@dslb-090-186-208-048.090.186.pools.vodafone-ip.de) |
| 2021-02-28 03:11:33 | <koz_> | reverse (:) also makes no sense |
| 2021-02-28 03:11:35 | <zq> | reflected in 03:01:53 < zq> so, foldl f ys (x:xs) = foldl f (x:ys) xs where f = reverse (:) -- where do i go from here? |
| 2021-02-28 03:11:37 | <koz_> | You can't reverse a function. |
| 2021-02-28 03:11:52 | <koz_> | So first, we need a _compiling_ LHS. |
| 2021-02-28 03:12:22 | <zq> | flip (:) -- it's been a while since i've haskelled |
| 2021-02-28 03:12:30 | <koz_> | OK, so our goal is |
| 2021-02-28 03:12:41 | <koz_> | foldl (flip (:)) ys xs == reverse xs ++ ys |
| 2021-02-28 03:12:43 | <koz_> | Right? |
| 2021-02-28 03:13:08 | × | Mrbuck quits (~Mrbuck@gateway/tor-sasl/mrbuck) (Remote host closed the connection) |
| 2021-02-28 03:13:19 | <zq> | yessir, and if proving inductively then this trivially holds when xs == [] so i've skipped ahead to xs == (s:ss) |
| 2021-02-28 03:13:54 | → | Mrbuck joins (~Mrbuck@gateway/tor-sasl/mrbuck) |
| 2021-02-28 03:15:24 | <zq> | i think i get it, rhs has to be expanded first and then leverage associativity of (++) |
| 2021-02-28 03:15:54 | <koz_> | zq: Here's a start: https://paste.tomsmeding.com/vbSX0vE2 |
| 2021-02-28 03:16:26 | <koz_> | This should help you see the next steps. |
| 2021-02-28 03:16:39 | <koz_> | Now, onto the other problem. |
| 2021-02-28 03:17:03 | <koz_> | How I see it is this - your Context monad is actually parameterized over what particular type you are examining at the moment. |
| 2021-02-28 03:17:14 | <koz_> | So it makes sense to talk about Context s a, not Context a. |
| 2021-02-28 03:17:28 | <koz_> | So you can have a Context a, which 'forgets' what state it's focused on. |
| 2021-02-28 03:17:47 | <koz_> | And then you have a function that turns a Context a into Context s a for some s. |
| 2021-02-28 03:17:54 | → | bergey joins (~user@pool-74-108-99-127.nycmny.fios.verizon.net) |
| 2021-02-28 03:18:00 | <koz_> | Problem is, you can't have this be universal, because there might not _be_ an 's' to project into. |
| 2021-02-28 03:18:20 | <koz_> | So you want one function per projection, as well as a 'forgetting' function. |
| 2021-02-28 03:18:20 | → | kw joins (d4662d5d@212.102.45.93) |
| 2021-02-28 03:18:27 | → | FinnElija joins (~finn_elij@gateway/tor-sasl/finnelija/x-67402716) |
| 2021-02-28 03:18:27 | finn_elija | is now known as Guest72499 |
| 2021-02-28 03:18:27 | FinnElija | is now known as finn_elija |
| 2021-02-28 03:18:32 | <koz_> | Then you can define MonadState s (Context s) and live your happy life. |
| 2021-02-28 03:18:35 | <minoru_shiraeesh> | you're talking about State s a? |
| 2021-02-28 03:18:47 | <koz_> | Context s would be equivalent to State s, yes. |
| 2021-02-28 03:18:59 | × | theelous3 quits (~theelous3@unaffiliated/theelous3) (Read error: Connection reset by peer) |
| 2021-02-28 03:19:45 | <minoru_shiraeesh> | but why forget what state it's focused on? that's just sugaring anyway |
| 2021-02-28 03:20:02 | <koz_> | Because then you can't have a Context which _doesn't_ know what type it's focusing on. |
| 2021-02-28 03:20:06 | <minoru_shiraeesh> | how do you glue them together? |
| 2021-02-28 03:20:07 | <koz_> | Which I assumed was the get-go goal. |
| 2021-02-28 03:20:15 | <koz_> | That is exactly how you glue them together. |
| 2021-02-28 03:20:44 | <minoru_shiraeesh> | but the module doesn't care about other contexts |
| 2021-02-28 03:20:50 | <minoru_shiraeesh> | and it's not going to use them |
| 2021-02-28 03:20:56 | <koz_> | So then what's the problem? |
| 2021-02-28 03:21:00 | <koz_> | I'm genuinely confused now. |
| 2021-02-28 03:21:12 | <kw> | What are the dangers of using `unsafePerformIO` with `newIORef` at the top level to create a cache? Values that aren't in the cache will be calculated, inserted into the cache, and returned as needed (in IO). |
| 2021-02-28 03:21:27 | × | Guest72499 quits (~finn_elij@gateway/tor-sasl/finnelija/x-67402716) (Ping timeout: 268 seconds) |
| 2021-02-28 03:21:40 | <koz_> | Why do you think you need this kw? |
| 2021-02-28 03:21:42 | × | pfurla quits (~pfurla@ool-182ed2e2.dyn.optonline.net) (Quit: gone to sleep. ZZZzzz…) |
| 2021-02-28 03:21:45 | <minoru_shiraeesh> | why don't we just provide a module with a simple State ModuleSpecificState a |
| 2021-02-28 03:22:02 | <koz_> | minoru_shiraeesh: I dunno, I'm just answering the posed question, as I understood it. |
| 2021-02-28 03:22:14 | <koz_> | If I misunderstood the posed question, NieDzejkob needs to clarify what they want. |
| 2021-02-28 03:22:47 | <kw> | koz_: It's a shared cache for data that has to be accessed from an external (C) library. |
| 2021-02-28 03:23:11 | <koz_> | If you're calling a C library, aren't you in IO already? |
All times are in UTC.