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

[Creighton Hogg]

2009/10/7 Robert Atkey <bob.atkey at ed.ac.uk>:
>
>> 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.

It's funny, because I wouldn't have thought about this in terms of
type classes from the top of my head.  What I've been thinking about a
lot lately (because I'm trying to prepare notes on it) is building
classifying categories from signatures, then considering the category
of all possible functorial "models" (read: "dsl embeddings") into the
target category.    I guess we're essentially talking about the same
thing.  The difference from looking at it as type classes is that you
really do get all your equations preserved with product preserving
functors from your classifying category; however, the topic came up
earlier today of what would a language look like if it had a built in
notion of functorial semantics - my guess is that it'd be like a
stronger version of ML functors, but I don't really know.

Cheers,
C