Coproducts?

[kbr-]

Hi,

I have a question. What is the status of coproduct support? Do they work? If they do, how to use them? Are there any working examples (couldn't find one)? If they don't, what should be done to make them work, or are there any alternatives? (I've seen a comment with "instance HasRep (a :+ b)" in Rep.hs implementing coproduct in terms of product, dunno if that's a good lead)

I tried to add this: , runSyn $ toCcc $ \x -> Left x :: Either Int Int to the examples, which results in an "oops: toCcc' called", even though there is an instance CoproductCat Syn.

Here is the last message of the trace

go ccc Syn: 
  Left @ Int @ Int
  :: Int -> Either Int Int
Couldn't build dictionary for
  reprC @ (->) @ (Either Int Int) @ (Rep (Either Int Int)) :: RepCat
                                                                (->)
                                                                (Either Int Int)
                                                                (Rep (Either Int Int)) =>
                                                              Either Int Int
                                                              -> Rep (Either Int Int):
  free id types: [HasRep (Either Int Int)]
Doing top Unhandled

when I changed "Left" to "A.inl" (from AltCat), the example worked. Investigating, I've found a rule "toCcc Prelude Left" toCcc Left = toCcc inl in AltCat, which would seem to solve this problem, however it's between #if 0, #endif. Why?

Goal: I would like to pass expressions involving Either (in standard Haskell, so Left, Right etc.) into toCcc, and then provide an implementation of coproducts in the category I'm working on (actually that last part I already did).

I would also like to translate ADTs into sums. For example, I have a category Kat implementing coproducts and a simple "instance r ~ Rep a => RepCat Kat a r". When I try the following:

data E = L | R

instance HasRep E where
    type Rep E = Either () ()
    repr L = Left ()
    repr R = Right ()
    abst (Left ()) = L
    abst (Right ()) = R
    {-# INLINE repr #-}
    {-# INLINE abst #-}

then running toCcc on

f :: Int -> E
f _ = L

results in an infinite compilation loop. This message shows up often:

Couldn't build dictionary for
  const @ Kat @ E @ (Either () ()) :: (ConstCat Kat E,
                                       Ok Kat (Either () ())) =>
                                      E -> Kat (Either () ()) (ConstObj Kat E):
  no bindings

seems like the plugin expects me to provide a ConstCat instance for E which, if I understand correctly, I shouldn't need to provide. Occurrences of E should be translated into Either () ()s, right? Maybe some rule is not fired for some reason.

When I change the HasRep instance to

instance HasRep E where
    type Rep E = Bool
    repr L = False
    repr R = True
    abst False = L
    abst True = R
    {-# INLINE repr #-}
    {-# INLINE abst #-}

it works. So it seems that the plugin doesn't like Eithers?

[conal]

I implemented translation support for coproducts in an earlier version of the CtoC plugin, and it wasn't complicated. I haven't gotten around to it for the current implementation. I guess I'm waiting for a fun use case. Do you have one in mind?

[kbr-]

Hi Conal,

thanks for the answer! Indeed I do have a use :D It's not really "useful" but I certainly find it "fun"(ny). I'm actually writing a... Haskell to C++ compiler, using your plugin. The Cartesian Closed part is already working (at least for the simple examples I tried), together with part of NumCat.

Check it out: https://github.com/kbr-/concat-cpp Running it produces a C++ program (which doesn't output anything: it evaluates an expression translated form Haskell inside main, just for me to check that it compiles). It requires the lib.h file (from the repo) and the boost variant library. I tested it with g++ v6.3.0.

The compiler is currently very stupid, producing some unnecessary lambdas etc. These can be eliminated with better implementations of the categories. But I just wanted to prove that it's doable for now.