Home freenode/#haskell: Logs Calendar

Logs: freenode/#haskell

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