如何使用范圍內的約束系列來證明運算式主體內的實體？-有解無憂

這是對我之前的問題的跟進。我在那里收到了一些很好的答案，但是，由于我簡化了實際問題的方式，我認為我誤導了回答者，我希望在這里解決這個問題。

TL; DR我有一個型別類Category從constrained-categories該值域限制它的域/Category使用TypeFamily（“約束的家庭”）稱為S Object。我想做一個 Free 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，并提供我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在謂詞的頭部使用 a 。

我也考慮過type Object p :: * -> Constraint在 Conal Elliot 的concat庫中使用類似的庫，但是，這需要不同的庫、不同的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

uj5u.com熱心網友回復：

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

轉載請註明出處，本文鏈接：https://www.uj5u.com/qukuanlian/365065.html

標籤：哈斯克尔类型类加特类型族量化约束

上一篇：Haskell：更改串列中串列中的第(n,m)個元素

下一篇：在Haskell的型別宣告中符號`!`是什么意思？