Remix.run Logo
solomonb 6 hours ago

From the article:

    validateNonEmpty :: [a] -> IO ()
    validateNonEmpty (_:_) = pure ()
    validateNonEmpty [] = throwIO $ userError "list cannot be empty"
    
    parseNonEmpty :: [a] -> IO (NonEmpty a)
    parseNonEmpty (x:xs) = pure (x:|xs)
    parseNonEmpty [] = throwIO $ userError "list cannot be empty"
Both consolidate all the invariants about your data; in this example there is only one invariant but I think you can get the point. The key difference between the "validate" and "parse" versions is that the structure of `NonEmpty` carries the proof that the list is not empty. Unlike the ordinary linked list, by definition you cannot have a nil value in a `NonEmpty` and you can know this statically anywhere further down the call stack.