代码之家 › 专栏 › 技术社区 › Liisi

如何使定长向量实例具有应用性?

gadt typeclass pattern-matching types haskell

Liisi · 技术社区 · 7 年前

我最近了解了晋升,决定尝试写向量。

{-# LANGUAGE DataKinds, GADTs, KindSignatures #-}
module Vector where
  data Nat = Next Nat | Zero
  data Vector :: Nat -> * -> * where
    Construct :: t -> Vector n t -> Vector ('Next n) t
    Empty :: Vector 'Zero t
  instance Functor (Vector n) where
    fmap f a =
      case a of
        Construct x b -> Construct (f x) (fmap f b)
        Empty -> Empty

到目前为止,一切正常。但我在尝试 Vector 的实例 Applicative 。

instance Applicative (Vector n) where
  a <*> b =
    case a of
      Construct f c ->
        case b of
          Construct x d -> Construct (f x) (c <*> d)
      Empty -> Empty
  pure x = _

我不知道该怎么办 pure 。我试过这个:

case n of
  Next _ -> Construct x (pure x)
  Zero -> Empty

但是得到了 Variable not in scope: n :: Nat 第一行错误和 Couldn't match type n with 'Zero 对于此表达式的第三行。

因此,我使用了以下黑客。

class Applicative' n where
  ap' :: Vector n (t -> u) -> Vector n t -> Vector n u
  pure' :: t -> Vector n t
instance Applicative' n => Applicative' ('Next n) where
  ap' (Construct f a) (Construct x b) = Construct (f x) (ap' a b)
  pure' x = Construct x (pure' x)
instance Applicative' 'Zero where
  ap' Empty Empty = Empty
  pure' _ = Empty
instance Applicative' n => Applicative (Vector n) where
  (<*>) = ap'
  pure = pure'

它完成了任务,但并不漂亮。它引入了一个无用的类 Applicative' 。每次我想用 实用的 对于 矢量 在任何函数中,我都必须提供额外的无用约束 Applicative' n 这实际上适用于任何 n 。

有什么更好、更干净的方法可以做到这一点?

4 回复 | 直到 7 年前

max630 7 年前

您可以直接这样做:

instance Applicative (Vector Zero) where
  a <*> b = Empty
  pure x = Empty

instance Applicative (Vector n) => Applicative (Vector (Next n)) where
  a <*> b = 
    case a of
      Construct f c ->
        case b of
          Construct x d -> Construct (f x) (c <*> d)
  pure x = Construct x (pure x)

正如我可以推理的那样:对于不同类型的类,代码应该是类型感知的。如果您有多个实例,不同的类型将得到不同的实现,并且很容易解决。但是,如果您尝试使用单个非递归实例,则在运行时基本上没有关于该类型的信息,并且始终相同的代码仍然需要决定要处理的类型。当您有输入参数时,可以利用GADT为您提供类型信息。但对于 pure 没有输入参数。所以你必须有一些背景 Applicative 例子

chi 7 年前

这是利用 singletons 包裹

粗略地说,Haskell不允许我们在类型级别的值上进行模式匹配,例如 n 在上述代码中。具有 单件 ,我们可以,但需要并提供一些 SingI 到处都是。

{-# LANGUAGE GADTs , KindSignatures, DataKinds, TemplateHaskell, 
             TypeFamilies, ScopedTypeVariables #-}
{-# OPTIONS -Wall #-}

import Data.Singletons.TH

-- Autogenerate singletons for this type
$(singletons [d|
   data Nat = Next Nat | Zero
   |])

-- as before
data Vector :: Nat -> * -> * where
   Construct :: t -> Vector n t -> Vector ('Next n) t
   Empty :: Vector 'Zero t

-- as before
instance Functor (Vector n) where
   fmap _ Empty = Empty
   fmap f (Construct x b) = Construct (f x) (fmap f b)        

-- We now require n to carry its own SingI instance.
-- This allows us to pattern match on n.
instance SingI n => Applicative (Vector n) where
   Empty <*> Empty = Empty
   -- Here, we need to access the singleton on n, so that later on we
   -- can provide the SingI (n-1) instance we need for the recursive call.
   -- The withSingI allows us to use m :: SNat (n-1) to provide the instance.
   (Construct f c) <*> (Construct x d) = case sing :: SNat n of
      SNext m -> withSingI m $ Construct (f x) (c <*> d)

   -- Here, we can finally pattern match on n.
   -- As above, we need to provide the instance with withSingI
   -- to the recursive call.
   pure x = case sing :: SNat n of
      SZero -> Empty
      SNext m -> withSingI m $ Construct x (pure x)

使用此选项需要提供 SingI n 实例,这有点不方便,但不是太多(IMO)。可悲的是 <*> 真的不需要 SingI n公司 ,因为原则上,它可以从手头的两个向量重新计算。然而 pure 没有输入向量,因此它只能与提供的单例进行模式匹配。

作为另一种选择,与原始代码类似,可以编写

instance Applicative (Vector Zero) where
   ...
instance Applicative (Vector n) => Applicative (Vector (Next n)) where
   ...

这不是完全等效的,需要添加上下文 Applicative (Vector n) => 在以后的所有函数中 n 未知,但可能足以用于多种用途。

K. A. Buhr 7 年前

将此视为@chi答案的附录,以提供对单例方法的额外解释。。。

我建议阅读 Hasochism paper 如果您还没有这样做。特别是,在那篇文章的第3.1节中,他们正好处理了这个问题,并将其作为一个激励示例,说明当隐式单例参数( SingI 关于@chi的答案 NATTY Hasochism论文中的type class)是必要的,而不仅仅是方便的。

由于它适用于您的代码,主要问题是 pure 需要一个应该生成的向量长度的运行时表示,以及类型级别变量 n 不符合要求。解决方案是引入一个新的GADT,即“单例”,它提供与升级类型直接对应的运行时值 Next 和 Zero :

data Natty (n :: Nat) where
  ZeroTy :: Natty Zero
  NextTy :: Natty n -> Natty (Next n)

我尝试使用与论文大致相同的命名约定: Natty 是相同的,并且 ZeroTy 和 NextTy 与报纸的 Zy 和 Sy 。

就其本身而言,这个显式单例是有用的。例如,请参见 vchop 在报纸上。此外,我们可以很容易地编写 纯净的 这需要显式单例来完成其工作:

vcopies :: Natty n -> a -> Vector n a
vcopies ZeroTy _ = Empty
vcopies (NextTy n) x = Construct x (vcopies n x)

我们还不能用这个来定义 纯净的 但是,因为 纯净的 的签名由 Applicative 类型,我们无法压缩显式单例 Natty n 在那里。

解决方案是引入隐式单例,它允许我们在需要时通过 natty 函数在以下类型类的上下文中:

class NATTY n where
  natty :: Natty n
instance NATTY Zero where
  natty = ZeroTy
instance NATTY n => NATTY (Next n) where
  natty = NextTy natty

现在,如果我们在 NATTY n 上下文,我们可以调用 vcopies natty 提供 vcopies 具有明确的 整洁时髦的 参数,它允许我们写入:

instance NATTY n => Applicative (Vector n) where
  (<*>) = vapp
  pure = vcopies natty

使用的定义 vcopies 和 整洁时髦的 以及 vapp 以下内容:

vapp :: Vector n (a -> b) -> Vector n a -> Vector n b
vapp Empty Empty = Empty
vapp (Construct f c) (Construct x d) = Construct (f x) (vapp c d)

请注意一个奇怪之处。我们需要介绍一下 vapp 助手函数,原因不明。以下实例没有 纳蒂 匹配您的 case -基于定义和类型检查精细:

instance Applicative (Vector n) where
  Empty <*> Empty = Empty
  Construct f c <*> Construct x d = Construct (f x) (c <*> d)
  pure = error "Argh!  No NATTY!"

如果我们添加 纳蒂 要定义的约束 纯净的 :

instance NATTY n => Applicative (Vector n) where
  Empty <*> Empty = Empty
  Construct f c <*> Construct x d = Construct (f x) (c <*> d)
  pure = vcopies natty

定义 (<*>) 不再进行类型检查。问题是 纳蒂n 第二个左侧的约束 (<*>) case并不自动意味着 NATTY n1 右侧约束(其中 Next n ~ n1 ),所以GHC不想让我们打电话 (<*>) 在右侧。在这种情况下,由于约束在第一次使用后实际上并不需要,因此没有 纳蒂 约束,即 vapp ,解决了问题。

@chi在上使用大小写匹配 整洁时髦的 和helper函数 withSingI 作为替代解决方案。这里的等效代码将使用一个helper函数,该函数将显式单例转换为隐式单例 纳蒂 上下文:

withNATTY :: Natty n -> (NATTY n => a) -> a
withNATTY ZeroTy a = a
withNATTY (NextTy n) a = withNATTY n a

允许我们编写:

instance NATTY n => Applicative (Vector n) where
  Empty <*> Empty = Empty
  Construct f c <*> Construct x d = case (natty :: Natty n) of
    NextTy n -> withNATTY n $ Construct (f x) (c <*> d)
  pure x = case (natty :: Natty n) of
    ZeroTy -> Empty
    NextTy n -> Construct x (withNATTY n $ pure x)

这两者都需要 ScopedTypeVariables 和 RankNTypes 。

无论如何,坚持使用helper函数,整个程序如下所示:

{-# LANGUAGE DataKinds, GADTs, KindSignatures #-}

module Vector where

data Nat = Next Nat | Zero
data Vector :: Nat -> * -> * where
  Construct :: t -> Vector n t -> Vector ('Next n) t
  Empty :: Vector 'Zero t

data Natty (n :: Nat) where
  ZeroTy :: Natty Zero
  NextTy :: Natty n -> Natty (Next n)

class NATTY n where
  natty :: Natty n
instance NATTY Zero where
  natty = ZeroTy
instance NATTY n => NATTY (Next n) where
  natty = NextTy natty

instance Functor (Vector n) where
  fmap f a =
    case a of
      Construct x b -> Construct (f x) (fmap f b)
      Empty -> Empty

instance NATTY n => Applicative (Vector n) where
  (<*>) = vapp
  pure = vcopies natty

vapp :: Vector n (a -> b) -> Vector n a -> Vector n b
vapp Empty Empty = Empty
vapp (Construct f c) (Construct x d) = Construct (f x) (vapp c d)

vcopies :: Natty n -> a -> Vector n a
vcopies ZeroTy _ = Empty
vcopies (NextTy n) x = Construct x (vcopies n x)

与 singletons 图书馆是:

$(singletons [d|
  data Nat = Next Nat | Zero
  |])

自动生成单例(使用构造函数 SZero 和 SNat 而不是 零度 和 NatTy ;和类型 SNat公司 而不是 整洁时髦的 )和隐式singleton类(称为 辛格 而不是 纳蒂 以及使用函数 sing 而不是 整洁时髦的 ),给出完整的程序:

{-# LANGUAGE DataKinds, GADTs, KindSignatures, TemplateHaskell, TypeFamilies #-}

module Vector where

import Data.Singletons
import Data.Singletons.TH

$(singletons [d|
  data Nat = Next Nat | Zero
  |])

data Vector :: Nat -> * -> * where
  Construct :: t -> Vector n t -> Vector ('Next n) t
  Empty :: Vector 'Zero t

instance Functor (Vector n) where
  fmap f a =
    case a of
      Construct x b -> Construct (f x) (fmap f b)
      Empty -> Empty

instance SingI n => Applicative (Vector n) where
  (<*>) = vapp
  pure = vcopies sing

vapp :: Vector n (a -> b) -> Vector n a -> Vector n b
vapp Empty Empty = Empty
vapp (Construct f c) (Construct x d) = Construct (f x) (vapp c d)

vcopies :: SNat n -> a -> Vector n a
vcopies SZero _ = Empty
vcopies (SNext n) x = Construct x (vcopies n x)

更多关于 单件 图书馆的功能和建造方式,我建议阅读 Introduction to Singletons 。

dfeuer 7 年前

其他几个答案引入了 Natty 或 SNat 要实施的类型 pure 。实际上,拥有这样的类型大大减少了对一次性类型类的需要。传统的 整洁时髦的 / SNat公司 然而,GADT是您的程序将实际构建表示,然后使用它,即使 Nat 在编译时已知。这通常 不会的 使用辅助类方法。您可以通过使用不同的表示来绕过此问题。

我将使用以下名称:

data Nat = Z | S Nat

假设我们定义

data Natty n where
  Zy :: Natty 'Z
  Sy :: Natty n -> Natty ('S n)

我们可以这样写它的消除器(感应原理):

natty :: p 'Z -> (forall k. p k -> p ('S k)) -> Natty n -> p n
natty z _ Zy = z
natty z s (Sy n) = s (natty z s n)

就我们的目的而言,我们真的不需要 整洁时髦的 ;我们只需要它的归纳原理!那么让我们定义另一个版本。我想这种编码有一个合适的名称,但我不知道它可能是什么。

newtype NatC n = NatC
  { unNatC :: forall p.
              p 'Z  -- base case
           -> (forall k. p k -> p ('S k))  -- inductive step
           -> p n }

这与 整洁时髦的 :

nattyToNatC :: Natty n -> NatC n
nattyToNatC n = NatC (\z s -> natty z s n)

natCToNatty :: NatC n -> Natty n
natCToNatty (NatC f) = f Zy Sy

现在我们可以为 Nat公司 我们知道如何消除:

class KnownC n where
  knownC :: NatC n
instance KnownC 'Z where
  knownC = NatC $ \z _ -> z
instance KnownC n => KnownC ('S n) where
  knownC = NatC $ \z s -> s $ unNatC knownC z s

现在,这里有一个向量类型(我已经重命名了东西以符合我自己的口味):

infixr 4 :<
data Vec :: Nat -> * -> * where
  (:<) :: t -> Vec n t -> Vec ('S n) t
  Nil :: Vec 'Z t

因为 Vec 的长度参数不是最后一个,我们必须将其翻转才能用于 NatC :

newtype Flip f a n = {unFlip :: f n a}

induct2 :: f 'Z a
         -> (forall k. f k a -> f ('S k) a)
         -> NatC n -> f n a
induct2 z s n = unFlip $ unNatC n (Flip z) (\(Flip r) -> Flip (s r))

replC :: NatC n -> a -> Vec n a
replC n a = induct2 Nil (a :<) n

instance KnownC n => Applicative (Vec n) where
   pure = replC knownC
   (<*>) = ...

现在,如果向量长度在编译时已知,则 纯净的 矢量将直接构建,无需中间结构。