Python from Wise Guy's Viewpoint

[prunesquallor at comcast.net]

Darius <ddarius at hotpop.com> writes:

> On Sat, 25 Oct 2003 23:27:46 GMT
> prunesquallor at comcast.net wrote:
>
>> I think I have a stumper.  I'll be impressed if a type checker can
>> validate this.  The same-fringe function takes a pair of arbitrary
>> trees and lazily determines if they have the same leaf elements in the
>> same order.  Computation stops as soon as a difference is found so
>> that if one of the trees is infinite, it won't cause divergence.
>
> -- this is all sooo pointless in Haskell

Well, yeah.

> data LazyList a
>   = Nil 
>   | Cons (forall r. ((a,() -> LazyList a) -> r) -> r)

I specifically didn't define the LazyList type.  I don't want to write
type annotations.  I want the type inference engine to deduce them.

I should have been more specific: I *know* that all these things can
be done in a statically typed language.  What I don't know is whether
these can be done as *easily*.  Will this type check without giving
the type checker hints about the type of 
(lambda (x y) (lambda (z) (z x y)))?  Will it type check if you
don't tell it that the `cons' in lazySequence is the same `cons'
in lazySame and lazyFringe?  

> I already have a bunch of Church encoded data structures as well if
> that's next.

I'm not just trying to come up with convoluted examples for the sake
of quizzing you.  I'm trying to find the point where the type checker
gets confused.  I'm not writing it in Haskell because I don't know
Haskell, so I'm writing in Lisp.  It will always be possible to
*recast* the problem in your favorite language, but can you
transliterate it and let the type checker infer that the program is
correct?