Измените значения на индексы в `Conkin.Traversable` без` unsafeCoerce` - PullRequest
Новая
       107

Измените значения на индексы в `Conkin.Traversable` без` unsafeCoerce`

0 голосов
/ 20 сентября 2018

Используя пакет 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 и dump , в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 s на 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

1 Ответ

0 голосов
/ 28 сентября 2018

Я предполагаю, что невозможно реализовать 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.

...