Сделал-таки.

[thesz]

Продолжение вчерашнего.


{-# LANGUAGE MultiParamTypeClasses, TypeOperators, FlexibleInstances #-}
{-# LANGUAGE EmptyDataDecls, FlexibleContexts, OverlappingInstances #-}
{-# LANGUAGE GADTs, FunctionalDependencies, TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}

module A where

infixr 5 :*: -- as for ':' operator

-------------------------------------------------------------------------------
-- Standard arithmetic in types.

data S n
data Z

-------------------------------------------------------------------------------
-- Standard HList.

data HNil
data a :*: b

class HList a
instance HList HNil
instance HList tail => HList (a :*: tail)

-------------------------------------------------------------------------------
-- Sets in types.

class HList set => InSet a set
instance HList tail => InSet a (a :*: tail)
instance (HList tail, InSet a tail) => InSet a (b :*: tail)

-- добавление элемента к множеству осуществляется простым (elem :*: set).
-- удаление требует процедуры:
class (HList seta, HList setb) => DelSet x seta setb
instance DelSet x HNil HNil
instance HList tail => DelSet x (x :*: tail) tail
instance DelSet x tail tail1 => DelSet x (y :*: tail) (y :*: tail1)

t1 :: InSet Z (Z :*: HNil) => ()
t1 = ()

t2 :: DelSet (S Z) (S Z :*: HNil) (S Z :*: HNil) => ()
t2 = ()

class (HList lesser, HList bigger) => Subset lesser bigger
instance HList bigger => Subset HNil bigger
instance (InSet x bigger, Subset tail bigger) => Subset (x :*: tail) bigger

class SetEq a b
instance (Subset a b, Subset b a) => SetEq a b

-------------------------------------------------------------------------------
-- Parametrized monad.

class PMonad s where
returnPM :: a -> s p p a
(>==) :: s i t a -> (a -> s t o b) -> s i o b

data PState si so a = PState { unPState :: (si -> (so,a))}

-- один-к-одному монада состояний, только тип состояния не фиксирован.
instance PMonad PState where
returnPM a = PState $ \p -> (p,a)
(PState f) >== q = PState $ \si -> let
(st,a) = f si
in
unPState (q a) st

-------------------------------------------------------------------------------
-- .

type EmptyNLState = AsyncNLState HNil HNil Z
data AsyncNLState used defined cnt where
Empty :: AsyncNLState HNil HNil Z
Define :: AsyncNLState used defined cnt
-> S cnt
-> AsyncNLState used (S cnt :*: defined) (S cnt)
Use :: pipe -> AsyncNLState used defined cnt
-> AsyncNLState (pipe :*: used) defined cnt

-- операция по определению нового канала.
-- заносим его в defined.
definePipe :: PState
(AsyncNLState used defined cnt)
(AsyncNLState used (S cnt :*: defined) (S cnt))
(S cnt)
definePipe = PState $ \si -> (Define si pipe,pipe)
where
pipe = undefined

usePipe :: pipe -> PState
(AsyncNLState used defined cnt)
(AsyncNLState (pipe :*: used) defined cnt)
()
usePipe pipe = PState $ \si -> (Use pipe si,())

entity :: SetEq used defs
=> PState EmptyNLState (AsyncNLState used defs cnt) a
-> () -- должен быть разумный тип, наподобие Entity, пока сойдёт.
entity create = ()

--create1 :: PState EmptyNLState (AsyncNLState HNil HNil cnt) ()
create1 = definePipe >==
\pipe1 -> definePipe >==
\pipe2 -> usePipe pipe2 >==
\_ -> usePipe pipe1

{-
*A> :t entity create1
entity create1 :: ()
*A> :t create1
create1 :: PState
(AsyncNLState used defined cnt)
(AsyncNLState
(S cnt :*: (S (S cnt) :*: used))
(S (S cnt) :*: (S cnt :*: defined))
(S (S cnt)))
()
-}

Добавил равенство множеств типов, вместо удаления сделал добавление и сравниваю равенство множеств добавленных и определённых типов.

Теперь надо попробовать описать нормальную асинхронную схему. Что потребует описания всевозможных вариантов соединений - разветвлений, арбитров и тп. Да и зацикливание надо добавить - как описать машину Мили? - а это мне пока не очень понятно.