

Product and Sum Types
On the left, this table compares the byvalue aspects of Ambidexter with the corresponding features of the strict language C++.
The right side compares the byname aspects of Ambidexter with the features of the nonstrict language Haskell. The center of the table shows how each feature of Ambidexter can fulfill two roles. A program written in strict style will use the feature for one purpose, while a program written in nonstrict style will use the same feature for a different purpose.
 terms  coterms  
C++  Ambidexter  Haskell 
strict product  intro 
div a={2,1}; 
(&2&1&) 
(&([(n)]<+return1$[(n)]+1) &([(k)]<+return2$[(k)]2)&) 
case x of A n>n+1 B k>k2  elim  nonstrict sum 
elim 
x.quo+x.rem 
x(\&quo&rem&>quo+rem) (huh<+x$[&quo&rem&>quo+rem$huh]) 
[&a&_&>a$42] 
A 42 
intro 
strict sum  intro 
union u={a,{.a=42}}; 
(a_<+42$a) 
x[\quorem<+quo+rem] [huh>(quorem<+huh$quo+rem)$x] 
(\(quo,rem)>quo+rem)x 
elim 
nonstrict product 
elim 
switch(x.kind){ case a:x.n+1; case b:x.p; }; 
(ret<+x$[[n>n+1$ret] ret]) 
[21] 
(2,1) 
intro 
Notice how the same construct is used both to introduce a product term and to eliminate a sum coterm. Similarly, the same construct is used for both eliminating a product term and introducing a sum coterm. And dually as well.
 Switch and case correspond to the most complex Ambidexter code. C++ switch is a lame feature, its correct use demanding a disciplined use of 'break'. Notice that all of the other constructs in C++ are expressions, whereas switch is a control construct. Dually, the Haskell case forces evaluation of the coterm 'x'. In Haskell this forcing of evaluation singles out the case construct. Note that in comparison to strict product elimination by pattern matching, at first glance nonstrict product and sum appear to operate similarly. However, if the pattern is for a product data type, it is natural to use a lazy pattern and not evaluate the argument. This is one factor leading to some very unexpected behavior in Ambidexter's nonstrict product elimination. The above code samples work around the misbehavior by evaluating the argument.
 In DCACD, Filinski points out that the difficulties of nonstrict sum types correspond to a dual problem in strict product types, in that they evaluate every field of the record regardless of whether it is demanded.
