Add inject class for coproducts

[garyb]

No description provided.

[LiamGoodacre]

This can't work like that - constraints don't contribute to selection therefore injectLeft and injectRight are the same from an apartness point of view.

[LiamGoodacre]

Would need to be something like:

instance injectReflexive :: Inject f f where
  inj = identity
  prj = Just

else instance injectLeft :: Inject f (Coproduct f g) where
  inj = Coproduct <<< Left
  prj = coproduct Just (const Nothing)

else instance injectRight :: Inject f g => Inject f (Coproduct h g) where
  inj = Coproduct <<< Right <<< inj
  prj = coproduct (const Nothing) prj

[LiamGoodacre]

Wait, what's the difference between this and purescript-deprecated/purescript-inject#10

[garyb]

Gonna deprecate inject :)

[LiamGoodacre]

Oh right we are deprecating -inject?

[garyb]

I'll come back to this as I'm doing something else right now, but I can't seem to find any variation of this that works now - it just seems to commit to the first instance and fail so that it's not possible to have both of these working:

injL :: forall f g. f ~> Coproduct f g
injL = inj

injR :: forall f g. g ~> Coproduct f g
injR = inj

And if the chain starts with the reflexive case neither of them work. 😨

[LiamGoodacre]

This all works fine for me:

class Inject f g where
  inj :: f -> g
  prj :: g -> Maybe f


instance injectRefl :: Inject x x where
  inj x = x
  prj x = Just x
else instance injectLeft :: Inject l (Either l r) where
  inj x = Left x
  prj (Left x) = Just x
  prj _ = Nothing
else instance injectRight :: Inject x r => Inject x (Either l r) where
  inj x = Right (inj x)
  prj (Right x) = prj x
  prj _ = Nothing


inj0 :: Either Int (Either String Boolean)
inj0 = inj 42

inj1 :: Either Int (Either String Boolean)
inj1 = inj "Hello"

inj2 :: Either Int (Either String Boolean)
inj2 = inj true


prj00 :: Maybe Int
prj00 = prj inj0

prj01 :: Maybe String
prj01 = prj inj0

prj02 :: Maybe Boolean
prj02 = prj inj0


prj10 :: Maybe Int
prj10 = prj inj1

prj11 :: Maybe String
prj11 = prj inj1

prj12 :: Maybe Boolean
prj12 = prj inj1


prj20 :: Maybe Int
prj20 = prj inj2

prj21 :: Maybe String
prj21 = prj inj2

prj22 :: Maybe Boolean
prj22 = prj inj2

[LiamGoodacre]

Your scenarios of:

injL :: forall f g. f ~> Coproduct f g
injL = inj

injR :: forall f g. g ~> Coproduct f g
injR = inj

don't make sense, you'd need the Inject f g constraint. Or use a specific f and g. I.e injL :: Maybe ~> Coproduct Maybe (Coproduct Array List)

[LiamGoodacre]

Wait, am I lying? Hold on.

[LiamGoodacre]

No I'm not lying. The issue is the reflexive case. The compiler doesn't know that f /~ Coproduct f g (even though that is impossible).

[LiamGoodacre]

I will raise an issue to make the apartness checker take that into consideration.

[LiamGoodacre]

However, you would still need the constraint for injR because we don't know that f /~ g.

[LiamGoodacre]

Issue: purescript/purescript#3329

[garyb]

Thanks! I see what's going on now.