-- $Id: NonEmptyList.hs,v 1.1 2019/09/26 01:59:51 leavens Exp leavens $
module NonEmptyList (module Nat, module NonEmptyList) where
import Nat
data NonEmptyList a = Sing a | a :# (NonEmptyList a)
deriving (Eq)
-- for a Show instance, load the module NonEmptyListShow
-- the following makes :# right associative (and same precedence as colon)
infixr 5 :#
maxl :: (Ord a) => (NonEmptyList a) -> a
maxl (Sing x) = x
maxl (x :# xs) = max x (maxl xs)
-- an alternative second clause:
-- maxl (x :# xs) = if x > mxs then x else mxs
-- where mxs = maxl xs
examples = [
(maxl (Sing 3)) == 3,
(maxl (4 :# (0 :# (2 :# (Sing 0))))) == 4,
(maxl (0 :# (2 :# (Sing 0)))) == 2,
(maxl (2 :# (Sing 0))) == 2,
(maxl (Sing 0)) == 0
]
nth :: (NonEmptyList a) -> Nat -> a
nth (Sing x) Zero = x
nth (x :# xs) Zero = x
nth (Sing x) (Succ _) = undefined
nth (x :# xs) (Succ n) = (nth xs n)