Introduction of ConstCat instance unexpectedly changing result of toCcc

[null-a]

I'm playing with a toy example of defining my own categorical instances in order to get a feel for using the plugin, and I'm running into unexpected behavior. I have a data type to record the categorical expressions generated, and I'm trying to transform a simple function to that. Note that my data type has a constructor that isn't covered by any of the categorical type classes, so I'm using unCcc with that.

With the code as is, this all works fine. For example, the function:

f :: () -> (Bool, Bool)
f () = let x = prim 0.0
           y = prim 0.0
       in (x,y)

... is transformed into:

Comp (Const ?) (Comp (Dup) (Par (Prim) (Prim)))

... which is correct. The unexpected part, is that when I uncomment this ConstCat instance and re-run stack run, the output changes to:

Comp (Dup) (Par (Const ?) (Const ?))

... which is not what I expect -- the Prim arrows have disappeared.

I'd be grateful to hear any suggestions about what might be happening and how I might fix this.

Here's the output I see with the plugin debug flags set on the erroneous case:

``` concat-example-0.1.0.0: unregistering (local file changes: src/MyLib.hs) concat-example> configure (lib + exe) Configuring concat-example-0.1.0.0... concat-example> build (lib + exe) Preprocessing library for concat-example-0.1.0.0.. Building library for concat-example-0.1.0.0.. [2 of 2] Compiling MyLib Preprocessing executable 'concat-example-exe' for concat-example-0.1.0.0.. Building executable 'concat-example-exe' for concat-example-0.1.0.0.. [1 of 2] Compiling Main [MyLib changed] go ccc C: f :: () -> (Bool, Bool) Doing top unfold toCcc' f --> toCcc' @ C @ () @ (Bool, Bool) (\ (ds_d3uJ :: ()) -> case ds_d3uJ of { () -> lvl_s7JJ }) go ccc C: \ (ds_d3uJ :: ()) -> case ds_d3uJ of { () -> lvl_s7JJ } :: () -> (Bool, Bool) Doing lam Case nullary toCcc' \ (ds_d3uJ :: ()) -> case ds_d3uJ of { () -> lvl_s7JJ } --> toCcc' @ C @ () @ (Bool, Bool) (\ (ds_d3uJ :: ()) -> lvl_s7JJ) go ccc C: \ _ [Occ=Dead] -> lvl_s7JJ :: () -> (Bool, Bool) Couldn't build dictionary for const @ C @ (Bool, Bool) @ () :: (ConstCat C (Bool, Bool), Ok C ()) => (Bool, Bool) -> C () (ConstObj C (Bool, Bool)): no bindings Doing lam unfold toCcc' \ _ [Occ=Dead] -> lvl_s7JJ --> toCcc' @ C @ () @ (Bool, Bool) (\ _ [Occ=Dead] -> (lvl_s7JG, lvl_s7JI)) go ccc C: \ _ [Occ=Dead] -> (lvl_s7JG, lvl_s7JI) :: () -> (Bool, Bool) Couldn't build dictionary for const @ C @ (Bool, Bool) @ () :: (ConstCat C (Bool, Bool), Ok C ()) => (Bool, Bool) -> C () (ConstObj C (Bool, Bool)): no bindings Doing lam Pair toCcc' \ _ [Occ=Dead] -> (lvl_s7JG, lvl_s7JI) --> &&& @ C @ () @ Bool @ Bool ($fProductCatC, $fMonoidalPCatC) (($fYes1ka @ * @ (), $fYes1ka @ * @ Bool, $fYes1ka @ * @ Bool) `cast` (((%,,%) (Sym (R:OkC[0]) <()>_N) (Sym (R:OkC[0]) _N) (Sym (R:OkC[0]) _N))_R :: (Yes1 (), Yes1 Bool, Yes1 Bool) ~R# (Ok C (), Ok C Bool, Ok C Bool))) (toCcc' @ C @ () @ Bool (\ _ [Occ=Dead] -> lvl_s7JG)) (toCcc' @ C @ () @ Bool (\ _ [Occ=Dead] -> lvl_s7JI)) go ccc C: \ _ [Occ=Dead] -> lvl_s7JG :: () -> Bool Doing lam mkConst' toCcc' \ _ [Occ=Dead] -> lvl_s7JG --> const @ C @ Bool @ () $fConstCatCBool (($fYes1ka @ * @ ()) `cast` (Sub (Sym (R:OkC[0])) <()>_N :: Yes1 () ~R# Ok C ())) lvl_s7JG go ccc C: \ _ [Occ=Dead] -> lvl_s7JI :: () -> Bool Doing lam mkConst' toCcc' \ _ [Occ=Dead] -> lvl_s7JI --> const @ C @ Bool @ () $fConstCatCBool (($fYes1ka @ * @ ()) `cast` (Sub (Sym (R:OkC[0])) <()>_N :: Yes1 () ~R# Ok C ())) lvl_s7JI ccc final: [lvl_s7JG :: Bool [LclId, Unf=Unf{Src=, TopLvl=True, Value=False, ConLike=False, WorkFree=False, Expandable=False, Guidance=IF_ARGS [] 30 0}] lvl_s7JG = prim (D# 0.0##), lvl_s7JI :: Bool [LclId, Unf=Unf{Src=, TopLvl=True, Value=False, ConLike=False, WorkFree=False, Expandable=False, Guidance=IF_ARGS [] 30 0}] lvl_s7JI = prim (D# 0.0##), lvl_s7JJ :: (Bool, Bool) [LclId, Unf=Unf{Src=, TopLvl=True, Value=True, ConLike=True, WorkFree=True, Expandable=True, Guidance=IF_ARGS [] 10 30}] lvl_s7JJ = (lvl_s7JG, lvl_s7JI), f :: () -> (Bool, Bool) [LclIdX, Arity=1, Unf=Unf{Src=, TopLvl=True, Value=True, ConLike=True, WorkFree=True, Expandable=True, Guidance=ALWAYS_IF(arity=1,unsat_ok=True,boring_ok=True)}] f = \ (ds_d3uJ :: ()) -> case ds_d3uJ of { () -> lvl_s7JJ }, $trModule_s4GG :: Addr# [LclId, Unf=Unf{Src=, TopLvl=True, Value=True, ConLike=True, WorkFree=True, Expandable=True, Guidance=IF_ARGS [] 20 0}] $trModule_s4GG = "main"#, $trModule_s4GH :: TrName [LclId, Unf=Unf{Src=, TopLvl=True, Value=True, ConLike=True, WorkFree=True, Expandable=True, Guidance=IF_ARGS [] 10 20}] $trModule_s4GH = TrNameS $trModule_s4GG, $trModule_s4GI :: Addr# [LclId, Unf=Unf{Src=, TopLvl=True, Value=True, ConLike=True, WorkFree=True, Expandable=True, Guidance=IF_ARGS [] 20 0}] $trModule_s4GI = "Main"#, $trModule_s4GJ :: TrName [LclId, Unf=Unf{Src=, TopLvl=True, Value=True, ConLike=True, WorkFree=True, Expandable=True, Guidance=IF_ARGS [] 10 20}] $trModule_s4GJ = TrNameS $trModule_s4GI, $trModule :: Module [LclIdX, Unf=Unf{Src=, TopLvl=True, Value=True, ConLike=True, WorkFree=True, Expandable=True, Guidance=IF_ARGS [] 10 30}] $trModule = Module $trModule_s4GH $trModule_s4GJ, main_s6ni :: String [LclId, Unf=Unf{Src=, TopLvl=True, Value=False, ConLike=False, WorkFree=False, Expandable=False, Guidance=IF_ARGS [] 190 0}] main_s6ni = $fShowC_$cshow @ () @ (Bool, Bool) (reveal @ C @ () @ (Bool, Bool) (&&& @ C @ () @ Bool @ Bool ($fProductCatC, $fMonoidalPCatC) (($fYes1ka @ * @ (), $fYes1ka @ * @ Bool, $fYes1ka @ * @ Bool) `cast` (((%,,%) (Sym (R:OkC[0]) <()>_N) (Sym (R:OkC[0]) _N) (Sym (R:OkC[0]) _N))_R :: (Yes1 (), Yes1 Bool, Yes1 Bool) ~R# (Ok C (), Ok C Bool, Ok C Bool))) (const @ C @ Bool @ () $fConstCatCBool (($fYes1ka @ * @ ()) `cast` (Sub (Sym (R:OkC[0])) <()>_N :: Yes1 () ~R# Ok C ())) lvl_s7JG) (const @ C @ Bool @ () $fConstCatCBool (($fYes1ka @ * @ ()) `cast` (Sub (Sym (R:OkC[0])) <()>_N :: Yes1 () ~R# Ok C ())) lvl_s7JI))), main :: IO () [LclIdX, Arity=1, Unf=Unf{Src=, TopLvl=True, Value=True, ConLike=True, WorkFree=True, Expandable=True, Guidance=IF_ARGS [] 40 60}] main = hPutStr' stdout main_s6ni True, main_s7JA :: State# RealWorld -> (# State# RealWorld, () #) [LclId, Arity=1, Unf=Unf{Src=, TopLvl=True, Value=True, ConLike=True, WorkFree=True, Expandable=True, Guidance=IF_ARGS [] 20 60}] main_s7JA = runMainIO1 @ () main, main :: IO () [LclIdX, Arity=1, Unf=Unf{Src=, TopLvl=True, Value=True, ConLike=True, WorkFree=True, Expandable=True, Guidance=ALWAYS_IF(arity=0,unsat_ok=True,boring_ok=True)}] main = main_s7JA `cast` (Sym (N:IO[0] <()>_R) :: (State# RealWorld -> (# State# RealWorld, () #)) ~R# IO ())] ```

