Cayenne (programming language)


Cayenne is a dependently typed functional programming language created by Lennart Augustsson in 1998, making it one of the earliest dependently typed programming languages. A notable design decision is that the language allows unbounded recursive functions to be used on the type level, making type checking undecidable. Most dependently typed proof assistants and later dependently typed languages such as Agda included a termination checker to prevent the type checker from looping, while the contemporary Dependent ML restricted the expressivity of the type-level language to maintain decidability.
There are very few building blocks in the language, but much syntactic sugar to make it more readable. The basic types are functions, products, and sums. Functions and products use dependent types to gain additional power. The syntax is largely borrowed from Haskell. There is no special module system, because with dependent types records are powerful enough to define modules.
The Cayenne implementation was written in Haskell, and it also translated to Haskell, but is currently no longer being maintained.

Example

The main aim with Cayenne is not to use the types to express specifications, but rather to use the type system to give type to more functions. An example of a function that can be given a type in Cayenne is printf.

PrintfType :: String -> #
PrintfType = String
PrintfType = Int -> PrintfType cs
PrintfType = String -> PrintfType cs
PrintfType = PrintfType cs
PrintfType = PrintfType cs
aux :: -> String -> PrintfType fmt
aux out = out
aux out = \ -> aux cs
aux out = \ -> aux cs
aux out = aux cs
aux out = aux cs
printf :: -> PrintfType fmt
printf fmt = aux fmt Nil