使用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但是解算器似乎并不知道交换性和关联性+(类型函数通常不是交换的或关联的!)

我知道如果我定义类型级别的Peano自然是可能的,但是我想知道是否有办法在GHC中使用类型nat的当前实现(7.8.0 here.)

所以我试着帮忙:

> 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自然很容易,而且类型级文字很难:使用Peano自然,添加一个是应用类型构造函数.GHC知道应用类型构造函数是一个内射运算.事实上,它是GHC类型系统的关键点之一.因此,当您使用Peano天然产品时,您只需要使用GHC已经非常适合处理的结构.

相比之下,GHC并不知道有关算术的事情.它不知道这(+1)是一个内射函数Nat.所以它无法知道它可以从中衍生m ~ n出来(m + 1) ~ (n + 1).它也没有关于算术的基本属性的想法Nat,如关联,分配和交换属性.集成SMT求解器背后的想法是SMT求解器非常擅长处理这些属性.

使用GHC 7.8,您可以轻松地将类型级文字转换为Peano自然文件,但是:

{-# 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))))