ezyang/nf

NF data type to statically enforce normal form

nf's Issues

Consider adding seriously bogus version

We have

newtype NF a = UnsafeNF a
instance NFData (NF a) where
  rnf x = x `seq` ()

which asserts that NF a is in normal form if it's in WHNF. Sometimes, it's useful to make an even stronger claim.

newtype AlreadyNF a = AlreadyNF a
instance NFData (AlreadyNF a) where
    rnf _ = ()

This asserts that if I have something of type AlreadyNF then it is already in normal form. This offers a way to force the structure of a container without forcing any of its contents:

import Data.Sequence

forceStructure :: Seq a -> ()
forceStructure = rnf . fmap AlreadyNF

Without relying on the fmap/coerce rules in Data.Sequence, this could be written something like

forceStructure = rnf . (coerce :: Seq a -> Seq (AlreadyNF a))

What type role should NF's parameter have?

Currently, we let GHC infer

type role NF representational

I think there's a minor potential problem here. Suppose we have

data T = ...
newtype U = U T

instance NFData T where ...
instance NFData U where ... -- Something *different*

We can coerce from NF T (which is in T-normal form) to NF U (which claims to be in U-normal form). It's not quite clear to me whose problem this is. Should whoever defined U be expected to hide its constructor? Or should we have type role NF nominal?

In practice, I suspect this to come up rather rarely, since types are generally expected to have just one notion of normal form, but there could be exceptions out there.

Travis build

https://github.com/hvr/multi-ghc-travis should be good enough for our needs. Let's use the new-build version.