[This page has not been updated for a long time. You may want to take a look at Agda instead./PJ 080213]
Cayenne is a simple(?) functional language with a powerful type system. The basic types are functions, products, and sums. Functions and products use dependent types to gain additional power.
There are very few building blocks in the language, but a lot of "syntactic sugar" to make it more readable.
There is no separate module language in Cayenne since the dependent types allow the normal expression language to be used at the module level as well.
The design of Cayenne has been heavily influenced by Haskell and constructive type theory and with some things borrowed from Java.
The drawback of such a powerful type system is that the type checking becomes undecidable.