How can I use a Constraint Family that's in scope to prove instances within the body of an expr-CodePudding

This is a follow up to my previous question. I recieved some good answers there, but, because of the way I simplified my actual problem, I think I misled the answerers, and I hope to remedy that here.

TL;DR I have a typeclass Category from constrained-categories which constrains the domain/codomain of it's Categorys using a TypeFamily ("constraint family") called Object. I would like to make a Free Category, but am struggling to get proofs that expressions satisfy the Object constraint.

Consider my Free data type, and its constrained-categories.Category instance:

data Free p a b where
  Id :: Object p a => Free p a a
  Comp :: Object p b => Free p b c -> Free p a b -> Free p a c

instance Category (Free p) where
  type Object (Free p) a = Object p a -- passes through the constraints from instantiated `p`
  id = Id
  (.) = Comp

To explain a bit more, let's also consider a non-free Category I might like to eval to:

newtype MyArr a b = MyArr (a -> b)

instance Category MyArr where
  type Object MyArr a = () -- trivial, no constraints needed
  id = MyArr P.id
  MyArr g . MyArr f = MyArr (g . f)

I would like to write an expression like this (which is obviously far simpler than expressions I'll be writing in practice):

-- error: Could not deduce: Object p Int arising from a use of ‘Id’
e0 :: Free p Int Int
e0 = Id

I can fix this the obvious way, but this becomes verbose for larger expressions. Imagine composing functions of tuples, and needing to explicitly provide an Object p _ instance for every interim step in the composition:

e1 :: Object p Int => Free p Int Int
e1 = Id

I could choose to not abstract the Category p, and, that works:

e2 :: Free MyArr Int Int
e2 = Id

But I'd like to abstract it. I should think adding a constraint Category p should work, and bring into scope its constraint that type Object (Free p) a = Object p a, and give me any Object p _ instance I need, but alas, it does not work.

-- error: Could not deduce: Object p Int arising from a use of ‘Id’
e3 :: Category p => Free p Int Int
e3 = Id

It seems to me that QuantifiedConstraints might help, eg forall a. Object (Free p) a => Object p a, but you can't have a TypeFamily in the head of the predicate.

I've also considered using a type Object p :: * -> Constraint like in Conal Elliot's concat library, but, that would require a different library, a different Category class, and, last time I used categories constrained that way, it seemed a bit more cumbersome and I'm not even sure if that would solve my boilerplate issue. A comment in that library suggests the usefulness of QuantifiedConstraints, but, I'm pretty twisted up at this point and don't know in which direction to trudge forward.

Runnable

{-# LANGUAGE GADTs #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE TypeFamilies #-}

module ConstrainedCategoryFreeArrow3 where

import Prelude hiding (id, (.))
import qualified Prelude as P
import Control.Category.Constrained


-- * A Free 'Category'

data Free p a b where
  Id :: Object p a => Free p a a
  Comp :: Object p b => Free p b c -> Free p a b -> Free p a c

instance Category (Free p) where
  type Object (Free p) a = Object p a -- passes through the constraints from instantiated `p`
  id = Id
  (.) = Comp

eval :: (Category p, Object p a, Object p b) => Free p a b -> p a b
eval Id = id
eval (Comp g f) = eval g . eval f


-- * A specific (trivial) 'Category'

newtype MyArr a b = MyArr (a -> b)

instance Category MyArr where
  type Object MyArr a = () -- trivial, no constraints needed
  id = MyArr P.id
  MyArr g . MyArr f = MyArr (g . f)


-- * A generic expression

-- -- error: Could not deduce: Object p Int arising from a use of ‘Id’
-- e0 :: Free p Int Int
-- e0 = Id


-- works, but becomes verbose. Imagine for instance building an expression with
-- functions of tuples; you would need to provide an incredible amount of
-- boilerplate constraints for each permutation of types in tuples used anywhere
-- in the body. The problem is a little worse than this once you account for
-- `Cartesian` which has a Constraint Family called `PairObjects` where you need
-- to prove that each tuple is an allowed product in the current constrained
-- category.
e1 :: Object p Int => Free p Int Int
e1 = Id


-- works, but is no longer abstract in the category `p`
e2 :: Free MyArr Int Int
e2 = Id


-- -- ideal solution, but alas
-- -- error: Could not deduce: Object p Int arising from a use of ‘Id’
-- e3 :: Category p => Free p Int Int
-- e3 = Id

CodePudding user response：

{-# LANGUAGE GADTs, RankNTypes, TypeApplications, AllowAmbiguousTypes #-}

I'm afraid keeping the object constraints all “in sync” with the p category, but at the same time being abstract in that category, will inevitably get very cumbersome.

I would suggest you avoid that by using your own object hierarchy, which will be stronger than the p hierarchy. You then need a class to implement the translation/weakening from your own hierarchy into the target category's.

The simplest case would be that p really has no constraint, i.e. what would also be expressed by ∀ a. Object (Free p) a. This would be the class

class UnconstrainedCat p where
  proveUnconstrained :: ∀ a r . (Object p a => r) -> r

...but this is rather unrealistic; if that were the situation then you wouldn't need to use constrained-categories in the first place.

Let's say the objects you need in your expressions are Ints, ()s, and nested tuples of those. (Could be easily extended to other types, or a list of atom-types.) Then we can trace at the value-level what type it is we're actually dealing with:

data IntTupleFlavour t where
  UnitCase :: IntTupleFlavour ()
  IntCase :: IntTupleFlavour Int
  TupleCase :: IntTupleFlavour a -> IntTupleFlavour b -> IntTupleFlavour (a,b)

class IntTuple t where
  intTupleFlavour :: IntTupleFlavour t
instance IntTuple () where
  intTupleFlavour = UnitCase
instance IntTuple Int where
  intTupleFlavour = IntCase
instance (IntTuple a, IntTuple b) => IntTuple (a,b) where
  intTupleFlavour = TupleCase intTupleFlavour intTupleFlavour

data IntFree a b where
  IntId :: IntTupleFlavour a -> IntFree a a
  IntCompo :: IntTupleFlavour b -> IntFree b c -> IntFree a b -> IntFree a c

instance Category IntFree where
  type Object IntFree a = IntTuple a
  id = IntId intTupleFlavour
  (.) = IntCompo intTupleFlavour

Now it's easy to write expressions of this free category – the compiler knows what are objects here, and p isn't even mentioned yet.

e4 :: IntFree Int Int
e4 = id

p only comes in when you eventually translate to that category.

class IntMonoiCat p where
  proveIntTupleInstance :: IntTupleFlavour t -> (Object p t => r) -> r

instance IntMonoiCat MyArr where
  proveIntTupleInstance _ q = q
    -- trivial, because `MyArr` doesn't even have a constraint! In general,
    -- you would need to pattern-match on the `IntTupleFlavour` here.

Then

instance EnhancedCat MyArr IntFree where
  arr (IntId itf) = proveIntTupleInstance itf id
  arr (IntCompo f g) = ...
        -- here you still need to extract the `IntTupleFlavours`
        -- for the `a` and `c` types. That requires digging into
        -- the free-category structure with a helper function.