haskell - 如何最好地表示某个固定尺寸的笛卡尔积？

Question

根据@leftaroundabout的建议，该问题已被严重重写。在编辑历史记录中可能会看到较早的版本。

Haskell以促进思考，允许对数学抽象进行更直接的编码而闻名。笛卡尔积是从很小的时候起就已经为许多人所熟悉的非常基本的心理对象。但是，Haskell中几乎没有这种类型。我认为我需要一个，以使我的思想得以传播，如果没有别的。 （尽管这篇文章实际上是受到我手头的一些实际代码的启发。）然后，让我们对笛卡尔笛卡尔的东西（我简称为笛卡尔笛卡尔）形成一个共识。

给定一系列长度为d :: Int的集合（例如[[1,2], ['a', 'b']]），我想让它们的元素的所有组合都触手可及。这意味着对其进行操作，就好像它们处于常用的仿函数，可折叠，可遍历，Monoid等等。实际上，我们可以将任何笛卡尔表示为适当嵌套的元组列表：

type Lattice = [[(x, y)]]

type WeightedLattice = [[(x, y, w)]]

zipWith2 :: (a -> b -> c) -> [[a]] -> [[b]] -> [[c]]
zipWith2 f = zipWith (zipWith f)

fmap2 :: (Functor f, Functor g) => (a -> b) -> g (f a) -> g (f b)
fmap2 = fmap . fmap

sequence2 :: (Traversable s, Traversable t, Monad m) => t (s (m a)) -> m (t (s a))
sequence2 = sequence . fmap sequence

对于任何深度的嵌套，都可以手工编写类似的构造。

现在，我们介​​绍笛卡尔和初始笛卡尔之间的区别：


通过从每个集合中获取一个元素，并按顺序将它们与适当类型的函数组合在一起，可以从集合的异构序列中构造n维笛卡尔坐标。签名[Int，Char，Bool]的笛卡尔可以由以下函数形成：

f :: Int -> Char -> Bool -> Either Char Int
f i c b = if b then Left c else Right i 

初始笛卡尔由匹配Arity的元组构造函数形成：

initial :: Int -> Char -> Bool -> (Int, Char, Bool)
initial = (,,)

显而易见，我们可以将初始的笛卡尔（表示为嵌套列表）转换为具有嵌套深度的任何其他笛卡尔，其功能类似于：

    (fmap . ... . fmap) (uncurryN f)

但是，我们不一定总是回来。实际上，很难从Char恢复正确的Right 3。因此，可以使用初始笛卡尔坐标来代替任何特定的笛卡尔坐标，但并非总是相反。

例如，我们可以使用上面定义的Lattice类型来可视化字段，为空间中某些规则分布的点计算其值。我们可以使用分配坐标值的函数来实现。可能有许多个这样的函数，它们在相同的点上描述了不同的字段，每个函数对应于相似尺寸的晶格。但是只有一个初始格，除了坐标之外什么都不包含。

但是，我们的嵌套列表编码有其缺点。除了诱使为每个下一维度拼写所有必需的功能之外，它也不安全：没有什么可以让您避免将64 x 128矩阵与128 x 64矩阵错误地压缩在一起，最终得到64 x 64个代替;元组中事物的顺序可能与列表嵌套的顺序相对应，也可能不相对应。另一方面，类型系统对您不利，不允许使用foldr (.) id [replicate d concat]之类的东西来减轻您的痛苦。一点也不急。

但是，此系统最令人失望的原因是它没有以任何明显的方式支持笛卡尔直觉的最基本的直觉：其Monoid实例。这是一个属性，使我们可以认为一个点没有一个，不是一些，而是具有任意数量的p属性，可以轻松地添加，组合或丢弃它们-实际上就像列表中的元素一样。被钉到一定的嵌套深度和一定的元组对等会切掉您的翅膀。笛卡尔乘积是Set类别中的Monoid是类别理论的基本事实，但是我们可以在任意嵌套元组的任意嵌套列表上定义Monoid吗？

因此，编写笛卡尔完成的挑战涉及以下目标：


