How to make illegal values unrepresentable? [duplicate]

A common idiom is to use a smart constructor.

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 

This will verify emails at runtime, not compile time.

For compile time verification, one would need to exploit a GADT-heavy variant of String, or use Template Haskell (metaprogramming) to do the checks (provided the email value is a literal).

Dependent types can also ensure values are of the right form, for those languages that support them (e.g. Agda, Idris, Coq). F-star is a variant of F# that can verify preconditions/postconditions, and achieve some advanced static checks.

I usually do the way @chi has done. As he stated, you can also you Template Haskell to do checks on the provided email at compile time. An example of doing that:

#!/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|] } 

Now, if you load this up in ghci:

> :set -XQuasiQuotes > [email|[email protected]|] "[email protected]" > [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|] 

You can see how you get compile error on the invalid input.

As it appears, both answers of @chi and @Sibi are what Refinement Types are about. I.e., the types which enclose other types, while restricting the range of supported values with a validator. The validation can be done both at run-time and compile-time depending on the use-case.

It just so happens that I've authored "refined", a library, which provides abstractions for both cases. Follow the link for an extensive introduction.

To apply this library in your scenario, in one module define the predicate:

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 

Then use it in any other module (this is required due to Template Haskell).

You can construct the values both at compile-time and run-time:

-- * Constructing ------------------------- {-| Validates your input at run-time. Abstracts over the Smart Constructor pattern. -} dynamicallyCheckedEmailLiteral :: Either String EmailBytes dynamicallyCheckedEmailLiteral = refine "[email protected]" {-| Validates your input at compile-time with zero overhead. Abstracts over the solution involving Lift and QuasiQuotes. -} staticallyCheckedEmailLiteral :: EmailBytes staticallyCheckedEmailLiteral = $$(refineTH "[email protected]") -- * 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 

Also please beware that this is just a surface of what Refinement Types can cover. There's actually much more useful properties to them.

This was answered for me recently.

Here's the post.

The context of your question is in regards to a valid email. The overall structure of your code will leverage Active Patterns:

module File1 = type EmailAddress = private | Valid of string | Invalid of string let createEmailAddress (address:System.String) = if address.Length > 0 then Valid address else Invalid address // Exposed patterns go here let (|Valid|Invalid|) (input : EmailAddress) : Choice<string, string> = match input with | Valid str -> Valid str | Invalid str -> Invalid str module File2 = open File1 let validEmail = Valid "" // Compiler error let isValid = createEmailAddress "" // works let result = // also works match isValid with | Valid x -> true | _ -> false