Ambidexter rationale

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.

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?

• 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.

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.