Cayenne (Programmiersprache) - Cayenne (programming language)
Cayenne ist eine abhängig typisierte funktionale Programmiersprache , die 1998 von Lennart Augustsson entwickelt wurde. Damit ist sie eine der frühesten abhängig typisierten Programmiersprachen (im Gegensatz zu Proof-Assistenten oder logischen Frameworks ). Eine bemerkenswerte Entwurfsentscheidung ist, dass die Sprache die Verwendung unbegrenzter rekursiver Funktionen auf Typebene ermöglicht, wodurch die Typprüfung unentscheidbar wird . Die meisten abhängig typisierten Proofassistenten und später abhängig typisierten Sprachen wie Agda enthielten einen Terminierungsprüfer, um zu verhindern, dass der Typprüfer eine Schleife durchläuft, während die zeitgenössische abhängige ML die Ausdruckskraft der Sprache auf Textebene einschränkte, um die Entscheidbarkeit aufrechtzuerhalten.
Es gibt nur sehr wenige Bausteine in der Sprache, aber viel syntaktischen Zucker , um sie besser lesbar zu machen. Die Grundtypen sind Funktionen, Produkte und Summen. Funktionen und Produkte verwenden abhängige Typen, um zusätzliche Leistung zu erhalten. Die Syntax ist weitgehend von Haskell entlehnt . Es gibt kein spezielles Modulsystem, da Datensätze (Produkte) bei abhängigen Typen leistungsfähig genug sind, um Module zu definieren.
Die Cayenne-Implementierung wurde in Haskell geschrieben und auch in Haskell übersetzt, wird aber derzeit nicht mehr gewartet.
Beispiel
Das Hauptziel mit Cayenne ist nicht die Art zu verwenden Spezifikationen zum Ausdruck bringen (obwohl dies getan werden kann), sondern die verwenden Typsystem Typen mehr Funktionen zu geben. Ein Beispiel für eine Funktion, die in Cayenne einen Typ erhalten kann, ist 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