Haskell has a type called NFData
with the following shape:
class NFData a
where
rnf :: a -> ()
Types that are more "data-ish" than "function-ish" can be equipped with instances of NFData
. Each such instance thoroughly case analyzes a given value of the type and anything it transitively contains. This forces thunks and explodes latent bottoms.
NB: Somewhat mysteriously, even "function-ish" types are equipped with instances, although they do not actually reduce their argument to normal form.
So much for case analysis. But sometimes it's useful to take the dual perspective, and think about things that are more akin to codata than data. Instead of analyzing a sum down to its cases, we would like to build a record up to its fields.
So, without having any real idea of what I'm talking about, I might muddle along thusly, turning around whatever arrows I encounter and peppering in a few choice Co
s:
class NFCodata a
where
cornf :: () -> a
I would expect instances of the following form for types representing finite-products of non-strict fields (roughly, "single constructor" types):
instance NFCodata ()
where
cornf () = ()
instance NFCodata a => NFCodata (Solo a)
where
cornf () = Solo $ cornf ()
instance (NFCodata a, NFCodata b) => NFCodata (a, b)
where
-- you get the idea
And for all data-ish types with less/more than one constructor, I would expect an instance of the following form:
instance NFCodata Void
where
cornf () = undefined
instance NFCodata (Either a b)
where
cornf () = undefined
instance NFCodata Int
where
cornf () = undefined
-- ...
NB: This is perhaps a bit fishy, but if we don't give these instances we devolve to only types isomorphic to ()
having an instance of NFCodata
.
The net result should be that the derived instance for a type like this:
data Foo = Foo
{ bar :: Bar
, baz :: Baz
}
deriving stock Generic
deriving anyclass NFCodata
data Bar = Bar
{ someInt :: Int
, someString :: String
}
deriving stock Generic
deriving anyclass NFCodata
data Baz = Baz
deriving stock Generic
deriving anyclass NFCodata
behaves like this:
-- $> cornf () :: Foo
-- => Foo
-- { bar = Bar
-- { someInt = undefined
-- , someString = undefined
-- }
-- , baz = Baz
-- }
The idea being that one can use lenses for Foo
, Bar
, etc. to fill in the contents of this empty spine.
So ... questions:
- Does it make any sense to have a class like this? Is there already some way of obtaining the "spine" of a codata type with bottoms for its contents? Does
NFCodata
already exist in some other, more principled form? - Is there some rigorous sense in which there is an analogy between {NF}data and {NF}Codata?
- Is "NF" really the right prefix to use in "NFCodata"? Is there a more apt mathematical term (and more importantly, way of thinking) that applies here?