Rather than choose between a lazy and an eager dynamics for products, we can instead distinguish two...

Rather than choose between a lazy and an eager dynamics for products, we can instead distinguish two forms of product type, called the positive and the negative. The statics of the negative product is given by rules (10.1), and the dynamics is taken to be lazy. The statics of the positive product, written t1 t2, is given by the following rules:G ? e1 : ??1 G ` e2 : ??12/ G ? fuse(e1; e2) : ??1 ??2G ? el: ??1 ??2 G x1 : ??1 x2 : ??2 ` e : ??/ G ? split(e0; ??1, ??2e) : ??The dynamics of fuse, the introductory form for the positive pair, is taken to be eager, essentially because the eliminatory form, split, extracts both components simultaneously. Show that the negative product is definable in terms of the positive product using the unit and function types to express the lazy semantics of negative pairing. Show that the positive product is definable in terms of the negative product, provided that we have at our disposal a let expression with a by-value dynamics so that we may ensure eager evaluation of positive pairs.