将固定长度矢量函数应用于较长固定长度矢量的初始部分

Question

我使用ghcs扩展定义了固定长度向量GADTs,TypeOperators并且DataKinds:

data Vec n a where
    T    :: Vec VZero a
    (:.) :: a -> Vec n a -> Vec (VSucc n) a 

infixr 3 :.

data VNat  =  VZero |  VSucc VNat  -- ... promoting Kind VNat

type T1 = VSucc VZero
type T2 = VSucc T1

以及TypeOperator的以下定义:+:

type family (n::VNat) :+ (m::VNat) :: VNat 
type instance VZero :+ n = n
type instance VSucc n :+ m = VSucc (n :+ m)

为了让我的整个有意义的库有意义,我需要将一个固定长度的矢量函数类型(Vec n b)->(Vec m b)应用于较长向量的内部部分Vec (n:+k) b.我们称之为该功能prefixApp.它应该有类型

prefixApp :: ((Vec n b)->(Vec m b)) -> (Vec (n:+k) b) -> (Vec (m:+k) b)

这是一个固定长度矢量函数的示例应用程序,change2定义如下:

change2 :: Vec T2 a -> Vec T2 a
change2 (x :. y :. T) = (y :. x :. T)

prefixApp应该能够应用change2长度> = 2的任何矢量的前缀,例如

Vector> prefixApp change2 (1 :. 2 :. 3 :. 4:. T)
(2 :. 1 :. 3 :. 4 :. T)

有谁知道如何实施prefixApp？(问题是,必须使用固定长度向量函数类型的一部分来获取正确大小的前缀...)

编辑:Daniel Wagners(非常聪明!)解决方案似乎与ghc 7.6的某些候选版本(不是正式版本!)一起工作.恕我直言,它不应该工作,原因有两个:

1. 类型声明在上下文中prefixApp缺少一个VNum m(用于prepend (f b)正确检查).
2. 更有问题的是:ghc 7.4.2不假设TypeOperator :+在其第一个参数中是单射的(也不是第二个,但这里不重要),这会导致类型错误:从类型声明,我们知道vec必须有type Vec (n:+k) a和type-checker推断split vec出定义右侧的表达式是一种类型Vec (n:+k0) a.但是:类型检查器不能推断出k ~ k0(因为不能保证:+是单射的).

有谁知道第二个问题的解决方案？我怎么能:+在第一个论证中声明是单射的和/或我怎么能避免遇到这个问题呢？

Answer 1

上课:

class VNum (n::VNat) where
    split   :: Vec (n:+m) a -> (Vec n a, Vec m a)
    prepend :: Vec n a -> Vec m a -> Vec (n:+m) a

instance VNum VZero where
    split     v = (T, v)
    prepend _ v = v

instance VNum n => VNum (VSucc n) where
    split   (x :. xs)   = case split xs of (b, e) -> (x :. b, e)
    prepend (x :. xs) v = x :. prepend xs v

prefixApp :: VNum n => (Vec n a -> Vec m a) -> (Vec (n:+k) a -> (Vec (m:+k) a))
prefixApp f vec = case split vec of (b, e) -> prepend (f b) e

Answer 2

这是split不在类型类中的版本.在这里,我们为自然数(SN)构建一个单例类型,它可以在split'的定义中对'n'进行模式匹配.然后可以通过使用类型类(ToSN)来隐藏这个额外的参数.

类型Tag用于手动指定非推断参数.

(这个答案是与Daniel Gustafsson共同撰写的)

这是代码:

{-# LANGUAGE TypeFamilies, TypeOperators, DataKinds, GADTs, ScopedTypeVariables, FlexibleContexts #-}
module Vec where
data VNat = VZero | VSucc VNat  -- ... promoting Kind VNat

data Vec n a where
    T    :: Vec VZero a
    (:.) :: a -> Vec n a -> Vec (VSucc n) a·

infixr 3 :.

type T1 = VSucc VZero
type T2 = VSucc T1

data Tag (n::VNat) = Tag

data SN (n::VNat) where
  Z :: SN VZero
  S :: SN n -> SN (VSucc n)

class ToSN (n::VNat) where
  toSN :: SN n

instance ToSN VZero where
  toSN = Z

instance ToSN n => ToSN (VSucc n) where
  toSN = S toSN

type family (n::VNat) :+ (m::VNat) :: VNat
type instance VZero :+ n = n
type instance VSucc n :+ m = VSucc (n :+ m)

split' :: SN n -> Tag m -> Vec (n :+ m) a -> (Vec n a, Vec m a)
split' Z     _ xs = (T , xs)
split' (S n) _ (x :. xs) = let (as , bs) = split' n Tag xs in (x :. as , bs)

split :: ToSN n => Tag m -> Vec (n :+ m) a -> (Vec n a, Vec m a)
split = split' toSN

append :: Vec n a -> Vec m a -> Vec (n :+ m) a
append T ys = ys
append (x :. xs) ys = x :. append xs ys

prefixChange :: forall a m n k. ToSN n => (Vec n a -> Vec m a) -> Vec (n :+ k) a -> Vec (m :+ k) a
prefixChange f xs = let (as , bs) = split (Tag :: Tag k) xs in append (f as) bs