不确定我在Haskell中了解这种类型

Eli Braginskiy 发表于 Dev

伊莱·布拉金斯基（Eli Braginskiy）

好的，所以继续我以前的问题，我有一个类型Enumeration，称为

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

并定义为：

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

这是一个 Finite Bucket

> type Finite a = [a]

因此，如果我理解正确，那么“ an”Enumeration类似于列表列表吗？它是一个从Int到列表的函数，它应该像索引一样采用一个int，然后返回一个列表。

但是我不明白的是它是否确实是一个列表列表，它在哪里存储它“列表”，以便以后可以使用indexI提供的返回它们。

我已经为这种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)

所以我的问题是：

我Enumeration是否正确理解类型
如果可以，我定义的功能是否正确？

巴库留

我们可以证明它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总数（应该返回[]“未定义的索引”）。如果我们限制为list的无限列表，则以上两个函数是同构的，否则它仅保持“最大++empties”（如果xss为无限，则xss = xss++empties因为我们将永远无法访问empties部分）。

因此，如果您希望保持这种“同构”，则应确保所有功能都是完整的（看一下singleE'...），但除此之外，它们看起来还不错。

我希望上面的示例可以提示您如何推理所定义的函数是否正确。

本文收集自互联网，转载请注明来源。

如有侵权，请联系[email protected] 删除。