Cayenne programming language

Cayenne programming language is a historical 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...

21Years Old

20Users

0Jobs

• Cayenne programming language ranks in the top 50% of languages
• the Cayenne programming language wikipedia page
• Cayenne programming language first appeared in 1998
• See also: agda, dependent-ml, haskell
• I have 24 facts about Cayenne programming language. what would you like to know? 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 July 22nd, 2019