Logo Questions Linux Laravel Mysql Ubuntu Git Menu
 

How do I enforce run-time conditions on data in Haskell?

I want to define a function f [Int] -> Int where f is equal to the sum of the elements in the list if the length of the list is a perfect square and is undefined otherwise. What is the idiomatic way to do this in Haskell?

In an imperative language I'd add a line to the effect of assert sqrt(len(xs)) is integer to generate an exception for the undefined cases. In a strongly-typed functional language like Haskell you want to build undefined conditions into the type system, however that can't be done here since there is no "list of length perfect square" type.

I'd prefer to have the program halt with an error in the undefined case rather than have the function return Nothing.

like image 794
W.P. McNeill Avatar asked Dec 10 '18 23:12

W.P. McNeill


2 Answers

If you want to be formal about it it might be a good opportunity to use a smart constructor.

module PSqList
    ( PSqList   -- constructor *not* exported
    , fromList
    )
where

newtype PSqList a = PSqList [a]
    deriving (Functor, Foldable)

fromList :: [a] -> Maybe (PSqList a)
fromList xs
    | isPerfectSquare (length xs) = Just (PSqList xs)
    | otherwise = Nothing

Then when you use the PSqList module, you may only construct a PSqLists that have perfect square lengths.

It feels a bit strange to use a whole module for something like this; maybe you want a more general invariant-tracking system. This is a domain of a dependently typed language like Agda in general, but there is a lovely midpoint available in Haskell shown in the functional pearl Ghosts of Departed Proofs.

like image 76
luqui Avatar answered Oct 25 '22 16:10

luqui


I'd prefer to have the program halt with an error in the undefined case rather than have the function return Nothing.

The standard and idiomatic way to do this is certainly to return a Maybe Int, rather than to do what you say you'd prefer to do.

If you're asking how to raise an error from pure code, you can do

f ... = error "oops it wasn't a perfect square"

Another possibility is that your input [Int] is not the right type. Perhaps what you want is a list that is guaranteed to be a power of two length. In that case you can create a smart constructor (a function that is the only way of producing a PowerOfTwoList a, and which does validation). You could also use some kind of length-indexed vector, where the type-level natural is the power of two (i.e. the length of the list is represented in the type, and is also correct by construction)

like image 39
jberryman Avatar answered Oct 25 '22 17:10

jberryman