GHC具有类型级别的文字Nats。例如,我可以在这里读到一些关于它们的东西:
https://ghc.haskell.org/trac/ghc/wiki/TypeNats
不幸的是,关于它们的文档似乎很少,我尝试用它们做的几乎没有任何实际有效的方法。
来自this page的注释18提到了这个大小参数化的Vecs的简单示例(我添加了语言编译指示和一个导入语句):
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE TypeOperators #-}
import GHC.TypeLits
data Vec :: Nat -> * -> * where
Nil :: Vec 0 a
(:>) :: a -> Vec n a -> Vec (n+1) a
(+++) :: Vec n a -> Vec m a -> Vec (n+m) a
Nil +++ bs = bs
(a :> as) +++ bs = a :> (as +++ bs)
它当时不能工作,但后来应该修改了实现,这样它就能工作了。那是5年前的事了。但它在我的GHC 7.10.1上不起作用:
trash.hs:15:20:
Could not deduce ((n + m) ~ ((n1 + m) + 1))
from the context (n ~ (n1 + 1))
bound by a pattern with constructor
:> :: forall a (n :: Nat). a -> Vec n a -> Vec (n + 1) a,
in an equation for ‘+++’
at trash.hs:15:2-8
NB: ‘+’ is a type function, and may not be injective
Expected type: Vec (n + m) a
Actual type: Vec ((n1 + m) + 1) a
Relevant bindings include
bs :: Vec m a (bound at trash.hs:15:15)
as :: Vec n1 a (bound at trash.hs:15:7)
(+++) :: Vec n a -> Vec m a -> Vec (n + m) a
(bound at trash.hs:14:1)
In the expression: a :> (as +++ bs)
In an equation for ‘+++’: (a :> as) +++ bs = a :> (as +++ bs)
这是怎么回事?类型级别的文字Nats应该对这种事情有用吗?如果是,我该如何实现(+++)函数?如果不是,它们的用例是什么?
发布于 2015-10-29 05:23:01
正如评论者所提到的,类型检查器目前无法履行这个等式,因为它们需要代数。虽然你和我都知道n + m = n1 + m + 1
给了n = n1 + 1
,但没有人教过GHC类型检查器如何执行这种算术。在Ada、Idris或Coq这样的语言中,你可以教编译器这些规则,或者算术规则可以在库中提供给你,但在Haskell中,类型检查器有点僵化(但在我看来,对现实世界的编程来说要友好得多),不幸的是,你不得不求助于类型检查器插件。
据我所知,在这个问题上最积极的人是one Iavor Diatchki。这篇论文就在愚蠢的ACM付费墙后面,但你可以找到他的Haskell Symposium 2015 talk here on YouTube --它解释得很好!他的演讲使用了与您相同的示例,即一直流行的向量。His branch in the GHC repository致力于将其合并到主线GHC中,但据我所知还没有设定日期。现在你不得不使用typechecker插件,这并不是很糟糕。毕竟,最初的goal of Plugins/Typechecker是为了支持像这样有趣的工作,而不必将所有内容都合并到源代码中。对于模块化来说,这是有道理的!
https://stackoverflow.com/questions/31918427
复制相似问题