P.S. Thanks for sharing this wonderful work!

[conal]

I’m glad to see that you’re giving this project a spin!

I would indeed expect const x . f to get rewritten to const x, and there’s an explicit rule for doing so. Other rewrite rules can interfere in some cases. Does that rewrite raise concerns for you? Your example suggests an additional useful rule: const x &&& const y = const (x,y) (or variant). From your definition, I’d expect the whole thing to get rewritten to const p or unitArrow p for a suitable p.

[null-a]

Thanks @conal!

I would indeed expect const x . f to get rewritten to const x

Yes, me too. I think perhaps my Comp constructor, which is left-to-right composition, was confusing things.

Either way, I've now simplified my example highlighting (what I think is) the problem, so let me share that with you:

I'm now transforming this function:

f :: () -> Bool
f () = prim 0.0

Where:

prim :: Double -> Bool
prim = unCcc Prim

... and Prim is a constructor of a datatype:

data C :: * -> * -> * where
  Comp :: C a b -> C b c -> C a c
  Const :: Show b => b -> C a b
  Prim :: C Double Bool
  -- more constructors ...

(See Main.hs and MyLib.hs for the full code.)

This initially works as expected -- the function f is transformed in to Comp (Const ?) (Prim). (Again, Comp is left-to-right composition. Const ? is a constant arrow, and the ? just stems from my odd Show instance.)

