Change values to indices in a `Conkin.Traversable` without `unsafeCoerce`

Question

Using the conkin package: https://hackage.haskell.org/package/conkin

I want to be able to take any Conkin.Traversable and dump it out to a Tuple leaving behind indices into that Tuple so that I can reconstruct it.

I'm using a few language extensions:

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

Module declaration

module TupleDump where

Imports

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

I want to not have to use an unsafeCoerce, but can't see a way around it:

import           Unsafe.Coerce        (unsafeCoerce)

Let's define an Index as:

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

We can use an index to extract an item from a Tuple:

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

We should be able to take anything which is an instance of Conkin.Traversable and dump it to a Tuple leaving behind an Index in place of each element. Then from the structure of indices and the tuple we can reconstruct the original Traversable structure:

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

The reconstruction part is easy:

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

This question is specifically how to implement toTupleDump. Below is my best attempt so far:

---

It involves a lot of helper functions and an unsafeCoerce

Existentially quantified functors:

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

Given an Int, construct some 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

Given a list of existentially quantified functors, group them into a (flipped) 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))

Traversal inside a Prelude.Applicative (rather than a 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}

And now we can define toTupleDump:

toTupleDump t =

We'll track the index as just an Int at first and dump our elements to a normal list. Since we're building the list with (:), it's going to be backwards.

  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

Now we reverse the list and convert it to a Tuple:

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

And we need to fmap over the res structure changing all the Ints into Indexes

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

Here's that unsafeCoerce. Since this approach involves two passes over the structure, we have to let the typechecker know that on the second pass, the type parameter is the same as it was on the first pass.

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

Answer 1

I conjecture that it is not possible to implement toTupleDump without unsafeCoerce.

The problem can be reduced to computing fillWithIndexes

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

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

where xs is the list of types collected in the traversal of the value of type t a. However, the type system can't guarantee that traversals over the result t (Index xs) produce the same list of types xs.

If the Traversable instance of t does not respect the Traversable laws, it is possible to concoct an implementation which actually changes the types.

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))

Can't we rule this case out by assuming the Traversable laws hold? Yes, we can rule it out, but the typechecker can't, which means that we must use unsafeCoerce.