具有类型 nat 的向量的应用实例

我目前正在与善良的人玩耍，并在尝试定义矢量数据类型的应用实例时陷入困境。

我认为一个合理的例子是pure 1 :: Vec 3 Int会给我一个长度为 3 的向量，所有元素均为值 1 和<*>运算符将函数与值压缩在一起。

我陷入困境的问题是它将是递归的，但取决于 nat 类型的值。

正如你在下面看到的，我使用了很多编译指示（我什至不知道哪些是必要的）和我发现的一些技巧（n ~ (1 + n0) and OVERLAPPINGpragmas）但似乎没有一个对我有用。

问题是是否可以用 Haskell 进行编码，如果可以，我错过了什么？

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE InstanceSigs #-}

import GHC.TypeLits


data Vec :: (Nat -> * -> *) where
  Nil  :: Vec 0 a
  Cons :: a -> Vec n a -> Vec (1 + n) a

instance Functor (Vec n) where
  fmap f Nil = Nil
  fmap f (Cons a as) = Cons (f a) (fmap f as)

instance {-# OVERLAPPING #-} Applicative (Vec 0) where
  pure _ = Nil
  a <*> b = Nil

instance {-# OVERLAPPABLE #-} n ~ (1 + n0) => Applicative (Vec n) where
  pure :: n ~ (1 + n0) => a -> Vec n a
  pure v = Cons v (pure v :: Vec n0 a)

  (<*>) :: n ~ (1 + n0) => Vec n (a -> b) -> Vec n a -> Vec n b
  (Cons f fs) <*> (Cons v vs) = Cons (f v) (fs <*> vs :: Vec n0 b)

EDIT:

我得到的错误是：

Could not deduce (a ~ a1)
from the context (Functor (Vec n), n ~ (1 + n0))
  bound by the instance declaration at Vectors.hs:27:31-65
  ‘a’ is a rigid type variable bound by
      the type signature for pure :: (n ~ (1 + n0)) => a -> Vec n a
      at Vectors.hs:28:11
  ‘a1’ is a rigid type variable bound by
       an expression type signature: Vec n1 a1 at Vectors.hs:29:20
Relevant bindings include
  v :: a (bound at Vectors.hs:29:8)
  pure :: a -> Vec n a (bound at Vectors.hs:29:3)
In the first argument of ‘pure’, namely ‘v’
In the second argument of ‘Cons’, namely ‘(pure v :: Vec n0 a)’

煮这个的方法不止一种Applicative实例。本杰明的评论指出了我通常的做法。您尝试这样做的方式也是有道理的。至少原则上是这样。我担心它在实践中会很困难，因为TypeLits机器对数字的了解还不够。问题归结如下：

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE ScopedTypeVariables #-}

module AV where

import GHC.TypeLits

grumble :: forall (f :: Nat -> *) (n :: Nat)(j :: Nat)(k :: Nat).
           (n ~ (1 + j), n ~ (1 + k)) => f j -> f k
grumble x = x

gives

Could not deduce (j ~ k)
from the context (n ~ (1 + j), n ~ (1 + k))

在这种情况下，要说服 GHC 两条尾巴具有相同的长度将是非常棘手的Cons for <*>没有承认1 +是单射的。