GHC 7.6.1 поставляется с новыми функциями для программирования на уровне типа, включая продвижение данных. Взяв пример о натуралах и векторах типа оттуда, я хотел бы иметь возможность писать функции на векторах, которые основываются на основных законах арифметики.
К сожалению, несмотря на то, что законы, которые я хочу, обычно легко доказывать на индуктивных naturals анализом случая и индукцией, я сомневаюсь, что я могу убедить в этом. В качестве простого примера для проверки наивной обратной функции ниже требуется подтверждение того, что 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