首页
学习
活动
专区
工具
TVP
发布
社区首页 >问答首页 >我可以向类型检查器提供GHC 7.6中归纳自然数的证明吗?

我可以向类型检查器提供GHC 7.6中归纳自然数的证明吗?
EN

Stack Overflow用户
提问于 2012-09-16 06:03:37
回答 1查看 658关注 0票数 18

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
EN
页面原文内容由Stack Overflow提供。腾讯云小微IT领域专用引擎提供翻译支持
原文链接:

https://stackoverflow.com/questions/12442858

复制
相关文章

相似问题

领券
问题归档专栏文章快讯文章归档关键词归档开发者手册归档开发者手册 Section 归档