Home freenode/#haskell: Logs Calendar

Logs: freenode/#haskell

←Prev  Next→
Page 1 .. 293 294 295 296 297 298 299 300 301 302 303 .. 5022
502,152 events total
2020-09-29 14:45:07 × xff0x quits (~fox@2001:1a81:53b0:3c00:65ac:b49c:d7d6:af9b) (Ping timeout: 240 seconds)
2020-09-29 14:45:16 <ski> hm, to a zeroth approximation, something like `Gen (exists b. cat a b)', but then one'd like to keep using that `b' onwards ..
2020-09-29 14:46:10 × nbloomf quits (~nbloomf@2600:1700:83e0:1f40:85d7:28a9:e9cf:26c5) (Quit: My MacBook has gone to sleep. ZZZzzz…)
2020-09-29 14:46:18 xff0x joins (~fox@2001:1a81:53b0:3c00:65ac:b49c:d7d6:af9b)
2020-09-29 14:46:42 ddellacosta joins (~dd@86.106.121.168)
2020-09-29 14:47:45 nbloomf joins (~nbloomf@2600:1700:83e0:1f40:f198:f10:f56d:4606)
2020-09-29 14:48:45 heatsink joins (~heatsink@107-136-5-69.lightspeed.sntcca.sbcglobal.net)
2020-09-29 14:49:26 <turion> ski: Yes. I guess there is a way to do this with an existential type somehow. Or maybe continuations...? But I'm wondering whether something like this has been studied systematically, because it must show up every time someone wants to write a generator for a GADT or existential type
2020-09-29 14:50:32 × snakemasterflex quits (~snakemast@213.100.206.23) (Read error: Connection reset by peer)
2020-09-29 14:50:57 snakemasterflex joins (~snakemast@213.100.206.23)
2020-09-29 14:51:33 <ski> if we imagine `class SomeArbitrary f where someArbitrary :: Gen (..f..)', one could have `instance SomeArbitrary (cat a) => SomeArbitrary (FreeCat cat a) where ..' with `someArbitrary :: Gen (exists b. SomeArbitrary (cat b) *> FreeCat cat a b)', maybe ?
2020-09-29 14:52:22 <ski> perhaps the constraint here could be an associated type
2020-09-29 14:52:40 <z0> dminuoso: "For each test, it will run an output instruction indicating how far the result of the test was from the expected value, where 0 means the test was successful. Non-zero outputs mean that a function is not working correctly; check the instructions that were run before the output instruction to see which one failed."
2020-09-29 14:52:45 herasmus joins (~mb@91-160-105-150.subs.proxad.net)
2020-09-29 14:52:58 <z0> but ignoring this, it now works as supposed
2020-09-29 14:53:00 <z0> thanks
2020-09-29 14:53:26 × heatsink quits (~heatsink@107-136-5-69.lightspeed.sntcca.sbcglobal.net) (Ping timeout: 256 seconds)
2020-09-29 14:54:03 <turion> ski: I'm not sure how exactly the generator case for Seq typechecks
2020-09-29 14:54:05 <Cale> I can imagine writing a generator something like (Arbitrary b, CoArbitrary a) => FreeCat (->) a b
2020-09-29 14:54:32 <Cale> which generated Seq terms by picking from a finite list of types that are known to have Arbitrary and CoArbitrary instances
2020-09-29 14:54:46 <z0> int-e: maybe i read too much into the sentence I pasted above
2020-09-29 14:54:55 <Cale> oops
2020-09-29 14:55:05 <Cale> I meant Gen (FreeCat (->) a b) obviously
2020-09-29 14:55:13 <ski> Cale : imagine `cat' is a basic GADT ?
2020-09-29 14:55:38 <turion> Cale: Yes, I guess that can work. Is there a framework that does this?
2020-09-29 14:56:05 <turion> Imagine we'd go on and do free arrows, and we want to reuse this list of types, how to abstract it
2020-09-29 14:57:09 <dminuoso> z0: Still, where does it say it has to halt?
2020-09-29 14:58:11 <Cale> I was thinking cat is a category
2020-09-29 14:58:11 <Cale> No, you'd have to write the thing yourself, and it will include too many details of this structure to be really generalisable
2020-09-29 14:58:11 <Cale> Or maybe I just lack the imagination to figure out how to generalise it
2020-09-29 14:58:12 <Cale> But it won't be a difficult thing to write
2020-09-29 14:58:27 <dminuoso> z0: `Finally, the program will output a diagnostic code and immediately halt. ` means it will halt *after* the final diagnostic code.
2020-09-29 14:58:58 heatsink joins (~heatsink@107-136-5-69.lightspeed.sntcca.sbcglobal.net)
2020-09-29 14:59:07 <Cale> Oh, well, if you take a function of type (forall a b. (CoArbitrary a, Arbitrary b) => cat a b), that's the only real missing piece
2020-09-29 14:59:36 <Cale> Or you could just insist on an instance Arbitrary (cat a b)
2020-09-29 14:59:42 herasmus is now known as Herasmus
2020-09-29 14:59:47 × mnrmnaugh quits (~mnrmnaugh@unaffiliated/mnrmnaugh) (Ping timeout: 240 seconds)
2020-09-29 15:00:13 <turion> Cale, let's assume we have (forall a b. (CoArbitrary a, Arbitrary b) => cat a b) already
2020-09-29 15:00:32 <Cale> It's the Free case which is more challenging than the Seq case. The Seq case just amounts to making a random decision about which type to factor through, and making acceptable choices for it
2020-09-29 15:01:00 <turion> Cale: It's this random decision of a type that I want to abstract
2020-09-29 15:01:17 mnrmnaugh joins (~mnrmnaugh@unaffiliated/mnrmnaugh)
2020-09-29 15:01:24 <Cale> oneof :: [Gen a] -> Gen a
2020-09-29 15:01:36 <Cale> ^^ use that :)
2020-09-29 15:01:40 <z0> dminuoso: well, you are not wrong :/
2020-09-29 15:01:42 <ski> for some applications, it seems it would be eaiser to pick the value first, and let the choice of that decide the type
2020-09-29 15:02:13 Lord_of_Life_ joins (~Lord@unaffiliated/lord-of-life/x-0885362)
2020-09-29 15:02:14 <Cale> You can imagine writing the generator which generates a random Seq term by always factoring through Integer
2020-09-29 15:02:21 <Cale> Or String or some such
2020-09-29 15:02:25 <Cale> right?
2020-09-29 15:02:28 <turion> We can also represent the free category differently:
2020-09-29 15:02:28 <turion> data FreeCat cat a b where
2020-09-29 15:02:28 <turion> Id :: FreeCat cat a a
2020-09-29 15:02:28 <turion> Comp :: cat a b -> FreeCat cat b c -> FreeCat cat a c
2020-09-29 15:02:35 <Cale> So you can combine those together with oneof
2020-09-29 15:02:53 <turion> ski: Yes, maybe there is a generator for cat a b that knows what the output type should be
2020-09-29 15:03:10 <turion> Cale: Yes, that part I know how to do. It's more that I'd like to abstract it
2020-09-29 15:03:19 <turion> Or rather to see whether someone has already done that
2020-09-29 15:03:28 <Cale> If you're writing the general instance, it'll just amount to pretty much Seq arbitrary arbitrary a bunch of times, but with type signatures on the arbitrary terms
2020-09-29 15:03:42 <Cale> er, Seq <$> arbitrary <*> arbitrary rather
2020-09-29 15:03:44 × heatsink quits (~heatsink@107-136-5-69.lightspeed.sntcca.sbcglobal.net) (Ping timeout: 272 seconds)
2020-09-29 15:03:48 <turion> Because it seems like an ubiquitous problem
2020-09-29 15:03:51 perdent joins (~blah@101.175.129.224)
2020-09-29 15:03:55 <ski> e.g. perhaps you have `data Fun :: * -> * -> * where Not :: Fun Bool Bool; Chr :: Fun Int Char; Ord :: Fun Char Int; Succ :: Fun Int Int; IsSpace :: Fun Char Bool', or something like that
2020-09-29 15:03:57 <Cale> hmm
2020-09-29 15:04:00 <z0> dminuoso: teaches me to keep no assumptions
2020-09-29 15:04:11 <ski> and then you want to generate `FreeCat Fun'
2020-09-29 15:04:43 luke joins (~luke@bitnomial/staff/luke)
2020-09-29 15:04:50 <ski> turion : i don't think that representation makes a huge difference to the problem here
2020-09-29 15:04:58 <turion> ski: That's a good example
2020-09-29 15:05:01 × Lord_of_Life quits (~Lord@unaffiliated/lord-of-life/x-0885362) (Ping timeout: 264 seconds)
2020-09-29 15:05:03 <Cale> Oh, also, Id will be interesting, actually
2020-09-29 15:05:10 Lord_of_Life_ is now known as Lord_of_Life
2020-09-29 15:05:11 <Cale> hmm
2020-09-29 15:05:14 Noldorin joins (~noldorin@unaffiliated/noldorin)
2020-09-29 15:05:22 <Cale> Unless you demand Typeable a, Typeable b in your instance head
2020-09-29 15:05:38 <Cale> So that you know when you're allowed to attempt to produce Id terms
2020-09-29 15:05:39 <turion> ski: No the representation isn't that important, I agree. (That was kind of the point. I wanted to draw the attention away from the difference between Seq and Free)
2020-09-29 15:07:11 <ski> Cale : hm, point
2020-09-29 15:07:18 <ski> well
2020-09-29 15:07:37 <ski> Cale : i guess you could allow `Id' for any `a' of the right kind
2020-09-29 15:08:02 <turion> Assume I have an interpreter for this Fun type and I want to quickcheck that it preserves composition from FreeCat Fun to its semantic domain. But in a very general setting, where I don't have to fix the input and output types
2020-09-29 15:08:47 × perdent quits (~blah@101.175.129.224) (Ping timeout: 260 seconds)
2020-09-29 15:09:05 heatsink joins (~heatsink@107-136-5-69.lightspeed.sntcca.sbcglobal.net)
2020-09-29 15:09:08 × nbloomf quits (~nbloomf@2600:1700:83e0:1f40:f198:f10:f56d:4606) (Quit: My MacBook has gone to sleep. ZZZzzz…)
2020-09-29 15:09:12 <Cale> ski: Well, if you're writing an instance (...) => Arbitrary (FreeCat cat a b), you need to know whether a ~ b so that you know whether it's valid to generate Id at all.
2020-09-29 15:09:34 <Cale> If a and b are not the same type, you can't generate Id terms, but you can still generate Comp/Free terms
2020-09-29 15:09:47 <ski> yea. but i'm more considering `Arbitrary (exists b. FreeCat cat a b)' :)
2020-09-29 15:09:56 <Cale> hmmm
2020-09-29 15:10:03 <Cale> fair enough :)
2020-09-29 15:10:16 <ski> (since we need something like that, for the composition)
2020-09-29 15:10:47 <ski> (or else, i guess, randomly generating `b0' and `b1', which are `Typeable', and then comparing that they're the same ..)
2020-09-29 15:10:56 <ski> (.. but that's not that nice)
2020-09-29 15:11:05 × Sanchayan quits (~Sanchayan@136.185.169.201) (Quit: leaving)
2020-09-29 15:11:27 <turion> Maybe at the end we need to build an Arbitrary (exists a b . FreeCat cat a b)
2020-09-29 15:11:55 <turion> (possibly with Typeable, Arbitrary, Coarbitrary etc. thrown in
2020-09-29 15:12:27 hackage th-orphans 0.13.11 - Orphan instances for TH datatypes https://hackage.haskell.org/package/th-orphans-0.13.11 (ryanglscott)
2020-09-29 15:12:30 nbloomf joins (~nbloomf@2600:1700:83e0:1f40:6d38:c363:743b:50e9)
2020-09-29 15:13:17 alp joins (~alp@88.126.45.36)
2020-09-29 15:13:38 × heatsink quits (~heatsink@107-136-5-69.lightspeed.sntcca.sbcglobal.net) (Ping timeout: 260 seconds)
2020-09-29 15:13:53 <ski> turion : the `Arbitrary' and `Coarbitrary' would be if `cat' say had constructors taking functions

All times are in UTC.