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
- ↑ Augustsson, Lennart (1998). "Cayenne — a language with dependent types".
- ↑ Altenkirch, Thorsten; McBride, Conor; McKinna, James (April 2005). Why dependent types matter. http://www.cs.nott.ac.uk/~txa/publ/ydtm.pdf.
 |
