Logs: freenode/#haskell
| 2021-03-28 07:06:21 | × | danvet quits (~Daniel@2a02:168:57f4:0:efd0:b9e5:5ae6:c2fa) (Ping timeout: 246 seconds) |
| 2021-03-28 07:09:47 | × | vs^ quits (vs@ip98-184-89-2.mc.at.cox.net) () |
| 2021-03-28 07:10:31 | × | Ariakenom quits (~Ariakenom@2001:9b1:efb:fc00:b497:8c3b:17d1:d29) (Read error: Connection reset by peer) |
| 2021-03-28 07:11:52 | → | stree joins (~stree@68.36.8.116) |
| 2021-03-28 07:15:18 | × | minoru_shiraeesh quits (~shiraeesh@46.34.207.10) (Ping timeout: 240 seconds) |
| 2021-03-28 07:18:30 | → | dsrt^ joins (dsrt@ip98-184-89-2.mc.at.cox.net) |
| 2021-03-28 07:20:10 | → | molehillish joins (~molehilli@2600:8800:8d06:1800:6438:fe04:a25d:577) |
| 2021-03-28 07:23:00 | × | davidfetter1 quits (~davidfett@37.120.211.188) (Remote host closed the connection) |
| 2021-03-28 07:29:16 | × | molehillish quits (~molehilli@2600:8800:8d06:1800:6438:fe04:a25d:577) (Ping timeout: 276 seconds) |
| 2021-03-28 07:30:43 | → | Vadrigar_ joins (~Vadrigar@ip5b417208.dynamic.kabel-deutschland.de) |
| 2021-03-28 07:31:18 | × | locrian9 quits (~mike@99-153-255-194.lightspeed.irvnca.sbcglobal.net) (Ping timeout: 240 seconds) |
| 2021-03-28 07:31:45 | → | gurmble joins (~Thunderbi@freenode/staff/grumble) |
| 2021-03-28 07:32:31 | × | Chai-T-Rex quits (~ChaiTRex@gateway/tor-sasl/chaitrex) (Remote host closed the connection) |
| 2021-03-28 07:32:40 | → | Lycurgus joins (~niemand@98.4.120.166) |
| 2021-03-28 07:32:50 | → | Chai-T-Rex joins (~ChaiTRex@gateway/tor-sasl/chaitrex) |
| 2021-03-28 07:33:32 | → | merijn joins (~merijn@83-160-49-249.ip.xs4all.nl) |
| 2021-03-28 07:33:49 | → | malumore joins (~malumore@151.62.119.109) |
| 2021-03-28 07:33:49 | × | ezzieyguywuf quits (~Unknown@unaffiliated/ezzieyguywuf) (Ping timeout: 276 seconds) |
| 2021-03-28 07:35:41 | × | grumble quits (grumble@freenode/staff/grumble) (Remote host closed the connection) |
| 2021-03-28 07:35:49 | gurmble | is now known as grumble |
| 2021-03-28 07:36:42 | → | minoru_shiraeesh joins (~shiraeesh@46.34.207.10) |
| 2021-03-28 07:36:46 | → | Kerberos88 joins (~Kerberos8@ppp-94-68-130-83.home.otenet.gr) |
| 2021-03-28 07:37:11 | × | Kerberos88 quits (~Kerberos8@ppp-94-68-130-83.home.otenet.gr) (Client Quit) |
| 2021-03-28 07:38:48 | → | zleap joins (~zleap@37.120.211.188) |
| 2021-03-28 07:41:18 | × | cole-h quits (~cole-h@c-73-48-197-220.hsd1.ca.comcast.net) (Ping timeout: 240 seconds) |
| 2021-03-28 07:41:51 | × | xsperry quits (~as@unaffiliated/xsperry) (Ping timeout: 260 seconds) |
| 2021-03-28 07:47:28 | → | Franciman joins (~francesco@host-79-53-62-46.retail.telecomitalia.it) |
| 2021-03-28 07:48:15 | → | molehillish joins (~molehilli@2600:8800:8d06:1800:6438:fe04:a25d:577) |
| 2021-03-28 07:51:21 | × | solvr quits (57e3c46d@87.227.196.109) (Quit: Connection closed) |
| 2021-03-28 07:52:49 | × | molehillish quits (~molehilli@2600:8800:8d06:1800:6438:fe04:a25d:577) (Ping timeout: 250 seconds) |
| 2021-03-28 07:54:39 | × | minoru_shiraeesh quits (~shiraeesh@46.34.207.10) (Ping timeout: 246 seconds) |
| 2021-03-28 07:59:36 | → | elfets joins (~elfets@ip-37-201-23-96.hsi13.unitymediagroup.de) |
| 2021-03-28 08:01:20 | × | olligobber quits (olligobber@gateway/vpn/privateinternetaccess/olligobber) (Ping timeout: 246 seconds) |
| 2021-03-28 08:02:53 | × | hidedagger quits (~nate@unaffiliated/hidedagger) (Quit: WeeChat 3.1) |
| 2021-03-28 08:07:34 | → | ADG1089 joins (~aditya@27.58.165.185) |
| 2021-03-28 08:08:10 | × | merijn quits (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 260 seconds) |
| 2021-03-28 08:08:13 | × | wroathe quits (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) (Ping timeout: 265 seconds) |
| 2021-03-28 08:10:12 | → | ezzieyguywuf joins (~Unknown@unaffiliated/ezzieyguywuf) |
| 2021-03-28 08:10:17 | → | borne joins (~fritjof@200116b8644f3500f7ed9fd86a2491f0.dip.versatel-1u1.de) |
| 2021-03-28 08:16:04 | × | danso quits (~dan@2001:1970:52e7:d000:96b8:6dff:feb3:c009) (Ping timeout: 276 seconds) |
| 2021-03-28 08:16:34 | → | olligobber joins (olligobber@gateway/vpn/privateinternetaccess/olligobber) |
| 2021-03-28 08:17:32 | → | Gurkenglas joins (~Gurkengla@unaffiliated/gurkenglas) |
| 2021-03-28 08:26:13 | × | p3n quits (~p3n@2a00:19a0:3:7c:0:d9c6:7cf6:1) (Remote host closed the connection) |
| 2021-03-28 08:26:35 | × | idhugo_ quits (~idhugo@87-49-147-45-mobile.dk.customer.tdc.net) (Ping timeout: 265 seconds) |
| 2021-03-28 08:27:14 | → | p3n joins (~p3n@2a00:19a0:3:7c:0:d9c6:7cf6:1) |
| 2021-03-28 08:29:10 | × | Lycurgus quits (~niemand@98.4.120.166) (Quit: Exeunt) |
| 2021-03-28 08:29:37 | → | idhugo_ joins (~idhugo@87-49-147-45-mobile.dk.customer.tdc.net) |
| 2021-03-28 08:30:20 | → | danso joins (~dan@d67-193-121-2.home3.cgocable.net) |
| 2021-03-28 08:31:32 | → | Wizek joins (uid191769@gateway/web/irccloud.com/x-ivxcahppedejjawd) |
| 2021-03-28 08:31:44 | → | curl joins (5ce955fb@gateway/web/cgi-irc/kiwiirc.com/ip.92.233.85.251) |
| 2021-03-28 08:31:46 | → | Sornaensis joins (~Sornaensi@077213203030.dynamic.telenor.dk) |
| 2021-03-28 08:32:55 | → | kuribas joins (~user@ptr-25vy0i929e202xlroa1.18120a2.ip6.access.telenet.be) |
| 2021-03-28 08:33:26 | <curl> | hi, yesterday we spoke about the concept of sum-records, and emulating them as a GADT |
| 2021-03-28 08:33:52 | → | txb920 joins (5af6ddfd@90.246.221.253) |
| 2021-03-28 08:34:12 | <curl> | extensible product types are sum types, and so to get eg list records we need sum-records |
| 2021-03-28 08:35:08 | × | Sorny quits (~Sornaensi@45.41.132.136) (Ping timeout: 252 seconds) |
| 2021-03-28 08:35:39 | → | Tuplanolla joins (~Tuplanoll@91-159-68-239.elisa-laajakaista.fi) |
| 2021-03-28 08:35:55 | <curl> | recursive programmes are also similarly extensible in construction, and require the same sum-record method |
| 2021-03-28 08:36:44 | <curl> | eg branching on the basecase |
| 2021-03-28 08:37:41 | <curl> | otherwise our programs if they were just nested function calls would be made of products |
| 2021-03-28 08:37:52 | <curl> | and sums enter on pattern matching for example |
| 2021-03-28 08:39:59 | <curl> | ie, the structure on which we can represent a lazy functional program must have sum-records, for the recursive accessors |
| 2021-03-28 08:41:05 | <curl> | as a form of cycle explicating reference |
| 2021-03-28 08:41:46 | → | xsperry joins (~as@unaffiliated/xsperry) |
| 2021-03-28 08:42:57 | <curl> | one thing im not sure about is how to get scope limitation |
| 2021-03-28 08:43:23 | → | sord937 joins (~sord937@gateway/tor-sasl/sord937) |
| 2021-03-28 08:43:40 | <curl> | since these records are available for anywhere in the datastructure to reference, its like being able to use different functions local scope, which is bad |
| 2021-03-28 08:44:15 | → | wonko7 joins (~wonko7@62.115.229.50) |
| 2021-03-28 08:45:27 | × | vicfred quits (vicfred@gateway/vpn/mullvad/vicfred) (Quit: Leaving) |
| 2021-03-28 08:45:41 | → | purelazy joins (502a2a96@80-42-42-150.dynamic.dsl.as9105.com) |
| 2021-03-28 08:45:51 | × | sord937 quits (~sord937@gateway/tor-sasl/sord937) (Remote host closed the connection) |
| 2021-03-28 08:46:16 | → | sord937 joins (~sord937@gateway/tor-sasl/sord937) |
| 2021-03-28 08:46:35 | <curl> | what you would want is eg, being able to have everything declared "at the same level" being with shared scope, but that requires something intrinsically listlike in the program datatypes structure |
| 2021-03-28 08:46:54 | × | purelazy quits (502a2a96@80-42-42-150.dynamic.dsl.as9105.com) (Client Quit) |
| 2021-03-28 08:47:28 | <curl> | scope access restrictions then seem quite a specific thing that would have a bizzare syntax that might be overboard, if this was actually going to make its way into something like GADT syntax |
| 2021-03-28 08:48:27 | <curl> | where the need to represent cyclic structures is more general than trying to represent recursive programs which seems to need an altered syntax |
| 2021-03-28 08:48:57 | <curl> | for scoping |
| 2021-03-28 08:48:59 | → | jacks2 joins (~bc8134e3@217.29.117.252) |
| 2021-03-28 08:49:35 | <curl> | which maybe isnt such an unnatural consideration when making these record references to make cycles |
| 2021-03-28 08:52:24 | <curl> | the main result is basically that all you need is record accessors instead of values to get cycles, and if this can have scope restriction |
| 2021-03-28 08:52:59 | <curl> | and that this needs sum-records |
| 2021-03-28 08:53:33 | <curl> | and actually, making the whole GADT in one go instead of making it in levels is not normal haskell |
| 2021-03-28 08:54:19 | <curl> | normally you put it together when you construct the value, rather than the GADT |
| 2021-03-28 08:54:41 | → | molehillish joins (~molehilli@2600:8800:8d06:1800:6438:fe04:a25d:577) |
| 2021-03-28 08:55:22 | <curl> | the type indexing for the referencing meaning its shape is designated at decleration of the GADT, and so there is no need to not have it be constructed there too |
| 2021-03-28 08:55:46 | <curl> | but this needs to bring with it some amount of machenery from how we construct values |
| 2021-03-28 08:56:10 | <curl> | its not easy to say, eg, repeat one branch n times, when declaring the GADT |
| 2021-03-28 08:56:29 | <curl> | whereas this is exactly how we would construct a value |
| 2021-03-28 08:56:40 | → | merijn joins (~merijn@83-160-49-249.ip.xs4all.nl) |
| 2021-03-28 08:58:04 | <curl> | at least with something like "where" in the GADT construction syntax |
| 2021-03-28 08:59:06 | × | molehillish quits (~molehilli@2600:8800:8d06:1800:6438:fe04:a25d:577) (Ping timeout: 258 seconds) |
| 2021-03-28 09:00:06 | × | jkaye[m] quits (jkayematri@gateway/shell/matrix.org/x-ennhxxzzzhkixwvh) (Quit: Idle for 30+ days) |
| 2021-03-28 09:00:06 | × | alecs[m] quits (malumorema@gateway/shell/matrix.org/x-rhoytvrhanidetkb) (Quit: Idle for 30+ days) |
| 2021-03-28 09:01:52 | × | merijn quits (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 265 seconds) |
| 2021-03-28 09:02:04 | × | shutdown_-h_now quits (~arjan@2001:1c06:2d0b:2312:71ef:dee2:f1b7:70aa) (Ping timeout: 245 seconds) |
| 2021-03-28 09:02:12 | <curl> | unless somehow the "referencing" was differed until the construction of values, but the point of bringing it into the GADT decleration was to have the references available there |
| 2021-03-28 09:02:37 | <curl> | the records to any position that could be referenced to create cycles |
| 2021-03-28 09:02:51 | <curl> | im unsure at this point |
| 2021-03-28 09:05:40 | <curl> | i think the version with cycles created at the value construction is the version we have now, and the GADT version would be better by handling cyclic references the same as branches in a nested datatype |
| 2021-03-28 09:07:13 | × | drbean_ quits (~drbean@TC210-63-209-190.static.apol.com.tw) (Quit: ZNC 1.8.2+cygwin2 - https://znc.in) |
All times are in UTC.