- html - 出于某种原因,IE8 对我的 Sass 文件中继承的 html5 CSS 不友好?
- JMeter 在响应断言中使用 span 标签的问题
- html - 在 :hover and :active? 上具有不同效果的 CSS 动画
- html - 相对于居中的 html 内容固定的 CSS 重复背景?
通过阅读商类型及其在函数式编程中的用法,我遇到了this post。作者提到 Data.Set
作为模块的示例,该模块提供了大量需要访问模块内部的功能:
Data.Set
具有36个函数,当确保集合含义(“这些元素是不同的”)真正需要的全部是toList
和fromList
时。
作者的观点似乎是,如果我们忘记了某些仅使用模块内部即可有效实现的功能,则需要“打开模块并破坏抽象”。
然后他说
我们可以用商类型减轻所有这些混乱。
但没有对该说法进行解释。
所以我的问题是:商类型在这里有什么帮助?
编辑
我进行了更多研究,找到了纸张"Constructing Polymorphic Programs with Quotient Types"。它详细说明了声明商容器,并在摘要和简介中提到了“有效”一词。但是,如果我没看错的话,它就不会提供任何有效表示形式“隐藏”在商容器之后的例子。
编辑2
第3章"[PDF] Programming in Homotopy Type Theory" paper揭示了更多内容。使用了商类型可以实现为依赖和的事实。介绍了关于抽象类型的 View (在我看来,它与类型类非常相似),并提供了一些相关的Agda代码。但是本章重点讨论抽象类型的推理,因此我不确定这与我的问题有何关系。
最佳答案
我最近做了一个blog post about quotient types,并在此处发表了评论。除了问题中引用的论文之外,博客文章还可以提供其他上下文。
答案实际上非常简单。一种解决方法是提出一个问题:为什么我们首先使用Data.Set
的抽象数据类型?
有两个截然不同的原因。第一个原因是将内部类型隐藏在接口(interface)后面,以便将来我们可以替换全新的类型。第二个原因是对内部类型的值强制执行隐式不变式。商类型及其对偶子集类型使我们可以将不变量明确化并由类型检查器强制执行,从而使我们不再需要隐藏表示形式。因此,我要非常清楚:商(和子集)类型不会为您提供任何隐藏的实现。如果您使用列表作为表示来实现商类型的Data.Set
,然后在以后决定要使用树,则需要更改所有使用该类型的代码。
让我们从一个简单的示例(leftaboutabout的示例)开始。 Haskell具有Integer
类型,但没有Natural
类型。使用组合语法将Natural
指定为子集类型的简单方法是:
type Natural = { n :: Integer | n >= 0 }
Integer
负数时会抛出错误。此类型表示只有
Integer
类型的值的子集有效。我们可以用来实现这种类型的另一种方法是使用商类型:
type Natural = Integer / ~ where n ~ m = abs n == abs m
h :: X -> T
的任何函数
T
都会在
X
上引起以等价关系
x ~ y = h x == h y
商定的商类型。这种形式的商类型更容易编码为抽象数据类型。通常,尽管如此,可能没有这么方便的功能,例如:
type Pair a = (a, a) / ~ where (a, b) ~ (x, y) = a == x && b == y || a == y && b == x
Natural
的第二个定义具有以下属性:存在两个表示
2
的值。即
2
和
-2
。商类型方面说,只要我们从不产生区分这两个代表的结果,就可以对底层的
Integer
做任何我们想做的事情。另一种看待这种情况的方式是,我们可以使用子集类型将商类型编码为:
X/~ = forall a. { f :: X -> a | forEvery (\(x, y) -> x ~ y ==> f x == f y) } -> a
forEvery
等同于检查功能是否相等。
Set
表示为以下内容:
data Tree a = Empty | Branch (Tree a) a (Tree a)
type BST a = { t :: Tree a | isSorted (toList t) }
type Set a = { t :: BST a | noDuplicates (toList t) } / ~
where s ~ t = toList s == toList t
isSorted
,
noDuplicates
或
toList
。我们“仅”需要说服类型检查器,这种类型的函数实现将满足这些谓词。商类型允许我们拥有冗余表示,同时强制我们以相同的方式对待等效表示。这并不意味着我们无法利用必须产生值的特定表示形式,而只是意味着我们必须说服类型检查器,如果使用不同的等效表示形式,我们将产生相同的值。例如:
maximum :: Set a -> a
maximum s = exposing s as t in go t
where go Empty = error "maximum of empty Set"
go (Branch _ x Empty) = x
go (Branch _ _ r) = go r
go t == go t'
时,它就是
toList t == toList t'
。如果我们使用一种表示来保证树是平衡的表示,例如如果是AVL树,则此操作将为
O(log N)
,同时转换为列表,然后从列表中选择最大值将为
O(N)
。即使具有这种表示形式,此代码也比转换为列表并从列表中获取最大的效率严格有效。注意,我们无法实现一个显示
Set
的树结构的函数。这样的功能将是错误的类型。
关于haskell - 商类型如何帮助安全地暴露模块内部?,我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/23596225/
我在前几天的测验中遇到了以下问题。 Consider the code fragment (assumed to be in a program in which all variables are
关闭。这个问题需要更多focused .它目前不接受答案。 想改进这个问题吗? 更新问题,使其只关注一个问题 editing this post . 关闭 9 年前。 Improve this qu
我刚开始接触 Objective-C,一般来说是 C,所以我想这也是一个 C 问题。它更像是一个为什么的问题,而不是一个如何做的问题问题。 我注意到,在除以两个整数时,小数部分向下舍入为 0,即使结果
我是一名优秀的程序员,十分优秀!