However, when I uncomment this innocuous seeming ConstCat instance, the output changes from Comp (Const ?) (Prim) to Const ?. (As though the uncommenting had introduced a new rule f . const x = const x.)

I hope that description makes sense?

[conal]

I would indeed expect const x . f to get rewritten to const x

Yes, me too. I think perhaps my Comp constructor, which is left-to-right composition, was confusing things.

Thanks! I’m afraid I responded hurriedly and assumed Comp was the other way around without following the source links you kindly provided.

However, when I uncomment this innocuous seeming ConstCat instance, the output changes from Comp (Const ?) (Prim) to Const ?. (As though the uncommenting had introduced a new rule f . const x = const x.)

I hope that description makes sense?

Indeed it does, now that I’m reading you more carefully.

I think I know what’s going on here (thanks to having been bitten similarly). With the “innocuous seeming ConstCat instance” (for Bool), you’re allowing const (prim 0.0) to be translated to Const (prim 0.0), since prim 0.0 :: Bool. Without that instance, the transformation for function application under lambdas gets applied instead, in which case, prim and 0.0 get translated separately. One subtle point here is that you never evaluate prim 0.0, because your show is non-strict in the argument to Const, so we see “Const ?” rather than “Const” and then an error from trying to evaluate unCcc Prim.

Since you have a Show constraint in your Const constructor, how about changing the corresponding show clause to show the argument? If my hunch is right, you’ll encounter the the unCcc “oops” error

[null-a]

If my hunch is right, you’ll encounter the the unCcc “oops” error

You're right -- I made the change you suggested and I'm seeing exactly that.

Is there a way I can have both of the ConstCat instances defined, and still see Comp (Const 0.0) Prim rather than the error?

[conal]

Is there a way I can have both of the ConstCat instances defined, and still see Comp (Const 0.0) Prim rather than the error?

I don’t think so, since the ConstCat C Bool instance exactly directs the plugin to insert Bool-valued constants whenever \ x -> c is encountered for Core expressions c :: Bool not involving x. Here, the expression c is prim 0.0, which is undefined.

If you want to define prim for (->) as well as for C, you can do so by making prim the method of a new class and give two instances. (Really, I think you’d need to do as in the tedious AltCat-vs-Category split to avoid premature method inlining. Sigh.)

What motivates you to want the Core C Bool instance and yet not constant-fold prim 0.0 at compile time?

