How to create Type which contains String with limited length in Haskell [duplicate]

Question

Possible Duplicate:
How to make a type with restrictions

Is it possible in Haskell to create a type for example "Name" which is a String but containing no more then 10 letters?

If not how can I forbid to create a Person with to long name (where Person is defined like that: data Person = Person Name).

Maybe it is not important at all, maybe that kind of problems should be solved in Haskell in a different way?

Answer 1

You described the type perfectly well. You'll soon regret it of course...

data Name  = N1 Char
           | N2 Char Char
           | N3 Char Char Char
           | N4 Char Char Char Char
           | N5 Char Char Char Char Char
           | N6 Char Char Char Char Char Char
           | N7 Char Char Char Char Char Char Char
           | N8 Char Char Char Char Char Char Char Char
           | N9 Char Char Char Char Char Char Char Char Char
           | N10 Char Char Char Char Char Char Char Char Char Char
           deriving (Show, Eq,Ord)

prettyName :: Name -> String
prettyName (N1 a) = a:[]
prettyName (N2 a b) = a:b:[]
prettyName (N3 a b c) = a:b:c:[]
prettyName (N4 a b c d) = a:b:c:d:[]
prettyName (N5 a b c d e) = a:b:c:d:e:[]
prettyName (N6 a b c d e f) = a:b:c:d:e:f:[]
prettyName (N7 a b c d e f g) = a:b:c:d:e:f:g:[]
prettyName (N8 a b c d e f g h) = a:b:c:d:e:f:g:h:[]
prettyName (N9 a b c d e f g h i) = a:b:c:d:e:f:g:h:i:[]
prettyName (N10 a b c d e f g h i j) = a:b:c:d:e:f:g:h:i:j:[]

And while we're importing Text.PrettyPrint here in ghci, why not a parser?

import Text.ParserCombinators.Parsec
import Control.Applicative ((<*))
-- still lame
pN :: Parser Name
pN = do letters <- many1 alphaNum <* space
        case letters of 
            a:[]  -> return $ N1 a  
            a:b:[]  -> return $ N2 a b  
            a:b:c:[]  -> return $ N3 a b c  
            a:b:c:d:[]  -> return $ N4 a b c d  
            a:b:c:d:e:[]  -> return $ N5 a b c d e  
            a:b:c:d:e:f:[]  -> return $ N6 a b c d e f  
            a:b:c:d:e:f:g:[]  -> return $ N7 a b c d e f g  
            a:b:c:d:e:f:g:h:[]  -> return $ N8 a b c d e f g h  
            a:b:c:d:e:f:g:h:i:[]  -> return $ N9 a b c d e f g h i  
            a:b:c:d:e:f:g:h:i:j:[]  -> return $ N10 a b c d e f g h i j
            _ -> unexpected "excess of letters"

-- *Main> parseTest pN "Louise "
-- N6 'L' 'o' 'u' 'i' 's' 'e'
-- *Main> parseTest pN "Louisiana "
-- N9 'L' 'o' 'u' 'i' 's' 'i' 'a' 'n' 'a'
-- *Main> parseTest (fmap prettyName pN) "Louisiana "
-- "Louisiana"
-- *Main> parseTest pN "Mississippi "
-- parse error at (line 1, column 13):
-- unexpected excess of letters

... Maybe this wasn't such a good idea ...

Answer 2

dave4420 has the answer for what you should do. That is, only export smart constructors. In a dependently typed language you could limit data types to certain forms. But, Haskell is not dependently typed.

Wait, no that is not true. Haskell is "the worlds most popular dependently typed language". You just have to fake the dependent types. Stop. Read no further if you are 1. still learning basic Haskell 2. not totally insane.

It is possible to encode your "no longer than 10 characters" constraint in the type system. with a type like

data Name where
    Name :: LessThan10 len => DList Char len -> Name

but I'm getting ahead of myself

first of all, you need tons of extensions (I assume GHC 7.4, early versions can still do it, but it is much more of a pain)

