Purescript中的新類型是否可能存在約束條件？

Question

是否可以對Purescript中的類型構造函數施加某些限制？例如：

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

Answer 1

對於約束，答案是一定否定的，因爲它取決於String的價值，Purescript沒有相關的類型。

在伊德里斯（或阿格達）你可以自由地做到以下幾點：

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

其中IsTrue b是具有值當且僅當b計算結果爲true的類型。這將做你想要的。也許一些未來的Purescript版本將支持這樣的事情。

Answer 2

正如在另一個答案中提到的，你需要一些發燒友類型的系統能夠像這樣編碼它，所以通常達到你想要的方式是爲newtype提供一個「智能構造函數」，然後不要出口構造本身，人的這種方式只能構建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 3

不同的解決方案是通過數據類型的代數結構來強制約束：

data Name = Name Char Char Char Char Char String 

根據您的用例，這可能比智能構造函數更方便和/或更高效。