Thanks for your reply. I tried a few ways but none worked. One is like: shorter as bs = f id id as bs where f ca cb [] _ = ca [] f ca cb _ [] = cb [] f ca cb (a:as) (b:bs) = f (ca.(a:)) (cb.(b:)) as bs However this will result in a non-terminating loop for shorter [1..] [2..], since the first two patterns of f shall never match. Another way, I could guarantee that the evaluation of shorter [1..5] (shorter [1..] [2..]) terminate but I lose the information to figure out which list was the shortest one. Using zips: shorter = zipWith (\a b -> undefined) -- this returns the length, but not the content of the shorter list (\a b -> undefined) could be replaced with something that encode the contents of the two lists, but it makes no difference since I won't know which one is the answer. The difficulty is that I cannot have these both: A. if one list is finite, figure out the shorter one B. if both are infinite, returning an infinite list could work BTW, there IS an way to implement this functionality for a finite list of (possibly infinite) lists: shortest = measureWith [] where measureWith ruler as = f matches where ruler' = undefined : ruler matches = filter p as p a = length (zip ruler' a) == length (zip ruler a) f [] = measureWith ruler' as f matches = matches which somehow makes it unnecessary to find the function "shorter", but the original simple problem is interesting itself. Thanks. On 10/10/06, Neil Mitchell wrote:

Hi,

The trick is not call "length", since length demands the whole of a list, and won't terminate on an infinite list. You will want to recurse down the lists.

Is this a homework problem? It's best to declare if it is, and show what you've managed to do so far.

Thanks

Neil

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 wrote:

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

ihope wrote:

It's possible to make both "infinite list" and "finite list" datatypes:

data Inf a = InfCons a (Inf a) data Fin a = FinCons a !(Fin a) | FinNil

At least, I think the Fin type there has to be finite...

No, your Fin type can also hold infinite values. The strictness annotation on the (Fin a) component merely ensures that the tail exists to one constructor's depth (Head Normal Form). It does not force strictness all the way down (full Normal Form). Regards, Malcolm

On Wed, Oct 11, 2006 at 11:40:59AM +0100, Malcolm Wallace wrote:

To: haskell-cafe@haskell.org From: Malcolm Wallace Date: Wed, 11 Oct 2006 11:40:59 +0100 Subject: Re: [Haskell-cafe] beginner's problem about lists

ihope wrote:

...

It's possible to make both "infinite list" and "finite list" datatypes:

data Inf a = InfCons a (Inf a) data Fin a = FinCons a !(Fin a) | FinNil

At least, I think the Fin type there has to be finite...

No, your Fin type can also hold infinite values. The strictness annotation on the (Fin a) component merely ensures that the tail exists to one constructor's depth (Head Normal Form). It does not force strictness all the way down (full Normal Form).

let q = FinCons 3 q in case q of FinCons i _ -> i ==> _|_ does that contradict, or did i just not understand what you are saying? matthias

Malcolm Wallace wrote:

Matthias Fischmann wrote:

...

...

No, your Fin type can also hold infinite values.

let q = FinCons 3 q in case q of FinCons i _ -> i ==> _|_

does that contradict, or did i just not understand what you are saying?

That may be the result in ghc, but nhc98 gives the answer 3.

It is not entirely clear which implementation is correct. The Language Report has little enough to say about strict components of data structures - a single paragraph in 4.2.1. It defines them in terms of the strict application operator ($!), thus ultimately in terms of seq, and as far as I can see, nhc98 is perfectly compliant here.

The definition of seq is seq _|_ b = _|_ seq a b = b, if a/= _|_

In the circular expression let q = FinCons 3 q in q it is clear that the second component of the FinCons constructor is not _|_ (it has at least a FinCons constructor), and therefore it does not matter what its full unfolding is.

The translation given in the language report says this expression is equivalent to let q = (\x1 x2 -> (( FinCons' $ x1) $! x2) ) 3 q in q (where FinCons' is a "lazy" constructor) in terms of seq let q = (\x1 x2 -> x2 `seq` ( FinCons' x1 x2 ) ) 3 q in q this evaluates to let q = (q `seq` ( FinCons' 3) ) in q hence on top-level q is rather a seq-expression than a constructor-expression ;-) Regards, David

On Wed, Oct 11, 2006 at 11:04:49AM -0400, Robert Dockins wrote:

let q = seq q (FinCons 3 q) in q (beta)

We have (from section 6.2): seq _|_ y = _|_ seq x y = y iff x /= _|_

Now, here we have an interesting dilemma.

The meaning of a recursive definition is the least fixed point of the equation, in this case _|_. Same as let x = x in x.

For my own edification (experts: please remark if I stray from any conventional notions--be as picky as possible) and perhaps for anyone who didn't quite grok Ross Paterson's punchline, I'm going to try to answer the question "How does seq affect the definedness CPO?" At the heart of these two recursive definitions q = 3 : q (1) r = r `seq` (3 : r) (2) we find these two functions f and g f x = 3 : x g x = x `seq` (3 : x) such that q = lfp f r = lfp g This is the least fixed point approach to recursive definitions. (From Scott and Strachey? I'm not sure of the origins...) In the CPO of definedness, x < y means that "x is less-defined than y". Since _|_ is "undefined": forall x . _|_ <= x. For a more meaty case, consider l1 = Cons 3 Nil l2 = Cons 3 _|_ l2 > l1 because l1 is more defined. If values don't share the same structure, (a tree and a list for instance) I don't think their comparison is meaningful (experts?). The intuition behind the lfp as a definition principle is that of refinement/approximation. When constructing a value for the recursively definition, we begin with _|_ which represents no information. Finding the lfp of function means that we apply the function as many times as is necessary to define the value. Each application of the function refines the value a bit more until we have the sufficient approximation of the full value. What constitutes "sufficient" is determined by how the value is used: consider ((head . tail) q) versus (length q). Intuitively q = lfp f = f(f(f(f(f(f .... (f(f(f _|_)))...))))) (*) r = lfg g = g(g(g(g(g(g .... (g(g(g _|_)))...))))) (**) q is infinite 3s because f is non-strict. Operationaly, when f is applied to the thunk representing the final q value, it contributes the (3:) constructor to the definition of q, making q more defined. Note that it does not need to force the evaluation of q in order to make this contribution. Thus, the intuitive (f _|_) of (*) is never evaluated. r is _|_ because g is strict. When g is applied to the thunk representing the final q value, it forces its evaluation which operationaly leads us to g again being applied to the final q value thunk without making any contribution to the definition. Thus, the intuitive (g _|_) of (**) is always evaluated. Since g is strict, g _|_ = _|_ and this reduction trickles all the way out until r = _|_. As Robert Dockins showed, any recursive definition of a Fin value unfolds to an equation like (2) because of the strictness annotation in the datatype. We just discussed that the lfp semantics of an equation of (2)'s form will always result in _|_. On the other hand, any finite definition of a Fin value works fine. So ihope's Fin data type is either a finite list or _|_, as was purposed. Was that all square? Dotted i's and such? Nick On 10/11/06, Ross Paterson wrote:

On Wed, Oct 11, 2006 at 11:04:49AM -0400, Robert Dockins wrote:

...

let q = seq q (FinCons 3 q) in q (beta)

We have (from section 6.2): seq _|_ y = _|_ seq x y = y iff x /= _|_

Now, here we have an interesting dilemma.

The meaning of a recursive definition is the least fixed point of the equation, in this case _|_. Same as let x = x in x.

_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

Nicolas, I think you gave a fine explanation. Just a few minor remarks...

l1 = Cons 3 Nil l2 = Cons 3 _|_

l2 > l1 because l1 is more defined.

Surely you mean l2 < l1, then. Moreover, are you sure you need to define your order in such a way that l2 < l1. I'd say, for these purposes, it's enough to state that (<) = { (_|_, x) | x <- Whnf, x /= _|_ } . But maybe I'm overlooking something here... Cheers, Stefan

On Tue, Oct 10, 2006 at 08:58:05AM -0400, Lennart Augustsson wrote:

...

a function that takes two lists and decides whether one of them is finite or not , without being given further information on the lists, does not exist.

A function that takes two lists and decides if one is finite does indeed exist. But if both are infinite you'll get partial information out.

The example shorter [1..5] (shorter [2..] [3..]) is a little tricky, but certainly doable.

right, my implementation wouldn't cover this case. i was meaning termination, though: if a function accepts two possibly infinte lists, it cannot unconditionally return with the shorter one. i think the best you can do is Hennings solution (and mine, but i was too slow :) that hits bottom once you touch any element in (shorter [2..] [3..]), instead of merely the lengths of its prefices. matthias

On Tue, 10 Oct 2006, Henning Thielemann wrote:

On Tue, 10 Oct 2006 falseep@gmail.com wrote:

...

Hi all,

I'm trying to implement a function that returns the shorter one of two given lists, something like shorter :: [a] -> [a] -> [a] such that shorter [1..10] [1..5] returns [1..5], and it's okay for shorter [1..5] [2..6] to return either.

Simple, right?

However, it becomes difficult when dealing with infinite lists, for example, shorter [1..5] (shorter [2..] [3..]) Could this evaluate to [1..5]? I haven't found a proper implementation.

Again it's ok for shorter [2..] [3..] to return whatever that can solve the above problem correctly. An infinite list could work, I guess, but I don't know how.

With PeanoNumbers, http://darcs.haskell.org/htam/src/Number/PeanoNumber.hs I would first attach a lazy length information to each list before any call to 'shorter', then I would remove this information after the last call to 'shorter'.

Untested code follows:

attachLength :: [a] -> (PeanoNumber.T, [a]) attachLength xs = (genericLength xs, xs)

detachLength :: (PeanoNumber.T, [a]) -> [a] detachLength = snd

shorter :: (PeanoNumber.T, [a]) -> (PeanoNumber.T, [a]) -> (PeanoNumber.T, [a]) shorter (xl,xs) (yl,ys) = (min xl yl, if xl < yl then xs else ys)

Ah, here is a simpler solution: compareLength :: [a] -> [b] -> Ordering compareLength (_:xs) (_:ys) = compareLength xs ys compareLength [] [] = EQ compareLength (_:_) [] = GT compareLength [] (_:_) = LT shorter :: [a] -> [a] -> [a] shorter xs ys = let lt = compareLength xs ys == LT in zipWith (\x y -> if lt then x else y) xs ys zipWith returns the length of the shorter list lazily and the elements are chosen after the shortest list is determined.

Sorry, I realized that it does not cover the shorter [1..5] (shorter [2..] [3..]) case... Eugene Crosser wrote:

On Tue, 10 Oct 2006 falseep@gmail.com wrote:

...

Hi all, I'm trying to implement a function that returns the shorter one of two given lists, something like shorter :: [a] -> [a] -> [a] such that shorter [1..10] [1..5] returns [1..5], and it's okay for shorter [1..5] [2..6] to return either.

Simple, right?

I am still very much of a newbie myself, so sorry for possibly un-haskellish style and all, but this seems to work for me:

===== data WhichOne = SelUnknown | SelLeft | SelRight

shorter :: [a] -> [a] -> [a] shorter la lb = selectedof $ sorttuple (SelUnknown,la,lb)

selectedof :: (WhichOne,[a],[a]) -> [a] selectedof (SelLeft,la,lb) = la selectedof (SelRight,la,lb) = lb selectedof (_,la,lb) = error "selectedof unselected tuple"

sorttuple :: (WhichOne,[a],[a]) -> (WhichOne,[a],[a]) sorttuple (_,(a:xa),(b:xb)) = prefixt a b (sorttuple (SelUnknown,xa,xb)) sorttuple (_,[],[]) = (SelLeft,[],[]) sorttuple (_,(a:xa),[]) = (SelRight,(a:xa),[]) sorttuple (_,[],(b:xb)) = (SelLeft,[],(b:xb))

prefixt :: a -> a -> (WhichOne,[a],[a]) -> (WhichOne,[a],[a]) prefixt a b (w,la,lb) = (w,(a:la),(b:lb)) =====

What do you think?