haskell - 使用 TypeLits 追加类型级编号列表

Question

使用 GHC.TypeLits ，我们可以写一个简单的类型级编号列表(或向量)。

> {-# LANGUAGE TypeOperators, KindSignatures, GADTs, DataKinds, ScopedTypeVariables #-}

> import GHC.TypeLits

> data Vec :: * -> Nat -> * where
>   VNil :: Vec e 0
>   (:-) :: e -> Vec e n -> Vec e (n+1)

这是带有 TypeLits 的规范向量定义.直观地，追加操作应如下所示:

> vecAppend :: Vec e n -> Vec e m -> Vec e (n + m)
> vecAppend VNil vec = vec
> vecAppend (a :- as) vec = a :- vecAppend as vec

但是 GHC 的求解器在算术上存在问题:

Could not deduce (((n1 + m) + 1) ~ (n + m))
from the context (n ~ (n1 + 1))

当然，因为 n1 + 1 ~ n , (n1 + m) + 1 ~ n1 + 1 + m ~ n + m ，但求解器似乎不知道 + 的交换性和结合性(类型函数通常不是可交换的或关联的!)

我知道如果 I define type-level Peano naturals 是可能的，但我想知道是否有办法使用 GHC 中类型 nats 的当前实现(此处为 7.8.0。)

所以我试图帮助:

> vecAppend :: Vec e (n+1) -> Vec e m -> Vec e ((n + 1) + m)
> vecAppend VNil vec = vec
> vecAppend (a :- as) vec = a :- vecAppend as vec

但这只是将问题推迟到类型变量的正确实例化。

Could not deduce (((n1 + 1) + m) ~ ((n + m) + 1))
from the context ((n + 1) ~ (n1 + 1))
  bound by a pattern with constructor
             :- :: forall e (n :: Nat). e -> Vec e n -> Vec e (n + 1),
       in an equation for ‘vecAppend’
NB: ‘+’ is a type function, and may not be injective
Expected type: Vec l ((n + 1) + m)
  Actual type: Vec l ((n + m) + 1)
Relevant bindings include
  l :: Vec l m
  as :: Vec l n1
  vecAppend :: Vec l (n + 1) -> Vec l m -> Vec l ((n + 1) + m)

还有两个很像这个。

因此，让我们确定它们的范围。

> vecAppend ∷ ∀ e n m. Vec e (n+1) → Vec e m → Vec e (n + 1 + m)
> vecAppend VNil l = l
> vecAppend ((a :- (as ∷ Vec e n)) ∷ Vec e (n+1)) (l ∷ Vec e m) = a :- (vecAppend as l ∷ Vec e (n+m))

唉，

Could not deduce (n1 ~ n)
from the context ((n + 1) ~ (n1 + 1))
  bound by a pattern with constructor
             :- :: forall e (n :: Nat). e -> Vec e n -> Vec e (n + 1),
           in an equation for ‘vecAppend’
  ‘n1’ is a rigid type variable bound by
       a pattern with constructor
         :- :: forall e (n :: Nat). e -> Vec e n -> Vec e (n + 1),
       in an equation for ‘vecAppend’
  ‘n’ is a rigid type variable bound by
      the type signature for
        vecAppend :: Vec e (n + 1) -> Vec e m -> Vec e ((n + 1) + m)
Expected type: Vec e n1
  Actual type: Vec e n
Relevant bindings include
  vecAppend :: Vec e (n + 1) -> Vec e m -> Vec e ((n + 1) + m)
In the pattern: as :: Vec e n
In the pattern: a :- (as :: Vec e n)
In the pattern: (a :- (as :: Vec e n)) :: Vec e (n + 1)

有没有办法用当前的求解器来做到这一点，而不用定义你自己的 Peano nats？我更喜欢 3 的样子至 Succ (Succ (Succ Zero)))在我的类型签名中。

编辑 :由于目前似乎没有办法做到这一点(直到 GHC 7.10)，我将重新提出我的问题:任何人都可以告诉我为什么没有办法吗？不幸的是，我还没有看过 SMT 求解器，所以我不知道原则上什么是可能的。

这个想法是我对类型级计算不是很有经验，我想学会辨别我可以重新表述我的问题以便它工作的情况，以及我不能的情况(这是(目前)的一个实例后者。)

Answer 1

当然有办法。这不是一个好方法，但有一个方法.. 放置 unsafeCoerce 的全部目的在这种语言中，您知道某些内容输入正确，但 GHC 无法自行判断。所以..有办法。

这个故事应该在 GHC 7.10 中得到显着改善。目前的计划是包括一个 SMT 求解器，用于处理类型级 Nat 值。

编辑:

哦。至于为什么使用 Peano naturals 很容易，而使用类型级文字却很难:使用 Peano naturals，添加一个就是应用类型构造函数。 GHC 知道应用类型构造函数是一个单射操作。事实上，它是 GHC 类型系统的关键点之一。因此，当您使用 Peano naturals 时，您仅使用 GHC 已经非常适合处理的结构。

相比之下，GHC 对算术一无所知。它不知道 (+1)是 Nat 上的单射函数.所以它无法知道它可以导出m ~ n来自 (m + 1) ~ (n + 1) .它也没有关于 Nat 上的算术基本属性的想法。 ，例如关联性、分配性和交换性。集成 SMT 求解器背后的想法是，SMT 求解器非常擅长处理这些属性。

不过，使用 GHC 7.8，您可以轻松地将类型级文字转换为 Peano naturals:

{-# LANGUAGE DataKinds, TypeFamilies, TypeOperators, UndecidableInstances #-}

import GHC.TypeLits

data Z
data S a

type family P (n :: Nat) where
    P 0 = Z
    P n = S (P (n - 1))

这利用了新的封闭类型族特性来创建类型函数 P用于从文字转换为 Peano 表示，如下所示:

*Main> :t undefined :: P 5
undefined :: P 5 :: S (S (S (S (S Z))))