haskell - 使用静态大小列表减少堆栈溢出

Question

我有以下代码实现静态大小的向量，这些向量实现为编译良好的列表:

{-# OPTIONS_GHC -fplugin GHC.TypeLits.Normalise #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE IncoherentInstances #-}

import GHC.TypeLits

infixr 5 :.
data Vector :: Nat -> * -> * where
  (:-:):: Vector 0 a
  (:.) :: a -> Vector (n-1) a -> Vector n a

deriving instance Show a => Show (Vector n a)

instance Functor (Vector n) where
  fmap f (:-:) = (:-:)
  fmap f (x :. xs) = f x :. fmap f xs

type x > y = CmpNat x y ~ 'GT

instance Applicative (Vector 0) where
  pure f    = (:-:)
  (<*>) _ _ = (:-:)

instance (Applicative (Vector (n-1)), n > 0 ) => Applicative (Vector n) where
  pure (f::a)          = f :. (pure f :: Vector (n-1) a)
  (f:.fs) <*> (x:.xs) = f x :. (fs <*> xs)

但是，当我尝试为这些向量定义元素总和时，如下所示:

(<+>) :: Num a => Vector n a -> Vector n a -> Vector n a
v1 <+> v2 = (+) <$> v1 <*> v2

我收到编译错误

Reduction stack overflow; size = 201
When simplifying the following type: Applicative (Vector s0)
(...)
In the expression: (+) <$> v1 <*> v2

如果我可以在 ghci 中输入右 watch 达式并且工作正常，那么导致此错误的原因是什么？将来如何避免它？

我正在使用 ghc 8.0.1 和 natnormalize 0.5.2

Answer 1

A guess: don't you need to put the [constraints] in the signature of (<+>) as well?

[您的]Applicative约束建议有效。您能否详细说明为什么我需要指定 (Vector n)是 Applicative 的实例，因为所有向量长度都应该实例化为 applicatives？

简而言之，GHC 无法归纳得出该结论。相反，类型检查器在被告知您需要 Applicative (Vector n) 时会做什么正在退后一步，看着 Applicative (Vector (n - 1)) ，以便查看是否 (Applicative (Vector (n - 1)), n > 0) => Applicative n很满意。因为您没有使用混凝土 n ，永远不会终止(这是与特定值的测试的区别)。既然如此，您需要提供额外的信息。顺便说一句，如果您尝试一些更平淡的事情，您将得到相同的“归约堆栈溢出”错误，例如:

GHCi> :t undefined == (undefined :: [[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[[a]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]]])

自 Eq [a]需要Eq a ，如果a ~ [b]然后Eq b还必须进行检查，等等。

另一方面，据我所知，更常见的做法是用 KnownNat 来编写此类约束。而不是例如Applicative ，为了最大限度地减少必须在函数签名中传播的约束量。比照。例如the source of CLaSH.Sized.Vector (比我更精通这种类型级编程的人可能能够提供更具体的建议)。