Hi Bob,
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?
greetings,
Sjoerd
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.
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.
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
--
Sjoerd Visscher
sjo...@w3future.com
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
