GHC 7.6.1 enthält neue Funktionen für die Programmierung auf Typebene, einschließlichDatentyp-Promotion. Am Beispiel von Typnaturalen und Vektoren möchte ich Funktionen auf Vektoren schreiben können, die sich auf Grundgesetze der Arithmetik stützen.

Obwohl die Gesetze, die ich will, normalerweise leicht durch Fallanalyse und Induktion auf induktiven Naturalien zu beweisen sind, bezweifle ich, dass ich den Typprüfer davon überzeugen kann. Als einfaches Beispiel erfordert die Überprüfung der naiven Umkehrfunktion einen Beweis dafürn + Su Ze ~ Su n.

Gibt es eine Möglichkeit, diesen Beweis zu erbringen, oder bin ich jetzt wirklich im Bereich ausgewachsener abhängiger Typen?

{-# LANGUAGE DataKinds, KindSignatures, GADTs, TypeFamilies, TypeOperators #-}

data Nat = Ze | Su Nat

data Vec :: * -> Nat -> * where
  Nil  :: Vec a Ze
  Cons :: a -> Vec a n -> Vec a (Su n)

type family (m :: Nat) + (n :: Nat) :: Nat

type instance Ze + n = n
type instance (Su m + n) = Su (m + n)

append :: Vec a m -> Vec a n -> Vec a (m + n)
append Nil ys = ys
append (Cons x xs) ys = Cons x (append xs ys)

rev :: Vec a n -> Vec a n
rev Nil = Nil
rev (Cons x xs) = rev xs `append` Cons x Nil