Cayenne (programming language)

Cayenne is a dependently typed functional programming language created by Lennart Augustsson in 1998,[1] making it one of the earliest dependently typed programming languages (as opposed to proof assistants or logical frameworks). A notable design decision is that the language allows unbounded recursive functions to be used on the type level, making type checking undecidable.[2] 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 (products) 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 (although this can be done), 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 (Nil)          = String
PrintfType ('%':('d':cs)) = Int    -> PrintfType cs
PrintfType ('%':('s':cs)) = String -> PrintfType cs
PrintfType ('%':( _ :cs)) =           PrintfType cs
PrintfType ( _ :cs)       =           PrintfType cs

aux :: (fmt::String) -> String -> PrintfType fmt
aux  (Nil)          out = out
aux  ('%':('d':cs)) out = \ (i::Int)    -> aux  cs (out ++ show i)
aux  ('%':('s':cs)) out = \ (s::String) -> aux  cs (out ++ s)
aux  ('%':( c :cs)) out =                  aux  cs (out ++ c : Nil)
aux  (c:cs)         out =                  aux  cs (out ++ c : Nil)

printf :: (fmt::String) -> PrintfType fmt
printf fmt = aux fmt Nil

References
  1. Augustsson, Lennart (1998). "Cayenne — a language with dependent types".
  2. Altenkirch, Thorsten; McBride, Conor; McKinna, James (April 2005). "Why dependent types matter" (PDF). Cite journal requires |journal= (help)
This article is issued from Wikipedia. The text is licensed under Creative Commons - Attribution - Sharealike. Additional terms may apply for the media files.