Haskell Signaturen

Die Signatur eines abstrakten Datentypen besteht aus dem Typen selbst und den Signaturen der darüber definierten Funktionen

Signatur = “Typ” eines Modules

data Map a b   
empty :: Map a b   
lookup :: Eq a => a -> Map a b -> Maybe b   
insert :: Eq a => a -> b -> Map a b -> Map a b   
delete :: Eq a => a -> Map a b -> Map a b  

Signatur informiert über:

• typkorrekte Nutzung des ADTs
• Anwendbarkeit von Funktionen
• Reihenfolge von Parametern

Signatur beschreibt nicht:

• Bedeutung und Verhalten der Funktionen (Semantik), also z.B.
• Wie werden Daten aus dem ADT ausgelesen?
• Welches Verhalten hat die Abbildung?

Haskell Eigenschaften

Eigenschaften endlicher Abbildungen

• Aus einer leeren Abbildung kann nichts ausgelesen werden
• Wenn etwas in die Abbildung geschrieben und an der gleichen Stelle ausgelesen wird, dann erhält man den geschriebenen Wert
• Wenn etwas in die Abbildung geschrieben und an einer anderen Stelle etwas ausgelesen wird, dann hat der Schreibvorgang keinen Einfluss
• Wenn zweimal an der gleichen Stelle in die Abbildung geschrieben wird, dann überschreibt der zweite den ersten Wert
• Schreiben an unterschiedlichen Stellen verhält sich kommutativ

Haskell Axiome

-- Elementare Prädikate  
s == t  
s < t  
  
-- Zusammengesetzte Prädikate  
not p  
p && q   
p || q   
p => q  

Axiome für Map

lookup a (empty :: Map Int String) == Nothing  
  
lookup a (insert a v (s :: Map Int String)) == Just v  
lookup a (delete a (s :: Map Int String)) == Nothing  
  
a /= b ==> lookup a (insert b v s) == lookup a (s :: Map Int String)  
a /= b ==> lookup a (delete b s) == lookup a (s :: Map Int String)  

Link to original

Link to original