具有种类 nats 的向量的应用实例

Question

我目前正在尝试使用 kind nats，但在尝试定义矢量数据类型的应用实例时卡住了。

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

我卡住的问题是它将递归但取决于 nat 类型的值。

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

问题是是否可以在 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)

编辑：

我得到的错误是：

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)’

Answer 1

烹饪这个 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

给予

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

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

具有种类 nats 的向量的应用实例

Applicative instance of a vector with kind nats

haskell

data-kinds