The Lowly Mathematician


> module Quotable where


This is a nice little code dump I was trying to have posted yesterday, I’ve finally got most of the formatting bugs worked out. I wasn’t thinking I was going to post this till I got about 2/3rd the way through it, so it’s pretty rough. Think of it as a look into my notebook. Enjoy.

One of the things I like about Scheme is the ability to seamlessly jump from code as code and code as data, or vice versa. This is called “Quoting” and it works something like this:

(define a-list '(1 2 3))
(define quoted-list 'a-list)
;;;;
a-list =: (1 2 3)
(eval quoted-list) =: (1 2 3)

Quoting allows us to pass things by name, and evaluated them as needed, that is, if I define a bit of scheme a la:

(define (stream generator initial-value)
   (define next-val (generator initial-value))
   (cons initial-value
        `(stream ,generator ,next-val)))

(define (head/s a-stream)
    (car a-stream))

(define (tail/s a-stream)
    (eval (cdr a-stream)))

(define naturals
    (stream (lambda (x) (+ x 1)) 0))

This will give a lazy-list function given a generator which operates on one initial value and inductively defines the next and so on. It uses something called “quasiquoting” which allows for partially quoted sexps. All we really do in the above is construct an infinite list one element at a time. When we call “head/s” we’re just taking the already computed value, when we call “tail/s”, we simply compute the second half of the cons pair, which we stored as the quoted function

`(stream ,generator ,next-val)

, which gives us a new stream (of the same form) but which has the next-value in the first position, and a new quoted function as:

`(stream ,generator ,(generator (eval (stream ,generator ,next-val))))

(more or less) This does exactly what Haskell does for it’s lazy-lists, (and it’s lazyness in general) it computes what it needs as you ask for it. However, we don’t have this neat quoting ability exposed in Haskell. So how can we recreate it?

Well, first of all, We need to examine exactly what a “quote” is, each of these different quote-functions, namely quote (written as ‘) quasi-quote (written as `) and unquote (written as ,), are just maps of the following form: Quotable a => a -> Quoted a Similarly, we need an inverse function, going from a Quoted a -> a. In scheme, we call this ‘eval’, for our case, let’s call it dequote- since eval is used for more than just quoting/dequoting. Dequote has the signature:

Quotable a => Quoted a -> a

and the property

> prop_inv x = x == (dequote . quote) x

holds. So, we notice one interesting thing, Quoting has a monadic looking signature, namely that ‘quote’ looks a good bit like ‘return’, in fact, quoting does form a monad under

(x >>= f) = (f . dequote) x
return x = quote x

Not a very interesting monad, but a monad nonetheless, a quick proof of the monad-ness of quoting is as follows: Left Identity:

(return x) >>= f = (f . dequote) $ (quote x)          -- definition
                                 = f . dequote . quote $ x -- definition
                                 = f . id $ x           -- prop_inv
                                 = f x                          -- identity property

Right Identitiy:

(x >>= return) = (quote . dequote) $ x -- definition
                         = id $ x            -- prop_inv
                         = x                 -- identity

Associativity:

(x >>= f) >>= g == (x >>= (\y -> f x >>= g))                      -- given
                                 == ((\y -> f x >>= g) . dequote $ x -- definition
                                 == f (dequote x) >>= g                    -- beta-reduction (iirc)
                                 == (g . dequote) $ f (dequote x)          -- definition
remember that, momentarily
(x >>= f) >>= g == (g . dequote) $ (f . dequote $ x) -- definition
                                 == (g . dequote) $ f (dequote x)        -- simplification
but this is the same as the above side, so the law holds.

I’m fairly sure that the definition

x >>= f = f . quote $ x
return x = dequote x

is a monad too. I’ll leave that as an excercise. A quick recap, we haven’t written any actual code yet, but we know that the two functions (quote/dequote) yield two monads. We might ask if it satisfies any other constraints. Before that, though, lets write up some code.

> newtype Quote a = Q a
> quote :: a -> Quote a
> quote = undefined -- we don't care how it's implemented, we just need to pretend
>                       -- it exists
> dequote :: Quote a -> a
> dequote = undefined

> instance Monad Quote where
>       return x = quote x
>       x >>= f = (f . dequote) x 

Note how we are only proving that these types check out- we’re not saying how to build this quoting mechanism, simply that if it does exist, then it has the property of being a monad. Later, we might try to actually build such a infrastructure, but for now, let’s just do some math. Specifically, lets look at whats available? One natural area to look at is functors and their applicative variants: Recall that a functor implies the structure can be mapped over, that is there exists some function:

fmap :: Functor f => (a -> b) -> f a -> f b

This obeys the following laws:

fmap id = id
fmap (f . g) = fmap f . fmap g

We can easily show Quote is a functor, a la:

> instance Functor Quote where
>       fmap f = (quote . f . dequote)

This satisfies the laws as follows:

fmap id = quote . id . dequote  -- hypothesis
                = quote . dequote       -- defn
                = id                    -- prop_inv

fmap (f . g) = fmap f . fmap g                                          -- hypothesis
                         = (quote . f . dequote . quote . g . dequote) -- defn
                         = (quote . f . id . g . dequote)              -- prop_inv
                         = (quote . f . g . dequote)                 -- defn
                         = fmap (f . g)                                                                 

So we have a functor and a monad, we can also show that it’s an applicative functor, a la:

> instance Applicative Quote where
>       pure            = quote
>       qf <*> qx       = fmap (dequote qf) qx 

That needs to satisfy the following:

Identity:
pure id <*> v = v

Composition:
pure (.) <*> u <*> v <*> w = u <*> (v <*> w)

Homomorphism:
pure f <*> pure x = pure (f x)

Interchange:
u <*> pure y = pure ($ y) <*> u

We can show this also fairly easily:

Identity:
pure id <*> v = (quote id) <*> v                                -- defn
                         = fmap (dequote . quote . id) v        -- defn
                         = fmap (id . id) v                     -- prop_inv
                         = fmap id v                            -- defn
                         = v                                    -- functor law
Composition:
Left as an exercise

Homomorphism:
pure (f x) = pure f <*> pure x                        -- hypothesis
                 = (quote f) <*> (quote x)                    -- defn
                 = fmap ((dequote . quote) f) (quote x) -- defn
                 = fmap f (quote x)                           -- prop_inv
                 = pure (f x)                                 -- defn

Interchange:
Exercise                 

So, we’ve shown quoting to be a functor, applicative functor, and a monad. Possible interesting questions include: Is there a quote-identity? Which might give rise to a monoid instance? How many ways are there to implement this infrastructure? Obviously using read/show is nice, but would only allow quoting of read/show types, can we generalize it somehow? Can we somehow generalize this to a kind of class, meaning that we could have different quote/dequote functions, but still have a general monad instance for all of those types? Can we make quoting derivable?

In any case this was fun, I hope to come back sometime and actually implement some quoting ability for Haskell, but at least now I can see what kind of things that structure could do!