Logs: freenode/#haskell
| 2021-04-28 07:29:19 | × | ericsagn1 quits (~ericsagne@2405:6580:0:5100:4233:4fa2:ecc4:e3d1) (Ping timeout: 276 seconds) |
| 2021-04-28 07:29:24 | <letmein> | if it were, then haskell wouldn't be turing complete, assuming i understand the question correctly |
| 2021-04-28 07:29:47 | <maerwald> | ? |
| 2021-04-28 07:30:06 | <maerwald> | expressing totality /= everything must be total |
| 2021-04-28 07:30:23 | <olle> | Right |
| 2021-04-28 07:30:25 | <olle> | opqdonut: thanks |
| 2021-04-28 07:30:35 | → | fendor joins (~fendor@178.165.130.176.wireless.dyn.drei.com) |
| 2021-04-28 07:30:38 | <maerwald> | F* can express totality |
| 2021-04-28 07:30:45 | <olle> | As can Koka, in fact. |
| 2021-04-28 07:30:53 | <maerwald> | liquidhaskell too |
| 2021-04-28 07:31:05 | <letmein> | ah ok. my bad |
| 2021-04-28 07:31:07 | <maerwald> | to some degree I think |
| 2021-04-28 07:32:16 | × | zmijunkie quits (~Adium@109.90.32.89) (Ping timeout: 252 seconds) |
| 2021-04-28 07:32:39 | → | zmijunkie joins (~Adium@87.122.222.152) |
| 2021-04-28 07:33:18 | → | kuribas joins (~user@ptr-25vy0i8klmekwkijd9o.18120a2.ip6.access.telenet.be) |
| 2021-04-28 07:33:48 | → | cfricke joins (~cfricke@unaffiliated/cfricke) |
| 2021-04-28 07:34:32 | <olle> | Is there another word for "weak" totality, when it's guaranteed to act on all of the domain? |
| 2021-04-28 07:34:40 | <olle> | E.g. not missing a case |
| 2021-04-28 07:34:54 | → | lordyod joins (~lordyod@c-67-169-144-132.hsd1.ca.comcast.net) |
| 2021-04-28 07:35:13 | <opqdonut> | isn't that just totality? at least if "to act on" means "to terminate" |
| 2021-04-28 07:35:21 | <opqdonut> | or what do you mean? |
| 2021-04-28 07:36:27 | → | hiroaki joins (~hiroaki@2a02:8108:8c40:2bb8:a736:199e:991f:4edb) |
| 2021-04-28 07:37:12 | <olle> | opqdonut: You can have a function that acts on all cases, but one case throws an exception --> no totality |
| 2021-04-28 07:37:58 | <opqdonut> | how's that different from a non-total function that throws an exception on one case? |
| 2021-04-28 07:38:22 | <opqdonut> | or perhaps you mean something like "guaranteed to terminate with a value or an exception" |
| 2021-04-28 07:38:32 | <opqdonut> | that's perhaps even harder to track in a compiler than normal totality |
| 2021-04-28 07:38:49 | <olle> | Instead of totality, something like "no case missed" |
| 2021-04-28 07:39:10 | <opqdonut> | what I'm trying to say is how can you distinguish a "missed case" from some other reason for nontotality? |
| 2021-04-28 07:39:18 | <opqdonut> | arguably every nontotal function merely "misses a case" |
| 2021-04-28 07:39:21 | <olle> | Good question |
| 2021-04-28 07:40:16 | → | jgt joins (~jgt@95.12.112.152) |
| 2021-04-28 07:41:01 | × | stree quits (~stree@68.36.8.116) (Ping timeout: 276 seconds) |
| 2021-04-28 07:41:16 | → | ericsagn1 joins (~ericsagne@2405:6580:0:5100:b546:5594:c630:5696) |
| 2021-04-28 07:41:52 | → | ddellacosta joins (ddellacost@gateway/vpn/mullvad/ddellacosta) |
| 2021-04-28 07:41:53 | <maerwald> | GHC warns you if you're not matching on a value |
| 2021-04-28 07:42:23 | <maerwald> | that says nothing about whether the function terminates |
| 2021-04-28 07:42:42 | <opqdonut> | yeah, and it's only a local check |
| 2021-04-28 07:42:55 | <opqdonut> | calling head doesn't generate a warning :) |
| 2021-04-28 07:43:13 | <curiousgay> | I need help identifying which part of code for boggle https://pastebin.com/raw/yxC9Wvzm is really slow, I was sure lazy evaluation would take care of that (that terrible naming of findWord is not mine) |
| 2021-04-28 07:45:18 | <olle> | maerwald: right, you have this check. |
| 2021-04-28 07:45:58 | <olle> | maerwald: what do you call it? exhaustiveness? |
| 2021-04-28 07:46:06 | <olle> | so maybe that's the word to use, not "totality" |
| 2021-04-28 07:46:13 | <curiousgay> | I should be more concrete that's just the code for checking whether the word is on board or not |
| 2021-04-28 07:46:39 | × | ddellacosta quits (ddellacost@gateway/vpn/mullvad/ddellacosta) (Ping timeout: 265 seconds) |
| 2021-04-28 07:48:22 | <curiousgay> | maybe I'll solve that myself after taking a sleep... |
| 2021-04-28 07:48:29 | × | cgfbee quits (~bot@oc1.itim-cj.ro) (Remote host closed the connection) |
| 2021-04-28 07:50:23 | → | geowiesnot joins (~user@i15-les02-ix2-87-89-181-157.sfr.lns.abo.bbox.fr) |
| 2021-04-28 07:50:27 | → | Gurkenglas joins (~Gurkengla@unaffiliated/gurkenglas) |
| 2021-04-28 07:51:11 | <maerwald> | olle: yes, exhaustiveness |
| 2021-04-28 07:51:58 | <olle> | So you can say a function is exhaustive on its input...? Or is that weird wording? |
| 2021-04-28 07:52:05 | <olle> | Instead of total. |
| 2021-04-28 07:53:56 | → | stree joins (~stree@68.36.8.116) |
| 2021-04-28 07:55:04 | → | gehmehgeh joins (~ircuser1@gateway/tor-sasl/gehmehgeh) |
| 2021-04-28 07:58:13 | × | remby quits (~remby@bras-base-london1483w-grc-43-65-95-173-128.dsl.bell.ca) (Quit: remby) |
| 2021-04-28 07:58:57 | × | cole-h quits (~cole-h@c-73-48-197-220.hsd1.ca.comcast.net) (Ping timeout: 260 seconds) |
| 2021-04-28 08:01:03 | × | dvdp73 quits (59736826@38.104.115.89.rev.vodafone.pt) (Ping timeout: 240 seconds) |
| 2021-04-28 08:01:36 | × | evanjs quits (~evanjs@075-129-098-007.res.spectrum.com) (Read error: Connection reset by peer) |
| 2021-04-28 08:03:43 | → | evanjs joins (~evanjs@075-129-098-007.res.spectrum.com) |
| 2021-04-28 08:05:31 | → | Guest6509 joins (~laudiacay@45.162.228.190) |
| 2021-04-28 08:06:43 | × | kini quits (~kini@unaffiliated/kini) (Ping timeout: 258 seconds) |
| 2021-04-28 08:07:13 | → | Qwerky joins (~qwerky@37.170.48.251) |
| 2021-04-28 08:07:24 | × | xkapastel quits (uid17782@gateway/web/irccloud.com/x-wfrommuaxtjqnxrn) (Quit: Connection closed for inactivity) |
| 2021-04-28 08:09:47 | × | Guest6509 quits (~laudiacay@45.162.228.190) (Ping timeout: 246 seconds) |
| 2021-04-28 08:11:19 | × | letmein quits (~letmein@2601:1c1:4200:938f:f8bf:6a67:4eed:b2c1) (Ping timeout: 260 seconds) |
| 2021-04-28 08:12:31 | × | gitgood quits (~gitgood@80-44-9-246.dynamic.dsl.as9105.com) (Remote host closed the connection) |
| 2021-04-28 08:13:45 | <hc> | exhaustive is the proper term for it, I think |
| 2021-04-28 08:14:02 | <nshepperd2> | i think exhaustiveness is more a property of source code than functions |
| 2021-04-28 08:14:32 | → | kini joins (~kini@unaffiliated/kini) |
| 2021-04-28 08:15:49 | <nshepperd2> | if you have a function that has one case defined as 'undefined' that's semantically the same as a function with the case left out, it just indicates that the programmer did it on purpose |
| 2021-04-28 08:16:45 | × | hendursaga quits (~weechat@gateway/tor-sasl/hendursaga) (Ping timeout: 240 seconds) |
| 2021-04-28 08:17:58 | → | kritzefitz joins (~kritzefit@p200300ecdf3c5b009ca7d9f9eb7bbe17.dip0.t-ipconnect.de) |
| 2021-04-28 08:18:04 | × | geowiesnot quits (~user@i15-les02-ix2-87-89-181-157.sfr.lns.abo.bbox.fr) (Ping timeout: 276 seconds) |
| 2021-04-28 08:18:53 | → | hendursaga joins (~weechat@gateway/tor-sasl/hendursaga) |
| 2021-04-28 08:19:37 | → | m0rphism joins (~m0rphism@HSI-KBW-085-216-104-059.hsi.kabelbw.de) |
| 2021-04-28 08:21:08 | → | elfets joins (~elfets@ip-37-201-23-96.hsi13.unitymediagroup.de) |
| 2021-04-28 08:21:54 | → | ddellacosta joins (~ddellacos@83.143.246.104) |
| 2021-04-28 08:22:21 | → | zmijunkie1 joins (~Adium@109.90.32.89) |
| 2021-04-28 08:23:26 | × | zmijunkie quits (~Adium@87.122.222.152) (Ping timeout: 246 seconds) |
| 2021-04-28 08:24:53 | × | tzh quits (~tzh@c-24-21-73-154.hsd1.or.comcast.net) (Quit: zzz) |
| 2021-04-28 08:25:23 | → | knupfer joins (~Thunderbi@p200300eb4f122d00ac387efffe7e3251.dip0.t-ipconnect.de) |
| 2021-04-28 08:25:52 | × | kritzefitz quits (~kritzefit@p200300ecdf3c5b009ca7d9f9eb7bbe17.dip0.t-ipconnect.de) (Ping timeout: 276 seconds) |
| 2021-04-28 08:26:46 | × | ddellacosta quits (~ddellacos@83.143.246.104) (Ping timeout: 265 seconds) |
| 2021-04-28 08:27:49 | → | cgfbee joins (~bot@oc1.itim-cj.ro) |
| 2021-04-28 08:29:49 | × | kiweun quits (~kiweun@2607:fea8:2a62:9600:d524:f52b:e28c:9800) (Remote host closed the connection) |
| 2021-04-28 08:31:59 | × | knupfer quits (~Thunderbi@p200300eb4f122d00ac387efffe7e3251.dip0.t-ipconnect.de) (Quit: knupfer) |
| 2021-04-28 08:32:03 | → | alexander joins (~alexander@2a02:587:dc0a:2700:39fb:67a3:1f47:16d) |
| 2021-04-28 08:32:06 | → | knupfer joins (~Thunderbi@p200300eb4f122d00a42a28fffee81920.dip0.t-ipconnect.de) |
| 2021-04-28 08:32:32 | alexander | is now known as Guest78265 |
| 2021-04-28 08:37:40 | → | kritzefitz joins (~kritzefit@2003:5b:203b:200::10:49) |
| 2021-04-28 08:37:53 | → | raehik joins (~raehik@cpc95906-rdng25-2-0-cust156.15-3.cable.virginm.net) |
| 2021-04-28 08:38:53 | × | knupfer quits (~Thunderbi@p200300eb4f122d00a42a28fffee81920.dip0.t-ipconnect.de) (Quit: knupfer) |
| 2021-04-28 08:41:12 | × | PotatoHatsue quits (berbermanp@gateway/shell/matrix.org/x-cdgorrungfkvrlgk) (Quit: Bridge terminating on SIGTERM) |
| 2021-04-28 08:41:12 | × | johnnyboy[m] quits (gifumatrix@gateway/shell/matrix.org/x-hshpzcnkjnouscdq) (Quit: Bridge terminating on SIGTERM) |
| 2021-04-28 08:41:13 | × | ThaEwat quits (thaewraptm@gateway/shell/matrix.org/x-zrjvdaqjldoozbwe) (Quit: Bridge terminating on SIGTERM) |
| 2021-04-28 08:41:13 | × | sm[m] quits (simonmicma@gateway/shell/matrix.org/x-ebojkellpovkslxj) (Quit: Bridge terminating on SIGTERM) |
| 2021-04-28 08:41:13 | × | fgaz quits (fgazmatrix@gateway/shell/matrix.org/x-rybmlciotqdjbwga) (Quit: Bridge terminating on SIGTERM) |
| 2021-04-28 08:41:13 | × | JaakkoLuttinen[m quits (jluttinema@gateway/shell/matrix.org/x-iaezgisjxqykbikb) (Quit: Bridge terminating on SIGTERM) |
| 2021-04-28 08:41:14 | × | lambdaclan quits (lambdaclan@gateway/shell/matrix.org/x-srvssvttdughpnin) (Quit: Bridge terminating on SIGTERM) |
| 2021-04-28 08:41:14 | × | jtojnar quits (jtojnarmat@gateway/shell/matrix.org/x-uzcjomjncllflthl) (Quit: Bridge terminating on SIGTERM) |
| 2021-04-28 08:41:15 | × | jeffcasavant[m] quits (jeffcasava@gateway/shell/matrix.org/x-implyphghwvbpqxc) (Quit: Bridge terminating on SIGTERM) |
All times are in UTC.