是的,我认为我们这里有一个 XY 问题,所以让我们退后一步。
A Reader
是一个携带 a 的 monadvalue可以方便地阅读。你没有值——你有一个想要在类型级别强制执行的权限列表——所以我认为你不需要或不想要一个阅读器,或者一个异构列表,或者其他类似的东西。
相反,给定布尔权限列表:
data Permission = PermissionA | PermissionB deriving (Show)
您想要定义一个在类型级别参数化的 monad 及其授予的权限列表。围绕您的基础设施的新型包装器IO
单子会做:
{-# LANGUAGE DataKinds, KindSignatures, GeneralizedNewtypeDeriving #-}
newtype M (ps :: [Permission]) a = M (IO a) deriving (Functor, Applicative, Monad)
您还需要一个类型函数(又称类型族)来确定权限是否在权限列表中:
{-# LANGUAGE TypeFamilies, TypeOperators #-}
type family Allowed (p :: Permission) ps where
Allowed p '[] = False
Allowed p (p:ps) = True
Allowed p (q:ps) = Allowed p ps
现在,如果您想编写需要某些权限的函数,您可以编写如下内容:
deleteA :: (Allowed PermissionA ps ~ True) => M ps ()
deleteA = M $ print "Deleted A"
readB :: (Allowed PermissionB ps ~ True) => M ps ()
readB = M $ print "Read B"
copyBtoA :: ( Allowed PermissionA ps ~ True
, Allowed PermissionB ps ~ True) => M ps ()
copyBtoA = M $ print "Copied B to A"
运行一个M
action 中,我们引入了一个无需权限即可运行的函数:
-- runM with no permissions
runM :: M '[] a -> IO a
runM (M act) = act
请注意,如果您尝试runM readB
,你会得到一个类型错误(无法匹配False
with True
-- 不是最大的错误消息,但是......)。
为了授予权限,我们引入函数:
-- grant permissions
grantA :: M (PermissionA:ps) a -> M ps a
grantA (M act) = M act
grantB :: M (PermissionB:ps) a -> M ps a
grantB (M act) = M act
这些函数本质上是术语级别的恒等函数——它们只是展开并重新包装M
构造函数。但是,它们在类型级别的操作是为其输入参数添加权限。这意味着:
runM $ grantB $ readB
现在进行类型检查。所以这样做:
runM $ grantA . grantB $ readB
runM $ grantB . grantA $ readB
runM $ grantB . grantA . grantB $ readB
etc.
然后你可以编写如下程序:
program :: IO ()
program = runM $ do
grantA $ do
deleteA
grantB $ do
readB
copyBtoA
同时拒绝以下计划:
program1 :: IO ()
program1 = runM $ do
grantA $ do
deleteA
grantB $ do
readB
copyBtoA -- error, needs PermissionB
这个基础设施可能有点丑陋,但它应该是基于类型的、完全编译时权限检查所需的全部。
也许尝试一下这个版本,看看它是否满足您的需求。完整代码是:
{-# LANGUAGE DataKinds, KindSignatures, GeneralizedNewtypeDeriving,
TypeFamilies, TypeOperators #-}
data Permission = PermissionA | PermissionB deriving (Show)
newtype M (ps :: [Permission]) a = M (IO a) deriving (Functor, Applicative, Monad)
type family Allowed (p :: Permission) ps where
Allowed p '[] = False
Allowed p (p:ps) = True
Allowed p (q:ps) = Allowed p ps
-- runM with no permissions
runM :: M '[] a -> IO a
runM (M act) = act
-- grant permissions
grantA :: M (PermissionA:ps) a -> M ps a
grantA (M act) = M act
grantB :: M (PermissionB:ps) a -> M ps a
grantB (M act) = M act
deleteA :: (Allowed PermissionA ps ~ True) => M ps ()
deleteA = M $ print "Deleted A"
readB :: (Allowed PermissionB ps ~ True) => M ps ()
readB = M $ print "Read B"
copyBtoA :: ( Allowed PermissionA ps ~ True
, Allowed PermissionB ps ~ True) => M ps ()
copyBtoA = M $ print "Copied B to A"
program :: IO ()
program = runM $ do
grantA $ do
deleteA
grantB $ do
readB
copyBtoA
基于@dfeuer 评论的两个附加注释。首先,它提醒我grantA
and grantB
同样可以使用“安全”来编写coerce
函数来自Data.Coerce
如下。这个版本和上面的版本生成的代码没有区别,所以这只是个人喜好的问题:
import Data.Coerce
-- grant permissions
grantA :: M (PermissionA:ps) a -> M ps a
grantA = coerce
grantB :: M (PermissionB:ps) a -> M ps a
grantB = coerce
其次,@dfeuer 所说的是,用于控制权限的可信代码基础和依赖类型系统来强制执行权限系统的“其余”代码之间没有明确的区别。例如,模式匹配M
构造函数本质上是危险的,因为你可以提取一个IO a
从一个权限上下文中并在另一个权限上下文中重建它。 (这基本上就是grantA
and grantB
正在做无条件提升权限。)如果您在受信任的代码库之外“意外”执行此操作,您最终可能会绕过权限系统。在许多应用中,这并不是什么大问题。
但是,如果您试图证明系统安全,您可能需要一个小型的可信代码库来处理危险的情况。M
构造函数并仅导出“安全”API,通过类型系统确保安全性。在这种情况下,您将有一个导出类型的模块M
,但不是它的构造函数M(..)
。相反,您可以导出智能构造函数来创建M
具有适当权限的操作。
此外,由于模糊的技术原因,即使不导出M
构造函数中,“不受信任”的代码仍然有可能在不同的权限上下文之间进行强制:
stealPermission :: M (PermissionA:ps) a -> M ps a
stealPermission = coerce
因为第一个参数M
类型构造函数有一个所谓的“角色”,默认为“幻影”而不是“名义”。如果你覆盖这个:
{-# LANGUAGE RoleAnnotations #-}
type role M nominal _
then coerce
只能在构造函数位于作用域内的情况下使用,从而弥补了这个漏洞。不受信任的代码仍然可以使用unsafeCoerce
,但有一些机制(Google 表示“Safe Haskell”)可以防止这种情况发生。