Hellow,
My colleague asked me to give an example of the
continuation passing style
and demonstrate it in the form of Haskell program.
I had a naive idea that Haskell should understand any lambda-
expression. So I proposed the following example of the list length
function:
l = \xs c -> if null xs then 0 else 1+(c (tail xs) c)
lng xs = l xs l
But Haskell refused to find the type for `c'.
So there had arised a question of mere curiosity of how to make him
understand it.
We introduced data C a = C ([a] -> C a -> Int) ,
changed `lng' respecively to deal with this `C', and made `lng' work.
My questions, as the are summarized by
Yoshihiko Ichikawa ( [EMAIL PROTECTED] )
are the following.
1. Why the Haskell type system does not allow recursive type equation?
And, if so, what is the real hindrance, or what would happen if the
solver exists?
2. What is the relationship among the untyped lambda calculus,
the simply typed lambda calculus and the Haskell typing system?
Does the type system allows programmers to define a fixed point
combinator of type (a->a)->a without using recursive function
defintion?
3. If it is impossible, which kind of fixed point combinators
can be definable in Haskell?
Personanly, I am asking only the question (1).
For example, why Haskell cannot introduce this
data C a = C ([a] -> C a -> Int)
itself ?
For it manages to solve the recursive equations for the functions,
why cannot it solve types - in the simple cases ?
I do not agree to use the fix point combinator Y (fix) - unless we
express it as a pure lambda too in Haskell.
I failed to invent the acceptable type for Y - in the manner it was
done for `length' in Haskell.
Though I did not try much. Maybe it is impossible ?
Below follows certain discussion.
The Haskell list correspondents are invited with their comments.
Regards,
Sergey Mechveliani [EMAIL PROTECTED]
--------------------------------------------------------------------
--------------------------------------------------------------------
Yoshihiko Ichikawa ([EMAIL PROTECTED]) writes
I'm negative about the definability of Y in the Haskell type system,
altough I cannot prove it. (See appendix 3 for a problem raised by
assuming a general purpose recursive type solver).
<skipped ...>
Appendix 1.
Because of the morphism, Lambda =~= Lambda -> Lambda
the type of lambda terms should have types such as:
data Lambda = L (Lambda -> Lambda)
And the isomorphism between Lambda and Lambda -> Lambda are established
by the following two functions:
lambdaApp :: Lambda -> Lambda -> Lambda
lambdaApp (L x) y = x y
absLambda :: (Lambda -> Lambda) -> Lambda
absLambda fun = L fun
Intuitively, in Lisp, absLambda may correspond to #'(lambda ....) and,
lambdaApp may correspond to funcall.
Then, the rest of the constuction is very simple. Consider a definition
of the fixed point combinator (by Turing):
Y == ZZ, where Z == \zx.x(zzx)
First, zTuring is defined as follows:
zTuring :: Lambda
zTuring
= absLambda (\z ->
absLambda (\x -> lambdaApp x (lambdaApp (lambdaApp z z) x)))
So, yTuring can be defined simply apply zTuring to itself:
yTuring :: Lambda
yTuring = lambdaApp zTuring zTuring
There is no recursion here, and if you want, you can write down yTuring
without using function names.
...
How to play with the Lambda type.
The K operator defined as \xy.x is now:
kOp = absLambda (\x -> absLambda (\y -> x))
Consider the D-operator which have the following property:
Dxy0 = x
Dxyn = y, if n /= 0
where 0 and n are church numerals, \xy.y and \xy.x(x(....(xy))), respctively.
-----------
n times
By this setting, we can play a simple if-then-else game:
<skipped ...>
Arithmetic operations can also be defined using known operators.
I'm not testing the full properties of the above setting. So,
you might find more interesting style of the game.
...
And, writing a meaningful example using yTuring will be a hard work.
-------------------------------------------------------------------
-------------------------------------------------------------------
Sergey Mechveliani ([EMAIL PROTECTED]):
Thank you. I guess, this yTuring is what it is needed.
And let the data (lists and numbers) be reprersented as the lambda-s.
So all the type here are inhabited, are they ?
And what the Haskell people would say ?
-------------------------------------------------------------------
-------------------------------------------------------------------
Yoshihiko Ichikawa ([EMAIL PROTECTED]) :
Please notice that `error "something"' denotes a bottom.
Hence, even if some expression like yTuring can be defined in Haskell,
the expression at last may represent a bottom. The ``game'' I wrote
is played, just because `error ...' has a side-effect, i.e., printing a
message. For another example, there is `trace' in Glasgow Haskell.
The function is of type
_trace :: String -> a -> a
and, an expression,
let bottom = bottom
in trace "enter into a closure" bottom
denotes a bottom, but having the side-effect which prints a message.
So, even if you may define lamabda-terms, things would vanish
once you try to get represented values.
> And what the Haskell people would say ?
That's difficult to guess (^^;
