CODEWITHSUNDEEP
purescript
dgo.a
dgo.a

Reputation: 2764

Are constraints possible for new types in Purescript?

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

Upvotes: 4

Views: 755

Answers (3)

user1804599
user1804599

Reputation:

A different solution is to enforce the constraint through the algebraic structure of the data type:

data Name = Name Char Char Char Char Char String

Depending on your use case this may or may not be more convenient and/or efficient than smart constructors.

Upvotes: 0

gb.
gb.

Reputation: 4649

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

Upvotes: 5

András Kovács
András Kovács

Reputation: 30103

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.

Upvotes: 3

Related Questions