在类型级别上编码是否存在身份验证 [英] Codifying presence/absence of authentication at type level

问题描述

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

我正在写一个Telegram机器人，应该可以由我公司内的用户访问。为了实现这种限制，只要有人开始与机器人聊天，它会在表中查找 chat_id ，并检查一个有效的 oauth_token code>存在。如果没有，用户将首先被发送链接以完成Google OAuth（我们公司的电子邮件托管在Google Apps for Business中）。

  share [mkPersist sqlSettings，mkMigratemigrateAll] [persistLowerCase | 
 VLUser 
 email字符串
 chatId整数
 tgramUserId整数
 tgramFirstName字符串
 tgramLastName字符串可能
 tgramUsername字符串也许
 oauthToken字符串也许
导出显示
 |] 
  

具有有效 oauth_token 将能够给Telegram bot一些命令，这些未经授权的用户不应该给予。

现在，我是试图在类型层面上对这种逻辑进行编码。在我的Haskell代码中将会有一些函数可以接受作为参数的身份验证&未经认证的用户;而一些函数应该只接受通过身份验证的用户。

如果我不断传递相同类型的用户对象，即 VLUser 无处不在，那么我必须小心检查每个函数中是否存在 oauthToken 。有没有办法创建两个用户类型 - VLUser 和 VLUserAuthenticated 其中：

1. 两者都映射到相同的基础表


2. 可以实例化一个 VLUserAuthenticated 如果它有一个 oauthToken

解决方案

幻影类型的救援！ 是Bryan O'Sullivan使用在类型级别的示例> 幻像类型 。

同样，对于您的用例：

 数据未知 - 未知用户
数据已验证 - 已验证用户
 
新类型用户ai = Id我导出显示
  

数据构造函数 Id 是 不暴露给用户，但该模块提供了初始化和验证用户的函数：

   - 初始化未认证的用户
 newUser :: i  - >用户未知i 
 newUser = Id 
 
  - 验证用户
 authUser ::（User a i） - >用户身份验证我
 authUser（Id i）= Id i  - 虚拟执行
  

然后，您可以控制类型级别的访问而不用代码重复，没有运行时检查和没有运行时开销： b
$ b

   - 向所有用户开放
 getId ::用户ai  - > i 
 getId（Id i）= i 
 
  - 只有经过认证的用户可以通过
 getId'::用户认证的i  - > I 
 getId'（Id i）= i 
  

例如，如果

  \>让jim = newUserjim
 \>让joe = authUser $ newUserjoe
  

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

  \> getId joe 
joe
 \> getId'joe 
joe
  

然而，您将得到编译时如果您通过 jim 调用 getId'：错误：

  \> getId jim 
jim
 \> getId'jim  - 编译时错误！不是运行时错误！ 
 
< interactive>：28：8：
无法将类型'Unknown'与'Authenticated'
进行匹配预期类型：User Authenticated [Char] 
 Actual在'getId''的第一个参数中，即'jim'
在表达式中：getId'jim 
  

Context: I'm approaching Haskell from a standpoint of converting runtime errors to compile-time errors. My hypothesis is that this is possible if one can codify business logic within the program's types itself.

I'm writing a Telegram bot, which should be accessible by users within my company. To achieve this "restriction", whenever someone starts chatting with the bot it will look up the chat_id in a table and check if a valid oauth_token exists. If not, the user will first be sent a link to complete a Google OAuth (our company's email is hosted on 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
|]

Users with a valid oauth_token will be able to give the Telegram bot some commands, which unauthenticated users should not be able to give.

Now, I'm trying to codify this logic at the type level itself. There will be some functions in my Haskell code that will have the ability to accept, as arguments, both, authenticated & unauthenticated users; while some functions should accept only authenticated users.

If I keep passing user objects of the same type, i.e. VLUser everywhere, then I will have to be careful to check for the presence of oauthToken in every function. Is there a way to create two user types - VLUser and VLUserAuthenticated where:

1. Both map to the same underlying table
2. A VLUserAuthenticated can be instantiated ONLY IF it has an oauthToken

解决方案

Phantom types to the rescue! is Bryan O'Sullivan example of implementing read-only vs read/write access at the type level using phantom types.

Similarly, for your use-case:

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

newtype User a i = Id i deriving Show

It is important that the data constructor Id is not exposed to user, but the module provides functions to initialize and authenticate users:

-- 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

then, you may control access at the type level without code duplication, without run-time checks and without run-time cost:

-- 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

For example, if

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

joe is an authenticated user and can be passed to either function:

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

whereas, you will get compile-time error if you call getId' with 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

这篇关于在类型级别上编码是否存在身份验证的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！