On 9/15/07, Joachim Breitner <[EMAIL PROTECTED]> wrote: > today while mowing the lawn, I thought how to statically prevent some > problems with infinte lists. I was wondering if it is possible to > somehow mark a list as one of finite/infinite/unknown and to mark > list-processing functions as whether they can handle infinte lists.
One possibility would be to have some phantom markers in the list type. For example, newtype List isEmpty isFinite a = MarkList [a] data Finite data Infinite data Empty data Nonempty data Unknown This is possibly non-optimal, since emptiness and finiteness are semi-related. Specifically: emptyIsFinite :: List Empty f a -> List Empty Finite a infiniteIsNonempty :: List e Infinite a -> List Nonempty Infinite a You can test whether a list is (non)empty, but not whether it's (in)finite. nonEmpty :: List e f a -> Maybe (List Nonempty f a) Aside from unfoldr, most operations that create lists are explicit about whether the result is finite. Then you can mark the properties of the common operations. nil :: List Empty Finite a cons :: a -> List e f a -> List Nonempty f a repeat :: a -> List Nonempty Infinite a tail :: List Nonempty f a -> List Unknown f a last :: List Nonempty Finite a -> a map :: (a -> b) -> List e f a -> List e f b filter :: (a -> Bool) -> List e f a -> List Unknown f a foldl :: (a -> b -> b) -> b -> List e Finite a -> b length :: List e Finite a -> Int unfoldr :: (a -> Maybe (b,a)) -> a -> List Unknown Unknown b Note the type of "infiniteIsNonempty . tail". As a variation, we can use rank-2 types instead of Unknown; e.g. tail :: List Nonempty f a -> (forall e. List e f a -> w) -> w filter :: (a -> Bool) -> List e f a -> (forall e. List e f a -> w) -> w The most general form of (++) would require either fundeps or type families: (++) :: List e1 f1 a -> List e2 f2 a -> List (BothEmpty e1 e2) (BothFinite f1 f2) a type instance BothEmpty Empty Empty = Empty type instance BothEmpty Empty Unknown = Unknown type instance BothEmpty Empty Nonempty = Nonempty type instance BothEmpty Nonempty Unknown = Nonempty etc. -- Dave Menendez <[EMAIL PROTECTED]> <http://www.eyrie.org/~zednenem/> _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe