Generics and strictness

While the Generic representation of a data type expresses strictness of constructors/selectors in its Meta data, it appears that the constructors of the representation itself are always lazy, e.g. the two constructors of (:+:).

That means that the representation potentially contains more elements than the original type, so that (from,to) is an embedding-projection pair rather than an isomorphism. Is that on purpose? Or just the price we pay for not having four variants each of (:+:) and (:*:)?

Consider

module Natural where
import GHC.Generics

data Natural = Zero | Succ !Natural deriving (Show,Generic)

bottom :: Natural
bottom = Succ bottom

s :: Natural -> Rep Natural ()
s = M1 . R1 . M1 . M1 . K1 -- R1 is lazy, M1 and K1 are strict

leq :: Natural -> Rep Natural () -> Bool
leq n p = case (n, p) of
    (Zero, _) -> True
    (Succ _, M1 (L1 _)) -> False
    (Succ n',M1 (R1 (M1 (M1 (K1 p'))))) -> leq n' (from p')

We can observe that

(Succ Zero) `leq` (s bottom) == True

but

(Succ Zero) `leq` (from bottom)

diverges. Hence s bottom is an element of Rep Natural () that is not in the image of from.

3 Likes