如何使非法价值无法代表？

Question

功能编程中的一种设计方法是使非法国家无法代表.我总是看到这是通过类型的结构来完成的,但类型的价值呢？

如果我有一个名为Email的字符串怎么办？我只希望它保留一个有效的电子邮件地址(针对某些正则表达式进行检查)？如何以功能方式(不使用OOP)执行此操作？

Answer 1

一个常见的习惯用法是使用智能构造函数.

module Email (email, fromEmail, Email()) where

-- export the type, but not the constructor
newtype Email = Email String

-- export this
email :: String -> Maybe Email
email s | validEmail s = Just (Email s)
        | otherwise    = Nothing

-- and this
fromEmail :: Email -> String
fromEmail (Email s) = s

这将在运行时验证电子邮件,而不是编译时间.

对于编译时验证,需要利用GADT重的变体String,或者使用模板Haskell(元编程)来进行检查(假设电子邮件值是文字).

对于那些支持它们的语言(例如Agda,Idris,Coq),依赖类型也可以确保值的形式正确.F-star是F#的变体,可以验证前置条件/​​后置条件,并实现一些高级静态检查.

Answer 2

我假设,就像你做所有的运行时错误处理一样？

如果你"使用类和属性进行封装",你会抛出一个异常(即在setter中),某些代码,在调用链中更高的位置,必须要注意.不是你的"类和属性"神奇地解决了这个问题,抛出和捕获异常是你的纪律.在大多数任何FP语言中,您都有大量的表示形式,用于表示错误的值/输入,从简单Maybe或更详细Either(或在F#中调用的任何内容)到完全爆炸的异常,强制立即停止与stderr -信息.适合当前的app/lib上下文.

"在类型中使非法状态无法代表"是为了抢占许多易于制造的瞬间开发人员错误,因为类型系统/编译器理解操作方法:不是用户错误.

当然,我们如何将处理越来越多的错误类型转移到静态(编译)方面进行学术探索和研究,在Haskell中,LiquidHaskell就是一个突出的例子.但是,如果你有一个时间机器,如果编译后读取的输入是错误的,你不能追溯性地阻止你的程序编译:D换句话说,防止错误的电子邮件地址的唯一方法是强加一个不可能的GUI让一个通过.

Answer 3

我通常按​​照@chi的方式做.正如他所说,你也可以使用Template Haskell在编译时对提供的电子邮件进行检查.这样做的一个例子:

#!/usr/bin/env stack
{- stack
     --resolver lts-8.2
     exec ghci
     --package email-validate
     --package bytestring
-}

{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE DeriveLift #-}
{-# LANGUAGE TemplateHaskell #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE QuasiQuotes #-}

import Language.Haskell.TH
import Language.Haskell.TH.Quote
import Language.Haskell.TH.Syntax
import Data.ByteString.Char8
import Text.Email.Validate

instance Lift ByteString where
  lift b = [|pack $(lift $ unpack b)|]

instance Lift EmailAddress where
  lift email = lift (toByteString email)

email :: QuasiQuoter
email =
  QuasiQuoter
  { quoteExp =
    \str ->
       let (item :: EmailAddress) =
             case (validate (pack str)) of
               Left msg -> error msg
               Right email -> email
       in [|item|]
  }

现在,如果你加载它ghci:

> :set -XQuasiQuotes
> [email|sibi@mydomain.in|]
"sibi@mydomain.in"
> [email|invalidemail|]

<interactive>:6:1: error:
    • Exception when trying to run compile-time code:
        @: not enough input
CallStack (from HasCallStack):
  error, called at EmailV.hs:36:28 in main:EmailV
      Code: quoteExp email "invalidemail"
    • In the quasi-quotation: [email|invalidemail|]

您可以看到如何在无效输入上获得编译错误.

Answer 4

看来,@ chi和@Sibi的答案都是精炼类型的答案.即,包含其他类型的类型,同时使用验证器限制支持的值的范围.验证可以在运行时和编译时完成,具体取决于用例.

事实上,我已经创作了"精炼"这个库,它提供了两种情况的抽象.请点击链接进行广泛的介绍.

要在场景中应用此库,请在一个模块中定义谓词:

import Refined
import Data.ByteString (ByteString)

data IsEmail

instance Predicate IsEmail ByteString where
  validate _ value = 
    if isEmail value
      then Nothing
      else Just "ByteString form an invalid Email"
    where
      isEmail =
        error "TODO: Define me"

-- | An alias for convenince, so that there's less to type.
type EmailBytes =
  Refined IsEmail ByteString

然后在任何其他模块中使用它(由于模板Haskell,这是必需的).

您可以在编译时和运行时构造值:

-- * Constructing
-------------------------

{-|
Validates your input at run-time.

Abstracts over the Smart Constructor pattern.
-}
dynamicallyCheckedEmailLiteral :: Either String EmailBytes
dynamicallyCheckedEmailLiteral =
  refine "email@example.info"

{-|
Validates your input at compile-time with zero overhead.

Abstracts over the solution involving Lift and QuasiQuotes.
-}
staticallyCheckedEmailLiteral :: EmailBytes
staticallyCheckedEmailLiteral =
  $$(refineTH "email@example.info")


-- * Using
-------------------------

aFunctionWhichImpliesThatTheInputRepresentsAValidEmail :: EmailBytes -> IO ()
aFunctionWhichImpliesThatTheInputRepresentsAValidEmail emailBytes =
  error "TODO: Define me"
  where
    {-
    Shows how you can extract the "refined" value at zero cost.

    It makes sense to do so in an enclosed setting.
    E.g., here you can see `bytes` defined as a local value,
    and we can be sure that the value is correct.
    -}
    bytes :: ByteString
    bytes =
      unrefine emailBytes

另外请注意,这只是Refinement Types可以涵盖的表面.实际上它们有更多有用的属性.