haskell - 如何使用范围内的约束系列来证明表达式主体内的实例？

Question

这是对 my previous question 的跟进.我在那里收到了一些很好的答案，但是，由于我简化实际问题的方式，我认为我误导了回答者，我希望在这里纠正这个问题。

---

TL;DR 我有一个来自 constrained-categories 的类型类 Category，它限制了它的域/辅域 Category 使用名为 Object 的 TypeFamily(“约束系列”)。我想创建一个免费的 Category，但我正在努力获得表达式满足 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 纳入范围，并给我任何 我需要对象 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。

我还考虑过使用 type Object p::* -> Constraint 就像 Conal Elliot 的 concat库，但是，这将需要一个不同的库，一个不同的 Category 类，而且，上次我使用这种方式限制类别时，它似乎有点麻烦而且我什至不确定 那 会解决我的样板文件问题。 comment在该库中暗示了 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 也可以表达什么。对象(自由 p)a。这将是类

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

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

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

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.