不确定我是否理解 Haskell 中的这种类型

Question

好的，那么继续my previousquestions，我有一个类型叫Enumeration，它被描述为

现在，枚举是有限桶的无限序列， 自然数索引

并定义为：

> type Nat = Int 
> type Enumeration a = Nat -> Finite a

这是Finite Bucket

> type Finite a = [a]

如果我理解正确，Enumeration 类似于列表列表？它是一个从 Int 到列表的函数，它应该像索引一样接受一个 int，并返回一个列表。

但我无法理解的是，如果它确实是一个列表列表，它将“列表”存储在哪里，以便以后可以使用我提供的 index 返回它们。

我已经在 Enumeration 类型上定义了一些函数，但我不确定它们是否正确，因为我不确定我是否理解 Enumeration 的真正含义。

例如：

定义一个函数来进行单例枚举。 为简单起见，我建议您将唯一的项目放入存储桶 0。

> singleE' :: a -> Enumeration a
> singleE' a 0 = singleF a

定义枚举映射：

> imapE :: (a -> b) -> Enumeration a -> Enumeration b
> imapE f g = (imapF f) . g

定义不相交的枚举联合：

为简单起见，您可以逐桶进行此操作：结果枚举的第 i 个桶中的项目应从第 i 个桶中提取 两个参数枚举。

> plusE :: Enumeration a -> Enumeration b -> Enumeration (Either a b)
> plusE f g = \n -> [Left x | x <- f n] ++ [Right y | y <- g n]

定义枚举的笛卡尔积

这比较棘手，因为你不能再逐桶进行了， 就像你对 plusE 所做的那样（为什么不呢？）。最简单的技术是执行 一种卷积：结果枚举的桶 i 中的项目 应该从第一个参数的桶 j 中的那些构造 并在第二个桶 k 中，其中 j + k = i。

> timesE :: Enumeration a -> Enumeration b -> Enumeration (a,b)
> timesE f g = \n -> timesF (f n) (g n)

所以我的问题是：

1. 我是否正确理解Enumeration的类型

2. 如果我这样做了，我定义的函数是否正确？

Answer 1

我们可以证明Enumeration a（大部分）与列表的列表同构。 “同构”由以下函数给出：

enumerationToLists :: Enumeration a -> [[a]]
enumerationToLists f = map f [0..]

listsToEnumeration :: [[a]] -> Enumeration a
listsToEnumeration xss i = head $ drop i (xss++empties)

地点：

empties :: [[a]]
empties = []:empties

由于引用透明性，我们可以使用数学中的“等式推理”来证明它们确实形成了“同构”

证明listsToEnumeration . enumerationToLists = id：

    (listsToEnumeration . enumerationToLists) f
by definition of .
    = listsToEnumeration (enumerationToLists f)
by definition of enumerationToLists
    = listsToEnumeration (map f [0..])
by definition of map
    = listsToEnumeration [f 0, f 1, f 2, ...]
by definition of listsToEnumeration
    = \i -> head $ drop i ([f 0, f 1, f 2, ...]++empties)
concatenation of infinite lists
    = \i -> head $ drop i [f 0, f 1, f 2, ...]
by definition of drop and of the argument
    = \i -> head $ [f i, f (i+1), f (i+2), ...]
by definition of head
    = \i -> f i
eta reduction  (i.e. \x -> f x = f)
    = f

现在，鉴于xss = [xs1, xs2, ..., xsN] 和empties = []:empties，我们有(enumerationToLists . listsToEnumeration) (xss++empties) = xss++empties

    (enumerationToLists . listsToEnumeration) (xss++empties)
by definition of .
    = enumerationToLists (listsToEnumeration (xss++empties))
by definition of listsToEnumeration
    = enumerationToLists (\i -> head $ drop i (xss++empties++empties))
concatenation of infinite lists
    = enumerationToLists (\i -> head $ drop i (xss++empties))
by definition of empties
    = enumerationToLists (\i -> head $ drop i [xs1, xs2, ..., xsN, [], [], ...])
by definition of enumerationToLists
    = map (\i -> head $ drop i [xs1, xs2, ..., xsN, [], [], ...]) [0..]
by definition of map
    = let f = (\i -> head $ drop i [xs1, xs2, ..., xsN, [], [], ...]) in [f 0, f 1, ...]
by definition of f
    = [head $ drop 0 [xs1, xs2, ..., xsN, [], ...], head $ drop 1 [xs1, xs2, ..., xsN, [], ...], ...]
by definition of drop
    = [head [xs1, xs2, xsN, [], ...], head [xs2, ... xsN, [], ..], ..., head [xsN, [],...], head [[], ...], ..]
by definition of head
    = [xs1, xs2, ..., xsN, [], [], ...]
by definition of xss, empties and ++
    = xss ++ empties

显然我们假设Enumeration a 是总数（对于“未定义的索引”，它应该返回[]）。如果我们限制列表的无限列表，则上面的两个函数是同构的，否则它只包含“最多++empties”（如果xss 是无限的，我们有xss = xss++empties，因为我们将永远无法访问空部分)。

因此，如果您想保持这种“同构”，您应该确保所有功能都是完整的（查看singleE'...），但除此之外它们看起来都很好。

我希望上面的例子能给你一个提示，告诉你如何推断​​你定义的函数是否正确。