Logs: freenode/#haskell
| 2021-03-28 18:13:16 | × | Someguy123 quits (~someguy@unaffiliated/compgenius999) (Ping timeout: 240 seconds) |
| 2021-03-28 18:13:48 | <wz1000> | duckduckgo gave me this: http://smonad.com/problems/nonlocality.php |
| 2021-03-28 18:13:48 | × | elliott_ quits (~elliott@pool-108-51-101-42.washdc.fios.verizon.net) (Ping timeout: 246 seconds) |
| 2021-03-28 18:13:59 | <wz1000> | which is interesting, to say the least... |
| 2021-03-28 18:14:10 | <mniip> | oh, oh my |
| 2021-03-28 18:14:18 | <mniip> | % :t $(varE $ mkNameG_v "ghc-prim" "GHC.Types" "eq_sel") |
| 2021-03-28 18:14:19 | <yahb> | mniip: forall {k} {b :: k}. b GHC.Prim.~# b |
| 2021-03-28 18:14:46 | × | ezrakilty quits (~ezrakilty@97-113-58-224.tukw.qwest.net) (Remote host closed the connection) |
| 2021-03-28 18:15:23 | → | ezrakilty joins (~ezrakilty@97-113-58-224.tukw.qwest.net) |
| 2021-03-28 18:15:51 | <mniip> | ah of course, this is the tidied type |
| 2021-03-28 18:16:00 | <mniip> | really it's (a ~ b) => a ~# b |
| 2021-03-28 18:16:08 | → | v01d4lph4 joins (~v01d4lph4@122.180.248.16) |
| 2021-03-28 18:16:12 | <mniip> | contrast with |
| 2021-03-28 18:16:15 | <mniip> | % :t $(varE $ mkNameG_v "ghc-prim" "GHC.Types" "coercible_sel") |
| 2021-03-28 18:16:16 | <yahb> | mniip: forall {k} {a :: k} {b :: k}. Coercible a b => a ~R# b |
| 2021-03-28 18:16:23 | <ski> | wz1000 : yea, i got that too :( |
| 2021-03-28 18:18:00 | <ski> | mniip : so `~#' is like a heterogenous, unboxed, `:~:' ? |
| 2021-03-28 18:18:28 | <mniip> | the distinction between them all is more intricate in Core |
| 2021-03-28 18:19:26 | × | malumore quits (~malumore@151.62.119.109) (Ping timeout: 260 seconds) |
| 2021-03-28 18:19:26 | <mniip> | but yes, ~# is heterogeneous and unboxed |
| 2021-03-28 18:19:46 | × | star_cloud quits (~star_clou@ec2-34-220-44-120.us-west-2.compute.amazonaws.com) (Ping timeout: 240 seconds) |
| 2021-03-28 18:20:18 | × | v01d4lph4 quits (~v01d4lph4@122.180.248.16) (Ping timeout: 240 seconds) |
| 2021-03-28 18:20:39 | ← | galapagos parts (~galapagos@117.222.71.68) () |
| 2021-03-28 18:22:24 | → | idhugo_ joins (~idhugo@87-49-147-45-mobile.dk.customer.tdc.net) |
| 2021-03-28 18:25:07 | → | mouseghost joins (~draco@87-206-9-185.dynamic.chello.pl) |
| 2021-03-28 18:25:08 | × | mouseghost quits (~draco@87-206-9-185.dynamic.chello.pl) (Changing host) |
| 2021-03-28 18:25:08 | → | mouseghost joins (~draco@wikipedia/desperek) |
| 2021-03-28 18:25:37 | × | zebrag quits (~inkbottle@aaubervilliers-654-1-98-245.w86-212.abo.wanadoo.fr) (Quit: Konversation terminated!) |
| 2021-03-28 18:25:45 | → | bitmapper joins (uid464869@gateway/web/irccloud.com/x-qnuflznzjiymbjnq) |
| 2021-03-28 18:25:58 | → | zebrag joins (~inkbottle@aaubervilliers-654-1-98-245.w86-212.abo.wanadoo.fr) |
| 2021-03-28 18:26:32 | <ski> | mm. okay |
| 2021-03-28 18:28:13 | × | Guest19166 quits (~textual@zrcout.mskcc.org) (Quit: My MacBook has gone to sleep. ZZZzzz…) |
| 2021-03-28 18:28:16 | → | star_cloud joins (~star_clou@ec2-34-220-44-120.us-west-2.compute.amazonaws.com) |
| 2021-03-28 18:28:19 | × | borne quits (~fritjof@200116b8644f3500f7ed9fd86a2491f0.dip.versatel-1u1.de) (Ping timeout: 245 seconds) |
| 2021-03-28 18:28:39 | <ski> | wz1000 : hm, i wonder whether that's related to Leibniz' "Monadology" |
| 2021-03-28 18:28:43 | → | malumore joins (~malumore@151.62.119.109) |
| 2021-03-28 18:28:46 | × | elfets quits (~elfets@ip-37-201-23-96.hsi13.unitymediagroup.de) (Ping timeout: 252 seconds) |
| 2021-03-28 18:29:08 | <mniip> | % $(do { k <- newName "k"; a <- newName "a"; b <- newName "b"; pure <$> newtypeD (cxt []) (mkName ":~:#") [KindedTV a (VarT k), KindedTV b (VarT k)] Nothing (normalC (mkName "Refl#") [bangType (pure $ Bang NoSourceUnpackedness NoSourceStrictness) $ conT (mkNameG_tc "ghc-prim" "GHC.Prim" "~#") `appT` varT a `appT` varT b]) [] }); |
| 2021-03-28 18:29:08 | <yahb> | mniip: ; <interactive>:21:106: error:; * Couldn't match expected type: TyVarBndr (); with actual type: Kind -> TyVarBndr Language.Haskell.TH.Type; * Probable cause: `KindedTV' is applied to too few arguments; In the expression: KindedTV a (VarT k); In the third argument of `newtypeD', namely `[KindedTV a (VarT k), KindedTV b (VarT k)]'; In the second argument of `(<$> |
| 2021-03-28 18:29:19 | → | Alleria joins (~textual@zrcout.mskcc.org) |
| 2021-03-28 18:29:21 | <mniip> | % $(do { k <- newName "k"; a <- newName "a"; b <- newName "b"; pure <$> newtypeD (cxt []) (mkName ":~:#") [KindedTV a () (VarT k), KindedTV b () (VarT k)] Nothing (normalC (mkName "Refl#") [bangType (pure $ Bang NoSourceUnpackedness NoSourceStrictness) $ conT (mkNameG_tc "ghc-prim" "GHC.Prim" "~#") `appT` varT a `appT` varT b]) [] }); |
| 2021-03-28 18:29:21 | <yahb> | mniip: |
| 2021-03-28 18:29:26 | <mniip> | % :i :~:# |
| 2021-03-28 18:29:26 | <yahb> | mniip: type role (:~:#) nominal nominal; type (:~:#) :: forall k. k -> k -> TYPE ('TupleRep '[]); newtype (:~:#) a b = Refl# (a GHC.Prim.~# b); -- Defined at <interactive>:22:2 |
| 2021-03-28 18:29:29 | <mniip> | wild |
| 2021-03-28 18:29:38 | <mniip> | it doesn't work of course |
| 2021-03-28 18:29:42 | Alleria | is now known as Guest26792 |
| 2021-03-28 18:30:20 | × | nbloomf quits (~nbloomf@2600:1700:ad14:3020:6df1:6df7:a151:690b) (Quit: My MacBook has gone to sleep. ZZZzzz…) |
| 2021-03-28 18:32:00 | <ski> | % :k :~:# |
| 2021-03-28 18:32:00 | <yahb> | ski: ; <interactive>:1:1: error: Operator applied to too few arguments: :~:# |
| 2021-03-28 18:32:00 | × | geowiesnot quits (~user@87-89-181-157.abo.bbox.fr) (Ping timeout: 246 seconds) |
| 2021-03-28 18:32:06 | <ski> | % :k (:~:#) |
| 2021-03-28 18:32:06 | <yahb> | ski: k -> k -> TYPE ('TupleRep '[]) |
| 2021-03-28 18:32:58 | <mniip> | it would be really, really cool if you could have this as a newtype |
| 2021-03-28 18:33:05 | <mniip> | whilst also having Refl# :: a :~:# a |
| 2021-03-28 18:33:28 | <mniip> | unfortunately current Core machinery will die really painfully |
| 2021-03-28 18:34:06 | <mniip> | when you try to cast <a> :: a ~# a, along N::~:# :: (:~:#) ~R# (~#) |
| 2021-03-28 18:34:45 | × | Guest26792 quits (~textual@zrcout.mskcc.org) (Ping timeout: 268 seconds) |
| 2021-03-28 18:35:03 | → | heatsink joins (~heatsink@2600:1700:bef1:5e10:f0bc:f236:90c7:a6f5) |
| 2021-03-28 18:35:14 | → | kupi joins (uid212005@gateway/web/irccloud.com/x-rsqhffuuxfehttck) |
| 2021-03-28 18:35:28 | → | nbloomf joins (~nbloomf@2600:1700:ad14:3020:f167:a89:f05f:5d78) |
| 2021-03-28 18:35:39 | × | Xnuk quits (~xnuk@vultr.xnu.kr) (Quit: ZNC - https://znc.in) |
| 2021-03-28 18:36:09 | → | Sgeo joins (~Sgeo@ool-18b98aa4.dyn.optonline.net) |
| 2021-03-28 18:36:20 | → | Xnuk joins (~xnuk@45.76.202.58) |
| 2021-03-28 18:39:21 | × | heatsink quits (~heatsink@2600:1700:bef1:5e10:f0bc:f236:90c7:a6f5) (Ping timeout: 252 seconds) |
| 2021-03-28 18:43:13 | → | CrazyPython joins (~crazypyth@98.122.164.118) |
| 2021-03-28 18:43:59 | → | __minoru__shirae joins (~shiraeesh@109.166.57.99) |
| 2021-03-28 18:44:36 | × | minoru_shiraeesh quits (~shiraeesh@46.34.207.10) (Ping timeout: 246 seconds) |
| 2021-03-28 18:44:57 | × | stree quits (~stree@68.36.8.116) (Ping timeout: 246 seconds) |
| 2021-03-28 18:46:05 | <ski> | hm, so how does `~R#' differ ? |
| 2021-03-28 18:47:54 | → | cub3s_ joins (bifunc2@gateway/vpn/protonvpn/bifunc2) |
| 2021-03-28 18:48:27 | <cub3s_> | What is the state of the art with Nix for Haskell? Are people still using nixpkgs or are many people migrating to haskell.nix? https://www.youtube.com/watch?v=j71ZkinDeUM |
| 2021-03-28 18:53:58 | → | __monty__ joins (~toonn@unaffiliated/toonn) |
| 2021-03-28 18:54:53 | → | jamm_ joins (~jamm@unaffiliated/jamm) |
| 2021-03-28 18:57:38 | <mniip> | ski, ~R# is the representation coercion |
| 2021-03-28 18:57:57 | → | Alleria__ joins (~textual@2603-7000-3040-0000-908d-bfdf-28c9-9e71.res6.spectrum.com) |
| 2021-03-28 18:58:11 | → | stree joins (~stree@68.36.8.116) |
| 2021-03-28 18:59:24 | × | jamm_ quits (~jamm@unaffiliated/jamm) (Ping timeout: 258 seconds) |
| 2021-03-28 19:01:16 | × | ezrakilty quits (~ezrakilty@97-113-58-224.tukw.qwest.net) (Remote host closed the connection) |
| 2021-03-28 19:03:14 | × | DTZUZU quits (~DTZUZO@205.ip-149-56-132.net) (Ping timeout: 252 seconds) |
| 2021-03-28 19:06:28 | × | ddellacosta quits (ddellacost@gateway/vpn/mullvad/ddellacosta) (Remote host closed the connection) |
| 2021-03-28 19:08:26 | × | shailangsa quits (~shailangs@host86-161-220-11.range86-161.btcentralplus.com) () |
| 2021-03-28 19:09:14 | × | Gurkenglas quits (~Gurkengla@unaffiliated/gurkenglas) (Remote host closed the connection) |
| 2021-03-28 19:09:38 | × | Rudd0 quits (~Rudd0@185.189.115.108) (Ping timeout: 240 seconds) |
| 2021-03-28 19:10:19 | → | ezrakilty joins (~ezrakilty@97-113-58-224.tukw.qwest.net) |
| 2021-03-28 19:12:34 | <ski> | hm, so i suppose it's related to `Coercible' |
| 2021-03-28 19:12:57 | → | average joins (uid473595@gateway/web/irccloud.com/x-ouzrkvprxkvmvpoy) |
| 2021-03-28 19:13:37 | × | mollberg quits (~mollberg@78-69-80-125-no85.tbcn.telia.com) (Remote host closed the connection) |
| 2021-03-28 19:14:31 | → | mollberg joins (~mollberg@78-69-80-125-no85.tbcn.telia.com) |
| 2021-03-28 19:16:20 | → | locrian9 joins (~mike@cpe-104-173-20-162.socal.res.rr.com) |
| 2021-03-28 19:17:06 | → | luke joins (~luke@bitnomial/staff/luke) |
| 2021-03-28 19:17:33 | × | raichoo quits (~raichoo@dslb-092-073-192-171.092.073.pools.vodafone-ip.de) (Quit: Lost terminal) |
| 2021-03-28 19:18:19 | → | geowiesnot joins (~user@i15-les02-ix2-87-89-181-157.sfr.lns.abo.bbox.fr) |
| 2021-03-28 19:19:04 | ← | jakalx parts (~jakalx@base.jakalx.net) ("Disconnected: Replaced by new connection") |
| 2021-03-28 19:21:01 | × | Narinas quits (~Narinas@187-178-93-112.dynamic.axtel.net) (Ping timeout: 265 seconds) |
| 2021-03-28 19:22:44 | × | conal quits (~conal@198.8.81.202) (Quit: Computer has gone to sleep.) |
| 2021-03-28 19:29:07 | → | conal joins (~conal@64.71.133.70) |
| 2021-03-28 19:29:32 | × | bonz060 quits (~quassel@2001:bc8:47a4:a23::1) (Quit: https://quassel-irc.org - Chat comfortably. Anywhere.) |
| 2021-03-28 19:31:59 | → | bonz060 joins (~quassel@2001:bc8:47a4:a23::1) |
| 2021-03-28 19:32:52 | → | solidus-river joins (~mike@174.127.249.180) |
All times are in UTC.