Logs: freenode/#haskell
| 2021-03-28 15:11:54 | × | invaser quits (~Thunderbi@31.148.23.125) (Ping timeout: 260 seconds) |
| 2021-03-28 15:13:35 | → | alx741 joins (~alx741@186.178.109.231) |
| 2021-03-28 15:14:10 | → | nbloomf joins (~nbloomf@2600:1700:ad14:3020:6df1:6df7:a151:690b) |
| 2021-03-28 15:16:14 | → | Vadrigar_ joins (~Vadrigar@ip5b417208.dynamic.kabel-deutschland.de) |
| 2021-03-28 15:20:38 | × | Vadrigar_ quits (~Vadrigar@ip5b417208.dynamic.kabel-deutschland.de) (Ping timeout: 240 seconds) |
| 2021-03-28 15:22:02 | <edwardk> | pattern synonyms aren't updated to work with linear types yet |
| 2021-03-28 15:22:20 | <edwardk> | so the matchers that get inserted will have the wrong types |
| 2021-03-28 15:25:38 | × | zebrag quits (~inkbottle@aaubervilliers-654-1-98-245.w86-212.abo.wanadoo.fr) (Quit: Konversation terminated!) |
| 2021-03-28 15:25:44 | <edwardk> | oh wait, we don't care about Y being linear! |
| 2021-03-28 15:25:59 | → | zebrag joins (~inkbottle@aaubervilliers-654-1-98-245.w86-212.abo.wanadoo.fr) |
| 2021-03-28 15:28:30 | <edwardk> | so close to working |
| 2021-03-28 15:28:47 | <edwardk> | but the case analysis multiplicities get screwed, not just that Y has different counts |
| 2021-03-28 15:29:02 | → | raichoo joins (~raichoo@dslb-092-073-192-171.092.073.pools.vodafone-ip.de) |
| 2021-03-28 15:30:26 | × | EyalSK quits (~EyalSK@2a10:8003:382:0:8c97:7234:8b62:78bd) (Quit: Leaving) |
| 2021-03-28 15:31:24 | → | lawid_ joins (~quassel@dslb-090-186-171-096.090.186.pools.vodafone-ip.de) |
| 2021-03-28 15:31:36 | × | lawid quits (~quassel@dslb-090-186-199-034.090.186.pools.vodafone-ip.de) (Ping timeout: 268 seconds) |
| 2021-03-28 15:31:40 | × | conal quits (~conal@192.145.118.72) (Quit: Computer has gone to sleep.) |
| 2021-03-28 15:32:05 | → | heatsink joins (~heatsink@2600:1700:bef1:5e10:f0bc:f236:90c7:a6f5) |
| 2021-03-28 15:32:34 | × | nbloomf quits (~nbloomf@2600:1700:ad14:3020:6df1:6df7:a151:690b) (Quit: My MacBook has gone to sleep. ZZZzzz…) |
| 2021-03-28 15:33:47 | × | Lowl3v3l quits (~Lowl3v3l@dslb-002-207-103-026.002.207.pools.vodafone-ip.de) (Remote host closed the connection) |
| 2021-03-28 15:34:55 | → | haritz joins (~hrtz@62.3.70.206) |
| 2021-03-28 15:34:55 | × | haritz quits (~hrtz@62.3.70.206) (Changing host) |
| 2021-03-28 15:34:55 | → | haritz joins (~hrtz@unaffiliated/haritz) |
| 2021-03-28 15:35:28 | → | DavidEichmann joins (~david@47.27.93.209.dyn.plus.net) |
| 2021-03-28 15:35:36 | × | merijn quits (~merijn@83-160-49-249.ip.xs4all.nl) (Ping timeout: 246 seconds) |
| 2021-03-28 15:36:45 | × | heatsink quits (~heatsink@2600:1700:bef1:5e10:f0bc:f236:90c7:a6f5) (Ping timeout: 252 seconds) |
| 2021-03-28 15:37:52 | → | conal joins (~conal@192.145.118.71) |
| 2021-03-28 15:38:38 | × | petersen quits (~petersen@redhat/juhp) (Quit: petersen) |
| 2021-03-28 15:39:18 | → | petersen joins (~petersen@redhat/juhp) |
| 2021-03-28 15:39:54 | <edwardk> | got it to work |
| 2021-03-28 15:43:46 | × | conal quits (~conal@192.145.118.71) (Ping timeout: 240 seconds) |
| 2021-03-28 15:43:55 | <edwardk> | https://github.com/ekmett/linear-logic/blob/main/src/Linear/Logic/Y.hs <- clearly that is the foundation upon which all logic should be built |
| 2021-03-28 15:44:10 | → | Lowl3v3l joins (~Lowl3v3l@dslb-002-207-103-026.002.207.pools.vodafone-ip.de) |
| 2021-03-28 15:44:27 | <edwardk> | note the ~~ even |
| 2021-03-28 15:44:39 | → | conal joins (~conal@198.8.81.202) |
| 2021-03-28 15:46:44 | → | tzh joins (~tzh@c-24-21-73-154.hsd1.or.comcast.net) |
| 2021-03-28 15:47:17 | → | Vadrigar_ joins (~Vadrigar@ip5b417208.dynamic.kabel-deutschland.de) |
| 2021-03-28 15:47:33 | → | nbloomf joins (~nbloomf@2600:1700:ad14:3020:6df1:6df7:a151:690b) |
| 2021-03-28 15:47:54 | <ski> | what's the `~~' ? |
| 2021-03-28 15:48:21 | <ski> | heterogenous equality ? |
| 2021-03-28 15:48:58 | × | petersen quits (~petersen@redhat/juhp) (Quit: petersen) |
| 2021-03-28 15:49:40 | → | petersen joins (~petersen@redhat/juhp) |
| 2021-03-28 15:50:04 | <edwardk> | ski: yeah |
| 2021-03-28 15:50:09 | <edwardk> | i j and k can be different kinds |
| 2021-03-28 15:50:20 | <Uniaika> | I refuse to acknowledge the existence of this symbol if it has no entry in the Haskell Wiki |
| 2021-03-28 15:50:26 | <Uniaika> | https://wiki.haskell.org/Keywords <- no ~~, ergo it does not exist |
| 2021-03-28 15:50:33 | <edwardk> | its in Data.Type.Equality |
| 2021-03-28 15:50:49 | <edwardk> | and post dates that list |
| 2021-03-28 15:51:30 | <Uniaika> | curse, I will have to document it |
| 2021-03-28 15:53:45 | ← | jakalx parts (~jakalx@base.jakalx.net) ("Error from remote client") |
| 2021-03-28 15:53:53 | <wz1000> | Uniaika: it's not a keyword, is it? It is a legal identifier for a type operator |
| 2021-03-28 15:54:24 | → | tpefreedom joins (~tsomers@184-157-240-110.dyn.centurytel.net) |
| 2021-03-28 15:54:30 | × | Vadrigar_ quits (~Vadrigar@ip5b417208.dynamic.kabel-deutschland.de) (Ping timeout: 246 seconds) |
| 2021-03-28 15:55:24 | × | rkvist quits (~user@138.197.72.132) (Quit: wait wut) |
| 2021-03-28 16:00:13 | <Uniaika> | wz1000: idk if it can be arbitrarily given to your own type operators, GHC.Types defines it with an empty class declaration (in https://hackage.haskell.org/package/ghc-prim-0.6.1/docs/src/GHC.Types.html#~~ ) but since the comment right after it is a GHC Note, I would be inclined to say that it has a fair level of magic treatement by the compiler ;) |
| 2021-03-28 16:00:29 | × | mouseghost quits (~draco@wikipedia/desperek) (Quit: mew wew) |
| 2021-03-28 16:00:52 | <mniip> | ~~ can, ~ cannot |
| 2021-03-28 16:01:29 | <mniip> | (~) is built-in syntax like (:) |
| 2021-03-28 16:01:55 | <Uniaika> | mniip: even if it's also defined as an empty class declaration in GHC.Types? |
| 2021-03-28 16:01:56 | × | nbloomf quits (~nbloomf@2600:1700:ad14:3020:6df1:6df7:a151:690b) (Quit: My MacBook has gone to sleep. ZZZzzz…) |
| 2021-03-28 16:01:59 | <mniip> | (~~) is a special constraint, but not actually a special identifier/syntax |
| 2021-03-28 16:02:06 | <Uniaika> | oki doki |
| 2021-03-28 16:02:17 | <Uniaika> | ah wait, you meant term-level (~) |
| 2021-03-28 16:02:25 | <mniip> | I meant type level |
| 2021-03-28 16:02:29 | <Uniaika> | oh okay |
| 2021-03-28 16:02:52 | <mniip> | that class declaration is bogus anyway |
| 2021-03-28 16:03:09 | <Uniaika> | I'm interested to know why :) |
| 2021-03-28 16:03:51 | → | nbloomf joins (~nbloomf@2600:1700:ad14:3020:6df1:6df7:a151:690b) |
| 2021-03-28 16:03:53 | <mniip> | that class declaration suggests that the dictionary for (a ~~ b) is an empty box |
| 2021-03-28 16:04:24 | → | cole-h joins (~cole-h@c-73-48-197-220.hsd1.ca.comcast.net) |
| 2021-03-28 16:04:48 | × | jokester quits (~mono@unaffiliated/jokester) (Ping timeout: 258 seconds) |
| 2021-03-28 16:04:50 | <mniip> | it isn't |
| 2021-03-28 16:05:35 | <Uniaika> | ah, tricky indeed |
| 2021-03-28 16:05:45 | <mniip> | c.f. eq_sel and heq_sel |
| 2021-03-28 16:05:58 | <Uniaika> | oh, int-index has had this GHC proposal open https://github.com/ghc-proposals/ghc-proposals/pull/371 |
| 2021-03-28 16:06:27 | <Uniaika> | mniip: I don't follow you |
| 2021-03-28 16:06:34 | → | raehik joins (~raehik@cpc95906-rdng25-2-0-cust156.15-3.cable.virginm.net) |
| 2021-03-28 16:08:02 | → | jokester joins (~mono@unaffiliated/jokester) |
| 2021-03-28 16:08:27 | → | Vadrigar_ joins (~Vadrigar@ip5b417208.dynamic.kabel-deutschland.de) |
| 2021-03-28 16:09:14 | → | idhugo_ joins (~idhugo@87-49-147-45-mobile.dk.customer.tdc.net) |
| 2021-03-28 16:10:28 | × | txb920 quits (5af6ddfd@90.246.221.253) (Quit: Connection closed) |
| 2021-03-28 16:10:33 | <mniip> | ~~ has ~# as "superclass" |
| 2021-03-28 16:10:41 | × | raehik quits (~raehik@cpc95906-rdng25-2-0-cust156.15-3.cable.virginm.net) (Ping timeout: 240 seconds) |
| 2021-03-28 16:10:51 | <mniip> | i.e. the dictionary for (a ~~ b) has a "field" with (a ~# b) |
| 2021-03-28 16:11:08 | <mniip> | this field is selected by a function called heq_sel |
| 2021-03-28 16:11:23 | <mniip> | GHC.Types.heq_sel, I think |
| 2021-03-28 16:11:50 | × | vgtw quits (~vgtw@gateway/tor-sasl/vgtw) (Remote host closed the connection) |
| 2021-03-28 16:12:54 | → | raehik joins (~raehik@cpc95906-rdng25-2-0-cust156.15-3.cable.virginm.net) |
| 2021-03-28 16:14:16 | <mniip> | (I |
| 2021-03-28 16:14:30 | <mniip> | (I'm not sure what's preventing you from being able to look at it with :i) |
| 2021-03-28 16:14:47 | × | idhugo_ quits (~idhugo@87-49-147-45-mobile.dk.customer.tdc.net) (Ping timeout: 268 seconds) |
| 2021-03-28 16:15:29 | <Uniaika> | indeed :i doesn't show ~# as the superclass |
| 2021-03-28 16:15:57 | <mniip> | % :i (~~) |
| 2021-03-28 16:15:59 | <yahb> | mniip: type (~~) :: forall k0 k1. k0 -> k1 -> Constraint; class (a ~~ b) => (~~) a b; -- Defined in `GHC.Types'; infix 4 ~~ |
| 2021-03-28 16:16:04 | <mniip> | there is a superclass |
| 2021-03-28 16:16:08 | <wz1000> | Uniaika: type a ~~ b = (a,b) |
| 2021-03-28 16:16:10 | <wz1000> | that works |
| 2021-03-28 16:16:16 | <wz1000> | if you set -XTypeOperators |
| 2021-03-28 16:16:34 | <Uniaika> | wz1000: curse. Thanks! :) |
| 2021-03-28 16:16:36 | <mniip> | however there's some machinery that translates primitive equalities back into surface haskell |
All times are in UTC.