没有明确证明数据构造函数是单射的情况下进行相等性测试
是否可能定义一个简单的语法概念来表示相等（类似于GHC可能自动为Haskell 98类型派生的Eq实例），而不需要显式地证明每个数据构造器是单射的，或者采取类似的方法，例如定义每个构造器的收缩和使用cong？ 换句话说，是否可能更直接地利用数据构造器的单射性，而不必为每个构造器引入一个辅助函...
定义幽灵类型 - 无法编译示例
我正在尝试了解幻影类型。我正在阅读Ralf Hinze的《有趣的幻影类型》。他使用了一个我从未见过且无法编译的关键字with。当我尝试时，会出现=的解析错误。 data Type t = RInt with t = Int | R...
用Java模拟ADT
一个应用程序可以分为两种模式——“实时”模式和“采样”模式。在“实时”模式下，它会监视世界状态的每一次更新；而在“采样”模式下，它只会在每 T 毫秒查看一次世界状态。 如果我在写 Haskell（或者任何支持 ADTs 的语言），我会将其建模为： data Mode = RealTime ...
请确认或更正我对这个Haskell代码片段的"英文解释"
我是一名C#开发人员，正在阅读"Real World Haskell"这本书，以便真正理解函数式编程。这样当我学习F#时，我就可以真正领会它，而不仅仅是“用C#代码写F#代码”。 今天，我遇到了一个例子，我认为我已经理解了3次，然后才发现漏掉了某些东西，更新了我的解释，并递归（也诅咒过，相信...
为什么我们需要“代数数据类型”？
我阅读了一些关于代数数据类型的解释： 代数数据类型I 代数数据类型II 代数数据类型III 数据的代数和变异的微积分 这些文章提供了非常详细的描述和代码示例。 起初我以为代数数据类型只是为了轻松定义一些类型，然后我们可以使用模式匹配进行匹配。但是阅读了这些文章后，发现根本没有提到“...
C++中代数数据类型的等价物是什么？
假设我有以下的Haskell代码:data RigidBody = RigidBody Vector3 Vector3 Float Shape -- position, velocity, mass and shape data Shape = Ball Float -- radius ...
滥用代数数据类型的代数 - 为什么这样做有效？
"The '代数' 表达式对于具有数学背景的人非常有启发性。让我试着解释一下我的意思。定义了基本类型，如乘积 '•'，并集 '+'，单例 'X' 和单位 '1'。我们可以使用缩写 'X²' 表示 'X•X'，使用 '2X' 表示 'X+X' 等等，然后为链表等定义代数表达式。data List...
类型代数和Knuth的上箭头符号
阅读这个问题和这篇博客文章让我更加思考类型代数，特别是如何滥用它。 基本上， 1）我们可以将Either A B类型视为加法：A+B 2）我们可以将有序对(A,B)视为乘法：A*B 3）我们可以将函数A -> B视为指数：B^A 这里显然有一个模式：乘法是重复的加法，指数是重复...
数据结构区分，直觉建立
根据这篇论文，微分在数据结构中起作用。 根据这个回答： 微分，即数据类型D（表示为D'）的导数是具有单个“空洞”的D结构类型，即不包含任何数据的特殊位置。这些结构遵循微积分中相同的规则，这是令人惊奇的。 这些规则如下： 1 = 0 X′ = 1 (F + G)′ = F' + G′...
Haskell的构造函数（data constructors）构造什么？
Haskell可以使用类型构造器和数据构造器构建代数数据类型。例如，data Circle = Circle Float Float Float 我们被告知这个数据构造器（右侧的圆）是一个函数，当给定数据（例如x、y和半径）时可以构造一个圆。 Circle :: Float -> Fl...