In message <[EMAIL PROTECTED]:, S.D.Mechveliani writes:
:
: I tried to find out how Haskell understands the "lambda" programming.
: Here is the script for the length of a list.
: This is the so-called continuation passing stile, I believe.
:
: lng :: [a] -> Int
:
: lng = (\ xs ->
: ( (\xs c -> if null xs then 0 else 1+(c (tail xs) c) )
: xs
: (\xs c -> if null xs then 0 else 1+(c (tail xs) c) )
: )
: )
:
: This script is remarkable for it expresses the recursion and still
: does not contain the calls for the function names (we might avoid
: (+) too).
...
: But Haskell fails to find the type of the variable c.
...
: 1) Is it a principal feature that Haskell cannot derive this type for
: `c' ?
The type system prohibits self-application or the like, since it
cannot solve a type equation like this
me = [arg] -> me -> Int
The answer might have an infinite type. Hence, the fixed point combinator,
Y, cannot be defined in its lambda abstraction form:
\h.h(\x.h(xx))(\x.h(xx))
though they can be defined as follows
> fix :: (a -> a) -> a
> fix f = f (fix f)
Or, if you prefer continuation passing style, you may use restricted version
> fix' :: (a -> (a -> b) -> b) -> (a -> b)
> fix' c x = c x (fix' c) -- = fix (\r x -> c x r)
These can be defined, as the language internal implicitly or explicitly
utilizes the combinator to implement recursive functions.
: I was able to find it myself only by introducing the new data
: constructor and changing the script:
:
: data C a = C ([a] -> C a -> Int)
: ---
: lng xs =
: (\ xs (C c)-> if null xs then 0 else 1+(c (tail xs) (C c)))
: xs
: (C (\ xs (C c)-> if null xs then 0 else 1+(c (tail xs) (C c))) )
...
: 2) Is it necessary to introduce a new constructor to express recursion
: via continuation in the above task ?
Yes, if you want to pass `myself' to `my continuation'. However, if
you don't mind using fixed point combinators (even though they must be
defined through recursive definitions), you can write the function thus
> lng xs = fix (\f xs -> if null xs then 0 else 1 + f (tail xs)) xs
or
> lng xs = fix' (\xs c -> if null xs then 0 else 1 + c (tail xs)) xs
Fix and fix' pass `fixed point of myself' to `myself' as required.
# Sorry, my comments include misunderstanding. I also would like to
# hear from theoreticians.
Hope this helps.
----
Yoshihiko Ichikawa, Research Associate
Dept of Info Sci, Fac of Sci, Ochanomizu University
Phone: +81-3-5978-5388
Fax: +81-3-5978-5898
E-mail: [EMAIL PROTECTED]
