Cayenne programming language is a programming language created in 1998. Cayenne is a dependently typed functional programming language created by Lennart Augustsson in 1998, making it one of the earliest dependently type programming language (as opposed to proof assistant or logical framework). 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. Read more on Wikipedia...
- the Cayenne programming language wikipedia page
- Cayenne programming language first appeared in 1998
- See also: agda, dependent-ml, haskell
- Have a question about Cayenne programming language not answered here? Email me and let me know how I can help.
Example code from Wikipedia:
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
Last updated January 18th, 2020