在没有 `unsafeCoerce` 的情况下将值更改为 `Conkin.Traversable` 中的索引

Question

使用conkin 包：https://hackage.haskell.org/package/conkin

我希望能够获取任何 Conkin.Traversable 并将其转储到 Tuple 留下 indices 到 Tuple 中，以便我可以重建它。

我正在使用一些语言扩展：

{-# LANGUAGE DataKinds                 #-}
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE GADTs                     #-}
{-# LANGUAGE KindSignatures            #-}
{-# LANGUAGE PolyKinds                 #-}
{-# LANGUAGE RankNTypes                #-}
{-# LANGUAGE ScopedTypeVariables       #-}
{-# LANGUAGE TypeOperators             #-}

模块声明

module TupleDump where

进口

import           Control.Monad.State  (State, runState)
import qualified Control.Monad.State  as State
import           Data.Functor.Compose (getCompose)
import           Data.Functor.Const   (Const (Const), getConst)
import           Conkin               (Dispose (..), Flip (..), Tuple (..))
import qualified Conkin

我不想使用 unsafeCoerce，但看不到绕过它的方法：

import           Unsafe.Coerce        (unsafeCoerce)

让我们将Index 定义为：

data Index (xs :: [k]) (x :: k) where
  IZ :: Index (x ': xs) x
  IS :: Index xs i -> Index (x ': xs) i

我们可以使用索引从Tuple 中提取项目：

(!) :: Tuple xs a -> Index xs x -> a x
(!) (Cons x _) IZ      = x
(!) (Cons _ xs) (IS i) = xs ! i

我们应该能够将Conkin.Traversable 的任何实例转储到Tuple，留下一个索引来代替每个元素。那么从索引和元组的结构我们可以重构出原来的Traversable结构：

data TupleDump t a = forall xs. TupleDump (t (Index xs)) (Tuple xs a)

toTupleDump :: forall (t :: (k -> *) -> *) (a :: k -> *). Conkin.Traversable t
  => t a -> TupleDump t a
fromTupleDump :: Conkin.Functor t => TupleDump t a -> t a

重构部分很简单：

fromTupleDump (TupleDump inds vals) = Conkin.fmap (vals !) inds

这个问题具体是如何实现toTupleDump。以下是我迄今为止的最佳尝试：

---

它涉及到很多辅助函数和一个unsafeCoerce

存在量化的函子：

data Some (a :: k -> *) = forall (x :: k). Some (a x)

给定一个Int，构造一些Index：

mkIndex :: Tuple xs a -> Int -> Some (Index xs)
mkIndex Nil _ = error "Index out of bounds"
mkIndex _ n | n < 0 = error "Index out of bounds"
mkIndex (Cons _ _) 0 = Some IZ
mkIndex (Cons _ xs) n = case mkIndex xs (n - 1) of Some i -> Some $ IS i

给定一个存在量化的函子列表，将它们分组为（翻转的）Tuple：

fromList :: [Some a] -> Some (Flip Tuple a)
fromList [] = Some $ Flip Nil
fromList (Some x : xs) = case fromList xs of
  Some (Flip t) -> Some (Flip (Cons x t))

在Prelude.Applicative（而不是Conkin.Applicative）内遍历

traverseInPrelude :: (Prelude.Applicative f, Conkin.Traversable t)
  => (forall x. a x -> f (b x)) -> t a -> f (t b)
traverseInPrelude fn t =
  Conkin.fmap (unComposeConst . getFlip) . getCompose <$>
    getDispose (Conkin.traverse (Dispose . fmap ComposeConst . fn) t)

newtype ComposeConst a b c = ComposeConst {unComposeConst :: a b}

现在我们可以定义toTupleDump：

toTupleDump t =

我们首先将索引作为Int 进行跟踪，并将我们的元素转储到普通列表中。 由于我们使用(:) 构建列表，所以它会倒退。

  let
    nextItem :: forall (x :: k). a x -> State (Int, [Some a]) (Const Int x)
    nextItem x = do
      (i, xs') <- State.get
      State.put (i + 1, Some x : xs')
      return $ Const i
    (res, (_, xs)) = runState (traverseInPrelude nextItem t) (0, [])
  in

现在我们反转列表并将其转换为Tuple：

  case fromList (reverse xs) of
    Some (Flip (tup :: Tuple xs a)) ->

我们需要在 res 结构上使用 fmap 将所有 Ints 更改为 Indexes

      let
        indexedRes = Conkin.fmap (coerceIndex . mkIndex tup . getConst) res

这是unsafeCoerce。由于这种方法涉及对结构的两次遍历，因此我们必须让类型检查器知道在第二次遍历时，类型参数与在第一次遍历时相同。

        coerceIndex :: forall x. Some (Index xs) -> Index xs x
        coerceIndex (Some i) = unsafeCoerce i
      in
      TupleDump indexedRes tup

Answer 1

我猜想没有unsafeCoerce是不可能实现toTupleDump的。

问题可以归结为计算fillWithIndexes

data SomeIndex t = forall xs. SomeIndex (t (Index xs))

fillWithIndexes :: forall (t :: (k -> *) -> *) (a :: k -> *). Conkin.Traversable t
  => t a -> SomeIndex t

其中xs是在遍历t a类型的值时收集的类型列表。但是，类型系统不能保证遍历结果 t (Index xs) 会产生相同的类型列表 xs。

如果t 的Traversable 实例不遵守Traversable 法律，则可以编造一个实际更改类型的实现。

data T a = TBool (a Bool) | TChar (a Char)
instance Conkin.Functor T where
  fmap f (TBool a) = TBool (f a)
  fmap f (TChar a) = TChar (f a)

instance Conkin.Foldable T where
  foldr f z (TBool a) = f a z
  foldr f z (TChar a) = f a z

instance Conkin.Traversable T where
  traverse f (TBool a) = Conkin.pure (Compose (TChar undefined))
  traverse f (TChar a) = Conkin.pure (Compose (TBool undefined))

我们不能通过假设Traversable 法律来排除这种情况吗？是的，我们可以排除它，但是类型检查器不能，这意味着我们必须使用unsafeCoerce。