Home freenode/#haskell: Logs Calendar

Logs: freenode/#haskell

←Prev  Next→
Page 1 .. 107 108 109 110 111 112 113 114 115 116 117 .. 5022
— 502,152 events total
2020-09-21 07:59:16 <Axman6> Don't hold back Ed
2020-09-21 07:59:47 <edwardk> i just managed to get my 'types' library to let me use Constraint one of the many kinds i managed to lower to the term level
2020-09-21 07:59:48 siraben sends a request to the current effect handler to do a little dance
2020-09-21 07:59:53 <edwardk> this means Sing p subsumes Dict p
2020-09-21 08:00:21 <Axman6> :o
2020-09-21 08:00:22 <edwardk> and (:-) becomes able to move around any singleton through SingI instances, so it becomes a way to pass arbitrary functions between singleton types
2020-09-21 08:00:29 <edwardk> So now
2020-09-21 08:00:40 <edwardk> Sing (a :: Type) -- is TypeRep a
2020-09-21 08:00:46 <edwardk> Sing (a :: Constraint) -- is Dict a
2020-09-21 08:01:16 <edwardk> Sing (a :: String) -- is a type level string that you can actually cons on, take/drop from and otherwise manipulate unlike Symbol.
2020-09-21 08:01:35 <edwardk> etc.
2020-09-21 08:02:16 <Taneb> Ooh, that's pretty neat
2020-09-21 08:02:17 → heatsink joins (~heatsink@107-136-5-69.lightspeed.sntcca.sbcglobal.net)
2020-09-21 08:03:02 <edwardk> but the idea of a polykinded (:-) makes me super happy
2020-09-21 08:03:12 <edwardk> (:--) i guess to go with what :~~: does for HRefl
2020-09-21 08:03:16 → chaosmasttter joins (~chaosmast@p200300c4a70213017ae400fffe8093b8.dip0.t-ipconnect.de)
2020-09-21 08:03:39 <edwardk> would be any function from Sing a -> Sing b -- and can be lifted into Constraint!
2020-09-21 08:03:51 <edwardk> or maybe
2020-09-21 08:03:53 <Axman6> that last oe is excellent - do you have to construct the strings a char at a time?
2020-09-21 08:04:18 <edwardk> yeah they get built up out of nil and cons. because String is defined as [Char]
2020-09-21 08:04:20 <edwardk> and i can lift Char
2020-09-21 08:04:24 <edwardk> and I can lift []!
2020-09-21 08:04:36 <edwardk> i can give a little TH love to generating them
2020-09-21 08:05:14 → thc202 joins (~thc202@unaffiliated/thc202)
2020-09-21 08:05:31 → solonarv joins (~solonarv@astrasbourg-653-1-186-165.w90-13.abo.wanadoo.fr)
2020-09-21 08:05:37 <edwardk> oh, and i was able to overload things so that all the numeric types, injective or crappy like Nat can share a S and Z pattern
2020-09-21 08:06:16 <edwardk> er S and Z type family
2020-09-21 08:06:39 × heatsink quits (~heatsink@107-136-5-69.lightspeed.sntcca.sbcglobal.net) (Ping timeout: 265 seconds)
2020-09-21 08:06:45 → Gerula joins (~Gerula@unaffiliated/gerula)
2020-09-21 08:07:05 × aidecoe quits (~aidecoe@unaffiliated/aidecoe) (Ping timeout: 258 seconds)
2020-09-21 08:07:54 → aidecoe joins (~aidecoe@unaffiliated/aidecoe)
2020-09-21 08:08:44 <edwardk> > sing :: Sing '(1,Eq Int,Just (Z :: Int)) ==> Sing @(Nat,Constraint,(Maybe Int)) (1,Constraint Dict,Just 0)
2020-09-21 08:08:46 <lambdabot> <hint>:1:52: error: <hint>:1:52: error: parse error on input ‘@’
2020-09-21 08:09:02 → gnumonik joins (~gnumonik@c-73-170-91-210.hsd1.ca.comcast.net)
2020-09-21 08:09:02 × irc_user quits (uid423822@gateway/web/irccloud.com/x-yhvajookqrbnnurt) (Quit: Connection closed for inactivity)
2020-09-21 08:09:27 <edwardk> er didn't mean to > that
2020-09-21 08:10:09 → knupfer joins (~Thunderbi@dynamic-046-114-145-147.46.114.pool.telefonica.de)
2020-09-21 08:11:39 → Kaiepi joins (~Kaiepi@nwcsnbsc03w-47-55-157-9.dhcp-dynamic.fibreop.nb.bellaliant.net)
2020-09-21 08:12:10 × knupfer quits (~Thunderbi@dynamic-046-114-145-147.46.114.pool.telefonica.de) (Client Quit)
2020-09-21 08:12:31 → knupfer joins (~Thunderbi@dynamic-046-114-145-147.46.114.pool.telefonica.de)
2020-09-21 08:13:28 <Taneb> Is Z a pattern synonym there?
2020-09-21 08:13:50 <edwardk> Z there is actually a type family i have that expands to 0 in Nat and to various other things in other kinds
2020-09-21 08:14:01 × devalot quits (~ident@mail.pmade.com) (Ping timeout: 264 seconds)
2020-09-21 08:14:18 <Taneb> Right
2020-09-21 08:14:28 <edwardk> i hack Int to have a pair of injective type constructors for Z# and S# and it delegates to those for that kind
2020-09-21 08:15:30 <edwardk> testEquality (sing :: Sing Int) (sing :: Sing Int) ==> Just Refl
2020-09-21 08:16:08 <edwardk> i had to get fancy with S and Z because the lack of injectivity in Nat's (1+) approach to define Succ meant when you start building singletons on things like a Vec type that is indexed by a Nat you start breaking
2020-09-21 08:16:25 <edwardk> but if you use the fact that Natural now has Z and S which are injective for all kinds other than Nat it works fine
2020-09-21 08:17:35 → sQVe joins (~sQVe@unaffiliated/sqve)
2020-09-21 08:19:42 <edwardk> oh yeah, i forgot it is taken by the repl. i guess i need a better name
2020-09-21 08:19:45 <edwardk> er 'it'
2020-09-21 08:20:11 × Gerula quits (~Gerula@unaffiliated/gerula) (Ping timeout: 265 seconds)
2020-09-21 08:20:18 <edwardk> I and 'me' would be cute but the former too short. maybe You and you.
2020-09-21 08:20:41 <edwardk> no good ungendered singular pronouns
2020-09-21 08:21:57 × drbean quits (~drbean@TC210-63-209-64.static.apol.com.tw) (Ping timeout: 256 seconds)
2020-09-21 08:22:52 → heatsink joins (~heatsink@107-136-5-69.lightspeed.sntcca.sbcglobal.net)
2020-09-21 08:23:02 → Aquazi joins (uid312403@gateway/web/irccloud.com/x-bxvisodaildxgivh)
2020-09-21 08:23:17 <edwardk> ok, going with Me and me
2020-09-21 08:23:28 <edwardk> that way the template haskell function for building it is makeMe
2020-09-21 08:24:16 → Saten-san joins (~Saten-san@ip-83-134-202-127.dsl.scarlet.be)
2020-09-21 08:24:24 <edwardk> between that and makeNice this is becoming punnier than expected
2020-09-21 08:25:23 × denisse quits (~spaceCat@gateway/tor-sasl/alephzer0) (Ping timeout: 240 seconds)
2020-09-21 08:27:32 × knupfer quits (~Thunderbi@dynamic-046-114-145-147.46.114.pool.telefonica.de) (Read error: Connection reset by peer)
2020-09-21 08:27:39 × heatsink quits (~heatsink@107-136-5-69.lightspeed.sntcca.sbcglobal.net) (Ping timeout: 260 seconds)
2020-09-21 08:30:04 × mirrorbird quits (~psutcliff@2a00:801:44a:a00b:20c3:c64:eb15:73a2) (Quit: Leaving)
2020-09-21 08:31:25 <edwardk> and bugger
2020-09-21 08:32:23 <edwardk> there appears to be a bug where when i go to try to validate that i can't subvert things by using Sing on constraint, it yells about overlapping instances for StrictEq Constraint -- when there is no instance?
2020-09-21 08:32:28 <edwardk> i have one on Type
2020-09-21 08:32:38 <edwardk> but Constraint and Type are different types to the surface language
2020-09-21 08:32:47 <edwardk> but even so i only have the one instance
2020-09-21 08:35:15 <Axman6> time for a GHC bug report "Ed broke it again: Overlapping instances for StrictEq Constraint"
2020-09-21 08:35:32 → Gerula joins (~Gerula@unaffiliated/gerula)
2020-09-21 08:38:12 × danvet quits (~danvet@2a02:168:57f4:0:5f80:650d:c6e6:3453) (Quit: Leaving)
2020-09-21 08:38:29 <edwardk> ok, fixed it
2020-09-21 08:38:36 <edwardk> just crappy error reporting. whew
2020-09-21 08:43:43 → heatsink joins (~heatsink@107-136-5-69.lightspeed.sntcca.sbcglobal.net)
2020-09-21 08:43:56 <merijn> edwardk: You need to step up your GHC breaking, at least Iceland_Jack has got an error explicitly calling them out, why don't you? ;)
2020-09-21 08:45:02 <edwardk> merijn: i have a clip of simon shouting from the back of the room during a talk that he would change the compiler to make it stop allowing me to do something
2020-09-21 08:45:37 <merijn> :D
2020-09-21 08:45:58 → thir joins (~thir@p200300f27f0fc600ed2222922a5678d5.dip0.t-ipconnect.de)
2020-09-21 08:48:29 × heatsink quits (~heatsink@107-136-5-69.lightspeed.sntcca.sbcglobal.net) (Ping timeout: 258 seconds)
2020-09-21 08:50:32 × Saten-san quits (~Saten-san@ip-83-134-202-127.dsl.scarlet.be) (Quit: WeeChat 2.8)
2020-09-21 08:50:42 × thir quits (~thir@p200300f27f0fc600ed2222922a5678d5.dip0.t-ipconnect.de) (Ping timeout: 260 seconds)
2020-09-21 08:50:57 hackage hlatex 0.3.2 - A library to build valid LaTeX files https://hackage.haskell.org/package/hlatex-0.3.2 (NicolasPouillard)
2020-09-21 08:51:44 → zebrag joins (~inkbottle@aaubervilliers-654-1-112-47.w86-198.abo.wanadoo.fr)
2020-09-21 08:52:16 × inkbottle quits (~inkbottle@aaubervilliers-654-1-112-119.w86-198.abo.wanadoo.fr) (Ping timeout: 272 seconds)
2020-09-21 08:56:35 × dysfigured quits (dysfigured@2600:3c00::f03c:92ff:feb4:be75) (Remote host closed the connection)
2020-09-21 08:56:44 → dysfigured joins (dysfigured@2600:3c00::f03c:92ff:feb4:be75)
2020-09-21 08:57:33 → mirrorbird joins (~psutcliff@2a00:801:44a:a00b:20c3:c64:eb15:73a2)
2020-09-21 08:57:33 mirrorbird is now known as psut
2020-09-21 09:00:01 × unknown quits (~unknown@s91904426.blix.com) ()
2020-09-21 09:00:14 × avocado quits (renningmat@gateway/shell/matrix.org/x-cjscopkjowyvreqy) (Quit: Idle for 30+ days)
2020-09-21 09:00:30 × camlriot42 quits (camlriotma@gateway/shell/matrix.org/x-rtbhfsekxaemiuex) (Quit: Idle for 30+ days)
2020-09-21 09:02:52 → cpressey joins (~cpressey@88.144.93.20)
2020-09-21 09:05:13 <cpressey> Hi, I recently upgraded cabal from 1.24 (the version that ships with Ubuntu 18 LTS) to 3.0.2 and I'm seeing unusual behaviour: cabal build works, but doesn't detect when I've edited a source file, and cabal install tries to build and fails because it can't find my source files. I can post a minimal example in a gist if it helps.
2020-09-21 09:06:35 <[exa]> cpressey: do you have all modules listed in the cabal file? (otherwise, a MWE would certainly help)
2020-09-21 09:07:08 <maerwald> 3.0.2?
2020-09-21 09:07:27 <maerwald> that version doesn't exist
2020-09-21 09:07:44 <[exa]> probably meant 3.2.0.0?
2020-09-21 09:08:01 <cpressey> maerwald: "cabal-install version 3.0.0.0\ncompiled using version 3.0.2.0 of the Cabal library"
←Prev  Next→
Page 1 .. 107 108 109 110 111 112 113 114 115 116 117 .. 5022

All times are in UTC.