在类型级别编码身份验证的存在/不存在

Question

上下文:从将运行时错误转换为编译时错误的角度来看,我正在接近Haskell.我的假设是,如果可以在程序类型本身内编写业务逻辑,那么这是可能的.

我正在写一个Telegram bot,我公司的用户应该可以访问它.为了实现这种"限制",每当有人开始与机器人聊天时,它将chat_id在表格中查找并检查是否oauth_token存在有效.如果没有,系统会首先向用户发送完成Google OAuth的链接(我们公司的电子邮件托管在Google Apps for Business上).

share [mkPersist sqlSettings, mkMigrate "migrateAll"] [persistLowerCase|
VLUser
  email String
  chatId Integer
  tgramUserId Integer
  tgramFirstName String
  tgramLastName String Maybe
  tgramUsername String Maybe
  oauthToken String Maybe
  deriving Show
|]

具有有效权限的用户oauth_token将能够为Telegram bot提供一些命令,未经身份验证的用户无法提供这些命令.

现在,我试图在类型级别本身编写这个逻辑.我的Haskell代码中将有一些函数能够接受经过身份验证和未经身份验证的用户作为参数; 而某些功能应该只接受经过身份验证的用户.

如果我继续传递相同类型的用户对象,即VLUser无处不在,那么我将不得不小心检查oauthToken每个函数的存在.有没有办法创建两种用户类型 - VLUser以及VLUserAuthenticated:

1. 两者都映射到相同的基础表
2. VLUserAuthenticated只有在有A的情况下才能实例化oauthToken

Answer 1

幻影类型救援!是Bryan O'Sullivan使用幻像类型在类型级别实现只读vs读/写访问的示例.

同样,对于您的用例:

data Unknown       -- unknown users
data Authenticated -- verified users

newtype User a i = Id i deriving Show

这是很重要的是,数据构造Id是不暴露给用户,但该模块提供了初始化和验证用户:

-- initializes an un-authenticated user
newUser :: i -> User Unknown i
newUser = Id

-- authenticates a user
authUser :: (User a i) -> User Authenticated i
authUser (Id i) = Id i  -- dummy implementation

然后,您可以在没有代码重复的情况下控制类型级别的访问,无需运行时检查,也没有运行时成本:

-- open to all users
getId :: User a i -> i
getId (Id i) = i

-- only authenticated users can pass through
getId' :: User Authenticated i -> i
getId' (Id i) = i

例如,如果

\> let jim = newUser "jim"
\> let joe = authUser $ newUser "joe"

joe 是经过身份验证的用户,可以传递给任一函数:

\> getId joe
"joe"
\> getId' joe
"joe"

然而,如果您使用以下方法调用,则会出现编译时错误:getId'jim

\> getId jim
"jim"
\> getId' jim   -- compile-time error! not run-time error!

<interactive>:28:8:
    Couldn't match type ‘Unknown’ with ‘Authenticated’
    Expected type: User Authenticated [Char]
      Actual type: User Unknown [Char]
    In the first argument of ‘getId'’, namely ‘jim’
    In the expression: getId' jim