将带索引的函数式注入函数式余积

Question

我正在尝试使用一个索引的自由monad (Oleg有an intro)。我也希望这个免费的monad是从Data Types a la carte这样的函数器的联合产品中构建的。但是，我在使用联产品注入类型类时遇到了问题。这是我到目前为止所知道的：

{-# 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

所以尝试1会破坏类型推断。尝试2对用户来说人体工程学不好。尝试3似乎是正确的方法，但我不太清楚如何使相关的类型实例工作。这个注入应该是什么样子的？

Answer 1

我将首先介绍目前处理未结金额的标准方法。为了简单起见，我对普通的非索引函数器这样做是为了简单起见，因为索引函数器的构造是相同的。然后，我将介绍GHC8支持的一些增强功能。

首先，我们将n元函子和定义为由函子列表索引的GADT。这比使用二进制求和更方便、更简洁。

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

投影和注入都可以完成

直接注入一个类，但这需要重叠或不连贯的instances.

• Indirectly，首先计算我们想要注入的元素的索引，然后使用(
• )索引定义没有重叠的类实例。

后一种解决方案更可取，所以让我们来看看：

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)

现在在ghci中：

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

但是，我们的Find类型族有一些问题，因为它的缩减通常会被类型变量阻塞。GHC不允许在类型变量的不等式上进行分支，因为统一可能会在以后将不同的变量实例化为相同的类型(并且基于不等式过早决策可能会导致丢失解决方案)。

例如：

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

在第二个例子中，GHC没有遵守a和b的不等式，所以它不能跳过第一个列表元素。

这在历史上导致了数据类型和可扩展效果库中相当恼人的类型推断缺陷。例如，即使我们在函数器sum中只有一个State s效应，在只有Num n已知的上下文中编写(x :: n) <- get也会导致类型推断失败，因为当状态参数是类型变量时，GHC不能计算State效应的索引。

然而，使用GHC8，我们可以编写一个功能强大得多的Find类型族，它可以查看类型表达式，看看是否存在唯一的可能位置索引。例如，如果我们试图找到一个State s效果，如果在效果列表中只有一个状态，我们可以安全地返回它的位置，而不需要查看s参数，随后GHC将能够将s与列表中包含的其他状态参数统一起来。

首先，我们需要一个类型表达式的泛型遍历：

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按预定顺序将任意类型转换为其子表达式的列表。App表示类型构造函数应用程序发生的地方。例如：

> :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 '[]]

在此之后，编写新的Find只是一个函数式编程的问题。我下面的实现将类型列表转换为索引遍历对的列表，并通过比较列表元素和要找到的元素的遍历顺序从列表中过滤出条目。

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)

现在我们有：

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

这个Find可以在任何涉及开和的代码中使用，并且它同样适用于索引类型和非索引类型。

Here's一些示例代码，使用上面给出的那种注入/投影，以实现无索引的可扩展效果。

Answer 2

啊哈，我让它工作了！我从András Kovács第二次尝试(链接在注释中)中学到的关键是让实例头部保持通用，然后使用相等约束进行优化的技巧。

{-# 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

另外，我会看看我是否可以转向更好的开放联合编码，或者我是否也会遇到难以理解的GHC问题。