Injecting Indexed Functor into Functor Coproduct

Question

I'm trying to work with an indexed free monad (Oleg Kiselyov has an intro). I also want that free monad to be built from a from a coproduct of functors a la Data Types a la carte. However, I'm having trouble getting the coproduct injection type class to work out. Here's what I have so far:

{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE RebindableSyntax #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}

module Example where

import Control.Monad.Indexed
import Data.Kind
import Data.TASequence.FastCatQueue
import Prelude hiding ((>>), (>>=))

-- * Indexed free machinery

-- For use with `RebindableSyntax`
(>>=)
  :: (IxMonad m)
  => m s1 s2 a -> (a -> m s2 s3 b) -> m s1 s3 b
(>>=) = (>>>=)
(>>)
  :: (IxApplicative m)
  => m s1 s2 a -> m s2 s3 b -> m s1 s3 b
f >> g = imap (const id) f `iap` g

type family Fst x where
  Fst '(a, b) = a
type family Snd x where
  Snd '(a, b) = b

newtype IKleisliTupled m ia ob = IKleisliTupled
  { runIKleisliTupled :: Snd ia -> m (Fst ia) (Fst ob) (Snd ob)
  }

data Free f s1 s2 a where
  Pure :: a -> Free f s s a
  Impure ::
    f s1 s2 a ->
      FastTCQueue (IKleisliTupled (Free f)) '(s2, a) '(s3, b) ->
        Free f s1 s3 b

instance IxFunctor (Free f) where
  imap f (Pure a) = Pure $ f a
  imap f (Impure a g) = Impure a (g |> IKleisliTupled (Pure . f))
instance IxPointed (Free f) where
  ireturn = Pure
instance IxApplicative (Free f) where
  iap (Pure f) (Pure a) = ireturn $ f a
  iap (Pure f) (Impure a g) = Impure a (g |> IKleisliTupled (Pure . f))
  iap (Impure a f) m = Impure a (f |> IKleisliTupled (`imap` m))
instance IxMonad (Free f) where
  ibind f (Pure a) = f a
  ibind f (Impure a g) = Impure a (g |> IKleisliTupled f)

-- * Example application

data FileStatus
  = FileOpen
  | FileClosed
data File i o a where
  Open :: FilePath -> File 'FileClosed 'FileOpen ()
  Close :: File 'FileOpen 'FileClosed ()
  Read :: File 'FileOpen 'FileOpen String
  Write :: String -> File 'FileOpen 'FileOpen ()

data MayFoo
  = YesFoo
  | NoFoo
data Foo i o a where
  Foo :: Foo 'NoFoo 'YesFoo ()

data MayBar
  = YesBar
  | NoBar
data Bar i o a where
  Bar :: Bar 'YesBar 'NoBar ()

-- * Coproduct of indexed functors

infixr 5 `SumP`
data SumP f1 f2 t1 t2 x where
  LP :: f1 sl1 sl2 x -> SumP f1 f2 '(sl1, sr) '(sl2, sr) x
  RP :: f2 sr1 sr2 x -> SumP f1 f2 '(sl, sr1) '(sl, sr2) x

-- * Attempt 1

class Inject l b where
  inj :: forall a. l a -> b a

instance Inject (f i o) (f i o) where
  inj = id

instance Inject (fl il ol) (SumP fl fr '(il, s) '(ol, s)) where
  inj = LP

instance (Inject (f i' o') (fr is os)) =>
         Inject (f i' o') (SumP fl fr '(s, is) '(s, os)) where
  inj = RP . inj

send
  :: Inject (t i o) (f is os)
  => t i o b -> Free f is os b
send t = Impure (inj t) (tsingleton (IKleisliTupled Pure))

-- Could not deduce `(Inject (Bar 'YesBar 'NoBar) f s30 s40)`
prog
  :: (Inject (File 'FileClosed 'FileOpen) (f s1 s2)
     ,Inject (Foo 'NoFoo 'YesFoo) (f s2 s3)
     ,Inject (Bar 'YesBar 'NoBar) (f s3 s4)
     ,Inject (File 'FileOpen 'FileClosed) (f s4 s5))
  => Free f s1 s5 ()
prog = do
  send (Open "/tmp/foo.txt")
  x <- send Read
  send Foo
  send (Write x)
  send Bar
  send Close

-- * Attempt 2

bsend :: (t i o b -> g is os b) -> t i o b -> Free g is os b
bsend f t = Impure (f t) (tsingleton (IKleisliTupled Pure))

-- Straightforward but not very usable

bprog
  ::
    Free
      (File `SumP` Bar `SumP` Foo)
      '( 'FileClosed, '( 'YesBar, 'NoFoo))
      '( 'FileClosed, '( 'NoBar, 'YesFoo))
      ()
bprog = do
  bsend LP (Open "/tmp/foo.txt")
  x <- bsend LP Read
  bsend (RP . RP) Foo
  bsend (RP . LP) Bar
  bsend LP (Write x)
  bsend LP Close

-- * Attempt 3

class Inject' f i o (fs :: j -> j -> * -> *) where
  type I f i o fs :: j
  type O f i o fs :: j
  inj' :: forall x. f i o x -> fs (I f i o fs) (O f i o fs) x

instance Inject' f i o f where
  type I f i o f = i
  type O f i o f = o
  inj' = id

-- Illegal polymorphic type: forall (s :: k1). '(il, s)

instance Inject' fl il ol (SumP fl fr) where
  type I fl il ol (SumP fl fr) = forall s. '(il, s)
  type O fl il ol (SumP fl fr) = forall s. '(ol, s)
  inj' = LP

instance (Inject' f i' o' fr) =>
         Inject' f i' o' (SumP fl fr) where
  type I f i' o' (SumP fl fr) = forall s. '(s, I f i' o' fr)
  type O f i' o' (SumP fl fr) = forall s. '(s, O f i' o' fr)
  inj' = RP . inj

So Attempt 1 destroys type inference. Attempt 2 has bad ergonomics for the user. Attempt 3 seems like the right approach, but I can't quite figure out how to make the associated type instances work out. What should this injection look like?

Answer 1

I shall present first the currently standard way of handling open sums. I do it for plain non-indexed functors for the sake of simplicity and because the construction is the same for indexed ones. Then I'll introduce some enhancements enabled by GHC 8.

First, we define n-ary functor sums as a GADT indexed by a list of functors. This is more convenient and cleaner than using binary sums.

{-# language
  RebindableSyntax, TypeInType, TypeApplications,
  AllowAmbiguousTypes, GADTs, TypeFamilies, ScopedTypeVariables,
  UndecidableInstances, LambdaCase, EmptyCase, TypeOperators, ConstraintKinds,
  FlexibleContexts, MultiParamTypeClasses, FlexibleInstances #-}

import Data.Kind

data NS :: [* -> *] -> * -> * where
  Here  :: f x -> NS (f ': fs) x
  There :: NS fs x -> NS (f ': fs) x

instance Functor (NS '[]) where
  fmap _ = \case {}

instance (Functor f, Functor (NS fs)) => Functor (NS (f ': fs)) where
  fmap f (Here fx)  = Here  (fmap f fx)
  fmap f (There ns) = There (fmap f ns)

Projecting and injecting can be either done

• Directly with a class, but this needs overlapping or incoherent instances.
• Indirectly, first computing the index of the element where we'd like to inject, then using the (natural number) index to define class instances without overlapping.

The latter solution is the preferable one, so let's see that:

data Nat = Z | S Nat

type family Find (x :: a) (xs :: [a]) :: Nat where
  Find x (x ': xs) = Z
  Find x (y ': xs) = S (Find x xs)

class Elem' (n :: Nat) (f :: * -> *) (fs :: [* -> *]) where
  inj' :: forall x. f x -> NS fs x
  prj' :: forall x. NS fs x -> Maybe (f x)

instance (gs ~ (f ': gs')) => Elem' Z f gs where
  inj'           = Here
  prj' (Here fx) = Just fx
  prj' _         = Nothing

instance (Elem' n f gs', (gs ~ (g ': gs'))) => Elem' (S n) f gs where
  inj'            = There . inj' @n
  prj' (Here _)   = Nothing
  prj' (There ns) = prj' @n ns

type Elem f fs = (Functor (NS fs), Elem' (Find f fs) f fs)  

inj :: forall fs f x. Elem f fs => f x -> NS fs x
inj = inj' @(Find f fs)

prj :: forall f x fs. Elem f fs => NS fs x -> Maybe (f x)
prj = prj' @(Find f fs)

Now in ghci:

> :t inj @[Maybe, []] (Just True)
inj @[Maybe, []] (Just True) :: NS '[Maybe, []] Bool

However, our Find type family is somewhat problematic because its reduction is often blocked by type variables. GHC disallows branching on inequality of type variables, because unification can possibly instantiate different variables to equal types later (and making premature decisions based on inequality can lead to loss of solutions).

For example:

> :kind! Find Maybe [Maybe, []]
Find Maybe [Maybe, []] :: Nat
= 'Z  -- this works
> :kind! forall (a :: *)(b :: *). Find (Either b) [Either a, Either b]
forall (a :: *)(b :: *). Find (Either b) [Either a, Either b] :: Nat
= Find (Either b) '[Either a, Either b] -- this doesn't

In the second example GHC doesn't commit to the inequality of a and b so it can't step over the first list element.

This historically caused rather annoying type inference deficiencies in Data Types a la Carte and extensible effects libraries. For example, even if we have just a single State s effect in a functor sum, writing (x :: n) <- get in a context where only Num n is known results in type inference failure, because GHC can't compute the index of the State effect when the state parameter is a type variable.

However, with GHC 8 we can write a significantly more powerful Find type family, which looks into type expressions to see if there's a unique possible position index. For example, if we're trying to find a State s effect, if there's only a single State in the effect list, we can safely return its position without looking at the s parameter, and subsequently GHC will be able to unify s with the other state parameter contained in the list.

First, we need a generic traversal of type expressions:

import Data.Type.Bool

data Entry = App | forall a. Con a

type family (xs :: [a]) ++ (ys :: [a]) :: [a] where
  '[]       ++ ys = ys
  (x ': xs) ++ ys = x ': (xs ++ ys)

type family Preord (x :: a) :: [Entry] where
  Preord (f x) = App ': (Preord f ++ Preord x)
  Preord x     = '[ Con x]

Preord converts an arbitrary type into a list of its sub-expressions in preorder. App denotes the places where type constructor application occurs. For example:

> :kind! Preord (Maybe Int)
Preord (Maybe Int) :: [Entry]
= '['App, 'Con Maybe, 'Con Int]
> :kind! Preord [Either String, Maybe]
Preord [Either String, Maybe] :: [Entry]
= '['App, 'App, 'Con (':), 'App, 'Con Either, 'App, 'Con [],
   'Con Char, 'App, 'App, 'Con (':), 'Con Maybe, 'Con '[]]

After this, writing the new Find is just a matter of functional programming. My implementation below converts the list of types into a list of index-traversal pairs, and successively filters out entries from the list by comparing the traversals of the list elements and the to-be-found element.

type family (x :: a) == (y :: b) :: Bool where
  x == x = True
  _ == _ = False

type family PreordList (xs :: [a]) (i :: Nat) :: [(Nat, [Entry])] where
  PreordList '[]       _ = '[]
  PreordList (a ': as) i = '(i, Preord a) ': PreordList as (S i)

type family Narrow (e :: Entry) (xs :: [(Nat, [Entry])]) :: [(Nat, [Entry])] where
  Narrow _ '[]                     = '[]
  Narrow e ('(i, e' ': es) ': ess) = If (e == e') '[ '(i, es)] '[] ++ Narrow e ess

type family Find_ (es :: [Entry]) (ess :: [(Nat, [Entry])]) :: Nat where
  Find_ _        '[ '(i, _)] = i
  Find_ (e ': es) ess        = Find_ es (Narrow e ess)

type Find x ys = Find_ (Preord x) (PreordList ys Z)

Now we have:

> :kind! forall (a :: *)(b :: *). Find (Either a) [Maybe, [], Either b]
forall (a :: *)(b :: *). Find (Either a) [Maybe, [], Either b] :: Nat
= 'S ('S 'Z)

This Find can be used in any code involving open sums, and it works for indexed and non-indexed types all the same.

Here's some example code with the kind of injection/projection presented above, for non-indexed extensible effects.

Answer 2

Aha, I got it to work! The key thing I took from András Kovács second attempt (linked in a comment) is the trick with leaving the instance head general and then refining with an equality constraint.

{-# LANGUAGE FlexibleInstances, GADTs, MultiParamTypeClasses,
  RankNTypes, RebindableSyntax, TypeFamilies, TypeInType,
  TypeOperators, UndecidableInstances #-}

module Example2 (res, prog') where

import Control.Monad.Indexed
import Data.TASequence.FastCatQueue
import Prelude hiding ((>>), (>>=))

-- * Indexed free machinery

(>>=)
  :: (IxMonad m)
  => m s1 s2 a -> (a -> m s2 s3 b) -> m s1 s3 b
(>>=) = (>>>=)
(>>)
  :: (IxApplicative m)
  => m s1 s2 a -> m s2 s3 b -> m s1 s3 b
f >> g = imap (const id) f `iap` g

type family Fst x where
  Fst '(a, b) = a
type family Snd x where
  Snd '(a, b) = b

newtype IKleisliTupled m ia ob = IKleisliTupled
  { runIKleisliTupled :: Snd ia -> m (Fst ia) (Fst ob) (Snd ob)
  }

tApp :: (TASequence s, IxMonad m) => s (IKleisliTupled m) x y -> (IKleisliTupled m) x y
tApp fs =
  case tviewl fs of
    TAEmptyL -> IKleisliTupled ireturn
    f :< fs' ->
      IKleisliTupled
        (\a -> runIKleisliTupled f a >>= runIKleisliTupled (tApp fs'))

data Free f s1 s2 a where
  Pure :: a -> Free f s s a
  Impure ::
    f s1 s2 a ->
      FastTCQueue (IKleisliTupled (Free f)) '(s2, a) '(s3, b) ->
        Free f s1 s3 b

instance IxFunctor (Free f) where
  imap f (Pure a) = Pure $ f a
  imap f (Impure a g) = Impure a (g |> IKleisliTupled (Pure . f))
instance IxPointed (Free f) where
  ireturn = Pure
instance IxApplicative (Free f) where
  iap (Pure f) (Pure a) = ireturn $ f a
  iap (Pure f) (Impure a g) = Impure a (g |> IKleisliTupled (Pure . f))
  iap (Impure a f) m = Impure a (f |> IKleisliTupled (`imap` m))
instance IxMonad (Free f) where
  ibind f (Pure a) = f a
  ibind f (Impure a g) = Impure a (g |> IKleisliTupled f)

-- * Example application

data FileStatus
  = FileOpen
  | FileClosed
data File i o a where
  Open :: FilePath -> File 'FileClosed 'FileOpen ()
  Close :: File 'FileOpen 'FileClosed ()
  Read :: File 'FileOpen 'FileOpen String
  Write :: String -> File 'FileOpen 'FileOpen ()

foldFile :: File i o a -> a
foldFile (Open _) = ()
foldFile Close = ()
foldFile Read = "demo"
foldFile (Write _) = ()

data MayFoo
  = YesFoo
  | NoFoo
data Foo i o a where
  Foo :: Foo 'NoFoo 'YesFoo ()

data MayBar
  = YesBar
  | NoBar
data Bar i o a where
  Bar :: Bar 'YesBar 'NoBar ()

-- * Coproduct of indexed functors

infixr 5 `SumP`
data SumP f1 f2 t1 t2 x where
  LP :: f1 sl1 sl2 x -> SumP f1 f2 '(sl1, sr) '(sl2, sr) x
  RP :: f2 sr1 sr2 x -> SumP f1 f2 '(sl, sr1) '(sl, sr2) x

newtype VoidFunctor is os a = VoidFunctor (VoidFunctor is os a)
absurd :: VoidFunctor is os a -> b
absurd a = a `seq` spin a where
   spin (VoidFunctor b) = spin b

extract :: Free VoidFunctor '() '() a -> a
extract (Pure a) = a
extract (Impure f _) = absurd f

runPure
  :: (forall j p b. f j p b -> b)
  -> Free (f `SumP` fs) '(i, is) '(o, os) a
  -> Free fs is os a
runPure _ (Pure a) = Pure a
runPure f (Impure (RP cmd) q) = Impure cmd (tsingleton k)
  where k = IKleisliTupled $ \a -> runPure f $ runIKleisliTupled (tApp q) a
runPure f (Impure (LP cmd) q) = runPure f $ runIKleisliTupled (tApp q) (f cmd)

-- * Injection

class Inject l b where
  inj :: forall a. l a -> b a

instance Inject (f i o) (f i o) where
  inj = id

instance {-# OVERLAPPING #-}
  (is ~ '(il, s), os ~ '(ol, s)) =>
  Inject (fl il ol) (SumP fl fr is os) where
  inj = LP

instance (Inject (f i' o') (fr is' os'), is ~ '(s, is'), os ~ '(s, os')) =>
         Inject (f i' o') (SumP fl fr is os) where
  inj = RP . inj

send
  :: Inject (t i o) (f is os)
  => t i o b -> Free f is os b
send t = Impure (inj t) (tsingleton (IKleisliTupled Pure))

-- * In use

prog = do
  send (Open "/tmp/foo.txt")
  x <- send Read
  send Foo
  send (Write x)
  send Bar
  send Close
  ireturn x

prog' ::
  Free
    (File `SumP` Foo `SumP` Bar `SumP` VoidFunctor)
    '( 'FileClosed, '( 'NoFoo, '( 'YesBar, '())))
    '( 'FileClosed, '( 'YesFoo, '( 'NoBar, '())))
    String
prog' = prog

res :: String
res = extract . runPure (\Bar -> ()) . runPure (\Foo -> ()) . runPure foldFile $ prog

P.S. I'll see if I can move toward the nicer open union encoding or if I too will run into inscrutable GHC problems.