43

UML 是一个针对以 OO 语言编写的软件建模的标准，与 Java 密切相关。不过，它是否可能用于对打算以函数式编程范式编写的软件进行建模？考虑到嵌入的视觉元素，哪些图表会变得有用？

是否有针对函数式编程的建模语言，更具体地说是 Haskell？您会推荐哪些用于组合图表的工具？

由 OP 于 2009 年 9 月 2 日编辑：

我正在寻找的是对代码中发生的事情的最直观、最简单的表示。易于遵循的图表，不一定针对其他程序员的可视化模型。我很快就会在 Haskell 中开发一个游戏，但是因为这个项目是为了我的毕业总结工作，所以我需要介绍某种形式化的建议解决方案。我想知道是否有与 UML+Java 标准等效的，但对于 Haskell。我应该坚持使用故事板、书面描述、非形式化图表（一些类似于流程图的浅层图像）、非形式化用例描述吗？

jcolebrand 于 2012 年 6 月 21 日编辑：

请注意，提问者最初想要一个视觉隐喻，现在我们已经三年了，我们正在寻找更多/更好的工具。最初的答案都没有真正解决“视觉隐喻设计工具”的概念，所以......这就是新赏金所要提供的。

4

11 回答 11

43

我相信 Haskell 的建模语言被称为“数学”。它经常在学校教授。

于 2009-09-01T19:34:32.557 回答
31

是的，Haskell 有广泛使用的建模/规范语言/技术。它们不是视觉的。

在 Haskell 中，类型给出了部分规范。有时，该规范完全确定了意义/结果，同时留下了各种实现选择。超越 Haskell 到具有依赖类型的语言，如在 Agda 和 Coq（以及其他）中，类型作为一个完整的规范更有用。

在类型不够的地方，添加正式的规范，通常采用简单的函数形式。（因此，我相信，Haskell 选择的建模语言是 Haskell 本身或“数学”的答案。）在这种形式中，您给出了一个针对清晰和简单而优化的函数定义，而不是全部为了效率。该定义甚至可能涉及不可计算的操作，例如无限域上的函数相等。然后，一步一步地，将规范转换为高效可计算的功能程序的形式。每一步都保留语义（外延），因此最终形式（“实现”）保证在语义上与原始形式（“规范”）等价。您会看到这个过程被各种名称所指，包括“

典型推导中的步骤主要是“等式推理”的应用，并增加了一些数学归纳（和共同归纳）的应用。能够执行这种简单而有用的推理首先是函数式编程语言的主要动机，它们的有效性归功于“真正的函数式编程”的“外延”性质。（术语“外延”和“真正函数式”来自 Peter Landin 的开创性论文The Next 700 Programming languages。）因此，纯函数式编程的口号曾经是“有利于等式推理”，尽管我没有听到这种描述这些天几乎一样频繁。在哈斯克尔，IOIOSTM）。虽然指称/非指代IO类型有利于正确的等式推理，但IO/ 非指称类型被设计为不利于不正确的等式推理。

我在 Haskell 工作中尽可能经常使用的从规范派生的特定版本是我所说的“语义类型类态射”（TCM）。想法是为数据类型提供语义/解释，然后使用 TCM 原则通过类型类实例确定（通常是唯一的）类型的大部分或全部功能的含义。例如，我说Image类型的含义是作为二维空间的函数。然后，TCM 原理告诉我 、 、 、 、 和 实例的含义Monoid，Functor它们Applicative对应Monad于Contrafunctor函数Comonad的这些实例。这是很多具有非常简洁和引人注目的规格的图像上的有用功能！（规范是语义函数加上语义 TCM 原则必须遵守的标准类型类列表。）然而，我在如何表示图像方面拥有极大的自由，语义 TCM 原则消除了抽象泄漏。如果您想看看这个原理的一些实际例子，请查看论文Denotational design with type class morphisms。

于 2012-06-22T00:21:08.240 回答
21

我们使用定理证明器进行形式化建模（带有验证），例如 Isabelle 或 Coq。有时我们使用特定领域的语言（例如 Cryptol）来进行高级设计，然后再推导出“低级”Haskell 实现。

通常我们只是使用 Haskell 作为建模语言，并通过重写得到实际的实现。

QuickCheck 属性以及类型和模块分解也在设计文档中发挥作用。

于 2009-09-02T06:37:13.650 回答
13

是的，哈斯克尔。

我的印象是，使用函数式语言的程序员在考虑他们的设计时并不觉得有必要简化他们选择的语言，这是查看 UML 为您所做的一种（相当 glib）的方式。

于 2009-09-01T19:34:53.287 回答
6

我看过一些视频采访，并阅读了一些采访，比如 erik meijer 和 simon peyton-jones。似乎在建模和理解问题域时，他们使用类型签名，尤其是函数签名。

序列图（UML）可能与功能的组合有关。静态类图 (UML) 可能与类型签名相关。

于 2010-02-05T17:06:27.950 回答
5

在 Haskell 中，您按类型建模。

只需从编写函数、类和数据签名开始，无需任何实现，并尝试使类型适合。下一步是快速检查。

例如对排序进行建模：

class Ord a where
    compare :: a -> a -> Ordering

sort :: Ord a => [a] -> [a]
sort = undefined

然后测试

prop_preservesLength l = (length l) == (length $ sort l)
...

最后是实施......

于 2010-02-05T17:13:50.977 回答
4

虽然不推荐使用（因为它似乎无法下载），但HOPS 系统将术语图可视化，这通常是功能程序的方便表示。

HOPS 截图

它也可以被认为是一种设计工具，因为它支持记录程序以及构建它们；我相信如果您愿意，它也可以逐步重写条款，以便您可以看到它们的展开。

不幸的是，我相信它不再被积极开发。

于 2012-06-26T11:11:14.113 回答
2

我意识到我参加聚会迟到了，但我仍然会给出答案，以防有人发现它有用。

我想我会选择像 SADT/IDEF0 这样的系统方法。

可以使用在 Linux、Windows 和 MacOS 上都可用的 Dia 程序制作此类图表。

于 2014-04-23T09:46:49.333 回答
2

您可以按照Hideki John Reekie的实时信号处理：数据流、可视化和函数式编程中所述的数据流处理网络模型

例如对于像（Haskell）这样的代码：

fact n | n == 0    = 1
       | otherwise = n * fact (n - 1)

视觉表示将是：

在此处输入图像描述

于 2016-04-16T19:42:32.350 回答
1

用数学建模 Haskell 有什么意义？我认为 Haskell 的全部意义在于它与数学密切相关，以至于数学家可以拿起它并运行它。你为什么要把一种语言翻译成它本身？

在使用另一种函数式编程语言 (f#) 时，我在白板上使用图表来描述大块，然后使用 UML 以 OO 方式使用类对系统进行建模。在 f# 中的构建块中存在轻微的不匹配（将类拆分为数据结构和作用于它们的函数）。但是从商业角度理解它是一种享受。我想补充一点，这个问题是面向业务/Web 的，不知道该技术在财务方面的效果如何。我想我可能会将函数捕获为没有状态的对象，它们应该很好地适应。

这完全取决于您工作的领域。

于 2010-10-12T02:59:26.767 回答
0

我使用 USL - 通用系统语言。我正在学习 Erlang，我认为它非常适合。

太糟糕了，文档非常有限，没有人使用它。更多信息在这里。

于 2015-01-09T14:28:37.050 回答