时间戳

首页 > 解决方案 > 如何允许一个约束在 Haskell 中暗示另一个约束？

haskell - 如何允许一个约束在 Haskell 中暗示另一个约束？

问题描述

我正在玩一些类型级别的编程，我想实现一些有趣的实例，比如Num，允许在固定长度Vector的 s 上使用数学运算符。

我目前拥有的一些相关部分如下（除了一个Functor实例）：

data Nat = One
         | Succ Nat
             deriving (Show, Eq)

data Vector (n :: Nat) a where
  VecSing :: a -> Vector 'One a
  (:+) :: a -> Vector n a -> Vector ('Succ n) a

instance Num a => Num (Vector 'One a) where
  (+) = vecZipWith (+)
  (*) = vecZipWith (*)
  abs = fmap abs
  signum = fmap signum
  negate = fmap negate
  fromInteger = VecSing . fromInteger

instance (Num a, Num (Vector n a)) => Num (Vector ('Succ n) a) where
  (+) = vecZipWith (+)
  (*) = vecZipWith (*)
  abs = fmap abs
  signum = fmap signum
  negate = fmap negate
  fromInteger a = fromInteger a :+ fromInteger a

但是，当我真正想使用这些实例时，我遇到了一个问题。这是因为，据我推测，每当我想将两个Vectors 相加时，我必须指定它们实际上是 的实例Num，如下例所示。

addAndMultiply :: (Num a) => Vector n a -> Vector n a -> Vector n a -> Vector n a
addAndMultiply a b c = (a + b) * c
-- Compilation error snippet:
-- Could not deduce (Num (Vector n a)) arising from a use of `*'
--      from the context: Num a

我想要的是一种暗示，当你有 a 时Num a，任何Vector n as 也满足约束Num。

我试着看看这个解决方案，还有这个，但我不认为它们是完全一样的。提问者通常有一个数据类型，它接受一个约束，并用装箱的值做事，而我只是想隐含地暗示另一个约束；或者至少，我认为我愿意。

这可能吗？如果是这样，怎么做？

标签： haskelltype-level-computation

解决方案

首先，您实际上不需要在任何 num/vector-space 实例中解构大小参数。无论如何，实现基本上只是将所有内容传递给Functor实例；如果你还实现了Applicative一个，那么你可以基于它来做所有事情，比如

instance Num a => AdditiveGroup (Vector n a) where
  zeroV = pure 0
  negateV = fmap negate
  (^+^) = liftA2 (+)
instance Num a => VectorSpace (Vector n a) where
  type Scalar (Vector n a) = a
  μ *^ v = fmap (μ*) v

但是，这当然依赖于首先让该Applicative实例真正具有任意性n。这在直觉上应该是可能的，因为这两个构造函数Nat都会产生实例，但实际上编译器需要类型类形式的一些额外帮助。在类型级 nats 的标准版本中，这是KnownNat; 对于您自己的版本，您可以这样做：

{-# LANGUAGE GADTs, KindSignatures, TypeInType #-}
import Data.Kind

data NatS :: Nat -> Type where
  OneS :: NatS One
  SuccS :: KnownNat n => NatS (Succ n)

class KnownNat (n :: Nat) where
  natSing :: NatS n  -- I like to call such values “witnesses”, but
                     -- the conventional terminology is “singletons”.

instance KnownNat 'One where
  natSing = OneS
instance KnownNat n => KnownNat ('Succ n) where
  natSing = SuccS

然后以此为基础的仿函数实例：

{-# LANGUAGE ScopedTypeVariables, UnicodeSyntax, TypeApplications #-}
instance ∀ n . KnownNat n => Functor (Vector n) where
  fmap f = case natSing @n of
    OneS -> \(VecSing x) -> VecSing $ f x
    SuccS -> \(x :+ v) -> f x :+ fmap f v

同样对于Applicative。

然后，对于VectorSpace等实例，您不再需要显式处理这些单例，只需提及KnownNat n，您就可以利用该Applicative实例。

推荐阅读