purescript - Purescript 中的新类型是否可以进行约束？

Question

是否可以对 Purescript 中的类型构造函数施加某些约束？例如：

newtype Name = Name String
   -- where length of String is > 5

Answer 1

正如在另一个答案中提到的那样，您需要一些更高级的类型系统才能对其进行编码，因此通常实现您想要的方法是为 the 提供“智能构造函数”，newtype然后不导出构造函数本身，这样人们就只能用你想要的属性来构造新类型的值：

module Names (runName, name) where

import Prelude
import Data.Maybe (Maybe(..))
import Data.String (length)

newtype Name = Name String

-- No way to pattern match when the constructor is not exported,
-- so need to provide something to extract the value too
runName :: Name -> String
runName (Name s) = s

name :: String -> Maybe Name
name s =
  if length s > 5
  then Just (Name s) 
  else Nothing

Answer 2

对于那个约束，答案是肯定的，因为它取决于 的值String，而 Purescript 没有依赖类型。

在 Idris（或 Agda）中，您可以自由地执行以下操作：

data Name : Type where
    Name : (s : String) -> IsTrue (length s > 5) -> Name

where是一个类型，当且仅当计算结果为 trueIsTrue b时才具有值。b这将完全符合您的要求。也许未来的一些 Purescript 版本会支持这些东西。

Answer 3

另一种解决方案是通过数据类型的代数结构来强制执行约束：

data Name = Name Char Char Char Char Char String

根据您的用例，这可能会也可能不会比智能构造函数更方便和/或更高效。