[Haskell-cafe] Type-Marking finite/infinte lists?
David Menendez
zednenem at psualum.com
Sat Sep 15 16:27:37 EDT 2007
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/>
More information about the Haskell-Cafe
mailing list