Logs: freenode/#haskell
| 2021-05-20 00:09:08 | → | bennofs__ joins (~quassel@dynamic-089-012-045-213.89.12.pool.telefonica.de) |
| 2021-05-20 00:09:11 | × | dhil quits (~dhil@195.213.192.85) (Ping timeout: 240 seconds) |
| 2021-05-20 00:09:49 | × | thc202 quits (~thc202@unaffiliated/thc202) (Quit: thc202) |
| 2021-05-20 00:10:10 | → | nbloomf joins (~nbloomf@2600:1700:ad14:3020:582b:30d1:5899:a42a) |
| 2021-05-20 00:10:16 | × | __monty__ quits (~toonn@unaffiliated/toonn) (Quit: leaving) |
| 2021-05-20 00:10:39 | → | tim joins (~tim@112-141-128-42.sta.dodo.net.au) |
| 2021-05-20 00:10:47 | <heebo> | https://www.codepile.net/pile/rLoveZVj |
| 2021-05-20 00:10:51 | × | nbloomf quits (~nbloomf@2600:1700:ad14:3020:582b:30d1:5899:a42a) (Client Quit) |
| 2021-05-20 00:10:53 | × | Deide quits (~Deide@217.155.19.23) (Quit: Seeee yaaaa) |
| 2021-05-20 00:11:03 | tim | is now known as Guest75370 |
| 2021-05-20 00:11:04 | <heebo> | ok its not minimal its basically my cabal.project file |
| 2021-05-20 00:11:31 | → | kristijonas joins (~kristijon@78-56-32-39.static.zebra.lt) |
| 2021-05-20 00:11:48 | <heebo> | in that project I would like to have a Main.hs such that i can import Language.Plutus.Contract |
| 2021-05-20 00:11:58 | × | Guest87676 quits (~laudiacay@67.176.215.84) (Ping timeout: 258 seconds) |
| 2021-05-20 00:12:31 | × | Alleria__ quits (~textual@zrcout.mskcc.org) (Ping timeout: 260 seconds) |
| 2021-05-20 00:12:36 | → | nbloomf joins (~nbloomf@2600:1700:ad14:3020:582b:30d1:5899:a42a) |
| 2021-05-20 00:12:46 | × | bennofs_ quits (~quassel@dynamic-077-013-120-064.77.13.pool.telefonica.de) (Ping timeout: 240 seconds) |
| 2021-05-20 00:12:58 | → | sysadmin joins (~McCafe@23.108.51.26) |
| 2021-05-20 00:15:02 | × | dh quits (dh@bsd.ee) (Read error: Connection reset by peer) |
| 2021-05-20 00:15:21 | → | dh joins (~dh@bsd.ee) |
| 2021-05-20 00:16:07 | → | apache8080 joins (~rishi@wsip-70-168-153-252.oc.oc.cox.net) |
| 2021-05-20 00:18:23 | <dmwit> | Yeah ok, I'm not reading 150 lines of cabal.project. |
| 2021-05-20 00:18:47 | <dmwit> | Not to mention that it doesn't have the rest of what we would need to reproduce it anyway, like the cabal file and the Main.hs. |
| 2021-05-20 00:19:58 | <heebo> | lol, ok fair enough. If I can figure out a minimal example i will post another time, thanks anyway |
| 2021-05-20 00:20:44 | → | kupi joins (uid212005@gateway/web/irccloud.com/x-wambptnsccsnaikr) |
| 2021-05-20 00:22:04 | → | penttrioctium joins (49a0f450@c-73-160-244-80.hsd1.nj.comcast.net) |
| 2021-05-20 00:22:26 | <a6a45081-2b83> | why does he say: but if you write these functions merely by blindly following the types, it doesn’t count |
| 2021-05-20 00:22:41 | ← | dale parts (dale@unaffiliated/dale) () |
| 2021-05-20 00:23:00 | <monochrom> | Perhaps ask the author? |
| 2021-05-20 00:23:15 | → | werneta joins (~werneta@70-142-214-115.lightspeed.irvnca.sbcglobal.net) |
| 2021-05-20 00:23:37 | <dmwit> | Well, I've implemented the Monad instance for Cont at least four times and I still have no idea what it does, because the types make it so blindingly obvious what the implementation has to be that no part of the code actually has to pass through my conscious brain. |
| 2021-05-20 00:23:57 | <dmwit> | If I saw a sentence like what you quote there, I would guess it's to try to head off that problem before it happens. |
| 2021-05-20 00:24:14 | <monochrom> | I don't consider it a problem. |
| 2021-05-20 00:24:34 | <monochrom> | If you will never understand the code, that's a problem. |
| 2021-05-20 00:24:38 | <geekosaur> | it's from "lens over tea" |
| 2021-05-20 00:24:44 | <dmwit> | If you can write code that you understand, and that also type checks, that's a win. If you write code because of what the type checker says, but which you can't understand, well... that's not a good outcome if your plan is to learn what the code does. ^_^ |
| 2021-05-20 00:25:07 | <monochrom> | But between "understanding" and "work mechanically", there is no set order. |
| 2021-05-20 00:25:42 | <monochrom> | And truly, for some problems, it is actually better to work mechanically first, "understand" later. |
| 2021-05-20 00:26:10 | <dmwit> | Yes. I think I am on board with all you say, monochrom. I also think I am accurately presenting the answer to "why does he say X?". |
| 2021-05-20 00:26:21 | <monochrom> | Especially with most people's subjective, unobjective definition of "understand" = feel so good about yourself and can write an essay, but no predictive power. |
| 2021-05-20 00:26:44 | → | abhixec joins (~abhixec@c-67-169-139-16.hsd1.ca.comcast.net) |
| 2021-05-20 00:27:12 | <heebo> | do we care what the code does? doesnt the curry howard isomorphism *prove* that it works? |
| 2021-05-20 00:27:39 | <geekosaur> | it proves that it does something. whether that something is what is intended is another question |
| 2021-05-20 00:28:00 | × | abhixec quits (~abhixec@c-67-169-139-16.hsd1.ca.comcast.net) (Client Quit) |
| 2021-05-20 00:28:04 | <heebo> | the types make sure its intended surely |
| 2021-05-20 00:28:05 | <monochrom> | I met a prof who was disillusioned by curry-howard. |
| 2021-05-20 00:28:21 | × | zaquest quits (~notzaques@5.128.210.178) (Remote host closed the connection) |
| 2021-05-20 00:28:25 | <geekosaur> | \x -> x + 2, the types don't help if what was intended was x * 2 |
| 2021-05-20 00:28:27 | <monochrom> | "We didn't know what we proved but oh boy was it correct." |
| 2021-05-20 00:28:32 | → | elusive joins (~Jeanne-Ka@199.116.118.248) |
| 2021-05-20 00:28:54 | → | zarakshR1 joins (~Thunderbi@202.38.180.58) |
| 2021-05-20 00:30:02 | <heebo> | i actually agree , but im playing devils advocate |
| 2021-05-20 00:30:17 | <a6a45081-2b83> | so for e.g. I am trying to implement _1 I shouldn't look at _1 :: Lens (a,x) (b,x) a b or not at _1 :: Functor f => (a -> f b) -> (a, x) -> f (b, x) or neither |
| 2021-05-20 00:30:34 | <monochrom> | I care what the code does iff I am not doing proof erasure. |
| 2021-05-20 00:30:41 | × | zarakshR quits (~Thunderbi@1.39.134.203) (Ping timeout: 240 seconds) |
| 2021-05-20 00:30:42 | zarakshR1 | is now known as zarakshR |
| 2021-05-20 00:30:42 | magbo | is now known as magbo_go_to_libe |
| 2021-05-20 00:30:47 | magbo_go_to_libe | is now known as go_to_libera_cha |
| 2021-05-20 00:30:53 | go_to_libera_cha | is now known as goto_libera_chat |
| 2021-05-20 00:31:01 | <monochrom> | Like, I actually run the code. |
| 2021-05-20 00:31:44 | <heebo> | i often find , i follow the types first, then look at the code to understand that its correct |
| 2021-05-20 00:32:12 | elusive | is now known as Jeanne-Kamikaze |
| 2021-05-20 00:32:42 | <a6a45081-2b83> | so here I should be thinking along the lines of _1 takes a modifier and applies it to the first element inside a functor? |
| 2021-05-20 00:32:46 | <a6a45081-2b83> | and then implement it? |
| 2021-05-20 00:32:47 | <dmwit> | a6a45081-2b83: I think looking at `_1 :: Lens (a, x) (b, x) a b` is fine. The exercise is probably asking you not to look too hard at `_1 :: Functor f => (a -> f b) -> (a, x) -> f (b, x)` . |
| 2021-05-20 00:33:01 | × | plutoniix quits (~q@node-ujl.pool-125-24.dynamic.totinternet.net) (Ping timeout: 268 seconds) |
| 2021-05-20 00:33:23 | × | Bigcheese quits (~quassel@unaffiliated/bigcheese) (Ping timeout: 250 seconds) |
| 2021-05-20 00:33:28 | <dmwit> | a6a45081-2b83: Or rather: it is asking you not to write your implementation *only* by looking at `_1 :: Functor f => (a -> f b) -> (a, x) -> f (b, x)`. |
| 2021-05-20 00:33:43 | <dmwit> | If you look at that and something else, too, you're winning. |
| 2021-05-20 00:34:53 | <a6a45081-2b83> | got it |
| 2021-05-20 00:35:44 | <heebo> | adit.io lens in pictures was my best reference for understanding lens , https://adit.io/posts/2013-07-22-lenses-in-pictures.html its kinda for kids though i suppose |
| 2021-05-20 00:36:35 | → | regakakobigman joins (~regakakob@c-73-174-187-176.hsd1.pa.comcast.net) |
| 2021-05-20 00:36:52 | → | zaquest joins (~notzaques@5.128.210.178) |
| 2021-05-20 00:36:54 | → | ddellacosta joins (~ddellacos@86.106.143.22) |
| 2021-05-20 00:37:41 | × | zarakshR quits (~Thunderbi@202.38.180.58) (Ping timeout: 240 seconds) |
| 2021-05-20 00:39:03 | → | Bigcheese joins (~quassel@unaffiliated/bigcheese) |
| 2021-05-20 00:40:19 | → | aVikingTrex joins (~aVikingTr@2001:8003:340d:d00:b2de:b98:7a93:b0ea) |
| 2021-05-20 00:41:24 | × | ddellacosta quits (~ddellacos@86.106.143.22) (Ping timeout: 265 seconds) |
| 2021-05-20 00:43:49 | <a6a45081-2b83> | so for lens, I wrote this: lens get set f s = do { let v = get s; b <- f v; let t = set s b; return t } |
| 2021-05-20 00:44:06 | <a6a45081-2b83> | should be right? but it's for Monad f not Functor f |
| 2021-05-20 00:44:34 | <a6a45081-2b83> | feels like i'm writing imperitive style :-) |
| 2021-05-20 00:44:38 | → | plutoniix joins (~q@node-ujl.pool-125-24.dynamic.totinternet.net) |
| 2021-05-20 00:46:28 | <a6a45081-2b83> | heebo: that is really helpful |
| 2021-05-20 00:48:04 | <Axman6> | a6a45081-2b83: well, you know f in the tpoye is a Functor right? So what does that mean you can do with it? |
| 2021-05-20 00:48:04 | → | merijn joins (~merijn@83-160-49-249.ip.xs4all.nl) |
| 2021-05-20 00:48:19 | <Axman6> | what do we know about functors? |
| 2021-05-20 00:48:45 | <a6a45081-2b83> | lens get set f s = fmap set s . get s ? |
| 2021-05-20 00:48:58 | <a6a45081-2b83> | maybe fmap (set s) $ get s |
| 2021-05-20 00:49:09 | <Axman6> | what happened to f? |
| 2021-05-20 00:49:18 | <a6a45081-2b83> | maybe fmap (set s) $ f (get s) |
| 2021-05-20 00:49:29 | <Axman6> | does that type check? |
| 2021-05-20 00:49:48 | → | tromp joins (~tromp@dhcp-077-249-230-040.chello.nl) |
| 2021-05-20 00:50:02 | → | Guest87676 joins (~laudiacay@67.176.215.84) |
| 2021-05-20 00:50:09 | <a6a45081-2b83> | well it does, :)) , thanks! |
| 2021-05-20 00:50:26 | <Axman6> | I'm pretty dumb, can you explain to me what's happening there? |
| 2021-05-20 00:50:29 | × | killsushi_ quits (~killsushi@2607:fea8:3d40:767:a43a:b464:d0c6:6044) (Quit: Leaving) |
| 2021-05-20 00:50:49 | <Axman6> | what _ai_ f? s? |
| 2021-05-20 00:50:54 | <Axman6> | _is_* |
| 2021-05-20 00:52:04 | × | acidjnk_new2 quits (~acidjnk@p200300d0c72b958680cf6a8401116b8a.dip0.t-ipconnect.de) (Ping timeout: 245 seconds) |
| 2021-05-20 00:52:31 | <a6a45081-2b83> | :t lens get set f s = fmap (set s) $ f (get s) |
All times are in UTC.