I’m very much up for reconsidering some of the choices I made around constant folding criteria. Discussion & suggestions most welcome.

[null-a]

Thanks for the insights, this is helpful!

I'm imagining that my C a b represents a probability distribution over values of type b, parameterized by (or conditioned on) a value of type a.

My Prim :: C Double Bool could represent a primitive Bernoulli distribution -- a distribution over {True,False} parametized by the probability for True. I'll call this Bern from now on.

I'm imagining using your plugin to transform a Haskell function in to a value of my type C a b, which I'll then interpret further. For concreteness, we might imagine interpreting a C a b as a sampler, i.e. as something like a function a -> Random b.

I've updated my example to implement exactly this. (Main.hs, MyLib.hs)

As a simple example, I'd like to be able to describe the uniform distribution over Bool like so:

uniform :: () -> Bool
uniform () = bern 0.5

(Here bern = unCcc Bern :: Double -> Bool is my primitive Bernoulli distribution.)

My main function demonstrates this working as I had hoped. uniform is transformed to Comp (Const 0.5) Bern, which I then turn into a sampler, which I can run in order to draw a bunch of samples. So far so good!

What motivates you to want the Core C Bool instance

Here's a contrived example of why I'd like to add a ConstCat instance for Bool to what I have:

contrivedUniform :: () -> Bool
contrivedUniform () = if bern 0.5 then False else True

After running this through the plugin and then sample, I'm hoping this will also produce a sampler for the uniform distribution over Bool.

I believe I need the ConstCat instance for the Bool literals, but once I add that I'm seeing the Oops: unCcc' called error, presumably for the reasons we're discussing here.

and yet not constant-fold prim 0.0 at compile time?

I'm struggling to answer this precisely. Instead, I can only gesture towards things which are surprising or confusing to me. (Sorry I'm not able to do better!)

I think my expectation was that a Haskell function such as uniform would first be transformed into something like an expression in abstract categorical vocabulary, with the mapping to the target category happen after.

So uniform = const (bern 0.5) in Haskell code becomes bern . const 0.5 in abstract categorical vocabulary, which becomes Comp (Const 0.5) Bern when mapped to my target category.

It seems important here that even though the Haskell expression involves application, the expression in the categorical vocab doesn't, since my target category (values of type C a b) doesn't have application.

I became confused when you pointed out that the plugin might directly rewrite const (bern 0.5) to Const (bern 0.5). This seems problematic for my case, since I don't see how we could then translate bern 0.5, given that I don't have application in my target category.

So perhaps the problem is that I have assumed I can use this without a ClosedCat instance, and that's not the case?

[conal]

Thanks for these explanations, which help me see your intentions more clearly. I’m quite interested in seeing compiling-to-categories used for probabilistic computation.

I understand now why there can’t be a definition of bern for (->). I’ve run into some similar situations and am happy to see another, as I suspect there’s something interesting and valuable to learn from these cases.

I believe I need the ConstCat instance for the Bool literals, but […]

Maybe you do need this instance, but I don’t yet see why. Perhaps so that you can translate other constant boolean expressions. Even if you don’t need a ConstCat C Bool instance, however, I worry that you will run into the same difficulty with types other than Bool, particularly Double.

It seems important here that even though the Haskell expression involves application, the expression in the categorical vocab doesn’t, since my target category (values of type C a b) doesn’t have application.

I became confused when you pointed out that the plugin might directly rewrite const (bern 0.5) to Const (bern 0.5). This seems problematic for my case, since I don’t see how we could then translate bern 0.5, given that I don’t have application in my target category.

Really, the plugin would rewrite toCcc (const (bern 0.5)) to Const (bern 0.5) and then leave the bern 0.5 alone, since it’s not under a toCcc. Your category would not know or care about (nor be able to examine) the (Haskell/Core) expression that denotes its argument (crucial for tractable, sound reasoning).

So perhaps the problem is that I have assumed I can use this without a ClosedCat instance, and that’s not the case?

The topic of closure may indeed arise, but the plugin only introduces that vocabulary when it’s available (i.e., for closed target categories). Closure is handy and leads to more compact translations, but I’ve tried not to rely on it.

[conal]

I’m intrigued with your sample definition. It looks like there’s another category wanting to be made explicit here, wrapping a -> Rand b. Then another functor that relates this more semantic category with your current more syntactic category, with both steps being simpler and possibly more useful functors.

Remember that instances Category should really be categories, including the laws, despite Haskell’s type system being too weak to catch violations. Have you considered whether your C really is a category (i.e., satisfies the laws)? (Likewise for the Category subclasses.)

[null-a]

