功能编程范例是否有可视化建模语言或风格？

Question

UML是一个旨在用软件建模的标准,它将用OO语言编写,并与Java携手并进.它是否可能用于模拟软件的功能编程范式？鉴于嵌入的视觉元素,哪些图表将变得有用？

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

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

我正在寻找的是代码中发生的最直观,最轻的代表.易于遵循的图表,视觉模型不一定针对其他程序员.我很快就会在Haskell开发一款游戏,但由于这个项目是我的毕业结论工作,我需要介绍一下拟议解决方案的某种形式化.我想知道是否有相当于UML + Java标准,但对于Haskell.我应该坚持使用故事板,书面描述,非正式化的图表(一些浅的流程图图像),非正式的用例描述吗？

由jcolebrand编辑2012年6月21日:

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

Answer 1

我相信Haskell的建模语言叫做" 数学 ".它经常在学校教授.

Answer 2

是的,Haskell有广泛使用的建模/规范语言/技术.他们不是视觉上的.

在Haskell中,类型给出了部分规范.有时,此规范完全确定了意义/结果,同时留下了各种实现选择.超越Haskell到具有依赖类型的语言,如在Agda&Coq(以及其他)中,类型作为完整的规范通常更有用.

如果类型不够,请添加正式规范,这通常采用简单的功能形式.(因此,我相信,Haskell选择的建模语言是Haskell本身或"数学"的答案.)在这种形式中,您给出了一个功能定义,该定义针对清晰度和简单性进行了优化,而不仅仅是为了提高效率.该定义甚至可能涉及不可计算的操作,例如无限域上的函数相等性.然后,逐步将规范转换为高效可计算功能程序的形式.每一步都保留语义(外延),因此最终形式("实现")保证在语义上等同于原始形式("规范").您将看到此过程由各种名称引用,包括"程序转换","程序派生"和"程序计算".

典型推导中的步骤主要是"等式推理"的应用,增加了一些数学归纳(和共同归纳)的应用.能够执行这种简单有用的推理是函数式编程语言的主要动机,并且它们的有效性归功于"真正的函数式编程"的"外延"性质.(术语"外延"和"真正的功能"来自Peter Landin的开创性论文The Next 700 Programming languages.)因此,纯粹的函数式编程的口号曾经"有利于等式推理",尽管我没有听到这种描述这几天几乎一样.在Haskell中,外延对应于其他IO类型和依赖的类型IO(例如STM).虽然外延/非IO类型对于正确的等式推理是有益的,但是IO/非外延类型被设计为对于不正确的等式推理是不利的.

我在Haskell工作中尽可能经常使用的特定版本的规范派生就是我所谓的"语义类型态射"(TCM).其中的想法是为数据类型提供语义/解释,然后使用TCM原则通过类型类实例确定(通常唯一地)大多数或所有类型的功能的含义.例如,我说Image类型的含义是来自2D空间的函数.那么中医原理告诉我的意思Monoid,Functor,Applicative,Monad,Contrafunctor,和Comonad实例,为对应于功能的实例.这对于具有非常简洁和引人注目的规格的图像有很多有用的功能!(规范是语义函数加上语义TCM原则必须包含的标准类型列表.)然而,我对如何表示图像有很大的自由,而语义TCM原则消除了抽象泄漏.如果您想要看到这个原理的实例,请查看具有类型态射的论文Denotational design.

Answer 3

我们使用定理证明进行正式建模(带验证),例如Isabelle或Coq.在推导"低级"Haskell实现之前,有时我们使用特定于域的语言(例如Cryptol)来执行高级设计.

通常我们只使用Haskell作为建模语言,并通过重写来实现实际的实现.

QuickCheck属性也在设计文档中起作用,还包括类型和模块分解.

Answer 4

是的,哈斯克尔.

我得到的印象是,使用函数式语言的程序员在考虑他们的设计时并不需要简化他们的选择语言,这是一种(相当简单的)方式来查看UML为您所做的事情.

Answer 5

我观看了一些视频采访,并阅读了一些采访,其中包括erik meijer和simon peyton-jones.似乎在建模和理解问题域时,它们使用类型签名,尤其是函数签名.

序列图(UML)可能与函数的组成有关.静态类图(UML)可以与类型签名相关.

Answer 6

在Haskell中,您可以按类型进行建模.

首先编写函数,类和数据签名而不进行任何实现,并尝试使类型适合.下一步是QuickCheck.

例如,建模排序:

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

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

然后测试

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

最后实施......

Answer 7

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

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

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