[Haskell-cafe] Type-Marking finite/infinte lists?

[David Menendez]

On 9/15/07, Joachim Breitner <mail at joachim-breitner.de> 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 <dave at zednenem.com>
<http://www.eyrie.org/~zednenem/>