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...

22Years Old 20Users ?Jobs

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 August 9th, 2020

Edit Cayenne programming language on GitHub