В Haskell, базовая версия этого может быть выражено с GADT индексируется магазин тортов (представлен список Nat -s):
{-# LANGUAGE
TypeFamilies, GADTs, TypeOperators, PartialTypeSignatures,
DataKinds, PolyKinds #-}
import GHC.TypeLits
import Data.Proxy
import GHC.Exts
-- Allocate a new cake
type family New cs where
New '[] = 0
New (c ': cs) = c + 1
-- Constraint satisfiable if "c" is in "cs"
type family Elem c cs :: Constraint where
Elem c (c ': cs) =()
Elem c (c' ': cs) = Elem c cs
type family Remove c cs where
Remove c '[] = '[]
Remove c (c ': cs) = cs
Remove c (c' ': cs) = c' ': Remove c cs
data Bake :: [Nat] -> [Nat] -> * -> * where
Pure :: a -> Bake cs cs a
Bake :: (Proxy (New cs) -> Bake (New cs ': cs) cs' a) -> Bake cs cs' a
Eat :: Elem c cs => Proxy c -> Bake (Remove c cs) cs' a -> Bake cs cs' a
Keep :: Elem c cs => Proxy c -> Bake cs cs' a -> Bake cs cs' a
ok :: Bake '[] _ _
ok =
Bake $ \cake1 ->
Bake $ \cake2 ->
Eat cake1 $
Keep cake2 $
Eat cake2 $
Pure()
not_ok :: Bake '[] _ _
not_ok =
Bake $ \cake1 ->
Bake $ \cake2 ->
Eat cake1 $
Keep cake1 $ -- we already ate that
Eat cake2 $
Pure()
К сожалению, мы не можем удалить тип аннотации от Bake действий и оставить типы должны быть выведены:
foo =
Bake $ \cake1 ->
Bake $ \cake2 ->
Eat cake1 $
Pure()
-- Error: Could not deduce (Elem (New cs0) (New cs0 + 1 : New cs0 : cs0))
Очевидно, что (Elem (New cs0) (New cs0 + 1 : New cs0 : cs0)) выполнима для всех cs0, но GHC не может видеть это, потому что он не может решить, стоит ли New cs0 является неравенством к New cs0 + 1, потому что GHC ничего не может принять в отношении гибкой переменной cs0.
Если мы добавим NoMonomorphismRestriction, foo будет typecheck, но это сделает даже неправильные программы typecheck, нажав все ограничения Elem на верх. Тем не менее это все равно помешает делать что-нибудь полезное с неправильными терминами, но это довольно уродливое решение.
В целом, мы можем выразить Bake как индексированный свободной монады, которая получает нас do -notation с RebindableSyntax и позволяет определение для BakeF, который несколько яснее, чем то, что мы видели раньше. Это также могло бы уменьшить шаблон, похожий на обычную старую монаду Free, хотя я считаю маловероятным, что люди найдут применение для индексированных свободных монад в двух разных случаях в практическом коде.
{-# LANGUAGE
TypeFamilies, GADTs, TypeOperators, PartialTypeSignatures, StandaloneDeriving,
DataKinds, PolyKinds, NoImplicitPrelude, RebindableSyntax, DeriveFunctor #-}
import Prelude hiding (Monad(..))
import GHC.TypeLits
import Data.Proxy
import GHC.Exts
class IxFunctor f where
imap :: (a -> b) -> f i j a -> f i j b
class IxFunctor m => IxMonad m where
return :: a -> m i i a
(>>=) :: m i j a -> (a -> m j k b) -> m i k b
fail :: String -> m i j a
infixl 1 >>
infixl 1 >>=
(>>) :: IxMonad m => m i j a -> m j k b -> m i k b
ma >> mb = ma >>= const mb
data IxFree f i j a where
Pure :: a -> IxFree f i i a
Free :: f i j (IxFree f j k a) -> IxFree f i k a
liftf :: IxFunctor f => f i j a -> IxFree f i j a
liftf = Free . imap Pure
instance IxFunctor f => IxFunctor (IxFree f) where
imap f (Pure a) = Pure (f a)
imap f (Free fa) = Free (imap (imap f) fa)
instance IxFunctor f => IxMonad (IxFree f) where
return = Pure
Pure a >>= f = f a
Free fa >>= f = Free (imap (>>= f) fa)
fail = error
-- Old stuff for Bake
type family New cs where
New '[] = 0
New (c ': cs) = c + 1
type family Elem c cs :: Constraint where
Elem c (c ': cs) =()
Elem c (c' ': cs) = Elem c cs
type family Remove c cs where
Remove c '[] = '[]
Remove c (c ': cs) = cs
Remove c (c' ': cs) = c' ': Remove c cs
-- Now the return type indices of BakeF directly express the change
-- from the old store to the new store.
data BakeF cs cs' k where
BakeF :: (Proxy (New cs) -> k) -> BakeF cs (New cs ': cs) k
EatF :: Elem c cs => Proxy c -> k -> BakeF cs (Remove c cs) k
KeepF :: Elem c cs => Proxy c -> k -> BakeF cs cs k
deriving instance Functor (BakeF cs cs')
instance IxFunctor BakeF where imap = fmap
type Bake = IxFree BakeF
bake = liftf (BakeF id)
eat c = liftf (EatF c())
keep c = liftf (KeepF c())
ok :: Bake '[] _ _
ok = do
cake1 <- bake
cake2 <- bake
eat cake1
keep cake2
eat cake2
-- not_ok :: Bake '[] _ _
-- not_ok = do
-- cake1 <- bake
-- cake2 <- bake
-- eat cake1
-- keep cake1 -- already ate it
-- eat cake2
Не могли бы вы использовать фантомные типы, чтобы указать кастрированный баран торт был съеден - как 'Cake данные а = Cake' и' данных Eaten' 'данных Fresh' затем' испечь = Cake :: торт Fresh' и ' есть :: Торт Свежий -> Торт Съеден; есть Торт = Торт'? – epsilonhalbe
@epsilonhalbe Конечно, но если вы тогда «съелиCookie <- uneatenCookie», ничто не остановило бы вас от использования 'uneatenCookie' впоследствии. – sepp2k
Я вижу - вам нужно будет написать собственную версию '<-', которая позаботится об очистке' uneatenCookie', но я думаю, что это выходит за рамки моей haskpertise. – epsilonhalbe