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

Question

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

我正在编写一个 Telegram 机器人，我公司内的用户应该可以访问它。为了实现这种“限制”，每当有人开始与机器人聊天时，它都会查找 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 机器人一些命令，而未经身份验证的用户不应该给出这些命令。

现在，我正在尝试在类型级别本身编写此逻辑。我的 Haskell 代码中将有一些函数能够接受经过身份验证和未经身份验证的用户作为参数；而某些功能应该只接受经过身份验证的用户。

如果我不断传递相同类型的用户对象，即 VLUser到处都是，那么我将不得不小心检查是否存在 oauthToken在每个功能中。有没有办法创建两种用户类型 - VLUser和 VLUserAuthenticated在哪里:

两者都映射到同一个基础表

一个 VLUserAuthenticated仅当它具有 oauthToken 时才能实例化

Answer 1

Phantom types to the rescue!是 Bryan O'Sullivan 实现只读与读/写访问的示例 在类型级别 使用 phantom types .

同样，对于您的用例:

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