Logo Questions Linux Laravel Mysql Ubuntu Git Menu
 

Are constraints possible for new types in Purescript?

Tags:

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
like image 813
dgo.a Avatar asked Feb 08 '23 03:02

dgo.a


2 Answers

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
like image 83
gb. Avatar answered Feb 15 '23 15:02

gb.


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.

like image 30
András Kovács Avatar answered Feb 15 '23 15:02

András Kovács