如何使用范围内的约束族来证明表达式主体中的实例？

Question

这是我上一个问题的后续内容。我在那里得到了一些很好的答案，但由于我简化实际问题的方式，我认为我误导了回答者，我希望在这里纠正这一点。

---

TL；DR我有一个来自constrained-categories的类型类Category，它使用称为Object的类型族("约束族"(来约束它的Category的域/共域。我想制作一个FreeCategory，但我很难得到表达式满足Object约束的证明。

---

考虑我的Free数据类型及其constrained-categories.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

为了进一步解释，让我们还考虑一个非免费的Category，我可能希望eval为：

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)

我想写一个这样的表达式(这显然比我在实践中写的表达式简单得多(：

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

我可以用显而易见的方法解决这个问题，但对于较大的表达式来说，这会变得冗长。想象一下，组成元组的函数，并且需要为组成中的每个临时步骤显式地提供一个Object p _实例：

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

我可以选择而不是抽象Category p，这很有效：

e2 :: Free MyArr Int Int
e2 = Id

但我想抽象一下。我应该认为添加一个约束Category p应该有效，并将其约束type Object (Free p) a = Object p a纳入范围，并给我任何我需要的Object p _实例，但遗憾的是，它不起作用。

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

在我看来，QuantifiedConstraints可能会有所帮助，例如forall a. Object (Free p) a => Object p a，但谓词的头部不能有TypeFamily。

我也考虑过像Conal Elliot的concat库中那样使用type Object p :: * -> Constraint，但是，这需要一个不同的库，一个不同Category类，而且，上次我使用以这种方式约束的类别时，它似乎有点麻烦，我甚至不确定是否能解决我的样板问题。该库中的一条评论表明了QuantifiedConstraints的有用性，但是，在这一点上，我很困惑，不知道该朝哪个方向前进。

---

可运行

{-# 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

Answer 1

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

我担心，保持对象约束与p类别"同步"，但同时又在该类别中是抽象的，这将不可避免地变得非常麻烦。

我建议您使用自己的对象层次结构来避免这种情况，该层次结构将比p层次结构更强。然后，您需要一个类来实现从您自己的层次结构到目标类别的转换/弱化。

最简单的情况是p实际上没有约束，即∀ a. Object (Free p) a也表示什么。这将是类

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

但这是不现实的；如果是这种情况，那么您一开始就不需要使用constrained-categories。

假设表达式中需要的对象是Ints、()s以及它们的嵌套元组。(可以很容易地扩展到其他类型，或者原子类型列表。(然后我们可以在值级别跟踪我们实际处理的类型：

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

现在，编写这个自由类别的表达式很容易了——编译器知道这里的对象是什么，而p甚至还没有被提及。

e4 :: IntFree Int Int
e4 = id

p只有在您最终翻译到该类别时才会出现。

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.

然后

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.