首页
学习
活动
专区
工具
TVP
发布
社区首页 >问答首页 >将定长向量函数应用于较长的定长向量的起始部分

将定长向量函数应用于较长的定长向量的起始部分
EN

Stack Overflow用户
提问于 2012-09-01 02:54:26
回答 3查看 587关注 0票数 16

我使用ghcs扩展GADTsTypeOperatorsDataKinds对固定长度向量的定义如下:

代码语言:javascript
复制
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 :+的以下定义:

代码语言:javascript
复制
type family (n::VNat) :+ (m::VNat) :: VNat 
type instance VZero :+ n = n
type instance VSucc n :+ m = VSucc (n :+ m)

为了让我的整个意图库有意义,我需要对一个较长的向量Vec (n:+k) b的初始部分应用一个(Vec n b)->(Vec m b)类型的固定长度的向量函数。让我们将该函数称为prefixApp。它应该有类型

代码语言:javascript
复制
prefixApp :: ((Vec n b)->(Vec m b)) -> (Vec (n:+k) b) -> (Vec (m:+k) b)

下面是一个示例应用程序,其中的固定长度向量函数change2定义如下:

代码语言:javascript
复制
change2 :: Vec T2 a -> Vec T2 a
change2 (x :. y :. T) = (y :. x :. T)

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

代码语言:javascript
复制
Vector> prefixApp change2 (1 :. 2 :. 3 :. 4:. T)
(2 :. 1 :. 3 :. 4 :. T)

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

编辑:Daniel Wagners (非常聪明!)这个解决方案似乎适用于GHC7.6的一些候选版本(不是官方版本!)。然而,我认为它不能工作,有两个原因:

  1. prefixApp的类型声明在上下文中缺少代码(为了让prepend (f b)检查类型更有问题: ghc 7.4.2在第一个参数中没有假设TypeOperator代码是内射的(第二个参数也不是,但这在这里不是必需的),这会导致类型错误:从类型声明中,我们知道vec必须具有类型代码,并且类型检查器为定义右侧的表达式split vec推断出< :+ >D29vec>的类型。但是:类型检查器不能推断k ~ k0 (因为不能保证:+是内射的)。

有没有人知道第二个问题的解决方案?我如何在第一个参数中声明:+是内射的,以及/或者我如何避免遇到这个问题?

EN

回答 3

Stack Overflow用户

回答已采纳

发布于 2012-09-06 22:53:40

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

type标记用于手动指定非推断参数。

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

代码如下:

代码语言:javascript
复制
{-# 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
票数 7
EN

Stack Overflow用户

发布于 2012-09-01 03:41:24

创建一个类:

代码语言:javascript
复制
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
票数 7
EN

Stack Overflow用户

发布于 2012-09-05 00:12:46

如果你能接受一种稍微不同类型的prefixApp:

代码语言:javascript
复制
{-# LANGUAGE GADTs, TypeOperators, DataKinds, TypeFamilies #-}

import qualified Data.Foldable as F


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

type T1 = VSucc VZero
type T2 = VSucc T1
type T3 = VSucc T2

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

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


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

infixr 3 :.

-- Just to define Show for Vec
instance F.Foldable (Vec n) where
    foldr _ b T = b
    foldr f b (a :. as) = a `f` F.foldr f b as

instance Show a => Show (Vec n a) where
    show = show . F.foldr (:) []


class Splitable (n::VNat) where
    split :: Vec k b -> (Vec n b, Vec (k:-n) b)

instance Splitable VZero where
    split r = (T,r)

instance Splitable n => Splitable (VSucc n) where
    split (x :. xs) =
        let (xs' , rs) = split xs
        in ((x :. xs') , rs)

append :: Vec n a -> Vec m a -> Vec (n:+m) a
append T r = r
append (l :. ls) r = l :. append ls r

prefixApp :: Splitable n => (Vec n b -> Vec m b) -> Vec k b -> Vec (m:+(k:-n)) b
prefixApp f v = let (v',rs) = split v in append (f v') rs

-- A test
inp :: Vec (T2 :+ T3) Int
inp = 1 :. 2 :. 3 :. 4:. 5 :. T

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

test = prefixApp change2 inp -- -> [2,1,3,4,5]

实际上,您的原始签名也可以使用(通过增强的上下文):

代码语言:javascript
复制
prefixApp :: (Splitable n, (m :+ k) ~ (m :+ ((n :+ k) :- n))) =>
             ((Vec n b)->(Vec m b)) -> (Vec (n:+k) b) -> (Vec (m:+k) b)
prefixApp f v = let (v',rs) = split v in append (f v') rs

适用于7.4.1

更新:只是为了好玩,在Agda中的解决方案:

代码语言:javascript
复制
data Nat : Set where
  zero : Nat
  succ : Nat -> Nat

_+_ : Nat -> Nat -> Nat
zero + r = r
succ n + r = succ (n + r)

data _*_ (A B : Set) : Set where
  _,_ : A -> B -> A * B

data Vec (A : Set) : Nat -> Set where
  [] : Vec A zero
  _::_ : {n : Nat} -> A -> Vec A n -> Vec A (succ n)

split : {A : Set}{k n : Nat} -> Vec A (n + k) -> (Vec A n) * (Vec A k)
split {_} {_} {zero} v = ([] , v)
split {_} {_} {succ _} (h :: t) with split t
... | (l , r) = ((h :: l) , r)

append : {A : Set}{n m : Nat} -> Vec A n -> Vec A m -> Vec A (n + m)
append [] r = r
append (h :: t) r with append t r
... | tr = h :: tr

prefixApp : {A : Set}{n m k : Nat} -> (Vec A n -> Vec A m) -> Vec A (n + k) -> Vec A (m + k)
prefixApp f v with split v
... | (l , r) = append (f l) r
票数 4
EN
页面原文内容由Stack Overflow提供。腾讯云小微IT领域专用引擎提供翻译支持
原文链接:

https://stackoverflow.com/questions/12221080

复制
相关文章

相似问题

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