Logs: liberachat/#haskell
| 2021-06-08 00:29:50 | → | jmcarthur joins (~jmcarthur@c-73-29-224-10.hsd1.nj.comcast.net) |
| 2021-06-08 00:31:02 | × | raehik quits (~raehik@cpc95906-rdng25-2-0-cust156.15-3.cable.virginm.net) (Ping timeout: 250 seconds) |
| 2021-06-08 00:33:53 | × | nosewings quits (~ncoltharp@2603-8081-3e05-e2d0-0000-0000-0000-1aef.res6.spectrum.com) (Remote host closed the connection) |
| 2021-06-08 00:35:50 | → | hammock joins (~Hammock@2600:1700:19a1:3330::625) |
| 2021-06-08 00:37:57 | × | minare_window quits (~minare_wi@adsl-72-50-4-120.prtc.net) (Quit: Client closed) |
| 2021-06-08 00:38:47 | × | myShoggoth quits (~myShoggot@97-120-89-117.ptld.qwest.net) (Ping timeout: 258 seconds) |
| 2021-06-08 00:41:21 | × | shapr quits (~user@108.28.144.11) (Ping timeout: 252 seconds) |
| 2021-06-08 00:42:22 | → | ordinate joins (~ordinate@c-68-38-144-3.hsd1.in.comcast.net) |
| 2021-06-08 00:44:43 | × | falafel quits (~falafel@pool-96-255-70-50.washdc.fios.verizon.net) (Ping timeout: 264 seconds) |
| 2021-06-08 00:50:02 | × | waleee quits (~waleee@h-98-128-228-119.NA.cust.bahnhof.se) (Ping timeout: 272 seconds) |
| 2021-06-08 00:59:17 | × | eggplantade quits (~Eggplanta@2600:1700:bef1:5e10:90fb:e693:9986:91e0) (Remote host closed the connection) |
| 2021-06-08 01:00:25 | → | yd502 joins (~yd502@180.168.212.6) |
| 2021-06-08 01:02:21 | <blankhart> | when this paper (https://dl.acm.org/doi/10.1145/3371121) says that "guessing the right answer is typical of declarative type systems" what precisely is meant by "guess"? |
| 2021-06-08 01:03:23 | → | yd502_ joins (~yd502@180.168.212.6) |
| 2021-06-08 01:04:30 | → | merijn joins (~merijn@83-160-49-249.ip.xs4all.nl) |
| 2021-06-08 01:04:30 | <blankhart> | the paper is talking about guessing in recursive binding groups and adding kinds to a context before looking at the related declarations |
| 2021-06-08 01:06:32 | <cdsmith> | Yes, I suppose it just means that the declarative specification of the type system cannot be interpreted as an algorithm, or used as an implementation, because you need to know what the kinds are before you can evaluate the claims there. |
| 2021-06-08 01:06:34 | × | yd502 quits (~yd502@180.168.212.6) (Ping timeout: 250 seconds) |
| 2021-06-08 01:07:35 | <blankhart> | is the point that in "algorithmic type systems" a unification variable is used but in a declarative system the kind is "guessed" in the sense of being solved by whatever algorithm implements the system? |
| 2021-06-08 01:08:46 | × | sheepduck quits (~sheepduck@2607:fea8:2a60:b700::8a94) (Remote host closed the connection) |
| 2021-06-08 01:09:05 | → | sheepduck joins (~sheepduck@2607:fea8:2a60:b700::5d55) |
| 2021-06-08 01:10:25 | → | v01d4lph4 joins (~v01d4lph4@user/v01d4lph4) |
| 2021-06-08 01:11:15 | <cdsmith> | I'm not sure of the details here, sorry. Maybe someone else can help more! |
| 2021-06-08 01:14:44 | × | xff0x quits (~xff0x@2001:1a81:5240:1700:9a39:76e8:fdb4:2fab) (Ping timeout: 272 seconds) |
| 2021-06-08 01:14:54 | × | v01d4lph4 quits (~v01d4lph4@user/v01d4lph4) (Ping timeout: 252 seconds) |
| 2021-06-08 01:14:54 | × | Erutuon quits (~Erutuon@user/erutuon) (Ping timeout: 252 seconds) |
| 2021-06-08 01:15:59 | <ski> | blankhart : i think "guess" means that there's no way to order the premises, viewed as (calls to) relations that compute outputs from inputs, in such a way that every (meta-)variable is output before it needs to be input (considering the inputs of the conclusion relation as "initial inputs", and the corresponding outputs as "final outputs") |
| 2021-06-08 01:16:15 | → | xff0x joins (~xff0x@2001:1a81:5287:b700:62cf:6f80:f269:aa87) |
| 2021-06-08 01:17:06 | → | Erutuon joins (~Erutuon@user/erutuon) |
| 2021-06-08 01:19:38 | <blankhart> | so, for starters, we don't mean "guess" in the sense of something that might be wrong. it is more like, we consult an oracle that tells us what the answer would be if we had a constraint solving algorithm? |
| 2021-06-08 01:20:14 | <cdsmith> | Yes, "consult an oracle" sounds like exactly what they mean. |
| 2021-06-08 01:20:23 | <ski> | i believe that's the idea, yes |
| 2021-06-08 01:21:08 | <blankhart> | thanks both |
| 2021-06-08 01:21:28 | <ski> | (having some knowledge of logic programming is relevant here) |
| 2021-06-08 01:22:52 | <blankhart> | well haskell is declarative, so i was trying to think of an analogy with mutually recursive let bindings, but couldn't really get one that i would describe as involving "guessing" |
| 2021-06-08 01:24:23 | <ski> | well, the "declarative" in "declarative typing rules" isn't really related to the one in "declarative programming paradigm" |
| 2021-06-08 01:25:14 | <cdsmith> | Well, in some sense recursive let bindings present a similar issue, in that there could be multiple values that satisfy the system of equations. But we also have an algorithmic interpretation involving least fixed points in the definedness order. So that's the sense in which Haskell is more "algorithmic" and not purely "declarative" in the paper's usage of the words. |
| 2021-06-08 01:26:13 | <ski> | yes, recursive `let' also needs "guessing" in the same sense |
| 2021-06-08 01:27:29 | × | smitop2 quits (uid328768@id-328768.tinside.irccloud.com) (Quit: Connection closed for inactivity) |
| 2021-06-08 01:27:32 | <blankhart> | that was the missing piece thank you |
| 2021-06-08 01:27:39 | × | Topsi quits (~Tobias@dyndsl-095-033-093-145.ewe-ip-backbone.de) (Read error: Connection reset by peer) |
| 2021-06-08 01:28:23 | → | shapr joins (~user@pool-100-36-247-68.washdc.fios.verizon.net) |
| 2021-06-08 01:29:05 | × | epolanski quits (uid312403@id-312403.brockwell.irccloud.com) (Quit: Connection closed for inactivity) |
| 2021-06-08 01:30:18 | × | argento quits (~argent0@168-227-96-51.ptr.westnet.com.ar) (Ping timeout: 252 seconds) |
| 2021-06-08 01:30:43 | <ski> | (btw, i think i've heard the term "guess" even used in situations like e.g. the typing rule for function application, in that there's a (meta-)variable that occurs in the premises, that doesn't appear in the conclusion, and so, if you're attempting to build a typing derivation tree, from the root, you'd have to "guess" the argument type, when coming to an application. this corresponds to viewing all |
| 2021-06-08 01:30:49 | <ski> | (judgement) relation parameters as "input". however, at least in a typing (as opposed to a more general derivation, or logic programming, context) context, i think it's common to consider them as having both input and output parameters. cf. bidirectional type checking) |
| 2021-06-08 01:31:58 | <ski> | (for comparision, for deductive databases, all parameters would be considered "output", as the derivation tree is built bottom-up (rather than top-down), from the leaves/facts (rather than from the root/goal)) |
| 2021-06-08 01:34:22 | × | tv quits (~tv@user/tv) (Ping timeout: 272 seconds) |
| 2021-06-08 01:34:46 | → | eggplantade joins (~Eggplanta@2600:1700:bef1:5e10:90fb:e693:9986:91e0) |
| 2021-06-08 01:36:14 | → | zebrag joins (~chris@user/zebrag) |
| 2021-06-08 01:37:08 | <blankhart> | algorithmically interpreted as call by need, call by value, call by...both |
| 2021-06-08 01:38:38 | × | merijn quits (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 250 seconds) |
| 2021-06-08 01:39:26 | × | eggplantade quits (~Eggplanta@2600:1700:bef1:5e10:90fb:e693:9986:91e0) (Ping timeout: 272 seconds) |
| 2021-06-08 01:39:59 | <blankhart> | so the point of a "syntax-directed |
| 2021-06-08 01:40:02 | <ski> | hm ? |
| 2021-06-08 01:40:23 | <blankhart> | " declarative specification is that it is also algorithmic in that there is no need to guess? |
| 2021-06-08 01:40:45 | <ski> | not sure of a relation to the call-by-* stuff |
| 2021-06-08 01:41:33 | → | eggplantade joins (~Eggplanta@2600:1700:bef1:5e10:90fb:e693:9986:91e0) |
| 2021-06-08 01:43:03 | <ski> | blankhart : i'd say it's not that simple. i think syntax-directed would mean that there's only one (or maybe at most a few ?) rules to consider / choose from, given the term (or whatever one is syntax-directed wrt) as an input. but there could still be other (meta-)variables that would need to be "guessed", in the application of the selected rule |
| 2021-06-08 01:44:02 | ski | . o O ( attribute grammars ) |
| 2021-06-08 01:48:19 | × | td_ quits (~td@muedsl-82-207-238-142.citykom.de) (Ping timeout: 264 seconds) |
| 2021-06-08 01:50:25 | → | td_ joins (~td@94.134.91.135) |
| 2021-06-08 01:52:27 | <blankhart> | thank you ski i will think more about that |
| 2021-06-08 01:53:01 | × | Cajun quits (~Cajun@ip98-163-211-112.no.no.cox.net) (Quit: Client closed) |
| 2021-06-08 01:56:19 | × | geekosaur quits (~geekosaur@069-135-003-034.biz.spectrum.com) (Ping timeout: 245 seconds) |
| 2021-06-08 01:56:22 | × | zebrag quits (~chris@user/zebrag) (Remote host closed the connection) |
| 2021-06-08 01:57:21 | × | jmcarthur quits (~jmcarthur@c-73-29-224-10.hsd1.nj.comcast.net) (Quit: My MacBook Air has gone to sleep. ZZZzzz…) |
| 2021-06-08 01:58:17 | → | falafel joins (~falafel@pool-96-255-70-50.washdc.fios.verizon.net) |
| 2021-06-08 02:05:25 | → | ddellacosta joins (~ddellacos@86.106.143.10) |
| 2021-06-08 02:07:01 | → | zebrag joins (~chris@user/zebrag) |
| 2021-06-08 02:08:06 | × | falafel quits (~falafel@pool-96-255-70-50.washdc.fios.verizon.net) (Ping timeout: 250 seconds) |
| 2021-06-08 02:09:06 | → | notzmv joins (~zmv@user/notzmv) |
| 2021-06-08 02:09:19 | × | FinnElija quits (~finn_elij@user/finn-elija/x-0085643) (Ping timeout: 264 seconds) |
| 2021-06-08 02:10:01 | × | ddellacosta quits (~ddellacos@86.106.143.10) (Ping timeout: 258 seconds) |
| 2021-06-08 02:11:06 | → | FinnElija joins (~finn_elij@user/finn-elija/x-0085643) |
| 2021-06-08 02:12:00 | × | td_ quits (~td@94.134.91.135) (Ping timeout: 250 seconds) |
| 2021-06-08 02:13:38 | → | renzhi joins (~xp@2607:fa49:6500:bc00::e7b) |
| 2021-06-08 02:13:44 | × | notzmv quits (~zmv@user/notzmv) (Ping timeout: 250 seconds) |
| 2021-06-08 02:13:55 | → | td_ joins (~td@muedsl-82-207-238-242.citykom.de) |
| 2021-06-08 02:15:57 | → | thelounge926 joins (~thelounge@69.234.40.90) |
| 2021-06-08 02:17:17 | → | falafel joins (~falafel@pool-96-255-70-50.washdc.fios.verizon.net) |
| 2021-06-08 02:17:42 | × | thelounge92 quits (~thelounge@cpe-23-240-28-18.socal.res.rr.com) (Ping timeout: 264 seconds) |
| 2021-06-08 02:17:42 | thelounge926 | is now known as thelounge92 |
| 2021-06-08 02:23:46 | → | lbseale__ joins (~lbseale@ip72-194-54-201.sb.sd.cox.net) |
| 2021-06-08 02:25:04 | → | mpt joins (~tom@2a02:908:1862:49e0::5) |
| 2021-06-08 02:25:33 | → | myShoggoth joins (~myShoggot@97-120-89-117.ptld.qwest.net) |
| 2021-06-08 02:26:57 | × | lbseale_ quits (~lbseale@ip72-194-54-201.sb.sd.cox.net) (Ping timeout: 252 seconds) |
| 2021-06-08 02:37:59 | × | Brumaire quits (~quassel@81-64-14-121.rev.numericable.fr) (Ping timeout: 245 seconds) |
| 2021-06-08 02:41:26 | × | thelounge92 quits (~thelounge@69.234.40.90) (Read error: Connection reset by peer) |
| 2021-06-08 02:48:43 | → | Cajun joins (~Cajun@ip98-163-211-112.no.no.cox.net) |
| 2021-06-08 02:50:39 | × | myShoggoth quits (~myShoggot@97-120-89-117.ptld.qwest.net) (Ping timeout: 258 seconds) |
| 2021-06-08 02:51:12 | → | myShoggoth joins (~myShoggot@97-120-89-117.ptld.qwest.net) |
| 2021-06-08 02:52:14 | × | mpt quits (~tom@2a02:908:1862:49e0::5) (Ping timeout: 244 seconds) |
| 2021-06-08 02:52:58 | × | albet70 quits (~xxx@2400:8902::f03c:92ff:fe60:98d8) (Remote host closed the connection) |
| 2021-06-08 02:53:32 | × | hammock quits (~Hammock@2600:1700:19a1:3330::625) (Ping timeout: 272 seconds) |
| 2021-06-08 02:54:49 | × | blizzard quits (~winter@2603-6011-f901-9e5b-78b5-8b2f-cdb2-4171.res6.spectrum.com) (Ping timeout: 244 seconds) |
| 2021-06-08 02:56:58 | × | zebrag quits (~chris@user/zebrag) (Quit: Konversation terminated!) |
| 2021-06-08 02:57:10 | → | jmcarthur joins (~jmcarthur@c-73-29-224-10.hsd1.nj.comcast.net) |
| 2021-06-08 02:57:14 | → | albet70 joins (~xxx@2400:8902::f03c:92ff:fe60:98d8) |
| 2021-06-08 02:57:18 | × | albet70 quits (~xxx@2400:8902::f03c:92ff:fe60:98d8) (Remote host closed the connection) |
All times are in UTC.