{-# LANGUAGE ExistentialQuantification, TypeOperators, EmptyDataDecls #-}
module SList where
import PhantomTypes
data Safe
data Unsafe
-- Reimplemention of standard list constructors
-- instead of wrapping
-- Also switching the order of arguments to make
-- casting easier.
data List b a = Nil (a :=: Unsafe)
| forall c. Cons (a :=: Safe) b (List b c)
instance Show b => Show (List b a) where
show (Nil _) = "nil"
show (Cons _ x xs) = "(cons " ++ show x ++ " " ++ show xs ++ ")"
nil :: List b Unsafe
nil = undefined
cons :: b -> List b c -> List b Safe
cons = undefined
testnull :: List b a -> (List b Unsafe -> c) -> (List b Safe -> c) -> c
testnull l@(Nil p) is isnot = is undefined
testnull l@(Cons p _ _) is isnot = isnot undefined
-- For flexibilty, note we don't want the opposite conversion
-- Can't do this one.
-- forget :: List Safe b -> List Unsafe b
-- instead, can only do this one.
data ListUnsafe b = forall a. L ( List b a)
forget :: List b Safe -> ListUnsafe b
forget = undefined
instance Show a => Show (ListUnsafe a) where
show (L l) = show l
toList :: List b a -> [b]
toList (Nil _) = []
toList (Cons _ hd tl) = hd : toList tl
fromList :: [b] -> ListUnsafe b
fromList l = foldr (\x (L xs) -> L (cons x xs)) (L nil) l
-- Four operations that require non-empty lists
sHead :: List a Safe -> a
sHead (Cons _ hd tl) = hd
sTail :: List a Safe -> ListUnsafe a
sTail (Cons _ hd tl) = L tl
sLast :: List a Safe -> a
-- from prelude
-- last [x] = x
---last (x : xs) = last xs
sLast = undefined
sInit :: List a Safe -> ListUnsafe a
sInit = undefined
-- Other standard operations that work for any list
sElem :: Eq b => b -> List b a -> Bool
sElem b (Cons _ x xs) = if b == x then True else sElem b xs
sElem b (Nil _) = False
sMap :: (b1 -> b2) -> List b1 a -> List b2 a
sMap = undefined
-- Doesn't quite work
-- sMap f (Nil p) = nil
-- sMap f (Cons p x xs) = (cons (f x) (sMap f xs))
sFilter :: (b -> Bool) -> List b a -> ListUnsafe b
sFilter f (Nil _) = L nil
sFilter f (Cons _ x xs) =
if f x then case (sFilter f xs) of
L l -> L (cons x l)
else sFilter f xs
sLength :: List b a -> Int
sLength (Nil _) = 0
sLength (Cons _ x xs) = 1 + sLength xs
-- what is type of (binary) concat??
sConcat :: List b a1 -> List b a2 -> ListUnsafe b
sConcat (Nil _) l = L l
sConcat (Cons _ x xs) l = case (sConcat xs l) of
L l -> L (cons x l)