haskell - 将索引仿函数注入(inject)仿函数协积

Question

我正在尝试使用索引的免费单子(monad)(Oleg Kiselyov 有 an intro )。我还希望免费的 monad 是从仿函数的副产品 la Data Types a la carte 中构建的。 .但是，我无法让副产品注入(inject)类型类工作。这是我到目前为止所拥有的:

{-# 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 似乎是正确的方法，但我不太清楚如何使关联的类型实例发挥作用。这种注入(inject)应该是什么样子？

Answer 1

我将首先介绍当前处理未结金额的标准方法。为了简单起见，我对普通的非索引仿函数执行此操作，因为索引的构造是相同的。然后我将介绍 GHC 8 启用的一些增强功能。

首先，我们将 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)

可以进行投影和注入(inject)

直接使用一个类，但这需要重叠或不连贯的实例。

间接地，首先计算我们要注入(inject)的元素的索引，然后使用(自然数)索引来定义类实例而不重叠。

后一种解决方案是更可取的解决方案，所以让我们看看:

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 不 promise a 的不等式。和 b所以它不能越过第一个列表元素。

这在历史上导致了 Data Types a la Carte 和可扩展效果库中相当烦人的类型推断缺陷。例如，即使我们只有一个 State s仿函数总和中的效果，写作 (x :: n) <- get在只有 Num n 的情况下已知会导致类型推断失败，因为 GHC 无法计算 State 的索引当 state 参数是类型变量时生效。

但是，使用 GHC 8，我们可以编写更强大的 Find类型族，它查看类型表达式以查看是否存在唯一的可能位置索引。例如，如果我们试图找到 State s效果，如果只有一个 State在效果列表中，我们无需查看 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一些具有上述注入(inject)/投影类型的示例代码，用于非索引可扩展效果。