我正在建模一个系统,该系统具有创建资源的操作和消耗该资源的其他操作。但是,给定的资源只能使用一次 - 有没有办法可以保证在编译时?
具体来说,假设第一个操作烤蛋糕,还有另外两个操作,一个是“选择吃”蛋糕,一个是“选择吃蛋糕”,我只能做一个或另一个。
-- This is my current "weakly typed" interface:
bake :: IO Cake
eat :: Cake -> IO ()
keep :: Cake -> IO ()
-- This is OK
do
brownie <- bake
muffin <- bake
eat brownie
keep muffin
-- Eating and having the same cake is not OK:
do
brownie <- bake
eat brownie
keep brownie -- oops! already eaten!
通过在我们使用蛋糕后在蛋糕上设置一个标志,可以很容易地强制执行在运行时不保留已经吃过的蛋糕(反之亦然)的限制。但是有没有办法在编译时强制执行呢?
顺便说一句,这个问题是为了证明概念,所以我可以接受任何可以给我想要的静态安全的黑魔法。
最佳答案
在 Haskell 中,它的基本版本可以用一个 GADT 来表示,该 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
会进行类型检查,但通过推送所有 Elem
会使甚至不正确的程序进行类型检查到顶部的约束。尽管如此,这仍然会阻止使用不正确的术语做任何有用的事情,但这是一个相当丑陋的解决方案。更一般地,我们可以表示
Bake
作为一个索引的自由单子(monad),它得到我们do
-符号 RebindableSyntax
, 并允许定义 BakeF
这比我们以前看到的要清楚一些。它还可以像普通的 Free
一样减少样板文件。 monad,尽管我发现人们不太可能在实际代码中的两个不同场合发现索引自由 monad 的用途。{-# 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
关于haskell - 有没有办法在 Haskell 中模拟线性类型?,我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/34227536/