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

Question

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

我希望能够采取任何Conkin.Traversable并将其转储到 Tuple留下索引到 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)) ->

我们需要 fmap超过 res结构改变所有 Int转入 Index es

      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

我推测不可能实现toTupleDump没有 unsafeCoerce .

问题可以归结为计算 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 .

如果 Traversable t 的实例不尊重 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 .