GHC7.6.1为类型级别的编程带来了新特性,包括datatype promotion。以类型级自然变量和向量为例,我希望能够在依赖于基本算术法则的向量上编写函数。
不幸的是,尽管我想要的规则通常很容易通过案例分析和归纳在归纳自然语言上得到证明,但我怀疑我能否说服类型检查员相信这一点。作为一个简单的例子,下面的反向函数的类型检查需要一个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
https://stackoverflow.com/questions/12442858
复制相似问题