[Haskell-cafe] What *is* a DSL?
sjoerd at w3future.com
Mon Oct 12 09:49:51 EDT 2009
I tried to understand this by applying what you said here to your deep
embedding of a parsing DSL. But I can't figure out how to do that.
What things become the type class T?
On Oct 7, 2009, at 9:18 PM, Robert Atkey wrote:
>> 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.
> 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)):
> Examples of type classes that fit this schema include Monad,
> and Alternative. Ones that don't include Eq, Ord and Show. The Num
> 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
> embedding to any of the other implementations that preserves all the
> operations. The good thing about this definition is that anything we
> to the deep embedding, we can do to any of the other implementations
> 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
> 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
> embedding) of a given specification is the one you should be worrying
> about, because it often has a nice concrete representation and gives
> all you need to reason about any of the other implementations.
> The University of Edinburgh is a charitable body, registered in
> Scotland, with registration number SC005336.
> Haskell-Cafe mailing list
> Haskell-Cafe at haskell.org
sjoerd at w3future.com
More information about the Haskell-Cafe