A Pointless Library Proposal

Conor McBride ctm at Cs.Nott.AC.UK
Mon Oct 23 10:26:33 EDT 2006

Hi folks

This seems like the ideal time to make a wannabe library proposal which
is pointless, but pointless by design. The code's quite short:


> module Zero where

> -- import GHC.Prim -- if you can

The Zero type has nothing in it. Well, nothing worth worrying about anyway.

> data Zero

Elements of Zero are rather special, powerful things.

> magic :: Zero -> a
> magic _ = error "There's magic, as no such thing!"

It's a little frustrating to have to define this function lazily. I
prefer the strict definition with no lines, but it isn't valid

The main use of Zero is to give types |f Zero| to the closed
('elementless') values of some functorial structure f, especially
closed /terms/. These closed values should be embedded (as cheaply as
possible) into all the f-types which do permit elements.

> fMagic :: Functor f => f Zero -> f a
> fMagic = fmap magic -- if you must
> -- fMagic = unsafeCoerce# -- if you can


I'm not being facetious here. The reason it ought to be in a library
rather than ad hoc is that it (ideally) packs up a perfectly safe use of
unsafeCoerce#, which deserves some veneer of legitimacy. This is
seriously useful stuff if you want better static checking for scope (and
related notions), without taking a performace hit.

For example, you should all know the classic de Bruijn representation...

> data Tm x = V x | A (Tm x) (Tm x) | L (Tm (Maybe x)) deriving Show

...for which fmap does renaming...

> instance Functor Tm where
>   fmap rho (V x)   = V (rho x)
>   fmap rho (A f a) = A (fmap rho f) (fmap rho a)
>   fmap rho (L b)   = L (fmap (fmap rho) b)

...and (>>=) does capture-avoiding simultaneous substitution.

> instance Monad Tm where
>   return = V
>   V x   >>= sgm = sgm x
>   A f a >>= sgm = A (f >>= sgm) (a >>= sgm)
>   L b   >>= sgm = L (b >>= shift sgm) where
>     shift sgm Nothing  = V Nothing
>     shift sgm (Just x) = fmap Just (sgm x)

But operationally, you'd never do any such thing. See how capture is
avoided? The shift operator (aka traverse, but that's another story),
has to tweak all the free variables in the image of the substitution to
avoid capturing the new bound variable, Nothing. Ouch!

However, if you've ever fooled around with Int-based de Bruijn
representations, you'll know that the really cool thing is to substitute
/closed/ terms without any need for shifting. A term with no free
variables can't capture anything! Hence

> closedSubst :: (x -> Either (Tm Zero) y) -> Tm x -> Tm y
> closedSubst sgm (V x)    = either fMagic V (sgm x)
> closedSubst sgm (A f a)  = A (closedSubst sgm f) (closedSubst sgm a)
> closedSubst sgm (L b)    = L (closedSubst (shift sgm) b) where
>   shift sgm Nothing  = Right Nothing
>   shift sgm (Just x) = either Left (Right . Just) (sgm x)

Here, variables are either mapped to closed terms or renamed. We never
need to traverse the closed terms to push them under a binder: the shift
operator (aaka traverse, ahem) only shifts the renaming part (cheap!)
and the closed terms stay closed. When we finally hit a variable, the
closed images just get fMagic'd into the right scope!

So there you have it, a bone fide useful use of the Zero type, given a
module exporting a safe use of a usually dodgy operator. I don't think
module Zero is as pointless as the the datatype it defines.

My apologies for not providing any QuickCheck properties.

All the best


This message has been checked for viruses but the contents of an attachment
may still contain software viruses, which could damage your computer system:
you are advised to perform your own checks. Email communications with the
University of Nottingham may be monitored as permitted by UK legislation.

More information about the Libraries mailing list