GHC 7.6.1 поставляется с новыми функциями для программирования на уровне типов, в том числепродвижение типа данных, Взяв пример о натуральных числах и векторах на уровне типов, я хотел бы иметь возможность писать функции для векторов, которые основаны на основных законах арифметики.

К сожалению, даже несмотря на то, что законы, которые я хочу, обычно легко доказать на индуктивных натуральных факторах с помощью анализа случаев и индукции, я сомневаюсь, что смогу убедить в этом проверку типов. В качестве простого примера, проверка типа наивной обратной функции ниже требует доказательства того, чтоn + Su Ze ~ Su n.

Есть ли какой-нибудь способ, которым я могу предоставить это доказательство, или я действительно сейчас нахожусь в сфере полноценных зависимых типов?

{-# 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