Home freenode/#haskell: Logs Calendar

Logs: freenode/#haskell

←Prev  Next→ 502,152 events total
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.