Cayenne (limbaj de programare)

Cayenne este un limbaj de programare funcțional dependent, creat de Lennart Augustsson în 1998, făcându-l una dintre cele mai vechi limbi de programare dependente (spre deosebire de dovezi asistent sau cadru logic). O decizie notabilă de proiectare este aceea că limbajul permite ca funcțiile recursive nerestricționate să fie utilizate la nivelul tipului, făcând ca tipul de verificare să fie indecis.

Există foarte puține blocuri de construcție în limbă. Tipurile de bază sunt funcții, produse și sume. Funcțiile și produsele folosesc tipuri dependente pentru a obține o putere suplimentară. Sintaxa este în mare parte împrumutată de la Haskell. Nu există un sistem special de module, deoarece cu tipuri dependente de înregistrări (produse) sunt suficient de puternice pentru a defini module.

Implementarea lui Cayenne a fost scrisă în Haskell și, de asemenea, sa tradus la Haskell, dar în prezent nu mai este menținută.

Exemplu

Scopul principal al Cayenne nu este acela de a folosi tipurile pentru a exprima specificațiile (deși acest lucru se poate face), ci mai degrabă de a folosi sistemul de tip pentru a da tipului mai multe funcții. Un exemplu de funcție care poate fi dată unui tip în Cayenne este 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