任何尺寸。列表，矩阵和任何其他有限维空间都应具有类似的界面。可以选择一些常用的Data.List函数。
输入安全性。即，在类型系统中对给定笛卡尔坐标的类型和维进行编码。例如，如果我形成一个像[1..3] x ['a', 'b']的空间，另一个像[1,2] x ['a'..'c']的空间，则它们应该具有不同的可读类型，而不是压缩在一起。
由于笛卡尔是由尺寸的选择决定的，因此可以将任意两个笛卡尔组合起来，就像它们的尺寸列表一样。例如：

Cartesian [[1..3], ['a', 'b']] <> Cartesian [[True, False]]

-应该与以下内容相同：

Cartesian [[1..3], ['a', 'b'], [True, False]]

-就像他们的生成列表一样。
应该有一些关于初始笛卡尔坐标和放置在其上的装饰的概念，这样，点的坐标就不会丢失，除非强制丢失。例如，应将Lattice点的坐标与其描述的字段的导出属性分开存储。如果说格子描述它们“匹配”，那么我们可能会得到一个字段的叠加。
初始笛卡尔坐标应为Monoid。


我草绘了一些至少可以使用的可怜类型的东西，稍后我将其发布为答案，但是对于上述大部分内容，我感到茫然。它必须采取一些技巧。我感谢有关如何制作的任何想法。

Answer 1

这个问题相当模糊，但是您似乎可能对vinyl样式的记录感兴趣。我的定义与vinyl的定义有些不同；使用你喜欢的东西。

{-# language DataKinds, PolyKinds, TypeOperators, GADTs #-}
module Cart where
import Data.Kind (Type)
import Data.Functor.Identity

infixr 4 :<
data Rec :: [k] -> (k -> Type) -> Type where
  Nil :: Rec '[] f
  (:<) :: f a -> Rec as f -> Rec (a ': as) f

newtype HList xs = HList (Rec xs Identity)

prod :: Rec as [] -> [HList as]
prod = map HList . go
  where
    go :: Rec as [] -> [Rec as Identity]
    go Nil = [Nil]
    go (xs :< xss) = [ Identity x :< r | x <- xs, r <- go xss]

使用适当的Show实例（直接但有点烦人），您将获得类似

> prod $ [3,4,5] :< ["hello", "goodbye"] :< ['x'] :< Nil

[ H[3,"hello",'x'], H[3,"goodbye",'x'], H[4,"hello",'x']
, H[4,"goodbye",'x'], H[5,"hello",'x'], H[5,"goodbye",'x'] ]

prod的这个版本可能有点太具体，因为它仅与Identity和列表一起使用。这是一个简单的概括，遍历函数会“拆分” Rec的基本函子，并且我们使用任意的Applicative而不只是[]：

class Trav (t :: (k -> Type) -> Type) where
  trav :: Applicative g => (forall a. f a -> g (h a)) -> t f -> g (t h)

instance Trav (Rec as) where
  trav f Nil = pure Nil
  trav f (xs :< xss) = (:<) <$> f xs <*> trav f xss

这与Data.Vinyl.rtraverse类似，因为我终于迷失了自己的认知方式。



此类记录不会形成Monoid，因为无法键入mappend。但是您当然可以附加它们：

type family (++) xs ys where
  '[] ++ ys = ys
  (x ': xs) ++ ys = x ': xs ++ ys

(><) :: Rec xs f -> Rec ys f -> Rec (xs ++ ys) f
Nil >< ys = ys
(x :< xs) >< ys = x :< (xs >< ys)

这表现不错。特别是，您可以附加记录然后遍历它们，或遍历它们然后附加结果。

trav f (xs >< ys) = (><) <$> trav f xs <*> trav f ys

您也可以按原则方式（类似于气泡设备）重新排列它们。方式

forall f k (as :: [k]) (bs :: [k]). Rec as f -> Rec bs f

可以赋予任何重新排列Rec的函数而无需关心其中的内容。



由于您提到了映射：

class Functor1 (t :: (k -> Type) -> Type) where
  map1 :: (forall x. f x -> g x) -> t f -> t g

instance Functor1 (Rec as) where
  map1 f = runIdentity . trav (\x -> Identity (f x))

压缩也可以：

rzip :: (forall x. f x -> g x -> h x)
     -> Rec as f -> Rec as g -> Rec as h
rzip f Nil Nil = Nil
rzip f (x :< xs) (y :< ys) = f x y :< rzip f xs ys