Logs: freenode/#haskell
| 2021-03-23 19:40:29 | <monochrom> | So here is what I think dolio referred to as "type directed" and I take it and go big. |
| 2021-03-23 19:40:42 | <monochrom> | We have negate :: Num a => a -> a |
| 2021-03-23 19:41:02 | × | DavidEichmann quits (~david@47.27.93.209.dyn.plus.net) (Remote host closed the connection) |
| 2021-03-23 19:41:25 | <monochrom> | So what does "seq negate ()" mean? Does it mean "seq (negate @ Int) ()"? Does it mean "seq (negate @ MonochromsSecretNumInstance) ()"? |
| 2021-03-23 19:41:42 | × | ClaudiusMaximus quits (~claude@unaffiliated/claudiusmaximus) (Quit: ->) |
| 2021-03-23 19:41:43 | × | electricityZZZZ quits (~electrici@135-180-3-82.static.sonic.net) (Quit: Leaving) |
| 2021-03-23 19:41:43 | <monochrom> | Answer: "Ambiguous type variable a0 in ..." |
| 2021-03-23 19:41:50 | <Gurkenglas> | i agree |
| 2021-03-23 19:42:01 | <monochrom> | Meta-Answer: Why would it bother? I call XY Problem. |
| 2021-03-23 19:42:02 | → | heatsink joins (~heatsink@2600:1700:bef1:5e10:b09b:3609:dd4b:42c9) |
| 2021-03-23 19:42:16 | <Gurkenglas> | you mean, nobody would actually want to seq negate ()? |
| 2021-03-23 19:42:51 | <monochrom> | I mean the feature you're wanting is both half-baked and an XY problem. |
| 2021-03-23 19:42:57 | × | atraii quits (~atraii@2601:681:8700:c471:182c:49ac:c430:1f21) (Ping timeout: 268 seconds) |
| 2021-03-23 19:43:23 | × | Nahra quits (~Nahra@unaffiliated/nahra) (Ping timeout: 245 seconds) |
| 2021-03-23 19:43:34 | <Gurkenglas> | the X would be "giff Hask pls" |
| 2021-03-23 19:45:08 | <Gurkenglas> | or do you call that another Y |
| 2021-03-23 19:45:17 | <monochrom> | I think that to achieve Hask it is much simpler to just remove seq. |
| 2021-03-23 19:45:37 | → | Nahra joins (~Nahra@unaffiliated/nahra) |
| 2021-03-23 19:45:45 | × | jpds quits (~jpds@gateway/tor-sasl/jpds) (Remote host closed the connection) |
| 2021-03-23 19:45:56 | → | carlomagno joins (~cararell@148.87.23.5) |
| 2021-03-23 19:46:07 | → | jpds joins (~jpds@gateway/tor-sasl/jpds) |
| 2021-03-23 19:46:12 | × | kmein quits (~weechat@static.173.83.99.88.clients.your-server.de) (Quit: ciao kakao) |
| 2021-03-23 19:46:22 | → | wroathe joins (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) |
| 2021-03-23 19:46:31 | → | kmein joins (~weechat@static.173.83.99.88.clients.your-server.de) |
| 2021-03-23 19:47:23 | <Gurkenglas> | i like things like glb and lub though (glb a b = most defined value which is less defined than both of a and b; lub a b = least defined value which is more defined than both of a and b, if any such exist) |
| 2021-03-23 19:47:53 | × | raehik quits (~raehik@cpc95906-rdng25-2-0-cust156.15-3.cable.virginm.net) (Ping timeout: 268 seconds) |
| 2021-03-23 19:48:31 | <Gurkenglas> | not sure whether those require seq, but surely "\y -> if x is less defined than y then y else x" does |
| 2021-03-23 19:49:01 | <monochrom> | You can furthermore add back seq in a restricted, disciplined way by creating a class "class Seq a where seq :: a -> b -> b" so you can still have the niceness of foldl' but its type now has a Seq constraint. |
| 2021-03-23 19:50:00 | <monochrom> | This was actually the state of old Haskell versions. This means if you get your hands on a very old version of Hugs, it's actually an executable model of Hask that is highly faithful. |
| 2021-03-23 19:50:27 | <dolio> | Well, functions had an instance, though. |
| 2021-03-23 19:50:37 | <monochrom> | Ah damn. |
| 2021-03-23 19:50:38 | <dolio> | And it didn't do something undecidable. :) |
| 2021-03-23 19:51:17 | <monochrom> | Well, can always fork the source code and remove that. Hugs source code was and still is relatively simple. |
| 2021-03-23 19:52:08 | <Gurkenglas> | dolio, by undecidable do you mean seeing whether f touches its argument ⊥ without blowing up, or doing things depending on whether f is a function? |
| 2021-03-23 19:52:15 | → | Deide joins (~Deide@217.155.19.23) |
| 2021-03-23 19:52:23 | <monochrom> | But really if you are interested in Hask you don't need foldl' so you don't need seq so just remove it. |
| 2021-03-23 19:52:24 | → | kritzefitz joins (~kritzefit@212.86.56.80) |
| 2021-03-23 19:53:15 | <monochrom> | If you need it for one particular ADT, just write one specific function for that ADT. |
| 2021-03-23 19:53:15 | <Gurkenglas> | Why not want Hask and the ability to construct as many definedness-monotonic functions as possible? |
| 2021-03-23 19:53:39 | <dolio> | Testing if a function is point-wise bottom sounds undecidable. |
| 2021-03-23 19:53:58 | <dolio> | In general. |
| 2021-03-23 19:54:06 | <Gurkenglas> | dolio, what would require such a decision? |
| 2021-03-23 19:54:26 | <dolio> | The insistance that `⊥ = const ⊥` in domain theory. |
| 2021-03-23 19:54:46 | <monochrom> | I don't see how Hask itself doesn't already have many levels of definedness. |
| 2021-03-23 19:55:12 | <Gurkenglas> | dolio, how does this insistence require such a decision? |
| 2021-03-23 19:55:47 | <dolio> | Well, for one, your description of `seq` to begin this conversation was actually not what it is specified to do. You were changing the definition. |
| 2021-03-23 19:56:27 | <Gurkenglas> | dolio, sure, I was proposing a change of its behavior. One can do it the usual way and define a new term to work like I describe, then deprecate the old one over a bunch of years |
| 2021-03-23 19:56:29 | <dolio> | What it is specified to do is be ⊥ if its frist argument is ⊥, and equal to its second argument if its first argument is not ⊥. |
| 2021-03-23 19:56:59 | <dolio> | So, if you adhere to the domain theoretic notion of the function space, that requires determining if functions are point-wise ⊥. |
| 2021-03-23 19:58:03 | <Gurkenglas> | I see. I agree that seq as specified can't be implemented with ⊥ = const ⊥. |
| 2021-03-23 19:58:26 | × | frozenErebus quits (~frozenEre@94.128.81.87) (Ping timeout: 240 seconds) |
| 2021-03-23 19:59:04 | × | conal quits (~conal@64.71.133.70) (Quit: Computer has gone to sleep.) |
| 2021-03-23 19:59:10 | × | heatsink quits (~heatsink@2600:1700:bef1:5e10:b09b:3609:dd4b:42c9) (Remote host closed the connection) |
| 2021-03-23 19:59:33 | → | Noldorin joins (~noldorin@unaffiliated/noldorin) |
| 2021-03-23 20:00:02 | × | stree quits (~stree@68.36.8.116) (Ping timeout: 260 seconds) |
| 2021-03-23 20:00:08 | <dolio> | It might actually be implementable, but so expensive that it would be completely unusable. |
| 2021-03-23 20:00:37 | → | merijn joins (~merijn@83-160-49-249.ip.xs4all.nl) |
| 2021-03-23 20:00:41 | <dolio> | Because it needs to run the function on all possible inputs in parallel and see if any finish. |
| 2021-03-23 20:01:31 | <Gurkenglas> | i suppose it depends on whether we say it has to check all terms or all values - there are uncountably large types to use for the input, after all |
| 2021-03-23 20:01:33 | <dolio> | I mean, the fact that it is a valid domain theoretic function means that you can implement it in principle. |
| 2021-03-23 20:01:54 | <sclv> | i would run it on all possible inputs in serial, but just do it faster |
| 2021-03-23 20:02:09 | <monochrom> | As usual, denotational semantics happily ignores costs. |
| 2021-03-23 20:02:24 | <sclv> | u just need a system clock indexed by an uncountable ordinal |
| 2021-03-23 20:02:34 | → | royal_screwup21 joins (52254809@gateway/web/cgi-irc/kiwiirc.com/ip.82.37.72.9) |
| 2021-03-23 20:02:35 | <dolio> | The models where this would work would be able to enumerate all possible values, because only the ones definable in the language count. |
| 2021-03-23 20:02:41 | × | wroathe quits (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) (Ping timeout: 256 seconds) |
| 2021-03-23 20:02:52 | → | Sathiana joins (~kath@185-113-98-38.cust.bredband2.com) |
| 2021-03-23 20:02:59 | <monochrom> | sclv, ever heard of functional reactive programming? >:) |
| 2021-03-23 20:03:11 | <dolio> | So, check all possible Haskell terms. |
| 2021-03-23 20:03:13 | <monochrom> | its time model is the continuum. |
| 2021-03-23 20:03:33 | <monochrom> | although, not sure how much it insist on the ordinal aspect. |
| 2021-03-23 20:03:42 | <sclv> | ok sorry i should have send higher uncountable ordinal |
| 2021-03-23 20:04:18 | <dolio> | Of course, those models are in some sense bad in their own ways. |
| 2021-03-23 20:04:56 | <Gurkenglas> | dolio, but aren't there uncountably many valid domain-theoretic functions so they can't all be implementable? |
| 2021-03-23 20:05:31 | → | smerdyakov joins (~dan@5.146.195.159) |
| 2021-03-23 20:05:34 | × | petersen quits (~petersen@redhat/juhp) (Ping timeout: 256 seconds) |
| 2021-03-23 20:05:38 | <dolio> | This is how you implement it on a computer. Computers implementations aren't abstract mathematical domains. |
| 2021-03-23 20:06:00 | → | ubert1 joins (~Thunderbi@p200300ecdf25d9f2e6b318fffe838f33.dip0.t-ipconnect.de) |
| 2021-03-23 20:06:19 | <dolio> | The domain theoretic function is just given by the specification that `it is ⊥ if ...`. |
| 2021-03-23 20:06:46 | <sclv> | this is really about skolem's paradox https://en.wikipedia.org/wiki/Skolem%27s_paradox |
| 2021-03-23 20:08:29 | → | wroathe joins (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) |
| 2021-03-23 20:08:40 | → | petersen joins (~petersen@redhat/juhp) |
| 2021-03-23 20:08:51 | <dolio> | The domain theoretic description is just a simplifying abstraction for talking about the behavior of actual implementations. The implementations don't work in terms of domains. |
| 2021-03-23 20:08:56 | × | heebo quits (~user@cpc97956-croy24-2-0-cust20.19-2.cable.virginm.net) (Ping timeout: 244 seconds) |
| 2021-03-23 20:10:21 | <dolio> | The way the implementation works is that if the function is point-wise bottom, it will never find a value to stop the parallel evaluation, so the overall result will be bottom. |
| 2021-03-23 20:10:27 | → | redmp joins (~redmp@172.58.38.247) |
| 2021-03-23 20:11:23 | <dolio> | And if it's not point-wise bottom, eventually the right point might be found and work can continue. |
| 2021-03-23 20:12:19 | <dolio> | That behavior corresponds to the domain theoretic definition. |
| 2021-03-23 20:12:45 | → | stree joins (~stree@68.36.8.116) |
| 2021-03-23 20:13:23 | × | wroathe quits (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) (Ping timeout: 245 seconds) |
| 2021-03-23 20:15:29 | <Gurkenglas> | dolio, if the function f to be judged equal or not equal to const ⊥ has an argument type with a value more defined than any other, you can simply check whether f applied to that value is ⊥ :) |
| 2021-03-23 20:19:18 | <Gurkenglas> | (...such argument types are isomorphic to A -> () for some A, I think...) |
| 2021-03-23 20:21:03 | → | elfets joins (~elfets@ip-37-201-23-96.hsi13.unitymediagroup.de) |
| 2021-03-23 20:22:48 | × | cole-h quits (~cole-h@c-73-48-197-220.hsd1.ca.comcast.net) (Quit: Goodbye) |
| 2021-03-23 20:25:15 | × | smerdyakov quits (~dan@5.146.195.159) (Quit: Leaving) |
| 2021-03-23 20:25:35 | → | smerdyakov joins (~dan@5.146.195.159) |
| 2021-03-23 20:25:36 | × | zebrag quits (~inkbottle@aaubervilliers-654-1-109-157.w86-212.abo.wanadoo.fr) (Quit: Konversation terminated!) |
| 2021-03-23 20:25:53 | → | zebrag joins (~inkbottle@aaubervilliers-654-1-109-157.w86-212.abo.wanadoo.fr) |
| 2021-03-23 20:26:36 | × | vnz quits (~vnz@unaffiliated/vnz) (Quit: ZNC - http://znc.in) |
| 2021-03-23 20:26:47 | towel_ | is now known as towel |
All times are in UTC.