Logs: freenode/#haskell
| 2020-11-04 05:11:42 | <bqv> | darn. |
| 2020-11-04 05:11:47 | <bqv> | guess i'll do it the boring way |
| 2020-11-04 05:13:09 | <ski> | hm. i was thinking maybe you could do `instance MyClass MyA _ where ...', using `PartialTypeSignatures', but it seems that's not allowed |
| 2020-11-04 05:13:52 | <bqv> | heh |
| 2020-11-04 05:13:56 | → | Tario joins (~Tario@201.192.165.173) |
| 2020-11-04 05:14:41 | × | irc_user quits (uid423822@gateway/web/irccloud.com/x-mlbnqpkqljzoxqfd) (Quit: Connection closed for inactivity) |
| 2020-11-04 05:15:55 | × | Saukk quits (~Saukk@2001:998:f9:2914:1c59:9bb5:b94c:4) (Remote host closed the connection) |
| 2020-11-04 05:18:10 | <ski> | (hm, also it seems it doesn't work, if `b' is a `data' kind with just one (parameterless) constructor) |
| 2020-11-04 05:18:42 | × | Lycurgus quits (~niemand@98.4.97.110) (Quit: Exeunt) |
| 2020-11-04 05:19:14 | <bqv> | data as opposed to * ? |
| 2020-11-04 05:19:17 | <bqv> | first i've seen |
| 2020-11-04 05:19:22 | <ski> | yes |
| 2020-11-04 05:19:31 | <bqv> | what do they signify? |
| 2020-11-04 05:20:02 | → | jedws joins (~jedws@101.184.150.81) |
| 2020-11-04 05:20:48 | <ski> | can be used to "tag" (GADT) `data' constructors, e.g. to indicate some kind of "state" or current "mode" in which something is used |
| 2020-11-04 05:21:13 | <ski> | you should probably first look into `GADTs' |
| 2020-11-04 05:21:26 | <bqv> | hm, i see |
| 2020-11-04 05:21:47 | <bqv> | i've seen GADTs before, just not solid on the theoretical background |
| 2020-11-04 05:21:51 | × | jedws quits (~jedws@101.184.150.81) (Client Quit) |
| 2020-11-04 05:22:52 | <ski> | a very simple example could be an indexed state monad, which keeps track of (in the types) whether something is "open" or "closed". certain state-operations can only be done in certain states |
| 2020-11-04 05:24:32 | <ski> | (there are nicer examples, but i can't recall any, off the top of my head, atm) |
| 2020-11-04 05:24:57 | <bqv> | np :) |
| 2020-11-04 05:26:59 | <ski> | hm, i guess another example is to have a finite map, where the values associated with different keys, in the same map, can have different types. each key will know the type of the corresponding value |
| 2020-11-04 05:28:06 | <ski> | (or more generally, each key determines a "tag", and you have a value type that given a tag determines what type the corresponding value will have. so the tag doesn't have to be the value type itself, but it could determine it) |
| 2020-11-04 05:28:32 | → | ensyde joins (~ensyde@99-185-235-117.lightspeed.chrlnc.sbcglobal.net) |
| 2020-11-04 05:28:37 | <bqv> | hm |
| 2020-11-04 05:29:22 | <ski> | @hackage dependent-map |
| 2020-11-04 05:29:22 | <lambdabot> | https://hackage.haskell.org/package/dependent-map |
| 2020-11-04 05:30:30 | <ski> | the key type will generally be a GADT, and the value type could also be one. `Identity' is another common choice for it |
| 2020-11-04 05:33:08 | <bqv> | heh, obsidian systems. i know of them from another context |
| 2020-11-04 05:33:11 | → | dbmikus_ joins (~dbmikus@76.167.86.219) |
| 2020-11-04 05:33:13 | <ski> | so if you have `data Key :: * -> * where Name :: Key String; Address :: Key String; Age :: Key Int' then `DMap Key Identity' can have at most three associations. one mapping `Name' to a `String' value, one mapping `Address' to a `String' value, and one mapping `Age' to an `Int' value |
| 2020-11-04 05:33:25 | × | ensyde quits (~ensyde@99-185-235-117.lightspeed.chrlnc.sbcglobal.net) (Ping timeout: 240 seconds) |
| 2020-11-04 05:34:04 | <ski> | (in this case the "tag" is just an ordinary (concrete) type, of kind `*'. so this is not an example of `DataKinds') |
| 2020-11-04 05:35:32 | <bqv> | i follow, vaguely enough |
| 2020-11-04 05:35:43 | × | jamm_ quits (~jamm@unaffiliated/jamm) (Remote host closed the connection) |
| 2020-11-04 05:37:51 | <ski> | `DMap' is a way to have a "heterogenous" finite map. `DMap k v' is roughly `[exists i. (k i,v i)]' (except more efficient, presumably using a search tree instead of a list), where the index `i' is the "tag", each different association pair can have a different `i' |
| 2020-11-04 05:37:59 | × | dbmikus_ quits (~dbmikus@76.167.86.219) (Ping timeout: 258 seconds) |
| 2020-11-04 05:39:02 | → | ensyde joins (~ensyde@99-185-235-117.lightspeed.chrlnc.sbcglobal.net) |
| 2020-11-04 05:40:45 | <ski> | by pattern-matching on the value of `GADT' `k i', we can recover `i', discovering which specific index/tag was used in an association. this happens when we compare the given key with the keys in the map, discovering the `i's are the same, in case the two keys are equal |
| 2020-11-04 05:41:45 | → | day_ joins (~Unknown@unaffiliated/day) |
| 2020-11-04 05:43:58 | × | ensyde quits (~ensyde@99-185-235-117.lightspeed.chrlnc.sbcglobal.net) (Ping timeout: 260 seconds) |
| 2020-11-04 05:44:32 | × | acidjnk_new2 quits (~acidjnk@p200300d0c718f623213d210801ac68e4.dip0.t-ipconnect.de) (Ping timeout: 260 seconds) |
| 2020-11-04 05:44:49 | × | day quits (~Unknown@unaffiliated/day) (Ping timeout: 246 seconds) |
| 2020-11-04 05:44:49 | day_ | is now known as day |
| 2020-11-04 05:45:40 | × | elliott__ quits (~elliott@pool-108-51-141-12.washdc.fios.verizon.net) (Ping timeout: 256 seconds) |
| 2020-11-04 05:49:12 | → | ensyde joins (~ensyde@99-185-235-117.lightspeed.chrlnc.sbcglobal.net) |
| 2020-11-04 05:49:50 | × | pfurla quits (~pfurla@ool-182ed2e2.dyn.optonline.net) (Ping timeout: 264 seconds) |
| 2020-11-04 05:49:56 | → | jbox joins (~atlas@unaffiliated/jbox) |
| 2020-11-04 05:51:34 | → | pfurla joins (~pfurla@ool-182ed2e2.dyn.optonline.net) |
| 2020-11-04 05:54:28 | × | ensyde quits (~ensyde@99-185-235-117.lightspeed.chrlnc.sbcglobal.net) (Ping timeout: 260 seconds) |
| 2020-11-04 05:54:32 | → | guest1334598235 joins (83e40215@131.228.2.21) |
| 2020-11-04 05:55:27 | × | tsdgeos quits (~tsdgeos@195.140.213.38) (Remote host closed the connection) |
| 2020-11-04 05:55:56 | × | wroathe quits (~wroathe@c-68-54-25-135.hsd1.mn.comcast.net) (Quit: leaving) |
| 2020-11-04 05:59:18 | → | ensyde joins (~ensyde@99-185-235-117.lightspeed.chrlnc.sbcglobal.net) |
| 2020-11-04 06:04:05 | × | ensyde quits (~ensyde@99-185-235-117.lightspeed.chrlnc.sbcglobal.net) (Ping timeout: 260 seconds) |
| 2020-11-04 06:05:31 | hackage | generic-functor 0.2.0.0 - Deriving generalized functors with GHC.Generics https://hackage.haskell.org/package/generic-functor-0.2.0.0 (lyxia) |
| 2020-11-04 06:07:13 | → | hiroaki_ joins (~hiroaki@ip4d168e73.dynamic.kabel-deutschland.de) |
| 2020-11-04 06:08:39 | × | hiroaki quits (~hiroaki@ip4d176049.dynamic.kabel-deutschland.de) (Ping timeout: 258 seconds) |
| 2020-11-04 06:09:29 | → | ensyde joins (~ensyde@99-185-235-117.lightspeed.chrlnc.sbcglobal.net) |
| 2020-11-04 06:10:45 | × | Rudd0 quits (~Rudd0@185.189.115.108) (Ping timeout: 256 seconds) |
| 2020-11-04 06:14:18 | × | ensyde quits (~ensyde@99-185-235-117.lightspeed.chrlnc.sbcglobal.net) (Ping timeout: 260 seconds) |
| 2020-11-04 06:16:05 | → | merijn joins (~merijn@83-160-49-249.ip.xs4all.nl) |
| 2020-11-04 06:19:43 | → | ensyde joins (~ensyde@99-185-235-117.lightspeed.chrlnc.sbcglobal.net) |
| 2020-11-04 06:20:48 | × | merijn quits (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 256 seconds) |
| 2020-11-04 06:24:22 | × | ensyde quits (~ensyde@99-185-235-117.lightspeed.chrlnc.sbcglobal.net) (Ping timeout: 246 seconds) |
| 2020-11-04 06:28:54 | → | takuan joins (~takuan@178-116-218-225.access.telenet.be) |
| 2020-11-04 06:29:03 | × | mbomba quits (~mbomba@bras-base-toroon2719w-grc-49-142-114-9-241.dsl.bell.ca) (Quit: WeeChat 2.9) |
| 2020-11-04 06:30:14 | → | ensyde joins (~ensyde@99-185-235-117.lightspeed.chrlnc.sbcglobal.net) |
| 2020-11-04 06:33:02 | → | shatriff joins (~vitaliish@176.52.219.10) |
| 2020-11-04 06:35:21 | × | ensyde quits (~ensyde@99-185-235-117.lightspeed.chrlnc.sbcglobal.net) (Ping timeout: 260 seconds) |
| 2020-11-04 06:36:30 | × | Jeanne-Kamikaze quits (~Jeanne-Ka@68.235.43.110) (Quit: Leaving) |
| 2020-11-04 06:46:01 | × | zebrag quits (~inkbottle@aaubervilliers-654-1-104-94.w86-212.abo.wanadoo.fr) (Quit: Konversation terminated!) |
| 2020-11-04 06:48:25 | → | danvet joins (~Daniel@2a02:168:57f4:0:efd0:b9e5:5ae6:c2fa) |
| 2020-11-04 06:48:44 | → | zebrag joins (~inkbottle@aaubervilliers-654-1-104-94.w86-212.abo.wanadoo.fr) |
| 2020-11-04 06:52:50 | × | zhenchaoli quits (~user@2601:641:8000:4f00:955e:b059:4f08:2b29) (Ping timeout: 264 seconds) |
| 2020-11-04 06:54:23 | → | zhenchaoli joins (~user@2601:641:8000:4f00:955e:b059:4f08:2b29) |
| 2020-11-04 06:55:16 | → | elliott__ joins (~elliott@pool-108-51-141-12.washdc.fios.verizon.net) |
| 2020-11-04 06:55:22 | × | Katarushisu quits (~Katarushi@cpc149712-finc20-2-0-cust535.4-2.cable.virginm.net) (Ping timeout: 256 seconds) |
| 2020-11-04 06:55:54 | <bqv> | TIL: it's possible to write a file between the time GHC attempts to compile it and displays the error, so the displayed code doesn't match the error it shows |
| 2020-11-04 06:59:46 | → | sord937 joins (~sord937@gateway/tor-sasl/sord937) |
| 2020-11-04 07:00:04 | × | zebrag quits (~inkbottle@aaubervilliers-654-1-104-94.w86-212.abo.wanadoo.fr) (Quit: Konversation terminated!) |
| 2020-11-04 07:00:36 | × | elliott__ quits (~elliott@pool-108-51-141-12.washdc.fios.verizon.net) (Ping timeout: 265 seconds) |
| 2020-11-04 07:03:22 | → | idhugo joins (~idhugo@80-62-116-101-mobile.dk.customer.tdc.net) |
| 2020-11-04 07:05:37 | → | dbmikus_ joins (~dbmikus@cpe-76-167-86-219.natsow.res.rr.com) |
| 2020-11-04 07:06:51 | × | mmohammadi9812 quits (~mmohammad@188.210.118.100) (Read error: Connection reset by peer) |
| 2020-11-04 07:08:49 | × | idhugo quits (~idhugo@80-62-116-101-mobile.dk.customer.tdc.net) (Ping timeout: 265 seconds) |
| 2020-11-04 07:09:29 | → | mmohammadi9812 joins (~mmohammad@80.210.50.162) |
| 2020-11-04 07:10:29 | → | knupfer joins (~Thunderbi@i5E86B46C.versanet.de) |
| 2020-11-04 07:11:47 | → | mananamenos joins (~mananamen@84.122.202.215.dyn.user.ono.com) |
| 2020-11-04 07:13:12 | → | berberman joins (~berberman@unaffiliated/berberman) |
| 2020-11-04 07:14:22 | × | berberman_ quits (~berberman@unaffiliated/berberman) (Ping timeout: 260 seconds) |
| 2020-11-04 07:14:49 | → | cole-h joins (~cole-h@c-73-48-197-220.hsd1.ca.comcast.net) |
| 2020-11-04 07:14:55 | × | christo quits (~chris@81.96.113.213) (Remote host closed the connection) |
| 2020-11-04 07:15:13 | → | merijn joins (~merijn@83-160-49-249.ip.xs4all.nl) |
| 2020-11-04 07:17:20 | <suzu_> | big unlucky |
| 2020-11-04 07:17:35 | <bqv> | oh no it was fine, i noticed it instantly |
| 2020-11-04 07:19:36 | → | christo joins (~chris@81.96.113.213) |
| 2020-11-04 07:20:01 | × | merijn quits (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 264 seconds) |
| 2020-11-04 07:22:14 | → | gtk joins (~user@roc37-h01-176-170-197-243.dsl.sta.abo.bbox.fr) |
All times are in UTC.