Is it possible to put certain constraints on the type constructor in Purescript? For example:
newtype Name = Name String
-- where length of String is > 5
As mentioned in the other answer you'd need some fancier type system to be able to encode it like that, so commonly the way to achieve what you want is to provide a "smart constructor" for the newtype
and then not export the constructor itself, that way people will only be able to construct values of the newtype with the property you desire:
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
For that constraint, the answer is a definite no, because it depends on the value of the String
, and Purescript doesn't have dependent types.
In Idris (or Agda) you're free to do the following:
data Name : Type where
Name : (s : String) -> IsTrue (length s > 5) -> Name
where IsTrue b
is a type that has a value if and only if b
evaluates to true. This would do exactly what you wish for. Maybe some future Purescript version will support such things.
If you love us? You can donate to us via Paypal or buy me a coffee so we can maintain and grow! Thank you!
Donate Us With