Измените значения на индексы в `Conkin.Traversable` без`unsafeCoerce`
С использованием 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
эс
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
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
,