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 Haskell! 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 Conor 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.