9
Я пытаюсь работать с индексированной свободной монадой (Олег Киселев имеет an intro). Я также хочу, чтобы свободная монада была построена из копродукта функторов a la Data Types a la carte. Тем не менее, у меня возникли проблемы с тем, чтобы получить класс типа инъекции coproduct. Вот что у меня есть до сих пор:Инъекция Индексированный функтор в Functor Coproduct
{-# 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 Попытка 1 разрушает вывод типа. У попытки 2 есть плохая эргономика для пользователя. Попытка 3 кажется правильной, но я не могу понять, как сделать связанные экземпляры экземпляров работать. Как должна выглядеть эта инъекция?
Спасибо! Я знаком с вашим 'NS'. Проблема в том, что расширение его работы с индексированными функторами для меня не очевидно. 'data NS (fs :: [* -> *]) is os (a :: *)' Какие должны быть типы 'is' и' os' (если мы хотим поддерживать индексированные функторы, где каждый функтор может быть проиндексирован типами другого типа)? Уровень hlist типа? Список открытых профсоюзов? – JesseC
Кстати, экземпляр 'Functor (NS fs)' можно напрямую передать в терминах утверждения, что все 'fs' являются функторами: http://lpaste.net/5782847892658061312 – dfeuer
Не могли бы вы объяснить, как это помогает чтобы дать * обход * типа, а не только дерево, представляющее его, или сам тип? – dfeuer