Ambidexter summary

• statically typed
• functional, with higher order functions and lexical closures
• generics, parametric polymorphism
• abstraction, type constructors
• impredicative, i.e. first-class generic and abstract types
• rigorous pattern matching (not flexible like Haskell)
• garbage-collected
• not object-oriented
• no overloading
• no exceptions
• no reflection
• open source MIT license
• portable Haskell implementation

• The type system is logic, suitable for teaching.
• The logic is classical logic, including negation, which is common in logic but unusual in programming language type systems. This provides first class continuations, with their ability to build control constructs.
• Support both call-by-value and call-by-name.

• multithreading/concurrency
• modules
• field names, with possible subtyping

• Terms and coterms are indicated by parentheses and square brackets respectively.
• Function application appears as simple juxtaposition, with the argument first as in Forth or PostScript.
• Types can be constructed using either logical symbols (UTF-8) or ASCII alternatives. For example, logical or ∨, and its alternative pipe |.
• Value names and covalue names are introduced with \ (lambda). In addition, cut abstractions (Wadler dual) can introduce the same kinds of names.

• Just 2 functions have any interaction with the world.
• There is no explicit recursion, binding a name such that the name can be referenced within its definition, as in
  factorial n = if n == 0 then 1 else n*factorial(n-1)
  However, recursive functions can be defined using _fix. Recursive bindings will be added to the language when their interaction with types and semantics are better understood.
• There are no field names.
• No way to represent special characters, double quotes, or backslash in strings.
• No numerals in identifiers.
• No type annotations on patterns.
• There is no let-bound or implicit polymorphism. Instantiation of generic types is explicit. To use a polymorphic name in a monomorphic sense, an explicit pattern is required.
• Type checking error messages should provide some explanation.
• Error messages should indicate the location of the error more clearly.

• No user-defined algebraic types and type constructors

• Colists
• A type name introduced by the program can conflict with a use of the same type name in an outer scope.