Generics and strictness

Learn
1

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.

4 Likes
2

The representation is usually not part of the public API. In other words, as input, you convert from the actual data to Rep, where the extra laziness is never exercised; as output, you convert from Rep to the actual data, where the extra laziness is forced away by the conversion. In addition, in its most common use case (as a deriving mechanism), we expect the conversions to and from Rep to be fully inlined and optimised away by the compiler (otherwise we have far inferior performance compared to hand written instances), so I do not expect any problem caused by the laziness.

3

Interestingly, another definition of Natural can remove the extra element in the Generic representation:

newtype Fix f = Fix {unFix :: f (Fix f)} deriving (Generic)
data Succ x = Z | S !x deriving (Generic,Generic1)
type Natural = Fix Succ

Now the derived Generic instance layers only M1 newtypes on top of a K1 R newtype which refers to the strict Succ functor.

I am not concerned about performance issues. My interest is of theoretical nature: Given any type (that has a Generic instance), is there a lazyfication of it and what are its properties? The lazyfication of Natural would be Peano and total functions on the latter must be able to cope with infinity.
Yet it seems that due to K1 being strict, the added lazyness of (:+:) and (:*:), as observed above, is at most one layer deep. I guess one could define the lazyfication by swapping out K1 and Rec1 for lazy variants.