Search code examples
purescript

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
Solution

  • 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.