如何使定长向量实例化为Applicative? [英] How to make fixed-length vectors instance of Applicative?

问题描述

我最近了解了晋升，并决定尝试编写向量.

I recently learned about promotion and decided to try writing vectors.

{-# LANGUAGE DataKinds, GADTs, KindSignatures #-}
module Vector where
  data Nat = Next Nat | Zero
  data Vector :: Nat -> * -> * where
    Construct :: t -> Vector n t -> Vector ('Next n) t
    Empty :: Vector 'Zero t
  instance Functor (Vector n) where
    fmap f a =
      case a of
        Construct x b -> Construct (f x) (fmap f b)
        Empty -> Empty

到目前为止，一切正常.但是，当尝试制作 Applicative 的 Vector 实例时，我遇到了一个问题.

So far, everything is working. But I ran into a problem when trying to make Vector instance of Applicative.

instance Applicative (Vector n) where
  a <*> b =
    case a of
      Construct f c ->
        case b of
          Construct x d -> Construct (f x) (c <*> d)
      Empty -> Empty
  pure x = _

我不知道该怎么做 pure .我试过了:

I had no idea how to do pure. I tried this:

case n of
  Next _ -> Construct x (pure x)
  Zero -> Empty

但变量不在范围内:第一行出现n :: Nat 错误，此表达式第三行无法将类型n与'Zero 匹配

but got Variable not in scope: n :: Nat error for the first line and Couldn't match type n with 'Zero for the third line of this expression.

因此，我使用了以下技巧.

So, I used the following hack.

class Applicative' n where
  ap' :: Vector n (t -> u) -> Vector n t -> Vector n u
  pure' :: t -> Vector n t
instance Applicative' n => Applicative' ('Next n) where
  ap' (Construct f a) (Construct x b) = Construct (f x) (ap' a b)
  pure' x = Construct x (pure' x)
instance Applicative' 'Zero where
  ap' Empty Empty = Empty
  pure' _ = Empty
instance Applicative' n => Applicative (Vector n) where
  (<*>) = ap'
  pure = pure'

它可以完成工作，但这并不漂亮.它引入了一个无用的类 Applicative'.而且每次我想在任何函数中为 Vector 使用 Applicative 时，我都必须提供额外的无用约束 Applicative'n ，该约束实际上适用于任何 n .

It gets the job done, but it's not pretty. It introduces a useless class Applicative'. And every time I want to use Applicative for Vector in any function, I have to supply the additional useless constraint Applicative' n which actually holds for any n.

什么是更好，更清洁的方法?

What would be a better, cleaner way of doing this?

推荐答案

您可以直接进行以下操作:

You could make same directly:

instance Applicative (Vector Zero) where
  a <*> b = Empty
  pure x = Empty

instance Applicative (Vector n) => Applicative (Vector (Next n)) where
  a <*> b = 
    case a of
      Construct f c ->
        case b of
          Construct x d -> Construct (f x) (c <*> d)
  pure x = Construct x (pure x)

正如我可以推断的那样:对于不同类型的类，代码应具有类型感知能力.如果您有多个实例，则不同的类型将获得不同的实现，并且很容易解决.但是，如果尝试使用单个非递归实例来实现它，则在运行时中基本上没有有关类型的信息，并且始终相同的代码仍需要确定要处理的类型.输入参数后，您可以利用GADT为您提供类型信息.但是对于 pure ，没有输入参数.因此，您必须具有 Applicative 实例的上下文.

As I can reason about it: for different types of the class, the code should be type-aware. If you had several instances, different types would get different implementation, and it would be easily resolved. But, if you try to make it with single non-recursive instance, there is basically no information about the type in runtime, and code which is always the same still needs to decide which type to handle. When you have input parameters, you can exploit GADTs to provide you the type information. But for pure there are no input parameters. So you have to have some context for the Applicative instance.

这篇关于如何使定长向量实例化为Applicative?的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！