arrows pointing right and left

Ambidexter rationale


email Scott Turner
home
Ambidexter

summary
examples
tutorial
questions
rationale
download
reference
links


product/sum types duality pitfalls avoided

Ambidexter melds pass-by-value and pass-by-name in one language. Not only are the two argument-passing methods on an equal footing, but each has the same power that it has when used as the basis for a conventional strict or non-strict language. It is no news that a strict language can express laziness, e.g. Scheme's delay and force. Likewise Haskell's 'seq' and strictness annotations bring local strict evaluation to a lazy language. Combining by-value and by-name on an equal footing is the outstanding feature of Ambidexter.

These parameter-passing methods were combined through an insight I received from Philip Wadler's Call-by-value is Dual to Call-by-name. The evaluation loop is derived from that paper.

In comparison to Ambidexter, Symmetric Lambda Calculus (SLC) (presented in Filinski's DCaCD) is lacking explicit "not" types. Neither does it have a cut operator and the associated abstraction constructs. The syntactic symmetry in SLC is related to that of Ambidexter.

Paul B. Levy has another approach to combining by-value and by-name, described in his dissertation Call-By-Push-Value. The variant of CBPV which includes control effects appears to be comparable with Ambidexter in expressiveness. However the two differ on many elements of syntax. CBPV does not reflect the duality (described below) in its syntax. Ambidexter's syntax for by-name and by-value function definitions matches the customary, whereas writing either kind of function definition in CBPV involves inserting some operators.

The type system of Ambidexter fully supports universal and existential quantifiers. In the current implementation, the difficulties of an impredicative type system are avoided, by not providing implicit instantiation of quantified types.

Simon Peyton Jones says in his Wearing the hair shirt: a retrospective on Haskell that laziness has a performance cost, and is not what really matters about Haskell. He asks, "Do we want a type distinction between (say) a lazy Int and a strict Int?" Ambidexter makes the distinction, and it looks promising.

He considers purity and monads to be a major benefits of Haskell. Ambidexter has its IO functor, but unfortunately even though call-by-value combines beautifully with call-by-name, it takes away purity. See the questions.

The Duality

The duality between values and continuations is embodied in Ambidexter. A value is the result of a computation, representated by an expression, or term within a program. Examples of terms are "creation", a literal string value, and 2 2 plus which computes a value.

A covalue takes a value and does something with it. A continuation is a value representing a covalue. (Covalue and continuation denote the same things, and are almost synonymous, but in Ambidexter it matters whether something is a value or not, and often we will be dealing with covalues.) An example of a continuation is exit which takes an integer status code and returns it from the program.

An example of a covalue would be a lazy integer coterm, such as
    [1 0 _divide]
The value it takes is a continuation. It transfers control to the continuation, which may or may not compute the division value and encounter an error.

Gerhard Gentzen uncovered this duality 70 years ago, in the field of logic. Its implications for programming languages have only slowly been understood. For every type of value, there is a corresponding type of covalue, and vice versa. For every language construct involving basic types of values, there is a construct involving the corresponding types of covalues. For example, the dual of a record type is a discriminated union type. A discriminated union term indicates a single variant. The dual of that term is a coterm which selects a field from a record.

See this table for a details of the duality.

Why combine by-value and by-name?

This is the main experimental feature of Ambidexter. The potential benefits are:
  • Easier combination of strict and non-strict. Sometimes the laziness of the I/O monad isn't what you expect.
    x <- foo; return $! x
  • More precise combination of strict and non-strict. e.g. foldl'
  • The benefits of laziness whenever you want it, along with the efficiency of strictness.
  • Continuations better than "first class". (? Is there an example which can't be translated readily into Scheme? Look into the result which says Scheme's power is a little less than full classical logic. Perhaps this has to do with threads.)
  • Symmetry keeps the language simpler, and reveals the sense in which sum elimination (i.e. switch/case statements) is allied with continuations.
There will be costs to combining by-value and by-name in this way. The underlying logic is more detailed and complex. Error messages involving types will sometimes be more difficult to understand. The programmer will have more to think of, which may sometimes distract from the task at hand (the way efficiency considerations distract from clean design leading to the "avoid premature optimization" mantra).

Types

Following Gentzen and Wadler, when a value and a covalue are compatible, they have the same type. This takes some getting used to, because the value and covalue have distinct roles, both computationally and logically. The value has been computed; the covalue insists on doing something with a value. From a logical point of view the value represents support for the proposition, while the covalue is an assumption of the proposition for some purpose. If distinct types were used for values and covalues, the value types would have to be isomorphic to the covalue types, and there would be twice as many types. Another drawback would be that the types would not correspond to logical propositions. Using the same types for both covalues and values is more suited to Ambidexter's logical purpose.

A significant drawback to this is that an Ambidexter program written in pure call-by-name style will use types that are opposite to the customary. For example, an integer literal covalue has type ~Integer, and a by-name function from integer to string would have type ~Integer<+~String, i.e. not Integer is not implied by not String. That converts by elementary logic to ~(Integer->String), again the opposite of expectations. It would be easy enough to provide a way of specifying customary types in call-by-name style programs, but it's too early in the development of Ambidexter to provide another way to write the same program (commonly a disease of aging languages).

In contrast, the language does not take advantage of symmetry to use the same syntax within terms and coterms. Distinctions provide cues to a reader in understanding the operational differences between sum and product types, etc., which are crucial.

Support open standards!  
Valid XHTML 1.0!