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