Python from Wise Guy's Viewpoint

Collapse
This topic is closed.
X
X
 
  • Time
  • Show
Clear All
new posts
  • Brian McNamara!

    Re: Python from Wise Guy's Viewpoint

    prunesquallor@c omcast.net once said:[color=blue]
    >gt5163b@prism. gatech.edu (Brian McNamara!) writes:[color=green]
    >> Well, in C++ you could say
    >>
    >> template <class F, class A>
    >> typename result_of<F(A)> ::type
    >> noisy_apply( const F& f, const A& a ) {
    >> cout << "I am now about to apply " << f << " to " << a << endl;
    >> return f(a);
    >> }
    >>[/color]
    >
    >I don't mean to nitpick, but APPLY takes an arbitrary list of arguments.
    >How do you parameterize over that without enumerating the power set
    >of potential types?[/color]

    This isn't really possible for normal C++ functions.

    You can always program in a style where every function takes exactly
    one argument, which is an N-ary tuple, and use boost::mpl and
    boost::tuple to then generalize things. (Indeed, using such libraries,
    you can simulate "apply" rather convincingly. But somewhere under the
    hood, someone has to have written N different overloads for 0-arg,
    1-arg, ... N-arg, up to some fixed ("large enough") N.)

    So C++ can only mimic "noisy_appl y" so well. I expect that Haskell can
    mimic it better in this respect.
    [color=blue]
    >What if F `returns' void?[/color]

    It still works. (You are allowed to say "return f(a)" inside a template
    function returning void, provided f(a) "returns" void as well.)

    --
    Brian M. McNamara lorgon@acm.org : I am a parsing fool!
    ** Reduce - Reuse - Recycle ** : (Where's my medication? ;) )

    Comment

    • prunesquallor@comcast.net

      Re: Python from Wise Guy's Viewpoint

      Pascal Costanza <costanza@web.d e> writes:
      [color=blue]
      > P.S., to Joe Marshall: I hope you don't mind that I hire and fire you
      > within a split second. ;-)[/color]

      I'm getting used to it.

      Comment

      • prunesquallor@comcast.net

        Re: Python from Wise Guy's Viewpoint

        Darius <ddarius@hotpop .com> writes:
        [color=blue]
        > On Sat, 25 Oct 2003 23:27:46 GMT
        > prunesquallor@c omcast.net wrote:
        >[color=green]
        >> 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.[/color]
        >
        > -- this is all sooo pointless in Haskell[/color]

        Well, yeah.
        [color=blue]
        > data LazyList a
        > = Nil
        > | Cons (forall r. ((a,() -> LazyList a) -> r) -> r)[/color]

        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?
        [color=blue]
        > I already have a bunch of Church encoded data structures as well if
        > that's next.[/color]

        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?


        Comment

        • prunesquallor@comcast.net

          Re: Python from Wise Guy's Viewpoint

          gt5163b@prism.g atech.edu (Brian McNamara!) writes:
          [color=blue]
          > prunesquallor@c omcast.net once said:[color=green]
          >>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.[/color]
          >
          > Laziness is pretty orthogonal to static typing.
          >
          > This one is so easy, we do it in C++ just for spite. :)
          > I'm using the FC++ library as a helper.
          >[/color]
          [snip]

          Yuck! Type declarations *everywhere*. Where's this famous inference?

          What's this LispCons type? I don't have that in my source. My code
          is built of lambda abstractions. I don't have a lispvalue type either.
          And it isn't limited to integers in the list. Where did my functions go?

          And how can you compare a LispCons to an integer?

          This works, but it doesn't faithfully represent what I wrote.
          In addition, with all the type decorations, it only serves to reinforce
          the idea the static type checking means a lot of extra keystrokes.


          Comment

          • Darius

            Re: Python from Wise Guy's Viewpoint

            On Sun, 26 Oct 2003 04:11:44 GMT
            prunesquallor@c omcast.net wrote:
            [color=blue]
            > Darius <ddarius@hotpop .com> writes:
            >[color=green]
            > > data LazyList a
            > > = Nil
            > > | Cons (forall r. ((a,() -> LazyList a) -> r) -> r)[/color]
            >
            > 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.[/color]

            This is a data declaration, -not- a type declaration. For example,
            Bool is data Bool = True | False and lists would be data [a] = [] | a
            :[a]. If I were to use Java would I not be allowed to use 'class'?
            class introduces a type too.

            Furthermore, 'data' doesn't just give you a type. It also gives you
            constructors, destructors (kind of), and recognition.

            data Either a b = Left a | Right b
            The idiomatic Lisp functions that would correspond to what this
            declaration provides would be something like: left, right, leftp,
            rightp, eitherp, get-left, get-right.

            Also, that type distinction let's me add LazyList to typeclasses like
            Show, Read, Eq, Ord, Monad, Num, etc. Perhaps, I don't like my lazy
            lists displaying as #<closure> or my trees as ((3 2) (4)) when what I'd
            want is((3 . (2 . ()) . (4 . ())). Perhaps, I don't want
            (equal<the lazy list 1 2 3> <the lazy list 1 2 3>) to return nil because
            they aren't the same procedure.

            Also, ignoring the testit function, my code with those four laborious
            "type annotations" is 16 lines compared to 29 lines of lisp. (Including
            it, it's still shorter.)

            If all you want to do is show an example in Lisp that won't type check
            in most statically typed language without any alterations you could
            simply write,(list t 3) or (if t 'a 10).

            Finally, I don't want to write some insane continuation passing
            sequence. I want the language to not overevaluate. I guess lazy Lisp or
            dynamic Haskell beats us both.

            Comment

            • Dirk Thierbach

              Re: Python from Wise Guy's Viewpoint

              Brian McNamara! <gt5163b@prism. gatech.edu> wrote:[color=blue]
              > prunesquallor@c omcast.net once said:[/color]
              [color=blue][color=green]
              >>(defun black-hole (x)
              >> #'black-hole)[/color][/color]
              [color=blue][color=green]
              >>(for non lispers, the funny #' is a namespace operator.
              >> The black-hole function gobbles an argument and returns
              >> the black-hole function.)[/color][/color]
              [color=blue]
              > Finally, an example that I don't think you can type in Haskell.[/color]

              It's a bit tricky. As Remi has shown, you need recursive types.
              Recursive types in Haskell always need an intervening data type
              constructor. That's a conscious design decision, because recursive
              types are very often a result of a real typing error. (IIRC, that's
              why OCaml added an option to enable recursive typing after having it
              enabled as default for some time, but Remi should know that better
              than I do.)

              We also need an existential type in this constructor, because the
              argument can be of different type for each application of the black hole.
              [color=blue]
              > data BlackHole = BH (forall a. a -> BlackHole)[/color]

              Now we can write the black hole function itself:
              [color=blue]
              > black_hole :: BlackHole
              > black_hole = BH (\_ -> black_hole)[/color]

              That's it. However, we cannot apply it directly. We have to "unfold"
              it explicitely by taking it out of the data constructor. We define an
              auxiliary infix function to take care of that.
              [color=blue]
              > infixl 0 $$[/color]
              [color=blue]
              > ($$) :: BlackHole -> a -> BlackHole
              > (BH f) $$ x = f x[/color]

              Now we can write a function like
              [color=blue]
              > f = black_hole $$ "12" $$ 5 $$ True[/color]

              which will nicely typecheck.

              That's the first time one actually has to add non-obvious stuff to
              "please" the type checker. OTOH, the black hole function is pretty
              bogus, so one can argue that this is a realistic price to pay to say
              that you really really want this strange function. I would be very
              surprised if this function is of any use in a real-world program.

              And there is nothing else you can do with arguments of arbitary type
              but silently discard them, so I guess there are not many other examples
              like this.

              - Dirk

              Comment

              • Dirk Thierbach

                Re: Python from Wise Guy's Viewpoint

                prunesquallor@c omcast.net wrote:[color=blue]
                > gt5163b@prism.g atech.edu (Brian McNamara!) writes:[/color]
                [color=blue][color=green]
                >> This one is so easy, we do it in C++ just for spite. :)
                >> I'm using the FC++ library as a helper.[/color][/color]
                [color=blue]
                > Yuck! Type declarations *everywhere*. Where's this famous inference?[/color]

                You *did* notice that it is C++, which hasn't type inference (and
                a lousy typesystem? :-) So what Brian is saying that this is so easy
                he can even to it with hands tied on his back and standing on his
                head.
                [color=blue]
                > In addition, with all the type decorations, it only serves to reinforce
                > the idea the static type checking means a lot of extra keystrokes.[/color]

                Yes. C++ and Java are to blame for that, and it's a completely
                justified obverservation. Static typechecking in C++ and Java just
                sucks, and gets in the way all the time. If I had the choice between one
                of them and a dynamically typed language, I would of course use the
                dynamically typed one.

                But there are other statically typechecked languages where you don't
                have this kind of trouble. I don't know if this thread turns out do to
                something useful for anyone, but if it does, I would hope it gets at
                least this idea across.

                - Dirk

                Comment

                • Dirk Thierbach

                  Re: Python from Wise Guy's Viewpoint

                  Brian McNamara! <gt5163b@prism. gatech.edu> wrote:[color=blue]
                  > Pascal Costanza <costanza@web.d e> once said:[color=green]
                  >>Brian McNamara! wrote:[/color][/color]
                  [color=blue]
                  > But I suppose you really want this example[/color]
                  [color=blue][color=green][color=darkred]
                  >>>(defun f (x)
                  >>> (unless (< x 200)
                  >>> (cerror "Type another number"
                  >>> "You have typed a wrong number")
                  >>> (f (read)))
                  >>> (* x 2))[/color][/color][/color]
                  [color=blue]
                  > statically typed, huh?[/color]

                  After quite some time, I think I have finally figured out what Pascal
                  meant with
                  [color=blue][color=green]
                  >> The type system might test too many cases.[/color][/color]

                  I have the impression that he is confusing dynamic type errors and
                  runtime errors. In Lisp and Smalltalk they are more or less the same,
                  and since dynamic type errors map to static type errors, he may think
                  by analogy that other runtime errors must necessarily also map to
                  compile errors somehow involved with static typing. Of course this is
                  nonsense; those two are completely different things. The "too many
                  cases" referred to some cases of runtime errors he didn't want to be
                  checked at compile time. As you cannot get "too many test cases" by
                  type annotations static typing (which was the context where he made
                  this comment), like you cannot get "too many test cases" by writing too
                  many of them by hand, I really had a hard time figuring this out.

                  To sum it up: Unit tests (some, not all!) correspond to type
                  annotations, static type checking is the same as running the test
                  suite, dynamic types correspond to data types, runtime errors
                  correspond to runtime errors (surprise :-).
                  [color=blue]
                  > Ok, I'll try. If I come up short, I expect it's because I'm fluent
                  > in neither Haskell nor Lisp, not because it can't be done.[/color]

                  You don't really need runtime errors for the above example,
                  but here's a similar version to yours that throws an error in
                  'cerror' to return to the toplevel. No Maybe types.

                  cerror :: String -> String -> IO a -> IO a
                  cerror optmsg errmsg cont = do
                  print errmsg
                  print ("1: " ++ optmsg)
                  print ("2: Fail")
                  s <- getLine
                  x <- readIO s
                  let choice 1 = cont
                  choice 2 = ioError (userError errmsg)
                  choice x

                  f :: Integer -> IO (Integer)
                  f x =
                  if (x < 200)
                  then return (x * 2)
                  else cerror
                  "Type another number"
                  "You have typed a wrong number"
                  (getLine >>= readIO >>= f)
                  [color=blue][color=green]
                  >> I don't want an "approximat ion of cerror". I want cerror![/color][/color]

                  And you got it, exactly as you wanted. Perfectly typeable.
                  (Please don't say now "but I want to use the Lisp code, and
                  it should run exactly as it is, without any changes in syntax").
                  You could even assign the very same types in Lisp if any of the
                  extensions of Lisp support that. (I didn't try.)

                  - Dirk

                  Comment

                  • Andreas Rossberg

                    Re: Python from Wise Guy's Viewpoint

                    "Matthew Danish" <mdanish@andrew .cmu.edu> wrote:[color=blue][color=green]
                    > > It is not, because Lisp hasn't been designed with types in mind. It is
                    > > pretty much folklore that retrofitting a type system onto an arbitrary
                    > > language will not work properly. For example, Lisp makes no distinction
                    > > between tuples and lists, which is crucial for type inference.[/color]
                    >
                    > Tell that to the hackers who worked on the "Python" compiler found in
                    > CMUCL, SBCL, and some others. It does extensive type inference for both
                    > efficiency and correctness. But it doesn't get in the way (except in
                    > certain rare cases), it just (noisely) informs you what it thinks.[/color]

                    Clarification: I was talking about strong typing, i.e. full and precise
                    inference. As I wrote in another posting, I don't believe in soft typing,
                    since it has exactly the weaknesses that seems to make proponents of dynamic
                    typing judge type systems having marginal utility: its only use is to flag
                    more or less trivial errors, and unreliable so.

                    I would be very, very surprised to see a strong type system put on top of an
                    untyped language successfully, i.e. without changing or restricting the
                    language severely.
                    [color=blue][color=green]
                    > > If you want to have extensible overloading then static types are the[/color][/color]
                    only[color=blue][color=green]
                    > > way I know for resolving it. Witness Haskell for example. It has a very
                    > > powerful overloading mechanism (for which the term 'overloading'[/color][/color]
                    actually is[color=blue][color=green]
                    > > an understatement) . It could not possibly work without static typing,[/color][/color]
                    which[color=blue][color=green]
                    > > is obvious from the fact that Haskell does not even have an untyped
                    > > semantics.[/color]
                    >
                    > Correction: it could not work without typing--dynamic typing does not
                    > imply a lack of typing. I could be wrong, but it seems you would rule
                    > out generic functions in the CLOS (and dynamic dispatch in general) with
                    > the above statement.[/color]

                    See my example below.
                    [color=blue][color=green]
                    > > Erasing type information from a program that uses type abstraction to
                    > > guarantee certain post conditions will invalidate those post conditions.[/color][/color]
                    So[color=blue][color=green]
                    > > you get a program with a different meaning. It expresses something
                    > > different, so the types it contained obviously had some expressive[/color][/color]
                    power.[color=blue]
                    >
                    > This doesn't sound right: erasing type information should not invalidate
                    > the post conditions; it should simply make it more difficult
                    > (impossible?) to check the validity of the post conditions.[/color]

                    It does, because it also invalidates the pre conditions, on which the post
                    conditions depend.
                    [color=blue]
                    > This program should still work, even if you fail to type-check it, if
                    > said type-checking would have passed successfully.[/color]

                    This is only a meaningful observation if you look at a closed program. If
                    you simply erase types from some given piece of code it may or may not
                    continue to work, depending on how friendly client code will act. In that
                    sense it definitely changes meaning. You had to protect against that using
                    other, incomparable features. So there is a difference in expressiveness.

                    And making modular composition more reliable is exactly the main point about
                    the expressiveness types add!
                    [color=blue][color=green]
                    > > Erasing type information from a program that uses overloading simply[/color][/color]
                    makes[color=blue][color=green]
                    > > it ambiguous, i.e. takes away any meaning at all. So the types[/color][/color]
                    definitely[color=blue][color=green]
                    > > expressed something relevant.[/color]
                    >
                    > This statement is irrelevant because dynamic typing does not eliminate
                    > type information.[/color]

                    Yes it does. With "dynamic typing" in all its incarnations I'm aware of type
                    infromation is always bound to values. Proper type systems are not
                    restricted to this, they can express free-standing or relational type
                    information.

                    As an example of the kind of "overloadin g" (or type dispatch, if you want)
                    you cannot express in dynamically typed lagnuages: in Haskell, you can
                    naturally define functions which are overloaded on their return type, i.e.
                    you don't need any value at all at runtime to do the "dispatch". For
                    example, consider an overloaded function fromString, that produces values of
                    potentially arbitrary types from strings.

                    - Andreas



                    Comment

                    • Lex Spoon

                      Re: Python from Wise Guy's Viewpoint

                      "Andreas Rossberg" <rossberg@ps.un i-sb.de> writes:[color=blue]
                      > Clarification: I was talking about strong typing, i.e. full and precise
                      > inference.[/color]

                      Please let us be careful with the terminology. Strong typing means
                      that type checking happens at some point, and that a type error is
                      never allowed to complete (and thus do something non-sensical).
                      Inference is a completely independent axis -- any type system may or
                      may not have type inference. If you happen to like strong
                      *dynamically* typed languages then it is extremely irritating when
                      people assume strong typing can only happen at compile time.

                      I don't know the exact word you are looking for, unfortunately.
                      "complete" doesn't seem right, because that seems to be a property of
                      an inferencer: an inferencer is complete if it finds a type assignment
                      for any program that can be type checked. "sound" doesn't seem right,
                      either. A sound type system produces *correct* types, but those types
                      may not be tight enough to predict an absence of type errors.

                      Maybe you should just say "static checking". People will assume you
                      probably mean that programs get rejected if they have type errors.


                      [color=blue]
                      > As an example of the kind of "overloadin g" (or type dispatch, if you want)
                      > you cannot express in dynamically typed lagnuages: in Haskell, you can
                      > naturally define functions which are overloaded on their return type, i.e.
                      > you don't need any value at all at runtime to do the "dispatch". For
                      > example, consider an overloaded function fromString, that produces values of
                      > potentially arbitrary types from strings.[/color]


                      You can do this kind of thing in dynamically typed languages, too,
                      though unfortunately it is not very common. Do a web search on
                      "object-oriented" and "roles" and a lot comes up. This is the same
                      thing: depending on the role that a requestor sees an object under,
                      the object can respond differently even to the same messages. For
                      example, someone may respond to #requestPurchas e differently depending
                      on whether the request treats them like a father or treats them like
                      the president of a company. And it works for functional languages,
                      too, as is clearly exhibited by your fromString() overloaded function.
                      It could be viewed as acting differently depending on whether it is in
                      an int-producer role or a float-producer role.


                      (Incidentally, a lot of the results that turn up regard languages for
                      databases. I was surprised at how much interesting language research
                      happens in the database world. They take the view that long-lived
                      data is important. This is common to Smalltalk people, and perhaps to
                      people who like Lisp machines, but even Scheme and Lisp people don't
                      seem to think a whole lot about this idea. Database people certainly
                      do, however. You can't just repopulate a database all the time!)

                      Anyway, depending on the role that the requestor is talking to, a
                      responder (be it a function or an object) can act differently. In
                      some cases, the expected role can be figured out automatically,
                      instead of needing to be written explicitly. This is somewhat similar
                      to the behavior of C++ when you invoke a non-virtual method: the type
                      of the *variable* decides what will happen.


                      Getting aside from theory and research, Matlab and Perl both allow
                      this kind of context sensitivity. When you call a Matlab function,
                      the function knows how many return values you are expecting. If you
                      call a function in Perl, it can tell whether you want a scalar or a
                      vector back, and it can act accordingly. (At least, the built-in Perl
                      functions can do this.)



                      -Lex

                      Comment

                      • Joachim Durchholz

                        Re: Python from Wise Guy's Viewpoint

                        prunesquallor@c omcast.net wrote:[color=blue]
                        >
                        > Yuck! Type declarations *everywhere*. Where's this famous inference?[/color]

                        Hey, what do you expect of C++ code?

                        No type declarations in Haskell.

                        Regards,
                        Jo

                        Comment

                        • Joachim Durchholz

                          Re: What static typing makes difficult

                          David Mertz wrote:[color=blue]
                          > I would challenge any enthusiast of Haskell, SML, Mozart, Clean, or the
                          > like to come up with something similarly direct.[/color]

                          Take Mozart out: it uses run-time typing.

                          Regards,
                          Jo

                          Comment

                          • Pascal Costanza

                            Re: Python from Wise Guy's Viewpoint

                            Dirk Thierbach wrote:
                            [color=blue]
                            > Brian McNamara! <gt5163b@prism. gatech.edu> wrote:
                            >[color=green]
                            >>Pascal Costanza <costanza@web.d e> once said:
                            >>[color=darkred]
                            >>>Brian McNamara! wrote:[/color][/color]
                            >
                            >[color=green]
                            >>But I suppose you really want this example[/color]
                            >
                            >[color=green][color=darkred]
                            >>>>(defun f (x)
                            >>>> (unless (< x 200)
                            >>>> (cerror "Type another number"
                            >>>> "You have typed a wrong number")
                            >>>> (f (read)))
                            >>>> (* x 2))[/color][/color]
                            >
                            >[color=green]
                            >>statically typed, huh?[/color][/color]

                            Sidenote: The code above has a bug. Here is the correct version:

                            (defun f (x)
                            (if (< x 200)
                            (* x 2)
                            (progn
                            (cerror "Type another number"
                            "You have typed a wrong number")
                            (print '>)
                            (f (read)))))

                            (Noone spotted this bug before. All transliteration s I have seen so far
                            have silently corrected this bug. It is interesting to note that it
                            probably weren't the type systems that corrected it.)
                            [color=blue]
                            > After quite some time, I think I have finally figured out what Pascal
                            > meant with
                            >
                            >[color=green][color=darkred]
                            >>>The type system might test too many cases.[/color][/color]
                            >
                            >
                            > I have the impression that he is confusing dynamic type errors and
                            > runtime errors. In Lisp and Smalltalk they are more or less the same,
                            > and since dynamic type errors map to static type errors, he may think
                            > by analogy that other runtime errors must necessarily also map to
                            > compile errors somehow involved with static typing. Of course this is
                            > nonsense; those two are completely different things. The "too many
                            > cases" referred to some cases of runtime errors he didn't want to be
                            > checked at compile time. As you cannot get "too many test cases" by
                            > type annotations static typing (which was the context where he made
                            > this comment), like you cannot get "too many test cases" by writing too
                            > many of them by hand, I really had a hard time figuring this out.[/color]

                            I think you have a restricted view of what "type" means. Here is the
                            same program written in a "type-friendly" way. (Again, in standard ANSI
                            Common Lisp. Note that the type is defined inside of f and not visible
                            to the outside.)

                            (defun f (x)
                            (check-type x (real * 200))
                            (* x 2))

                            CL-USER 1 > (f 5)
                            10

                            CL-USER 2 > (f 666)

                            Error: The value 666 of X is not of type (REAL * 200).
                            1 (continue) Supply a new value of X.
                            2 (abort) Return to level 0.
                            3 Return to top loop level 0.

                            Type :b for backtrace, :c <option number> to proceed, or :? for other
                            options

                            CL-USER 3 : 1 > :c 1

                            Enter a form to be evaluated: 66
                            132
                            [color=blue][color=green]
                            >>Ok, I'll try. If I come up short, I expect it's because I'm fluent
                            >>in neither Haskell nor Lisp, not because it can't be done.[/color]
                            >
                            >
                            > You don't really need runtime errors for the above example,
                            > but here's a similar version to yours that throws an error in
                            > 'cerror' to return to the toplevel. No Maybe types.
                            >
                            > cerror :: String -> String -> IO a -> IO a
                            > cerror optmsg errmsg cont = do
                            > print errmsg
                            > print ("1: " ++ optmsg)
                            > print ("2: Fail")
                            > s <- getLine
                            > x <- readIO s
                            > let choice 1 = cont
                            > choice 2 = ioError (userError errmsg)
                            > choice x
                            >
                            > f :: Integer -> IO (Integer)
                            > f x =
                            > if (x < 200)
                            > then return (x * 2)
                            > else cerror
                            > "Type another number"
                            > "You have typed a wrong number"
                            > (getLine >>= readIO >>= f)
                            >
                            >[color=green][color=darkred]
                            >>>I don't want an "approximat ion of cerror". I want cerror![/color][/color]
                            >
                            >
                            > And you got it, exactly as you wanted. Perfectly typeable.[/color]

                            Nice.
                            [color=blue]
                            > (Please don't say now "but I want to use the Lisp code, and
                            > it should run exactly as it is, without any changes in syntax").[/color]

                            No, I don't care about syntax.

                            You have used CPS - that's a nice solution. However, you obviously
                            needed to make the type declaration for f :: Integer -> IO (Integer)

                            Note that my code is not restricted to integers. (But I don't know
                            whether this is actually a serious restriction in Haskell. I am not a
                            Haskell programmer.)
                            [color=blue]
                            > You could even assign the very same types in Lisp if any of the
                            > extensions of Lisp support that. (I didn't try.)[/color]

                            What you actually did is: you have assigned a "broad" type statically,
                            and then you revert to a manual dynamic check to make the fine-grained
                            distinction.

                            In both Lisp versions, you have exactly one place where you check the
                            (single) type. A static type system cannot provide this kind of
                            granularity. It has to make more or less distinctions.


                            I regard the distinction between dynamic type errors and runtime errors
                            to be an artificial one, and in fact a red herring. I would rather call
                            the former type _exceptions_. Exceptions are situations that occur at
                            runtime and that I have a chance to control and correct in one way or
                            the other. Errors are beyond control.

                            This might be terminological nitpicking, but I think it is a serious
                            confusion, and it probably stems from weakly typed languages that allow
                            for arbitrary memory access and jumps to arbitrary machine addresses.
                            The niche in which such languages are still useful is getting smaller by
                            the time. (Languages like Java, Python, Ruby, etc., did a fine job in
                            this regard, i.e. to promote writing safe programs, rather than using
                            languages for high-level purposes that are actually designed for writing
                            hardware drivers.)

                            Anything below real runtime errors (core dumps) has the chance to be
                            controlled and corrected at runtime. (Including endless loops - they
                            should never be unbreakable in the first place.)

                            This can give you a real advantage for long-running systems or for very
                            large applications that you don't want to, or cannot stop and restart on
                            a regular basis.

                            Both (correct) code snippets I have provided are considerably smaller
                            than your solution and both are more general. And my second solution
                            still provides a way to correct a wrong parameter at runtime at no
                            additional cost. I regard this a feature, not a problem.

                            Assume that you need to write a program that has only vague
                            specifications and requires a high level of such flexibility in its
                            specs. _I_ would fire the programmer who would insist to use a language
                            that requires him to program all this flexibility by hand, and
                            especially wants to see a specification for "unforeseen problems",
                            whether formal or not.

                            See http://www.dilbert.com/comics/dilber...-20031025.html ;)


                            Pascal

                            P.S.: Please always remember the original setting of this thread. The
                            original original questions was something along the lines of "why on
                            earth would one not want a static type system?" I don't want to prove
                            the general superiority of dynamic type checking over static type
                            checking. Heck, there isn't even a general superiority of typing over
                            no-typing-at-all. All these approaches have their respective advantages
                            and disadvantages, and should be used in the right circumstances.

                            Yes, you can clearly tell from my postings that I prefer dynamic typing
                            over static typing. This in turn means that I am probbaly not a good fit
                            for projects that require a strong static approach. And everyone who
                            prefers static typing is probably not a good fit for projects that
                            require a strong dynamic approach. So what? All of us who participate in
                            this discussion are probably not good fits for writing hardware drivers.
                            ;)

                            Everyone should do what they are best at, and everyone should use the
                            tools that fit their style most.

                            But why on earth should anyone want to prove that their own preferred
                            _personal_ style is generally superior to all others?



                            "If I have seen farther than others, it is because I was
                            standing on the shoulder of giants."

                            --- Isaac Newton


                            "In computer science, we stand on each other's feet."

                            --- Brian K. Reed


                            P.P.S.: And I still think that soft typing is the best compromise. It's
                            the only approach I know of that has the potential to switch styles
                            during the course without the need to completely start from scratch.

                            Comment

                            • Dirk Thierbach

                              Re: Python from Wise Guy's Viewpoint

                              Pascal Costanza <costanza@web.d e> wrote:[color=blue]
                              > Dirk Thierbach wrote:[/color]
                              [color=blue]
                              > Sidenote: The code above has a bug. Here is the correct version:
                              >
                              > (defun f (x)
                              > (if (< x 200)
                              > (* x 2)
                              > (progn
                              > (cerror "Type another number"
                              > "You have typed a wrong number")
                              > (print '>)
                              > (f (read)))))
                              >
                              > (Noone spotted this bug before. All transliteration s I have seen so far
                              > have silently corrected this bug.[/color]

                              Because all people who did transliteration s guessed what the program
                              does, instead of testing it directly. I don't have a Lisp system here,
                              so I couldn't try it out.
                              [color=blue]
                              > It is interesting to note that it probably weren't the type systems
                              > that corrected it.)[/color]

                              While doing the transliteration , I actually had quite a few attempts
                              that didn't work, and all of them had type errors. Once the typing
                              was right, everything worked. (And I had to put the continuation in,
                              because, as I said, non-local control transfers don't translate
                              one-to-one.)
                              [color=blue][color=green][color=darkred]
                              >>>>The type system might test too many cases.[/color][/color][/color]
                              [color=blue]
                              > I think you have a restricted view of what "type" means.[/color]

                              Maybe. It sure would help if you'd tell me your view instead of having
                              me guess :-) For me, a type is a certain class of values, and a static
                              type is given by a limited language describing such classes. A
                              dynamic type is a tag that is associated with a value. Arbitrary
                              classes of values (like "all reals less than 200") are not a type.
                              [color=blue]
                              > Here is the same program written in a "type-friendly" way.[/color]

                              I'm not sure what's "type-friendly" about it. It uses a dynamic check
                              with a mix of dynamic type checking and value checking, yes. (I guess
                              "(real * 200)" means "a real number below 200", does it?)
                              [color=blue]
                              > (Again, in standard ANSI Common Lisp. Note that the type is defined
                              > inside of f and not visible to the outside.)[/color]

                              You do not define any type, you do a dynamic check.
                              [color=blue]
                              > (defun f (x)
                              > (check-type x (real * 200))
                              > (* x 2))[/color]

                              [...][color=blue]
                              > You have used CPS - that's a nice solution. However, you obviously
                              > needed to make the type declaration for f :: Integer -> IO (Integer)[/color]

                              In this case, you're right, but I am not sure if you know the reason
                              for it :-) (I usually make type annotations for the same reason you
                              write unit tests, i.e. almost everwhere unless the function is
                              trivial) So why do I have to make it here? Is the type annotation for
                              cerror also necessary?
                              [color=blue]
                              > What you actually did is: you have assigned a "broad" type statically,
                              > and then you revert to a manual dynamic check to make the fine-grained
                              > distinction.[/color]

                              If you mean by "broad" type the static integer type, yes. I have to
                              assign some type. If I don't want to restrict it to integers, I assign
                              a more general type (like the Number type I used in the other example).

                              Dynamic type checks either can be dropped because static type
                              checking makes them unnecessary, or they translate to similar dynamic
                              checks in the other language.

                              Since you cannot statically verify that a user-supplied value is less
                              than 200, this check becomes a dynamic check (what else should it
                              translate to?)
                              [color=blue]
                              > In both Lisp versions, you have exactly one place where you check the
                              > (single) type.[/color]

                              You have one place where you do the dynamic check, I have one place where
                              I do the dynamic check. The static type is only there because there
                              has to be a type. It really doesn't matter which one I use statically.
                              The static type check does not play any role for the dynamic check.
                              [color=blue]
                              > A static type system cannot provide this kind of granularity.[/color]

                              I am sorry, but this is nonsense (and it isn't really useful either).

                              This is like saying "I don't write unit tests in Lisp, because I have
                              a single place inside my program where I can check everything that
                              can go wrong."
                              [color=blue]
                              > I regard the distinction between dynamic type errors and runtime errors
                              > to be an artificial one, and in fact a red herring. I would rather call
                              > the former type _exceptions_.[/color]

                              Fine with me. I would go further and say that without dynamic
                              type checking, there are in fact only exceptions.
                              [color=blue]
                              > Both (correct) code snippets I have provided are considerably smaller
                              > than your solution and both are more general. And my second solution
                              > still provides a way to correct a wrong parameter at runtime at no
                              > additional cost. I regard this a feature, not a problem.[/color]

                              I would debate both points, but this is about static typing, not about
                              comparisons a la "in my language I can write programs that are
                              two lines shorter than yours."
                              [color=blue]
                              > P.S.: Please always remember the original setting of this thread. The
                              > original original questions was something along the lines of "why on
                              > earth would one not want a static type system?"[/color]

                              The answer to this is of course "You use what you like best. End of
                              story."

                              What I wanted to do was to show that the claim "There are things that
                              are easy to do in a dynamically typed language, but one cannot do them
                              conveniently in a statically typed language, because they won't
                              typecheck. Hence, statically typed languages are less expressive" is
                              wrong in all but very very rare situations. Of course the amount of
                              convenience with which you can do something varies from language to
                              language, and with the available libraries, but static typing (if done
                              properly) is never a show-stopper.
                              [color=blue]
                              > Yes, you can clearly tell from my postings that I prefer dynamic typing
                              > over static typing.[/color]

                              And that's fine with me. What I am a bit allergic to is making
                              unjustified general claims about static typing (or any other things,
                              for that matter) that are just not true.
                              [color=blue]
                              > But why on earth should anyone want to prove that their own preferred
                              > _personal_ style is generally superior to all others?[/color]

                              I don't know. As far as I am concerned, this thread was never about
                              "superiorit y", and I said so several times.

                              - Dirk

                              Comment

                              • Don Geddis

                                Re: Python from Wise Guy's Viewpoint

                                > prunesquallor@c omcast.net reasonably noted:[color=blue][color=green]
                                > > If there are three values that can arise --- provable-mismatch,
                                > > provable-non-mismatch, and undecided --- then you cannot assume that
                                > > ~provable-mismatch = provable-non-mismatch.[/color][/color]

                                Dirk Thierbach <dthierbach@gmx .de> writes:[color=blue]
                                > Hindley-Milner type inference always terminates. The result is either
                                > a provable mismatch, or a provable-non-mismatch.[/color]

                                You're completely wrong, which can be easily demonstrated.

                                The fact that it terminates isn't the interesting part. Any inference
                                procedure can also "always terminate" simply by having a timeout, and reporting
                                "no proof" if it can't find one in time.

                                So what's interesting is whether the conclusions are correct.

                                Let's take as our ideal what a dynamic type system (say, a program in Lisp)
                                would report upon executing the program. The question is, can your type
                                inference system make exactly the same conclusions at compile time, and predict
                                all (and only!) the type errors that the dynamic type system would report at
                                run time?

                                The answer is no.
                                [color=blue]
                                > A provable mismatch means that there is an execution branch that will crash
                                > if you ever get there. If for some reason this branch will never get
                                > executed, either because it's (non-provably) dead code[/color]

                                That's one obvious case, so even you know that your claim of a "provable
                                mismatch" is incorrect. There are programs that will never have run-time
                                errors, but your static type inference will claim a type error.
                                [color=blue]
                                > or because you have an implicit restriction for possible arguments to this
                                > expression the type system doesn't know about, than you could call it a
                                > "valid program", but it will still be rejected, yes.[/color]

                                So haven't you just contradicted yourself? Perhaps you think this "implicit
                                restriction" is unfair, because you've kept information from the system.
                                But the real problem is that all the information might be there, but the
                                system isn't capable of making sufficient inferences to figure it out.

                                For example:
                                (defun foo (x)
                                (check-type x (integer 0 10))
                                (+ 1 x) )
                                (defun fib (n)
                                (check-type n (integer 0 *))
                                (if (< n 2)
                                1
                                (+ (fib (- n 1)) (fib (- n 2))) ))
                                (print (foo (fib 5)))

                                This program prints "9", and causes no run-time type errors. Will it be
                                successfully type-checked at compile time by a static system? Almost certainly
                                the answer is no.

                                In case the code isn't clear; FOO is a function that increments a number by
                                one. Its domain is [0,10], and its range is [1,11]. FIB is the Fibonacci
                                sequence, with domain [0,infinity] and range [1,infinity].

                                Are you allowed to call FOO with the output of FIB? In general, no, because
                                the range of FIB is much greater than the domain of FOO.

                                However, in the particular case of the particular code in this program, it
                                turns out that only (FIB 5) is called, which happens to compute to 8, well
                                within the domain of FOO. Hence, no run-time type error. Unfortunately, the
                                only way to figure this out is to actually compute the fifth Fibonacci number,
                                which surely no static type inference system is going to do. (And if you do
                                happen to find one, I'm sure I can come up with a version of the halting
                                problem that will break that system too.)

                                Do you now accept that your static type inference systems do NOT partition
                                all programs into "either a provable [type] mismatch, or a provable [type]
                                non-mismatch"?

                                Finally, to get back to the point of the dynamic typing fans: realizing that
                                type inference is not perfect, we're annoyed to be restricted to writing only
                                programs that can be successfully type checked at compile time. Nobody
                                objects to doing compile-time type inference (e.g. as the CMUCL compiler for
                                Common Lisp does) -- especially just to generate warnings -- but many people
                                object to refusing to compile programs that can not be proven type-safe at
                                compile time (by your limited type inference systems).

                                -- Don
                                _______________ _______________ _______________ _______________ _______________ ____
                                Don Geddis http://don.geddis.org/ don@geddis.org

                                Comment

                                Working...