I’m quite interested in seeing compiling-to-categories used for probabilistic computation.

Great! There are one or two things in that general area that I hope to try, once I'm over this initial hurdle.

Have you considered whether your C really is a category

That's a good point. To side-step this, we could just consider your Syn category, since (having just tried it) I now see that it has similarly confusing (to me) behavior. That prompts the following question: Can I add primitive arrows (beyond those provided by the type classes) to e.g. Syn?

For example, I can define:

primitive :: Syn Double Bool
primitive = app0 "primitive"

... and successfully combine that with other values of type Syn. e.g. I can write:

foo :: Syn () Bool
foo = primitive . const 0.5
-- λ> foo
-- primitive . const 0.5

My expectation was that I would be able to generate the value foo using the plugin, with something like:

primitive' :: Double -> Bool
primitive' = unCcc primitive

main :: IO ()
main = print $ toCcc @Syn (\_ -> primitive' 0.5)

... but if I run that I get Oops: unCcc' called, which makes me wonder whether a misunderstanding of how to introduce new primitives is my un-doing?

(If fact, I can't even do toCcc @Syn primitive', since that gives me Oops: toCcc' called. Urghh, I think I might be out of my depth!)

(The full code for this is here.)

[conal]

Have you considered whether your C really is a category

That’s a good point. To side-step this,

The meaning and correctness of compiling to categories depends on having a genuine category as target and a homomorphism that relates mathematical functions to that category. For this fundamental reason, I encourage facing these questions early and directly. Moreover, these questions often have lovely answers from which much else follows inevitably.

That said, I’m very interested in exploring cases in which we don’t know how to apply this neat, well-defined homomorphism story, and probabilistic programming may well be one. I wonder: can we find a compelling & precise specification for what we’re trying to accomplish here, as a homomorphism or otherwise?

we could just consider your Syn category, since (having just tried it) I now see that it has similarly confusing (to me) behavior. That prompts the following question: Can I add primitive arrows (beyond those provided by the type classes) to e.g. Syn?

The plugin knows about only a few of the class methods. Most of the translation is simple and generic, and works by assuming that toCcc is a homomorphism for every class operation to which it’s applied if that operation is instantiated at (->). The (->) operation is replaced by the corresponding operation for the target category if it’s available. You can easily add additional classes. For this technique, the catch is that the methods must exist for (->) in order for toCcc to be applicable and thus for the plugin to translate to your desired category/interpretation. We can give a bogus (->) instance, but then we’ll get the same constant-folding error. The other technique I’ve experimented with is unCcc, which purports to convert from your category to (->). As you may have surmised, unCcc has no actual implementation. Its purpose is only to cancel out with a toCcc applied to it, thanks to a rewrite rule. Two things can go wrong, however:

• No toCcc gets applied, or a toCcc to a category other than the one used with the unCcc, in which cases cancellation won’t happen.
• Constant folding can trigger evaluation, as in your foo example with Syn.

We can explore two paths for resolution:

• Search for a clear & compelling specification, including a computable model of something like “probabilistic functions” and relationship between this model and computable functions. This relationship must be mathematically well-defined but may be noncomputable (as with differentiation). Then we’ll be on firm footing for the rest of the project, including what it means for the implementation to be correct.
• Try to address implementation puzzles as they arise, without having a precise specification. For instance, there may be a decent solution to the implementation puzzle of constant folding and unCcc. Without a specification, I don’t know that we can do better than suppressing symptoms of our lack of understanding as those symptoms arise.

My sympathies are very much with the first path, leading to insight and correctness proofs rather than merely ignorance of incorrectness; while the second path is what I see as dominating the contemporary practice of programming. If our values & goals align, I’d be interested in collaborating or at least learning from each other.

[null-a]

Thanks for this, it's really helpful.

My sympathies are very much with the first path

I'm sympathetic too. It's an appreciation of your general approach that brought me here. I'd love to read "The simple essence of probabilistic programming", and I'd be keen to help bring that into existence if there's anything at all I can contribute.

I concede that the approach I have mind (which prompted me to open this issue) is rather less ambitious than that though -- partly because I doubt I'm up to the challenge of applying your method to this domain myself, and partly because I have an immediate need I might plausibly be able to address with this. Nevertheless, what I have may be of some interest to you, so when I get chance I'll pull some notes together and share them with you. It would be great to hear your thoughts if you have the time to take a look, and perhaps they could be a starting point for further discussion. (It will take me a while to get to this, since this isn't the day job, sadly.)

Thanks again for taking the time to discuss this with me, it's greatly appreciated.