-- Haskell98!
-- Safe list functions, by construction
module NList0 (FullList,
fromFL,
indeedFL,
decon,
head,
tail,
Listable (..)
) where
import Prelude hiding (head, tail)
-- Whether the data constructor |FullList| is exported or not
-- does not affect safety
data FullList a = FullList a [a] -- carry the head explicitly
fromFL (FullList x l) = x : l -- Injection into general lists
-- The following is an analogue of `maybe'
indeedFL :: [a] -> w -> (FullList a -> w) -> w
indeedFL x on_empty on_full = case x of
[] -> on_empty
(h:t) -> on_full $ FullList h t
-- A possible alternative, with an extra Maybe tagging
-- indeedFL :: [a] -> Maybe (FullList a)
-- A more direct analogue of `maybe', for lists
decon :: [a] -> w -> (a -> [a] -> w) -> w
decon [] on_empty on_full = on_empty
decon (h:t) on_empty on_full = on_full h t
-- The following are _total_ functions
-- They are guaranteed to be safe, and so we could have used
-- unsafeHead# and unsafeTail# if GHC provides though...
head :: FullList a -> a
head (FullList x _) = x
tail :: FullList a -> [a]
tail (FullList _ x) = x
-- Mapping over a non-empty list gives a non-empty list
instance Functor FullList where
fmap f (FullList h t) = FullList (f h) (map f t)
-- Adding something to a general list surely gives a non-empty list
infixr 5 !:
class Listable l where
(!:) :: a -> l a -> FullList a
instance Listable [] where
(!:) h t = FullList h t
instance Listable FullList where
(!:) h (FullList h' t) = FullList h (h':t)