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 sjoerd@w3future.com