Is there a visual modeling language or style for the functional programming paradigm?-Collection of common programming errors

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 typcal 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 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 is to hold.) And yet I have tremendous freedom of how to represent images, and the semantic TCM principle immediately flags 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.

Originally posted 2013-11-10 00:10:06.