函数式编程范式有没有可视化的建模语言或风格？

Question

UML是一种标准，旨在对将用面向对象语言编写的软件进行建模，与Java并驾齐驱。尽管如此，它可能被用来对以函数式编程范型编写的软件进行建模吗？考虑到嵌入的可视元素，哪些图表将变得有用？

有没有一种针对函数式编程的建模语言，更具体地说是Haskell？你会推荐哪些工具来组合图表呢？

编辑时间:2009年9月2日

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

jcolebrand于2012年6月21日编辑：

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

Answer 1

我们使用定理证明器进行正式建模(带有验证)，例如Isabelle或Coq。有时，在派生“低级”Haskell实现之前，我们使用领域特定的语言(例如Cryptol)来进行高级设计。

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

与类型和模块分解一样，QuickCheck属性也在设计文档中发挥作用。

Answer 2

我相信Haskell的建模语言叫做"math“。它通常在学校里被教授。

Answer 3

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

在Haskell中，类型给出了部分规范。有时，此规范完全决定了意义/结果，同时保留了各种实现选择。从Haskell到具有依赖类型的语言，如Agda和Coq (以及其他)，类型通常作为一个完整的规范更有用。

在类型不够的地方，添加形式规范，它通常采用简单的函数形式。(因此，我相信，Haskell选择的建模语言是Haskell本身或“数学”。)在这样的形式中，您给出了一个函数定义，它是为了清晰和简单而不是为了效率而优化的。该定义甚至可能涉及不可计算的操作，例如无限域上的函数相等。然后，一步一步地，将规范转换为有效计算的函数式程序的形式。每一步都保留了语义(表示)，因此最终形式(“实现”)在语义上与原始形式(“规范”)是等价的。您将看到这个过程有各种不同的名称，包括“程序转换”、“程序派生”和“程序计算”。

典型推导中的步骤主要是“等式推理”的应用，并增加了一些数学归纳(和联合归纳)的应用。能够执行如此简单和有用的推理是函数式编程语言最初的主要动机，它们的有效性归功于“真正的函数式编程”的“外延”性质。(术语“指示性”和“真正的功能性”来自彼得·兰丁的开创性论文“”。)因此，纯函数式编程的战斗口号曾经是“有利于等式推理”，尽管最近我几乎不经常听到这样的描述。在Haskell中，指示性对应于IO以外的类型和依赖于IO的类型(如STM)。虽然指称/非IO类型对正确的等式推理很好，但IO/非指称类型被设计成不适合不正确的方程推理。

我在Haskell的工作中尽可能多地使用从规范派生的一个特定版本，我称之为“语义类型类态射”(TCM)。这里的想法是为数据类型提供语义/解释，然后使用TCM原则通过类型类实例来确定(通常是唯一的)大多数或所有类型功能的含义。例如，我说Image类型的含义是来自2D空间的函数。然后，中医原理告诉我Monoid、Functor、Applicative、Monad、Contrafunctor和Comonad实例的含义，与这些函数实例相对应。这是一个非常简洁和引人注目的图片上的很多有用的功能！(规范是语义功能加上标准类型类的列表，对于这些标准类型类，语义TCM原则必须成立。)然而，我在如何表示图像方面拥有极大的自由，而语义中医原则消除了抽象泄漏。如果你很好奇，想看看这个原理的一些实际例子，可以查看论文。