Logs: liberachat/#haskell
| 2021-07-14 17:17:02 | <hololeap> | arkanoid: I think he means that the type system provides a proof of correctness, but the type system can't do _every_ kind of validation |
| 2021-07-14 17:17:20 | <hololeap> | for instance, reverse :: [a] -> [a] |
| 2021-07-14 17:17:42 | <hololeap> | the type system does nothing to prove that this function works the way it's intended to |
| 2021-07-14 17:17:51 | <davean> | Well you can never do every kinda of validation, correctness is with respect to a specification |
| 2021-07-14 17:19:07 | → | tzh joins (~tzh@c-24-21-73-154.hsd1.or.comcast.net) |
| 2021-07-14 17:19:11 | <davean> | arkanoid: do you have more around the quote? |
| 2021-07-14 17:19:39 | <hololeap> | davean: https://github.com/hmemcpy/milewski-ctfp-pdf/releases/download/v19-eb86347/category-theory-for-programmers--eb86347.pdf |
| 2021-07-14 17:19:43 | <hololeap> | top of page 20 |
| 2021-07-14 17:19:43 | → | koolazer joins (~koo@user/koolazer) |
| 2021-07-14 17:20:24 | → | merijn joins (~merijn@83-160-49-249.ip.xs4all.nl) |
| 2021-07-14 17:20:39 | <davean> | hum |
| 2021-07-14 17:21:20 | <davean> | No, I don't think he means the liquid haskell one there, and I think that claim is bullshit. |
| 2021-07-14 17:21:27 | → | P1RATEZ joins (piratez@user/p1ratez) |
| 2021-07-14 17:21:27 | <davean> | Though possibly technically correct in a sense |
| 2021-07-14 17:21:46 | <davean> | Though the liquid-haskell one might be of interest |
| 2021-07-14 17:22:21 | × | cheater quits (~Username@user/cheater) (Ping timeout: 255 seconds) |
| 2021-07-14 17:22:30 | → | cheater joins (~Username@user/cheater) |
| 2021-07-14 17:23:37 | × | fef quits (~thedawn@user/thedawn) (Remote host closed the connection) |
| 2021-07-14 17:24:40 | <davean> | The types are a proof of some sort of correctness, but often not valid proofs |
| 2021-07-14 17:24:55 | <davean> | and don't cover all the stuff you should care about |
| 2021-07-14 17:25:06 | <davean> | Sure, they help |
| 2021-07-14 17:25:38 | × | merijn quits (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 252 seconds) |
| 2021-07-14 17:27:40 | <davean> | The standard library more provides your axioms |
| 2021-07-14 17:29:38 | × | cheater quits (~Username@user/cheater) (Ping timeout: 265 seconds) |
| 2021-07-14 17:29:58 | → | cheater joins (~Username@user/cheater) |
| 2021-07-14 17:33:30 | × | P1RATEZ quits (piratez@user/p1ratez) (Ping timeout: 265 seconds) |
| 2021-07-14 17:34:20 | → | Guest27 joins (~Guest27@187.83.249.216.dyn.smithville.net) |
| 2021-07-14 17:35:35 | → | Deide joins (~Deide@217.155.19.23) |
| 2021-07-14 17:35:35 | × | Deide quits (~Deide@217.155.19.23) (Changing host) |
| 2021-07-14 17:35:35 | → | Deide joins (~Deide@user/deide) |
| 2021-07-14 17:37:11 | <arkanoid> | hololeap: yes is by Mr Milewski |
| 2021-07-14 17:40:39 | <arkanoid> | thanks for all the answers. Yes I do understand how that sentence might raise more than one eyebrow, but the author is clearly trying to make things easier and put things into categories (ba dum tss) |
| 2021-07-14 17:45:19 | × | elf_fortrez quits (~elf_fortr@adsl-72-50-4-118.prtc.net) (Ping timeout: 246 seconds) |
| 2021-07-14 17:45:38 | <monochrom> | I would s/not valid/weakened/ |
| 2021-07-14 17:46:06 | → | hexreel joins (~hr@69.233.98.238) |
| 2021-07-14 17:46:14 | × | chris_ quits (~chris@81.96.113.213) (Remote host closed the connection) |
| 2021-07-14 17:46:54 | <monochrom> | Also, while we're at curry-howard, types are claims, terms are proofs. |
| 2021-07-14 17:47:37 | <monochrom> | In Haskell, types are weakened claims, not invalid claims. This is a case of PEBKAC again. |
| 2021-07-14 17:48:19 | → | ubert joins (~Thunderbi@p2e5a50e5.dip0.t-ipconnect.de) |
| 2021-07-14 17:49:51 | → | chris_ joins (~chris@81.96.113.213) |
| 2021-07-14 17:51:04 | → | pfurla_ joins (~pfurla@ool-182ed2e2.dyn.optonline.net) |
| 2021-07-14 17:52:56 | <EvanR> | something tells me this is a different sort of 'weak' |
| 2021-07-14 17:53:26 | <EvanR> | by weak you mean comes with more caveats? |
| 2021-07-14 17:54:03 | → | ubikium joins (~ubikium@113x43x248x70.ap113.ftth.arteria-hikari.net) |
| 2021-07-14 17:54:04 | × | koolazer quits (~koo@user/koolazer) (Ping timeout: 246 seconds) |
| 2021-07-14 17:54:05 | <monochrom> | Yes. A "if it terminates" premise. |
| 2021-07-14 17:54:06 | × | pfurla quits (~pfurla@216.131.82.58) (Ping timeout: 268 seconds) |
| 2021-07-14 17:54:27 | × | ubikium quits (~ubikium@113x43x248x70.ap113.ftth.arteria-hikari.net) (Client Quit) |
| 2021-07-14 17:56:26 | <monochrom> | Meta-ly, I have not read Milewski's book closely, I do not know whether he actually wrote that. |
| 2021-07-14 17:57:02 | → | merijn joins (~merijn@83-160-49-249.ip.xs4all.nl) |
| 2021-07-14 17:57:46 | × | Atum_ quits (IRC@user/atum/x-2392232) (Quit: Atum_) |
| 2021-07-14 18:01:17 | → | Atum_ joins (IRC@user/atum/x-2392232) |
| 2021-07-14 18:01:31 | × | chris_ quits (~chris@81.96.113.213) (Remote host closed the connection) |
| 2021-07-14 18:02:00 | × | Obo quits (~roberto@70.pool90-171-81.dynamic.orange.es) (Ping timeout: 258 seconds) |
| 2021-07-14 18:02:51 | × | Kaiepi quits (~Kaiepi@nwcsnbsc03w-47-54-173-93.dhcp-dynamic.fibreop.nb.bellaliant.net) (Remote host closed the connection) |
| 2021-07-14 18:03:13 | × | euandreh quits (~euandreh@2804:14c:33:9fe5:50a8:9802:856c:54ce) (Quit: WeeChat 3.2) |
| 2021-07-14 18:03:54 | → | Kaiepi joins (~Kaiepi@nwcsnbsc03w-47-54-173-93.dhcp-dynamic.fibreop.nb.bellaliant.net) |
| 2021-07-14 18:05:35 | × | haykam1 quits (~haykam@static.100.2.21.65.clients.your-server.de) (Remote host closed the connection) |
| 2021-07-14 18:05:48 | → | haykam2 joins (~haykam@static.100.2.21.65.clients.your-server.de) |
| 2021-07-14 18:06:34 | × | Kaiepi quits (~Kaiepi@nwcsnbsc03w-47-54-173-93.dhcp-dynamic.fibreop.nb.bellaliant.net) (Remote host closed the connection) |
| 2021-07-14 18:06:56 | → | Kaiepi joins (~Kaiepi@nwcsnbsc03w-47-54-173-93.dhcp-dynamic.fibreop.nb.bellaliant.net) |
| 2021-07-14 18:07:21 | × | MidAutumnMoon9 quits (~MidAutumn@user/midautumnmoon) (Ping timeout: 255 seconds) |
| 2021-07-14 18:11:35 | × | cheater quits (~Username@user/cheater) (Ping timeout: 255 seconds) |
| 2021-07-14 18:12:07 | → | cheater joins (~Username@user/cheater) |
| 2021-07-14 18:12:27 | <davean> | monochrom: they're not valid in the sense they're based on unsafePerformIO, unsafeCoerce, and prim-ops without axinomial specifications |
| 2021-07-14 18:12:56 | <davean> | 'base' is unbased, they have to be the axioms |
| 2021-07-14 18:13:11 | → | chris_ joins (~chris@81.96.113.213) |
| 2021-07-14 18:14:19 | → | MidAutumnMoon9 joins (~MidAutumn@user/midautumnmoon) |
| 2021-07-14 18:18:18 | × | hexreel quits (~hr@69.233.98.238) (Quit: nyaa~) |
| 2021-07-14 18:20:05 | → | Obo joins (~roberto@70.pool90-171-81.dynamic.orange.es) |
| 2021-07-14 18:22:04 | × | Vajb quits (~Vajb@2001:999:62:1d53:26b1:6c9b:c1ed:9c01) (Read error: Connection reset by peer) |
| 2021-07-14 18:22:50 | → | Vajb joins (~Vajb@hag-jnsbng11-58c3a1-224.dhcp.inet.fi) |
| 2021-07-14 18:23:44 | × | epolanski quits (uid312403@id-312403.brockwell.irccloud.com) (Quit: Connection closed for inactivity) |
| 2021-07-14 18:24:42 | → | shapr joins (~user@pool-100-36-247-68.washdc.fios.verizon.net) |
| 2021-07-14 18:25:17 | × | ptrcmd quits (~ptrcmd@user/ptrcmd) (Quit: leaving) |
| 2021-07-14 18:25:47 | × | o1lo01ol1o quits (~o1lo01ol1@bl11-109-140.dsl.telepac.pt) (Remote host closed the connection) |
| 2021-07-14 18:26:44 | → | cheater1__ joins (~Username@user/cheater) |
| 2021-07-14 18:26:45 | <tomsmeding> | it's quite based! Indeed, it's based on Falso http://sigtbd.csail.mit.edu/pubs/2016/paper9.pdf |
| 2021-07-14 18:26:54 | × | cheater quits (~Username@user/cheater) (Ping timeout: 272 seconds) |
| 2021-07-14 18:26:57 | cheater1__ | is now known as cheater |
| 2021-07-14 18:30:33 | × | jneira_ quits (~jneira_@28.red-80-28-169.staticip.rima-tde.net) (Quit: Connection closed) |
| 2021-07-14 18:31:43 | × | merijn quits (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 268 seconds) |
| 2021-07-14 18:33:06 | × | myShoggoth quits (~myShoggot@97-120-70-214.ptld.qwest.net) (Ping timeout: 252 seconds) |
| 2021-07-14 18:35:25 | → | myShoggoth joins (~myShoggot@97-120-70-214.ptld.qwest.net) |
| 2021-07-14 18:42:06 | × | myShoggoth quits (~myShoggot@97-120-70-214.ptld.qwest.net) (Ping timeout: 272 seconds) |
| 2021-07-14 18:42:28 | → | myShoggoth joins (~myShoggot@97-120-70-214.ptld.qwest.net) |
| 2021-07-14 18:47:41 | → | jolly joins (~jolly@208.180.97.158) |
| 2021-07-14 18:49:00 | × | Guest27 quits (~Guest27@187.83.249.216.dyn.smithville.net) (Quit: Client closed) |
| 2021-07-14 18:53:09 | → | burnsidesLlama joins (~burnsides@dhcp168-025.wadham.ox.ac.uk) |
| 2021-07-14 19:03:22 | × | myShoggoth quits (~myShoggot@97-120-70-214.ptld.qwest.net) (Read error: Connection reset by peer) |
| 2021-07-14 19:03:36 | → | o1lo01ol1o joins (~o1lo01ol1@bl11-109-140.dsl.telepac.pt) |
| 2021-07-14 19:03:46 | → | myShoggoth joins (~myShoggot@97-120-70-214.ptld.qwest.net) |
| 2021-07-14 19:06:02 | × | prite quits (~pritam@user/pritambaral) (Ping timeout: 255 seconds) |
| 2021-07-14 19:06:46 | <burnsidesLlama> | Hi, I'm thinking about a general definition for 'partial sums' on [a], which is a family of functions of type [a] -> [b], generalising functions such as [1,2,3] -> [0, 0+1, 0+1+2, 0+1+2+3]. The idea I'm following writing partial sums as "foldr f e . tails" or "foldr f e . inits", depending on the 'direction' of summation. I asked the question 'which choice is more natural? inits or tails?' and it seems the answer i |
| 2021-07-14 19:06:46 | <burnsidesLlama> | s that they are both natural, and in some sense 'dual' to each other. The most precise I have made this is that "forall xs :: [a], zipWith (++) (inits xs) (tails xs) = repeat xs". Is there a rigorous notion of duality here? Are there other places where a similar idea of duality shows up? I am new to irc, please let me know if I've done something inappropriate. |
| 2021-07-14 19:07:29 | → | koolazer joins (~koo@user/koolazer) |
| 2021-07-14 19:08:01 | → | falafel joins (~falafel@pool-96-255-70-50.washdc.fios.verizon.net) |
| 2021-07-14 19:08:14 | × | o1lo01ol1o quits (~o1lo01ol1@bl11-109-140.dsl.telepac.pt) (Ping timeout: 265 seconds) |
| 2021-07-14 19:09:26 | <dminuoso> | burnsidesLlama: Shouldn't those definitions rather be some `fmap (foldr f e) . tails` or `fmap (foldr f e) . inits` ? |
| 2021-07-14 19:09:42 | × | qbt quits (~edun@user/edun) (Quit: WeeChat 3.2) |
All times are in UTC.