haskell - ixmap、数组和逆变仿函数之间的关系是什么？

Question

tl;dr

鉴于 ixmap 的签名和 contramap 的签名之间的相似性，我想了解 Array i e 是否是逆变第一类型论证中的仿函数，或者至少从范畴论的角度来看，这两个事物是如何相互关联的。

更长的时间

在 Chapter 12 from Real World Haskell 的末尾, 函数 ixmap被使用。

基于其签名

ixmap :: (Ix i, Ix j) => (i, i) -> (i -> j) -> Array j e -> Array i e

我忍不住注意到，一旦我们将它部分应用于第一个参数，例如我们传递给它 (1::Int, 1::Int) 为了简单起见，它的签名变成了

ixmap (1 :: Int,1 :: Int) :: Ix j => (Int -> j) -> Array j e -> Array Int e

与contramap的签名有些相似:

contramap :: (a' -> a) -> f a -> f a'

甚至更多关于 Op 的特化:

contramap :: (a' -> a0) -> Op a a0 -> Op a a'

毕竟，我认为类型 Array j e 可以被认为是将类型 j 的子集映射到类型 e< 的函数类型，一种带有“受限”j 的 j -> a。所以，就像 b -> a 是 a 中的 Functor 并且定义了 Op a b 使其成为 a b 中的逆变仿函数，我想我可以类似地定义:

newtype Array' e i = Array' { arr :: Array i e }

并为它写一个Contravariant实例:

instance Contravariant (Array' e) where
  contramap f a = undefined -- ???

令我不安的是，我不能真正将部分应用的 ixmap 用于 contramap，因为 (1) 我所做的部分应用了它？ (2) 这样做会阻止 i 类型(例如，在我的示例中为 Int)。

而且我什至想不出一种方法让 contrampa 从其他两个参数 f 中重新检索类型为 (i,i) 的所需对象::(i -> j) 和 a::Array j e，因为我没有从 j 到 i 的函数>.

Answer 1

Array 是一个 profunctor从索引重映射函数的类别到正常的 Hask 类别(无约束的 Haskell 类型，Haskell 函数作为态射)。

有一个相当普遍的 class for profunctors Hask → Hask , 但它无法表达 Ix 约束。这很容易在 constrained-categories 中表示^†虽然框架:

class (<a href="http://hackage.haskell.org/package/constrained-categories-0.4.1.0/docs/Control-Category-Constrained.html#t:Category" rel="noreferrer noopener nofollow">Category</a> r, Category t) => Profunctor p r t where
  dimap :: (<a href="http://hackage.haskell.org/package/constrained-categories-0.4.1.0/docs/Control-Category-Constrained.html#t:Object" rel="noreferrer noopener nofollow">Object</a> r a, Object r b, Object t c, Object t d)
     => r a b -> t c d -> p b c -> p a d

现在，要将其与 Array 一起实际使用，我们需要将允许索引的范围提升到类型级别。 IE。而不是使用 Int 作为索引类型——这有点不安全，因为它允许在范围之外进行索引……我们显然不能在类别理论设置中使用它! – 我们只使用一种包含允许范围的类型。与其实际将其写入 Array，不如让我使用 Vector(它不会提供不同的索引类型完全没有)作为低级表示:

{-# LANGUAGE DataKinds, TypeFamilies, AllowAmbiguousTypes, TypeApplications, ScopedTypeVariables, UnicodeSyntax #-}

import GHC.TypeLits (Nat, natVal)
import Data.Vector (Vector)
import qualified Data.Vector as V

newtype Range (lb :: Nat) (ub :: Nat)
     = Range { getIndexInRange :: Int -- from 0 to ub-lb-1
             }

newtype SafeArray i a = SafeArray {
    getFlattenedArray :: Vector a  -- length must equal `rangeLength @i`
  }

class ToLinearIndex r where
  rangeLength :: Int
  toLinearIndex :: r -> Int

instance ∀ lb ub . ToLinearIndex (Range lb ub) where
  rangeLength = fromInteger $ natVal @rb [] - natVal @lb []
  toLinearIndex = getIndexInRange
instance ∀ rx ry . (ToLinearIndex rx, ToLinearIndex ry)
     => ToLinearIndex (rx, ry) where
  rangeLength = rangeLength @rx * rangeLength @ry
  toLinearIndex (ix, iy)
      = toLinearIndex ix + rangeLength @rx * toLinearIndex iy

(!) :: ToLinearIndex i => SafeArray i a -> i -> a
SafeArray v ! i = V.unsafeIndex v $ toLinearIndex i

newtype IxMapFn r s = IxMapFn {
   getIxMapFn :: Int -> Int  -- input and output must be <rangeLength
                             -- of `r` and `s`, respectively
  }

instance Category IxMapFn where
  type Object IxMapFn i = ToLinearIndex i
  id = IxMapFn id
  IxMapFn f . IxMapFn g = IxMapFn $ f . g

saDiMap :: ∀ r s a b . (ToLinearIndex r, ToLinearIndex s)
      => IxMapFn s r -> (a -> b) -> SafeArray r a -> SafeArray s b
saDiMap (IxMapFn f) g (SafeArray v)
    = SafeArray . V.generate (rangeLength @s)
       $ g . V.unsafeIndex v . f

instance Profunctor SafeArray IxMapFn (->) where
  dimap = saDimMap

---

^†_{我从来没有想过要将 profunctor 类添加到 constrained-categories，主要是因为我认为 profunctor 在 Haskell 中有点被滥用了:通常当人们使用 endo-profunctors 时，他们实际想要表达的只是一个类别/Arrow .}