Logs: freenode/#haskell
| 2021-03-29 18:37:53 | <ski> | @where topology |
| 2021-03-29 18:37:53 | <lambdabot> | "topology in Haskell" <http://www.haskell.org/pipermail/haskell/2004-June/014134.html> and "Synthetic topology of data types and classical spaces" <http://www.cs.bham.ac.uk/~mhe/papers/entcs87.(pdf| |
| 2021-03-29 18:37:53 | <lambdabot> | dvi|ps)> by Mart�n Escard� |
| 2021-03-29 18:37:54 | × | stree quits (~stree@68.36.8.116) (Quit: Caught exception) |
| 2021-03-29 18:37:59 | <ski> | Gurkenglas ^ |
| 2021-03-29 18:38:01 | <ski> | also |
| 2021-03-29 18:38:02 | × | star_cloud quits (~star_clou@ec2-34-220-44-120.us-west-2.compute.amazonaws.com) (Read error: Connection reset by peer) |
| 2021-03-29 18:38:05 | × | heatsink quits (~heatsink@2600:1700:bef1:5e10:f0bc:f236:90c7:a6f5) (Remote host closed the connection) |
| 2021-03-29 18:38:06 | <ski> | @where impossible |
| 2021-03-29 18:38:06 | <lambdabot> | <http://math.andrej.com/2007/09/28/seemingly-impossible-functional-programs/>,<http://math.andrej.com/2008/11/21/a-haskell-monad-for-infinite-search-in-finite-time/> |
| 2021-03-29 18:38:21 | → | star_cloud joins (~star_clou@ec2-34-220-44-120.us-west-2.compute.amazonaws.com) |
| 2021-03-29 18:38:23 | → | stree joins (~stree@68.36.8.116) |
| 2021-03-29 18:38:28 | × | royal_screwup21 quits (52254809@gateway/web/cgi-irc/kiwiirc.com/ip.82.37.72.9) (Quit: Connection closed) |
| 2021-03-29 18:38:48 | → | royal_screwup21 joins (52254809@gateway/web/cgi-irc/kiwiirc.com/ip.82.37.72.9) |
| 2021-03-29 18:39:16 | → | pera joins (~pera@unaffiliated/pera) |
| 2021-03-29 18:39:29 | <ski> | Gurkenglas : and the paper by Andrej Bauer i linked to, one and a half hour ago |
| 2021-03-29 18:41:27 | <dolio> | Anyhow, there are many sorts of truth values computably. There is 2, for decidable truth, Σ for semi-decidable truth, and Ω for provable truth. |
| 2021-03-29 18:41:43 | × | darjeeling_ quits (~darjeelin@115.215.42.89) (Ping timeout: 265 seconds) |
| 2021-03-29 18:42:02 | <dolio> | Also perhaps ∇Ω for classical truth. |
| 2021-03-29 18:42:38 | <infinisil> | Okay I'm bringing out the big guns, type families |
| 2021-03-29 18:42:50 | <infinisil> | data Method = IsRoot | GetName |
| 2021-03-29 18:43:17 | <infinisil> | type family MethodInput (m :: Method) where MethodInput IsRoot = Int MethodInput GetName = Int |
| 2021-03-29 18:43:23 | <infinisil> | Similarly for MethodOutput |
| 2021-03-29 18:43:26 | × | ystael quits (~ystael@209.6.50.55) (Ping timeout: 240 seconds) |
| 2021-03-29 18:43:29 | × | royal_screwup21 quits (52254809@gateway/web/cgi-irc/kiwiirc.com/ip.82.37.72.9) (Ping timeout: 246 seconds) |
| 2021-03-29 18:43:34 | <dolio> | Domain theoretic semantics of something like Haskell allow you to encode some of the Σ part as procedures, but it doesn't have a good story for the rest. |
| 2021-03-29 18:43:36 | <infinisil> | This feels like a step in the right direction |
| 2021-03-29 18:43:39 | <infinisil> | tomsmeding: ^ |
| 2021-03-29 18:43:41 | <ski> | "How many is two?" by ibid in 2005-05-16 at <http://math.andrej.com/2005/05/16/how-many-is-two/> could also be interesting, yea |
| 2021-03-29 18:43:58 | × | pera quits (~pera@unaffiliated/pera) (Ping timeout: 240 seconds) |
| 2021-03-29 18:45:36 | × | slack1256 quits (~slack1256@dvc-186-186-101-190.movil.vtr.net) (Remote host closed the connection) |
| 2021-03-29 18:47:50 | → | shailangsa joins (~shailangs@host86-186-196-238.range86-186.btcentralplus.com) |
| 2021-03-29 18:48:07 | × | star_cloud quits (~star_clou@ec2-34-220-44-120.us-west-2.compute.amazonaws.com) (Excess Flood) |
| 2021-03-29 18:49:28 | → | star_cloud joins (~star_clou@ec2-34-220-44-120.us-west-2.compute.amazonaws.com) |
| 2021-03-29 18:49:47 | <tomsmeding> | infinisil: if it works, it works, but I don't see yet how to get the Show constraints in the right place that way; but I haven't thought about it much either :) |
| 2021-03-29 18:51:56 | → | Guest29 joins (~textual@109.246.40.24) |
| 2021-03-29 18:53:47 | × | ddellaco_ quits (~ddellacos@ool-44c73afa.dyn.optonline.net) (Remote host closed the connection) |
| 2021-03-29 18:54:07 | <monochrom> | ski: There is a Chinese novel that has this plot point of how a villain aquitted himself of a promise of "I won't tell this secret to the 5th person". So eventually he told the secret to a conference of a hundred people, and defended with "can you point out who's the 5th person?" >:) |
| 2021-03-29 18:54:34 | → | darjeeling_ joins (~darjeelin@122.245.122.120) |
| 2021-03-29 18:54:52 | <ski> | hm |
| 2021-03-29 18:55:08 | <monochrom> | (The number was 5 because initially this was a secret among 4 persons.) |
| 2021-03-29 18:55:27 | <ski> | i see |
| 2021-03-29 18:55:28 | × | atk quits (~Arch-TK@ircpuzzles/staff/Arch-TK) (Quit: Well this is unexpected.) |
| 2021-03-29 18:56:16 | <monochrom> | Conclusion: Intuitionistic constructivist logics are the root of all evil. >:) |
| 2021-03-29 18:56:30 | <ski> | slightly apropos, i always found it weird, how apparently, at least in some jurisdictions, two people who've helped each other to commit a crime, can both be acquitted by the court, on the grounds that it can't be determined "who held the knife" (or whatever) |
| 2021-03-29 18:57:07 | → | ph88 joins (~ph88@2a02:8109:9e00:7e5c:4080:7dc1:315d:729) |
| 2021-03-29 18:57:12 | <justsomeguy> | It seems like hackage is down. Is there a way for me to generate local documentation for QuickCheck with stack? |
| 2021-03-29 18:57:42 | <ski> | it always seemed to me that, at least in common cases, it ought to be possible to charge and convict both of them of commiting either of the two deeds, and, serving out the greatest lower bound of the two associated penances, to both of them |
| 2021-03-29 18:58:24 | → | ByteEater joins (57cd846a@gateway/web/cgi-irc/kiwiirc.com/ip.87.205.132.106) |
| 2021-03-29 18:58:28 | <ski> | hehe, monochrom ;) |
| 2021-03-29 18:59:13 | <monochrom> | Generally it looks like that if you put the burden of proof on one side you are bound to have this kind of asymmetries. |
| 2021-03-29 19:00:08 | <dolio> | You can easily well-order finite sets, though. :) |
| 2021-03-29 19:00:14 | → | atk joins (~Arch-TK@ircpuzzles/staff/Arch-TK) |
| 2021-03-29 19:00:20 | <dolio> | Even intuitionistically. |
| 2021-03-29 19:02:49 | <ski> | monochrom : iow, not "Either you committed this crime, or you committed that crime." but rather "You committed either this crime or that crime.". convicting both of them for the disjunction of the crimes |
| 2021-03-29 19:03:15 | <monochrom> | The story was set in 11th century China, and the conference was of the martial art community. So unfortunately most of them were easily bluffed by these logical subtleties, apart from a few exceptional smartass villains. |
| 2021-03-29 19:03:37 | <justsomeguy> | Seems that ''stack haddock'' was able to generate the html docs I was after. |
| 2021-03-29 19:03:48 | → | heatsink joins (~heatsink@2600:1700:bef1:5e10:a5da:1e25:ab26:50f2) |
| 2021-03-29 19:05:03 | × | justsomeguy quits (~justsomeg@unaffiliated/--/x-3805311) (Quit: WeeChat 3.0.1) |
| 2021-03-29 19:05:35 | <monochrom> | ski: Hey, how about this idea: Order the formation of a company of those two persons. Now there is just one legal person, the company, to convict. Then the sole two shareholders take the common punishment. |
| 2021-03-29 19:06:21 | <monochrom> | "homotopic criminal theory" >:) |
| 2021-03-29 19:07:24 | <ski> | monochrom : hm. around when was it written ? |
| 2021-03-29 19:07:41 | <monochrom> | 1960s or 1970s. |
| 2021-03-29 19:07:49 | <ski> | monochrom : hehe :) .. could a court really order such a formation ? |
| 2021-03-29 19:07:50 | <ski> | okay |
| 2021-03-29 19:08:18 | <ski> | (also, wouldn't that legal person have had to existed, at the time in question for the deed ?) |
| 2021-03-29 19:08:35 | → | ddellacosta joins (~ddellacos@ool-44c73afa.dyn.optonline.net) |
| 2021-03-29 19:08:52 | <monochrom> | Just another cunning plan from monochrom that doesn't really work in practice. :) |
| 2021-03-29 19:09:52 | → | ystael joins (~ystael@141.sub-174-242-80.myvzw.com) |
| 2021-03-29 19:10:05 | × | idhugo__ quits (~idhugo@87-49-147-45-mobile.dk.customer.tdc.net) (Remote host closed the connection) |
| 2021-03-29 19:10:24 | × | Erutuon_ quits (~Erutuon@97-116-16-233.mpls.qwest.net) (Ping timeout: 246 seconds) |
| 2021-03-29 19:12:37 | → | Erutuon_ joins (~Erutuon@97-116-16-233.mpls.qwest.net) |
| 2021-03-29 19:13:43 | ski | . o O ( "I have a cunning plan" <https://www.youtube.com/watch?v=AsXKS8Nyu8Q> ) |
| 2021-03-29 19:15:32 | × | heatsink quits (~heatsink@2600:1700:bef1:5e10:a5da:1e25:ab26:50f2) (Remote host closed the connection) |
| 2021-03-29 19:17:33 | → | Vadrigar_ joins (~Vadrigar@ip5b417208.dynamic.kabel-deutschland.de) |
| 2021-03-29 19:19:13 | → | sorki joins (~sorki@gateway/tor-sasl/sorki) |
| 2021-03-29 19:19:33 | → | hacxman joins (~hexo@gateway/tor-sasl/hexo) |
| 2021-03-29 19:19:57 | × | srk quits (~sorki@gateway/tor-sasl/sorki) (Ping timeout: 240 seconds) |
| 2021-03-29 19:19:57 | × | hexo quits (~hexo@gateway/tor-sasl/hexo) (Ping timeout: 240 seconds) |
| 2021-03-29 19:19:58 | hacxman | is now known as hexo |
| 2021-03-29 19:20:17 | → | woffs joins (3cd46299b2@woffs.de) |
| 2021-03-29 19:20:25 | × | ddellacosta quits (~ddellacos@ool-44c73afa.dyn.optonline.net) (Remote host closed the connection) |
| 2021-03-29 19:20:56 | × | wroathe quits (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) (Ping timeout: 268 seconds) |
| 2021-03-29 19:21:02 | → | ddellaco_ joins (~ddellacos@ool-44c73afa.dyn.optonline.net) |
| 2021-03-29 19:21:38 | × | Vadrigar_ quits (~Vadrigar@ip5b417208.dynamic.kabel-deutschland.de) (Ping timeout: 240 seconds) |
| 2021-03-29 19:21:59 | × | ddellaco_ quits (~ddellacos@ool-44c73afa.dyn.optonline.net) (Remote host closed the connection) |
| 2021-03-29 19:22:08 | <wz1000> | is there any nice way to define folds with unboxed result types? |
| 2021-03-29 19:22:16 | → | ddellaco_ joins (~ddellacos@ool-44c73afa.dyn.optonline.net) |
| 2021-03-29 19:22:23 | sorki | is now known as srk |
| 2021-03-29 19:22:26 | <wz1000> | I want something like `foldl :: forall r a (b :: TYPE r). (b -> a -> b) -> b -> [a] -> b` |
| 2021-03-29 19:22:34 | ← | woffs parts (3cd46299b2@woffs.de) () |
| 2021-03-29 19:22:57 | <wz1000> | s/unboxed result types/levity polymorphic result types/g |
| 2021-03-29 19:24:12 | <wz1000> | This is my best attempt so far: https://gist.github.com/wz1000/2dee93d3b07825d1ae43cf43012adcc0 |
| 2021-03-29 19:24:44 | <wz1000> | it works fine for "simple" RuntimeReps, but breaks down for anything more compilicated involving unboxed tuples/sums etc. |
| 2021-03-29 19:25:02 | <wz1000> | edwardk maybe? |
| 2021-03-29 19:27:11 | × | michalz quits (~user@185.246.204.46) (Ping timeout: 240 seconds) |
| 2021-03-29 19:27:26 | → | hidedagger joins (~nate@unaffiliated/hidedagger) |
| 2021-03-29 19:33:51 | → | wroathe joins (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) |
| 2021-03-29 19:34:07 | × | cfricke quits (~cfricke@unaffiliated/cfricke) (Quit: WeeChat 3.1) |
| 2021-03-29 19:39:05 | × | electricityZZZZ quits (~electrici@135-180-3-82.static.sonic.net) (Quit: Leaving) |
All times are in UTC.