{-# LANGUAGE TypeFamilies,
             DataKinds,
             GADTs,
             FlexibleInstances,
             FlexibleContexts,
             ConstraintKinds-}

import Prelude hiding (succ)

now we build some machinery for type level naturals...using the new DataKinds extension

data Nat = Z | S Nat

type N1 = S Z --makes writing numbers easier
type N2 = S N1
--etc
type N10 = S N9

now we need a data representation of numbers and a way to generate them

data Natural n where
    Zero :: Natural Z
    Succ :: Natural a -> Natural (S a)

class Reify a where
   reify :: a

instance Reify (Natural Z) where
   reify = Zero

instance Reify (Natural n) => Reify (Natural (S n)) where
   reify = Succ (reify)

okay, now we can encode the idea of number being less than 10, and write a helper to test it for boot

type family LTE (a :: Nat) (b :: Nat) :: Bool
type instance LTE Z b = True
type instance LTE (S a) Z = False
type instance LTE (S a) (S b) = LTE a b

--YAY constraint kinds!
type LessThan10 a = True ~ (LTE a N10)

data HBool b where
   HTrue :: HBool True
   HFalse :: HBool False

isLTE :: Natural a -> Natural b -> HBool (LTE a b)
isLTE Zero _ = HTrue
isLTE (Succ _) Zero = HFalse
isLTE (Succ a) (Succ b) =  isLTE a b

with all of that we can define length encoded strings

data DList a len where
   Nil :: DList a Z
   Cons :: a -> DList a len -> DList a (S len)

toList :: DList a len -> [a]
toList Nil = []
toList (Cons x xs) = x:toList xs

data Name where
   Name :: LessThan10 len => DList Char len -> Name

and even get the string back, and define a neat-oh Show instance for Name

nameToString :: Name -> String
nameToString (Name l) = toList l

instance Show Name where
   show n = "Name: " ++ nameToString n

the problem is that we need a way to turn a String into a Name. That is harder.

First up, lets figure out how long a String is

data AnyNat where
    AnyNat :: Natural n -> AnyNat

zero = AnyNat Zero
succ (AnyNat n) = AnyNat (Succ n)

lengthNat :: [a] -> AnyNat
lengthNat [] = zero
lengthNat (_:xs) = succ (lengthNat xs)

now it is a simple matter to turn lists into dependent lists

fromListLen :: Natural len -> [a] -> Maybe (DList a len)
fromListLen Zero [] = Just Nil
fromListLen Zero (x:xs) = Nothing
fromListLen (Succ a) [] = Nothing
fromListLen (Succ a) (x:xs) = do rs <- fromListLen a xs
                                 return (Cons x rs)

still not home free, but we are getting there

data MaybeName b where
    JustName :: LessThan10 len => DList Char len -> MaybeName True
    NothingName :: MaybeName False

maybeName :: MaybeName b -> Maybe Name
maybeName (JustName l) = Just $ Name l
maybeName (NothingName) = Nothing

stringToName' :: Natural len -> String -> MaybeName (LTE len N10)
stringToName' len str = let t = isLTE len (reify :: Natural N10)
                        in case t of
                           HFalse ->  NothingName
                           HTrue  -> case fromListLen len str of
                                          Just x -> JustName x
                                          --Nothing -> logic error

the last bit just involves convincing GHC we are not trying to blow the compiler's brains out unsafePerformIO $ produce evilLaugh

stringToNameLen :: Natural len -> String -> Maybe Name
stringToNameLen len str = maybeName $ stringToName' len str

stringToNameAny :: AnyNat -> String -> Maybe Name
stringToNameAny (AnyNat len) str = stringToNameLen len str

stringToName :: String -> Maybe Name
stringToName str = stringToNameAny (lengthNat str) str

wow, I write long stack overflow posts, but this takes the cake

we test it

*Main> stringToName "Bob"
Just Name: Bob
*Main> stringToName "0123456789"
Just Name: 0123456789
*Main> stringToName "01234567890"
Nothing

So it works, and the type system now can enforce the invariant that your names are no more than 10 characters. Seriously though, odds are this is not worth your effort.