Home freenode/#haskell: Logs Calendar

Logs: freenode/#haskell

←Prev  Next→
Page 1 .. 88 89 90 91 92 93 94 95 96 97 98 .. 5022
— 502,152 events total
2020-09-20 11:21:18 × oo_miguel quits (~miguel@89-72-187-203.dynamic.chello.pl) (Client Quit)
2020-09-20 11:22:35 <gpvs> Hello. I can't make this compile:
2020-09-20 11:22:35 <gpvs> Class (Show type_self, AWord type_word) => Animal type_self where
2020-09-20 11:22:35 <gpvs> say :: type_self -> [type_word]
2020-09-20 11:22:35 <gpvs> I tried:
2020-09-20 11:22:35 <gpvs> Class Show type_self => Animal type_self where
2020-09-20 11:22:36 <gpvs> say :: AWord type_word => type_self -> [type_word]
2020-09-20 11:22:36 <gpvs> and it compiled, but then
2020-09-20 11:22:37 <gpvs> instance Animal AnimalSpecific where
2020-09-20 11:22:37 <gpvs> say (AnimalSpecific arrayOfInstancesOfAWord) = arrayOfInstanceOfAWord
2020-09-20 11:22:37 × gpvs quits (~gp@37.57.178.79) (Killed (Sigyn (Spam is off topic on freenode.)))
2020-09-20 11:23:39 → Amras joins (~Amras@unaffiliated/amras0000)
2020-09-20 11:23:48 × DirefulSalt quits (DirefulSal@gateway/vpn/privateinternetaccess/direfulsalt) (Remote host closed the connection)
2020-09-20 11:23:48 ChanServ sets mode +o ski
2020-09-20 11:23:53 → gpvs joins (~gp@37.57.178.79)
2020-09-20 11:23:54 <Cale> oops
2020-09-20 11:24:15 <gpvs> Hello. How do I paste multiline here not getting banned?
2020-09-20 11:24:22 → DirefulSalt joins (DirefulSal@gateway/vpn/privateinternetaccess/direfulsalt)
2020-09-20 11:24:26 <Rembane> gpvs: What error message do you get? Can you put it in a pastebin? See topic for information.
2020-09-20 11:24:33 <Rembane> gpvs: You can access topic by running the command /topic
2020-09-20 11:24:33 <Cale> try https://dpaste.com/
2020-09-20 11:24:39 <niko> ski: already lifted
2020-09-20 11:24:50 ChanServ sets mode -o ski
2020-09-20 11:24:53 <ski> ok
2020-09-20 11:25:10 → tchouri joins (~tchouri@gateway/tor-sasl/hekkaidekapus)
2020-09-20 11:25:12 <Rembane> edwardk: Was it 33 years since you used an overlapping instance last time?! :O
2020-09-20 11:25:30 <edwardk> pretty close
2020-09-20 11:25:36 <edwardk> i used one other really
2020-09-20 11:26:02 <int-e> Overlapping instances is the devil's way of leading you towards incoherent instances.
2020-09-20 11:26:03 <edwardk> but i was granted an indulgence by one of the simons, so that sin never existed to be forgiven
2020-09-20 11:26:40 <phadej> I think that my overlapped instance count is negative
2020-09-20 11:26:43 × hekkaidekapus quits (~tchouri@gateway/tor-sasl/hekkaidekapus) (Ping timeout: 240 seconds)
2020-09-20 11:27:00 <edwardk> here i'm trying to hack around the fact that 1 + isn't injective for Nat.
2020-09-20 11:27:05 <edwardk> So I've had to get creative
2020-09-20 11:27:08 <Rembane> edwardk: Seems legit
2020-09-20 11:27:37 <edwardk> There appears to be a pattern synonym I _can't_ write without injectivity on succ, despite the fact that the GADT version typechecks, i can't emulate the GADT right.
2020-09-20 11:28:06 <Rembane> I'm probably extremely dense here, but I cannot see why 1 + isn't injective. What have I missed?
2020-09-20 11:28:20 <phadej> nobody told GHC
2020-09-20 11:28:37 <Rembane> Oh
2020-09-20 11:28:44 <edwardk> in theory if i can get the type information at just the right point so that names are in scopes maybe i can unsafeCoerce a :~~: to make the proof i need
2020-09-20 11:29:03 <edwardk> Rembane: the builtin Nat kind is crippled
2020-09-20 11:29:20 <edwardk> + only computes will fully grounded numbers
2020-09-20 11:29:32 × jespada quits (~jespada@90.254.241.6) (Quit: Sleeping)
2020-09-20 11:29:44 <Cale> At the term level, you have infinity = Succ infinity, which also messes up the injectivity of 1+
2020-09-20 11:29:48 <Rembane> edwardk: How terrible is it to uncripple it?
2020-09-20 11:29:51 <edwardk> so i wind up in situations where i need to know 0 and 1+x are disjoint, or that 1+x = 1 + y => x + y
2020-09-20 11:29:58 <Cale> er, nevermind
2020-09-20 11:30:03 <Cale> It's just a fixed point
2020-09-20 11:30:07 → heatsink joins (~heatsink@107-136-5-69.lightspeed.sntcca.sbcglobal.net)
2020-09-20 11:30:32 <phadej> I think though that GHC knows some weak version of injectivity for (+) though, as otherwise one would get a lot more ambiguous type erros
2020-09-20 11:30:36 <edwardk> Rembane: that is a ghc hq thing. nats have been terrible for several years, so i'm not holding my breath.
2020-09-20 11:30:59 <ski> gpvs : do you understand the problem you're getting ? perhaps you want to make `Animal' a MPTC, parameterized by both `type_self' and `type_word' ? do you really need to make a type class at all ?
2020-09-20 11:31:06 <Rembane> edwardk: Got it. Then I assume that it isn't "just" to e-mail a patch and hope for the best.
2020-09-20 11:31:13 <edwardk> phadej: oh? afaict all it does it leave it dangling there as a stuck type family
2020-09-20 11:31:43 <edwardk> unless the args are fully grounded out by previous applications of the magic rule for the type family
2020-09-20 11:33:18 <gpvs> ski: wait a second please, forming dpaste from another PC
2020-09-20 11:33:27 × gehmehgeh quits (~ircuser1@gateway/tor-sasl/gehmehgeh) (Quit: Leaving)
2020-09-20 11:33:55 <phadej> edwardk: if you write foo :: Proxy (x + y) -> Proxy x -> (); foo _ _ = () -- it is accepted
2020-09-20 11:34:21 <phadej> clearly means that (+ y) is injective.
2020-09-20 11:34:25 × oxide quits (~lambda@unaffiliated/mclaren) (Ping timeout: 264 seconds)
2020-09-20 11:34:31 <phadej> "clearly"
2020-09-20 11:34:38 × heatsink quits (~heatsink@107-136-5-69.lightspeed.sntcca.sbcglobal.net) (Ping timeout: 256 seconds)
2020-09-20 11:35:22 → oxide joins (~lambda@unaffiliated/mclaren)
2020-09-20 11:35:50 <edwardk> hrmm
2020-09-20 11:36:51 → gehmehgeh joins (~ircuser1@gateway/tor-sasl/gehmehgeh)
2020-09-20 11:37:32 <edwardk> the (+) type family is weird
2020-09-20 11:37:38 <phadej> git grep -i "interaction with inerts" in GHC code
2020-09-20 11:37:49 <phadej> I just know that makes that `foo` code type-checks
2020-09-20 11:37:53 × Cale quits (~cale@CPEf48e38ee8583-CM0c473de9d680.cpe.net.cable.rogers.com) (Ping timeout: 272 seconds)
2020-09-20 11:38:09 <phadej> but how, ask someone else
2020-09-20 11:38:22 <phadej> (e.g. why it doesn't make partially applied + injective)
2020-09-20 11:38:51 × Turmfalke quits (~user@unaffiliated/siracusa) (Quit: Bye!)
2020-09-20 11:38:56 <phadej> but yes, wired-in magic type-families are weird.
2020-09-20 11:39:05 <edwardk> the fact that + has some kind of privileged f'd up position explains a bit of how i get errors with it i can't get elsewhere
2020-09-20 11:39:10 → dddddd_ joins (~dddddd@unaffiliated/dddddd)
2020-09-20 11:39:15 × NieDzejkob quits (~quassel@188.123.215.55) (Quit: https://quassel-irc.org - Chat comfortably. Anywhere.)
2020-09-20 11:39:31 <phadej> re ground terms
2020-09-20 11:39:40 <phadej> 5 + n ~ 8 does simplify to n ~ 3
2020-09-20 11:39:49 <gpvs> I seek to explain to GHC that I want a Class. Class's requirement has a function. Function's "return" type must be instance of another specific Class. Here is what I tried and errors I got: dpaste.com/FTAG9S4MQ , dpaste.com/EG5RM5HXY
2020-09-20 11:40:03 × Unhammer quits (~Unhammer@gateway/tor-sasl/unhammer) (Ping timeout: 240 seconds)
2020-09-20 11:40:24 <edwardk> yet it can't figure out 1 + n ~ 1 + m => n ~ m
2020-09-20 11:40:29 <phadej> no
2020-09-20 11:40:34 <phadej> nobody told it *that* :)
2020-09-20 11:40:42 <phadej> there isn't ring-solver in GHC
2020-09-20 11:40:53 <phadej> (it's available as a plugin)
2020-09-20 11:41:09 <phadej> https://hackage.haskell.org/package/ghc-typelits-natnormalise
2020-09-20 11:41:12 <edwardk> yeah
2020-09-20 11:41:25 <edwardk> was going to try the natnormalize plugin to see if i could use it to compile the pattern i need
2020-09-20 11:41:37 × dddddd quits (~dddddd@unaffiliated/dddddd) (Ping timeout: 264 seconds)
2020-09-20 11:41:58 <phadej> I guess Christiaan would appreaciate if you tell him that *it works for you* ;)
2020-09-20 11:42:09 → NieDzejkob joins (~quassel@188.123.215.55)
2020-09-20 11:42:28 <ski> gpvs : so you want to associate each `type_self', that you make an instance for, with a particular `type_word'
2020-09-20 11:42:54 <edwardk> let me add the example i'm fighting with to the repo
2020-09-20 11:43:05 → utopic_int0x80 joins (~lucid_0x8@188.253.237.87)
2020-09-20 11:44:17 <gpvs> ski: If I got you correctly: I may, but where is no need to. AWord is good enough abstraction for Animal-s to work with, there is no need to bind particular animals to particular words
2020-09-20 11:44:29 <kicov> Got a few cpsy + liquid haskell examples: https://dpaste.com/3YX484ND7 and https://dpaste.com/FHMQ5DZ44 - just wondering how both examples could work using single cpsy annotation.
2020-09-20 11:44:41 <gpvs> ski: and if I must to associate it, how would I do that?
2020-09-20 11:44:46 <edwardk> oh weeee, more regressions
2020-09-20 11:44:47 × alx741 quits (~alx741@186.178.110.2) (Ping timeout: 265 seconds)
2020-09-20 11:45:42 → __Joker joins (~Joker@180.151.105.65)
←Prev  Next→
Page 1 .. 88 89 90 91 92 93 94 95 96 97 98 .. 5022

All times are in UTC.