Typen und Daten

• bisher: Funktionen von Daten nach Daten

  \ (x :: Int) -> x + 1

• heute: Funktionen von Typ nach Daten

  \ (t :: Type) -> \ (x :: t) -> x

• Funktionen von Typ nach Typ (ML, Haskell, Java, C#)

  \ (t :: Type) -> List t

• Funktionen von Daten nach Typ (dependent types)

  \ (t :: Typ) (n :: Int) -> Array t n

  Sprachen: Cayenne, Coq, Agda

  Eigenschaften: Typkorrektheit i. A. nicht entscheidbar,

  d. h. Programmierer muß Beweis hinschreiben.