Logs: freenode/#haskell
| 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.