Jes*_*seC 9 haskell dependent-type free-monad
我正在尝试使用索引的免费monad(Oleg Kiselyov有一个介绍).我也希望这个免费的monad可以从一个仿函数的副产品中构建出来,也可以单独使用数据类型.但是,我无法获得产品注入类型类.这是我到目前为止所拥有的:
{-# 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似乎是正确的方法,但我无法弄清楚如何使相关的类型实例工作.这次注射应该是什么样的？
我将首先介绍目前处理未结金额的标准方法.为了简单起见,我是为普通的非索引函子做的,因为索引的构造是相同的.然后我将介绍GHC 8启用的一些增强功能.
首先,我们将n-ary仿函数和定义为由仿函数列表索引的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)
投射和注射都可以完成
后一种解决方案是最好的解决方案,所以让我们看看:
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因此它不能跨过所述第一列表元素.
这在历史上引起了数据类型单点和可扩展效果库中相当恼人的类型推断缺陷.例如,即使我们State s在函子和中只有一个效应,(x :: n) <- get在仅Num n知道的上下文中写入会导致类型推断失败,因为State当状态参数是类型变量时,GHC无法计算效果的索引.
但是,使用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可以在涉及开放式总和的任何代码中使用,并且它适用于索引和非索引类型.
这是一些示例代码,其中包含上面提到的注入/投影类型,用于非索引的可扩展效果.