使用类型强制正确 [英] Using types to force correctness

问题描述

假设我们有一个商店管理应用程序。它有客户，可以 chargeFee（）。它应该只对活动的客户而这样做。

我看到这样做的一个常见方式（Java /伪代码）是这样的：

  class Customer {
 String name 
 StatusEnum status // 1 = active，2 = inactive 
} 
 
 //这是客户收取的
（c：Customer.listByStatus（StatusEnum.1））{
 c.chargeFee（）
} 
  

这样可以，但是不会停止有人从不活动的客户收取费用。即使 chargeFee（）检查客户的状态，那是一个运行时错误/事件。

所以，保持整个使非法状态无法代表的事情，一个方法如何设计这个应用程序（例如在Haskell中）？我想要一个编译错误，如果有人试图收取一个不活跃的客户。

---

我在想这样的事情，但我还是不允许我限制 chargeFee ，以便无法收取无效的客户。

 数据CustomerDetails = CustomerDetails {name :: String} 
数据客户a =活动a |不活动a 
 
 chargeFee :: Active a  - > Int  - 这不行，我需要DataKinds吗？ 
  

解决方案

你可以用幻像类型完成这样的事情： / p>

 模块客户
（CustomerKind（..），客户，{ - 注意：MkCustomer未导出 - } 
 makeCustomer，activate，chargeFee）其中
 
数据CustomerKind = Active |非活动
数据客户（x :: CustomerKind）= MkCustomer String 
 
 mkCustomer :: String  - >客户不活动
 mkCustomer = MkCustomer 
 
  - 也许`IO（客户活动）'或别的东西
 activate :: Customer Inactive  - >可能（客户有效）
 activate = ... 
 
 chargeFee ::客户主动 - > Int 
 chargeFee = ... 
  

这里 activate 将以某种方式确保给定的客户可以活跃（并且这样做），生产所述活跃的客户。但是尝试调用 chargeFee（mkCustomer ...）是一个类型错误。

请注意， DataKinds 不是严格要求的 - 以下是等价的：

 数据活动
数据无效
  - 其他一切不变
  

通过简单地声明两种类型 - ActiveCustomer 和 InactiveCustomer - 但幻影类型方法允许您编写不关心客户类型的功能：

  customerName :: Customer a  - > String 
 customerName（MkCustomer a）= ... 
  

Let's say that we have a store management application. It has Customers and can chargeFee(). It should do so only for active Customers however.

A common way I've seen this done (Java/pseudocode) is something like this:

class Customer {
    String name
    StatusEnum status  // 1=active, 2=inactive
}    

// and this is how the customers are charged
for (c:Customer.listByStatus(StatusEnum.1)) {
    c.chargeFee()
}

This is OK, but it doesn't stop someone from charging a fee from an inactive Customer. Even if chargeFee() checks the status of the Customer, that's a runtime error/event.

So, keeping the whole 'make illegal states unrepresentable' thing in mind, how would one approach design of this application (in Haskell for example)? I want a compile error if someone tries to charge an inactive customer.

---

I was thinking something like this, but I still doesn't allow me to restrict chargeFee so that an inactive Customer cannot be charged.

data CustomerDetails = CustomerDetails { name :: String }
data Customer a = Active a | Inactive a

chargeFee :: Active a -> Int -- this doesn't work, do I need DataKinds?

解决方案

You can accomplish such a thing with phantom types:

module Customer 
   (CustomerKind(..), Customer, {- note: MkCustomer is not exported -}       
    makeCustomer, activate, chargeFee) where

data CustomerKind = Active | Inactive 
data Customer (x :: CustomerKind) = MkCustomer String 

mkCustomer :: String -> Customer Inactive 
mkCustomer = MkCustomer 

-- perhaps `IO (Customer Active)' or something else
activate :: Customer Inactive -> Maybe (Customer Active) 
activate = ...

chargeFee :: Customer Active -> Int
chargeFee = ... 

Here activate will somehow ensure that the given customer can be made active (and do so), producing said active customer. But trying to call chargeFee (mkCustomer ...) is a type error.

Note that DataKinds are not strictly required - the following is equivalent:

data Active 
data Inactive 
-- everything else unchanged 

The same can be accomplished without phantom types, by simply declaring two types - ActiveCustomer and InactiveCustomer - but the phantom types approach allows you to write functions which don't care about the type of customer:

customerName :: Customer a -> String 
customerName (MkCustomer a) = ...

这篇关于使用类型强制正确的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！