Is there a visual modeling language or style for the functional programming paradigm?

Question

UML is a standard aimed at the modeling of software which will be written in OO languages, and goes hand in hand with Java. Still, could it possibly be used to model software meant to be written in the functional programming paradigm? Which diagrams would be rendered useful given the embedded visual elements?

Is there a modeling language aimed at functional programming, more specifically Haskell? What tools for putting together diagrams would you recommend?

Edited by OP Sept 02, 2009:

What I'm looking for is the most visual, lightest representation of what goes on in the code. Easy to follow diagrams, visual models not necessarily aimed at other programmers. I'll be developing a game in Haskell very soon but because this project is for my graduation conclusion work I need to introduce some sort of formalization of the proposed solution. I was wondering if there is an equivalent to the UML+Java standard, but for Haskell. Should I just stick to storyboards, written descriptions, non-formalized diagrams (some shallow flow-chart-like images), non-formalized use case descriptions?

Edited by jcolebrand June 21, 2012:

Note that the asker originally wanted a visual metphor, and now that we've had three years, we're looking for more/better tools. None of the original answers really addressed the concept of "visual metaphor design tool" so ... that's what the new bounty is looking to provide for.

Answer 1

I believe the modeling language for Haskell is called "math". It's often taught in schools.

Answer 2

Yes, there are widely used modeling/specification languages/techniques for Haskell. They're not visual.

In Haskell, types give a partial specification. Sometimes, this specification fully determines the meaning/outcome while leaving various implementation choices. Going beyond Haskell to languages with dependent types, as in Agda & Coq (among others), types are much more often useful as a complete specification.

Where types aren't enough, add formal specifications, which often take a simple functional form. (Hence, I believe, the answers that the modeling language of choice for Haskell is Haskell itself or "math".) In such a form, you give a functional definition that is optimized for clarity and simplicity and not all for efficiency. The definition might even involve uncomputable operations such as function equality over infinite domains. Then, step by step, you transform the specification into the form of an efficiently computable functional program. Every step preserves the semantics (denotation), and so the final form ("implementation") is guaranteed to be semantically equivalent to the original form ("specification"). You'll see this process referred to by various names, including "program transformation", "program derivation", and "program calculation".

The steps in a typical derivation are mostly applications of "equational reasoning", augmented with a few applications of mathematical induction (and co-induction). Being able to perform such simple and useful reasoning was a primary motivation for functional programming languages in the first place, and they owe their validity to the "denotative" nature of "genuinely functional programming". (The terms "denotative" and "genuinely functional" are from Peter Landin's seminal paper The Next 700 Programming languages.) Thus the rallying cry for pure functional programming used to be "good for equational reasoning", though I don't hear that description nearly as often these days. In Haskell, denotative corresponds to types other than IO and types that rely on IO (such as STM). While the denotative/non-IO types are good for correct equational reasoning, the IO/non-denotative types are designed to be bad for incorrect equational reasoning.

A specific version of derivation-from-specification that I use as often as possible in my Haskell work is what I call "semantic type class morphisms" (TCMs). The idea there is to give a semantics/interpretation for a data type, and then use the TCM principle to determine (often uniquely) the meaning of most or all of the type's functionality via type class instances. For instance, I say that the meaning of an Image type is as a function from 2D space. The TCM principle then tells me the meaning of the Monoid, Functor, Applicative, Monad, Contrafunctor, and Comonad instances, as corresponding to those instances for functions. That's a lot of useful functionality on images with very succinct and compelling specifications! (The specification is the semantic function plus a list of standard type classes for which the semantic TCM principle must hold.) And yet I have tremendous freedom of how to represent images, and the semantic TCM principle eliminates abstraction leaks. If you're curious to see some examples of this principle in action, check out the paper Denotational design with type class morphisms.