|
|
Product and Sum Types
On the left, this table compares the by-value aspects of Ambidexter with the corresponding features of the strict language C++.
The right side compares the by-name aspects of Ambidexter with the features of the non-strict 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 non-strict 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->k-2 | elim | non-strict 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[\|quo|rem|<+quo+rem] [huh->(|quo|rem|<+huh$quo+rem)$x] |
(\(quo,rem)->quo+rem)x |
elim |
non-strict product |
elim |
switch(x.kind){ case a:x.n+1; case b:x.p; }; |
(ret<+x$[|[n->n+1$ret] |ret|]) |
[|2|-1|] |
(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 non-strict 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 non-strict product elimination. The above code samples work around the misbehavior by evaluating the argument.
- In DCACD, Filinski points out that the difficulties of non-strict 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.
|