Cayenne (limbaj de programare)

Cayenne este un limbaj de programare funcțional dependent, creat de Lennart Augustsson în 1998,^[1] 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.^[2]

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

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