3

我目前正在玩一些善良的 nats，并在尝试定义矢量数据类型的应用实例时卡住了。

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

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

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

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

1 回答 1

9

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

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

于 2015-10-25T16:55:18.937 回答