I suppose using indicative types (dependent style) is out of the question? I presume i) that would over-simplify the problem and ii) we're tied to the [-] type. It deserves mention no less.
data Fin data Inf
data List l a = Cons a (List l a) | Nil
shorter :: List Inf a -> List Inf a -> List Inf a shorter :: List Fin a -> List Inf a -> List Fin a shorter :: List Inf a -> List Fin a -> List Fin a shorter :: List Fin a -> List Fin a -> List Fin a
where the result of the last typecase is the shorter one. shorter
would probably be defined in a type-class.
The normal un-typechecked code disclaimer applies.
Nick
On 10/10/06, Neil Mitchell
Hi
However this will result in a non-terminating loop for shorter [1..] [2..], since the first two patterns of f shall never match.
The specification of your problem makes this a guarantee. How do you know that a list is finite? You find the [] at the end. How do you know a list is infinite? You spend an infinite amount of time and never find the []. Hence you can't tell if you have two big lists, or two infinite lists.
Thanks
Neil _______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe