使用来自实例约束的量化类型平等约束

Question

要设置场景，以下是我们使用的一堆语言扩展，以及Clash中的一些简化定义：

{-# LANGUAGE GADTs, StandaloneDeriving #-}
{-# LANGUAGE TypeOperators, DataKinds, PolyKinds #-}
{-# LANGUAGE TypeFamilyDependencies, FlexibleContexts, FlexibleInstances #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE QuantifiedConstraints #-}
data Signal dom a
instance Functor (Signal dom) where
instance Applicative (Signal dom) where
class Bundle a where
    type Unbundled dom a = res | res -> dom a
    bundle :: Unbundled dom a -> Signal dom a
    unbundle :: Signal dom a -> Unbundled dom a

我想为N- ARY产品类型制作Bundle实例。类型本身定义如下：

import Control.Monad.Identity
data ProductF (f :: * -> *) (ts :: [*]) where
    NilP :: ProductF f '[]
    ConsP :: f a -> ProductF f ts -> ProductF f (a : ts)
deriving instance (Show (f t), Show (ProductF f ts)) => Show (ProductF f (t : ts))
headPF :: ProductF f (t : ts) -> f t
headPF (ConsP x xs) = x
tailP :: ProductF f (t : ts) -> ProductF f ts
tailP (ConsP x xs) = xs
-- Utilities for the simple case    
type Product = ProductF Identity
infixr 5 ::>    
pattern (::>) :: t -> Product ts -> Product (t : ts)
pattern x ::> xs = ConsP (Identity x) xs
headP :: Product (t : ts) -> t
headP (x ::> xs) = x

我想编写的是一个Bundle实例，该实例仅用Signal dom替换Identity。不幸的是，我们不能一次去做：

instance Bundle (Product ts) where
    type Unbundled dom (Product ts) = ProductF (Signal dom) ts
    bundle NilP = pure NilP
    bundle (ConsP x xs) = (::>) <$> x <*> bundle xs
    unbundle = _ -- Can't implement this, since it would require splitting on ts

在这里，unbundle需要为ts ~ []和ts ~ t : ts'做不同的事情。好的，让我们尝试在两个实例中写下它：

instance Bundle (Product '[]) where
    type Unbundled dom (Product '[]) = ProductF (Signal dom) '[]
    bundle NilP = pure NilP
    unbundle _ = NilP
instance (Bundle (Product ts), forall dom. Unbundled dom (Product ts) ~ ProductF (Signal dom) ts) => Bundle (Product (t : ts)) where
    type Unbundled dom (Product (t : ts)) = ProductF (Signal dom) (t : ts)
    bundle (ConsP x xs) = (::>) <$> x <*> bundle xs
    unbundle xs = ConsP (headP <$> xs) (unbundle $ tailP <$> xs)

因此，在第二种情况下，问题出现了。即使我们在实例约束中具有（量化的）类型等于forall dom. Unbundled dom (Product ts) ~ ProductF (Signal dom) ts，GHC 8.6.3在Typechecking期间不使用它：

bundle：

• Couldn't match type ‘Unbundled dom (Product ts)’
                 with ‘ProductF (Signal dom) ts’
  Expected type: Unbundled dom (Product ts)
    Actual type: ProductF (Signal dom) ts1
• In the first argument of ‘bundle’, namely ‘xs’
  In the second argument of ‘(<*>)’, namely ‘bundle xs’
  In the expression: (::>) <$> x <*> bundle xs

for unbundle：

• Couldn't match expected type ‘ProductF (Signal dom) ts’
              with actual type ‘Unbundled dom (ProductF Identity ts)’
• In the second argument of ‘ConsP’, namely
    ‘(unbundle $ tailP <$> xs)’
  In the expression: ConsP (headP <$> xs) (unbundle $ tailP <$> xs)
  In an equation for ‘unbundle’:
      unbundle xs = ConsP (headP <$> xs) (unbundle $ tailP <$> xs)

可能的解决方法

当然，我们可以沿着漫长的道路走：专门为Product做自己的课程，并将所有实际工作委派给其中。我在这里介绍了该解决方案，但我对比这更详细和临时的事物特别感兴趣。

class IsProduct (ts :: [*]) where
    type UnbundledProd dom ts = (ts' :: [*]) | ts' -> dom ts
    bundleProd :: Product (UnbundledProd dom ts) -> Signal dom (Product ts)
    unbundleProd :: Signal dom (Product ts) -> Product (UnbundledProd dom ts)
instance (IsProduct ts) => Bundle (Product ts) where
    type Unbundled dom (Product ts) = Product (UnbundledProd dom ts)
    bundle = bundleProd
    unbundle = unbundleProd

，然后IsProduct具有实际实现的优势：

type (:::) (name :: k) (a :: k1) = (a :: k1)
instance IsProduct '[] where
    type UnbundledProd dom '[] = dom ::: '[]
    bundleProd NilP = pure NilP
    unbundleProd _ = NilP
instance (IsProduct ts) => IsProduct (t : ts) where
    type UnbundledProd dom (t : ts) = Signal dom t : UnbundledProd dom ts
    bundleProd (x ::> xs) = (::>) <$> x <*> bundleProd xs
    unbundleProd xs = (headP <$> xs) ::> (unbundleProd $ tailP <$> xs)

Answer 1

好吧，原则上的解决方案将是单例：

-- | Reifies the length of a list
data SLength :: [a] -> Type where
   SLenNil :: SLength '[]
   SLenCons :: SLength xs -> SLength (x : xs)
-- | Implicitly provides @kLength@: the length of the list @xs@
class KLength xs where kLength :: SLength xs
instance KLength '[] where kLength = SLenNil
instance KLength xs => KLength (x : xs) where kLength = SLenCons kLength

Singletons背后的核心想法（其中之一）是，隐式Singleton类KLength可以考虑到像您这样的临时课程的需求。"优雅"进入了KLength，可以重复使用。"案例"进入了字面的case，而SLength是将它们粘合在一起的数据类型。

instance KLength ts => Bundle (Product ts) where
    type Unbundled dom (Product ts) = ProductF (Signal dom) ts
    bundle = impl
        -- the KLength xs constraint is unnecessary for bundle
        -- but the recursive call would still need it, and we wouldn't have it
        -- there's a rather unholy unsafeCoerce trick you can pull
        -- but it's not necessary yet
        where impl :: forall dom us. ProductF (Signal dom) us -> Signal dom (Product us)
              impl NilP = pure NilP
              impl (ConsP x xs) = (::>) <$> x <*> impl xs
    unbundle = impl kLength
        -- impl explicitly manages the length of the list
        -- unbundle just fetches the length of ts from the givens and passes it on
        where impl :: forall dom us. SLength us -> Signal dom (Product us) -> ProductF (Signal dom) us
              impl SLenNil _ = NilP
              impl (SLenCons n) xs = ConsP (headP <$> xs) (impl n $ tailP <$> xs)

Answer 2

平等编码以下事实：在两种情况下，'[]和t ': ts，Unbundled家族都定义为ProductF。一种简单的方法是在生成该ProductF之前不要在列表上进行模式匹配。这涉及分解班级的Unbundled家族：

type family Unbundled dom a = res | res -> dom a
class Bundle a where
    bundle :: Unbundled dom a -> Signal dom a
    unbundle :: Signal dom a -> Unbundled dom a

因此，您可以在两个类实例中使用单个类型实例：

type instance Unbundled dom (Product ts) = ProductF (Signal dom) ts
instance Bundle (Product '[]) where
    bundle NilP = pure NilP
    unbundle _ = NilP
instance (Bundle (Product ts), forall dom. Unbundled dom (Product ts) ~ ProductF (Signal dom) ts) => Bundle (Product (t : ts)) where
    bundle (ConsP x xs) = (::>) <$> x <*> bundle xs
    unbundle xs = ConsP (headP <$> xs) (unbundle $ tailP <$> xs)