[Haskell-cafe] What *is* a DSL?

[Robert Atkey]

> What is a DSL?

How about this as a formal-ish definition, for at least a pretty big
class of DSLs:

A DSL is an algebraic theory in the sense of universal algebra. I.e. it
is an API of a specific form, which consists of:
  a) a collection of abstract types, the carriers. Need not all be of 
     kind *.
  b) a collection of operations, of type 
         t1 -> t2 -> ... -> tn
     where tn must be one of the carrier types from (a), but the others 
     can be any types you like.
  c) (Optional) a collection of properties about the operations (e.g. 
     equations that must hold)

Haskell has a nice way of specifying such things (except part (c)): type
classes.

Examples of type classes that fit this schema include Monad, Applicative
and Alternative. Ones that don't include Eq, Ord and Show. The Num type
class would be, if it didn't specify Eq and Show as superclasses.

An implementation of a DSL is just an implementation of corresponding
type class. Shallowly embedded DSLs dispense with the type class step
and just give a single implementation. Deeply embedded implementations
are *initial* implementations: there is a unique function from the deep
embedding to any of the other implementations that preserves all the
operations. The good thing about this definition is that anything we do
to the deep embedding, we can do to any of the other implementations via
the unique map.

Thanks to Church and Reynolds, we can always get a deep embedding for
free (free as in "Theorems for Free"). If our DSL is defined by some
type class T, then the deep embedding is:
   type DeepT = forall a. T a => a
(and so on, for multiple carrier types, possibly with type
parameterisation).

Of course, there is often an easier and more efficient way of
representing the initial algebra using algebraic data types.

Conor McBride often goes on about how the initial algebra (i.e. the deep
embedding) of a given specification is the one you should be worrying
about, because it often has a nice concrete representation and gives you
all you need to reason about any of the other implementations.

Bob


-- 
The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.