librelist archives

« back to archive

Static typing

Static typing

From:
Ramakrishnan Muthukrishnan
Date:
2014-01-16 @ 14:14
I know this group need not be sold on static typing, but if you want to
convince someone and want some good arguments, watch this video:

This video from the NYC Haskell group, there are other videos from their
group meetings as well on Vimeo.

 <http://vimeo.com/72870631>

Re: [bangalorehaskell] Static typing

From:
Pradip Caulagi
Date:
2014-01-16 @ 18:08
On Thursday 16 January 2014 07:44 PM, Ramakrishnan Muthukrishnan wrote:
> I know this group need not be sold on static typing, but if you want to
> convince someone and want some good arguments, watch this video:
>
> This video from the NYC Haskell group, there are other videos from their
> group meetings as well on Vimeo.
>
>   <http://vimeo.com/72870631>

I have watched about half of it.

So is it correct to say that it is easier to prove a program is correct 
in a statically typed language (like Haskell) than a dynamically typed 
language (like Clojure)?

If this is correct, my contention is - it doesn't follow that it is 
easier to write correct programs.

-- 
Pradip P Caulagi
http://caulagi.com

Re: [bangalorehaskell] Static typing

From:
Pradip Caulagi
Date:
2014-01-17 @ 03:54
On Friday 17 January 2014 08:19 AM, Ramakrishnan Muthukrishnan wrote:
> Pradip Caulagi <caulagi@gmail.com> writes:
>
> Statically typed languages gives some guarantees at *compile time* on
> the types. Types are an *invariant* of a program. For example if you
> declare a function foo like this:
>
> foo :: String -> IO ()
>
> then it is guaranteed that there it takes a String and does some
> IO. Types does not say anything else about the program. So, I guess
> it depends what you mean by "correctness".
>
>> If this is correct, my contention is - it doesn't follow that it is
>> easier to write correct programs.
>
> I didn't quite follow that. Can you elaborate?

Consider the example of date arithmetic.  So adding 1 to 31 Jan gives 1 
Feb.  Adding 1 to 28 Feb gives 1 Mar for a non-leap year but 29 Feb for 
a leap year.

A correct program would be one that solves all these cases. Brian Hurt 
defines this as 'working solution'.

So my question is - how will the type system allow us to write 
'correct/working' solutions faster?  My contention is that, with a type 
system, we can only reason about the correctness (to some extent).

As you probably guessed, I just don't grok the point of static typing.

--
Pradip P Caulagi

Re: [bangalorehaskell] Static typing

From:
Ashok Gautham
Date:
2014-01-17 @ 22:11
**NOTE** I did not completely grok who said what in the conversation I
  have added towards the end of this mail (Intentional top-post). But
  here is my 2-cents on why I consider static typing STRICTLY SUPERIOR
  to dynamic typing.


# Static Typing helps you not waste time

Some may consider adding type annotations everywhere a waste of time
and effort. This is not very true in Haskell since the type inference
engine is magical. Still, even in cases where you need to annotate
types everywhere, "strong" static typing is better than "strong"
dynamic typing.

A colleague from work was working on this machine-learning application
in Python. Since the thing was supposed to run on terabytes of data,
his group diligently tested every function in the program. In a
fleeting moment of stupidity, the said colleague added this line to
his code just before starting the full run (that in general runs for 3
days).

    # a large chunk of code that runs for a long long time
    fileName = '/home/ibm1/ICML/dumps/relationships.dat'
    f = open(fileName, 'w')

    print("Going to dump to " + f)

    f.write(what_he_computed_for_3_days)

And as luck would have it, 3 days later, he got the following message
that made him want to cry

    TypeError: Can't convert '_io.TextIOWrapper' object to str
    implicitly

Now, you may say that it was his fault and that he had no business
touching the code after testing and before deployment. But seriously,
was it worth the group missing their paper deadline and 3 days of
their lives?

Now, this is what you would have done in a Haskell-flavoured Python

    fileName :: String -- Automatically inferred
    open :: String -> String -> Handle -- From libraries
    (+) :: String -> String -> String -- Automatically inferred
    print :: String -> IO ()

The compiler would immediately have cried out

    Hey, you are trying to pass a Handle where a String was expected
    in the second argument to (+)

And they could have changed it to `fileName` and lived happily ever
after.

But, but... this is a solved problem - Use unit-tests, the dynamic
typing aficionados bellow. But no, it only takes us to the next point

# Static typing makes testing easier

Given `k` conditional statements in the program, the number of testing
paths that you need to check is the cyclomatic complexity of its
control-flow graph. Conservatively, if you add one more conditional
statement, the number of test-cases needed to cover all code paths can
double.

In a dynamic language, unit-testing still does not guarantee stitching
the units properly for you. The `(+)` function works correctly. The
`open` function works correctly. But their combination does not.

If you use strong types correctly, the compiler will ensure that a
large class of bugs that ensue from stitching the individual functions
together no longer exist.

Further, libraries [QuickCheck][1] greatly benefit from the typing
information available to quickly generate tonnes of test-cases for
you. 

# Static Typing helps you use libraries better

Python libraries are a disaster. From time to time, I do a
`help(someLib.someFunc)` and get the following *useful* message
    someLib.someFunc(a,b)
        ...

OK. How do I know what I am supposed to pass as arguments `a` and `b`?

Let me stop picking on Python. Clojure is my new bunny.

    # lein repl
 
    user=> (doc some)
    -------------------------
    clojure.core/some
    ([pred coll])
      Returns the first logical true value of (pred x) for any x in coll,
      else nil.  One common idiom is to use a set as pred, for example
      this will return :fred if :fred is in the sequence, otherwise nil:
      (some #{:fred} coll)

    
    user=> (doc filter)
    -------------------------
    clojure.core/filter
    ([pred coll])
      Returns a lazy sequence of the items in coll for which
      (pred item) returns true. pred must be free of side-effects.

Now, clearly the standard-library doc-strings are good, which may not
be the case with other libraries. Even in this case, however, can you
tell me anything about the function `pred` quickly? The documentation
in `filter` tells me that `pred` should be side-effect free. But
`some` does not. Does this mean I can use a function with a
side-effect in `some` or did they just miss it while documenting the
function? How do I know what I get back as a return value?

Also, take a function that like
 
    user=> (doc +)
    -------------------------
    clojure.core/+
    ([] [x] [x y] [x y & more])
      Returns the sum of nums. (+) returns 0. Does not auto-promote
      longs, will throw on overflow. See also: +'

Where does this tell me that I cannot pass strings to it?

In comparison take some Haskell equivalents
    
    Prelude> :t filter
    filter :: (a -> Bool) -> [a] -> [a]

    Prelude> :t (+)
    (+) :: Num a => a -> a -> a
    
    Prelude> :t print
    print :: Show a => a -> IO ()

I clearly know what has a side-effect and the behaviour without having
to read through the documentation. The signature of `map` is beautiful.

    map :: (a -> b) -> [a] -> [b]

It describes the function even before I start reading the docs. 

Also, if I did know what sort of a function I needed, I could use
[Hoogle][2]. For instance, if I needed a function that converted an
integer to a character, I search for `Int -> Char` in Hoogle and I
immediately get the following 2 as the top results

    1. chr
    2. intToDigit

I don't know of any dynamically-typed implementation that lets me do
that.



# Other arguments

1. They are like easy doc-strings. For most cases.
2. Even stronger type-systems than Haskell's exist. Dependent types
   even let you impose constraints like "List should be of length 10
   and contain only even integers less than 30". I am not familiar
   with any dependently typed languages. Check out Agda [3] if you are
   really interested
3. The compiler can perform various optimizations like
   strength-reduction which it may not be able to do for dynamic
   languages since it cannot prove that some function will only
   receive integer arguments.
4. Robert Harper claims that dynamically typed languages are simply
   unityped statically typed languages [3]. This has met a lot of
   criticism, but then...
5. There have been times when I have worked backwards from the type to
   the implementation of the function. Not a general case, but still.


# Conclusion

Static Typing > Dynamic Typing. Static typing is not a
silver-bullet. It does not catch all errors. Haskell's type system for
instance cannot ensure using only types that

    add :: (Num a) -> a -> a -> a
    add a b = a - b

is wrongly implemented. But it does ensure that if you do use an
`String` which is not an instance of `Num`, the call would be
wrong. If the argument is "Either give me 100% correctness proofs or
give me 0", you need to be coding in a proof-assistant with dependent
types (which can still have logical bugs). But the overhead of
static-typing is so little especially in a language like Haskell that
it is illogical to throw away all the freebies that static typing
gives you for being a good boy.

[1] https://www.fpcomplete.com/user/pbv/an-introduction-to-quickcheck-testing
[2] http://www.haskell.org/hoogle/
[3] http://wiki.portal.chalmers.se/agda/pmwiki.php
[4] 
http://existentialtype.wordpress.com/2011/03/19/dynamic-languages-are-static-languages/


---- On Fri, 17 Jan 2014 03:54:39 +0000 Pradip Caulagi wrote ----

>On Friday 17 January 2014 08:19 AM, Ramakrishnan Muthukrishnan wrote: 
>> Pradip Caulagi  writes: 
>> 
>> Statically typed languages gives some guarantees at *compile time* on 
>> the types. Types are an *invariant* of a program. For example if you 
>> declare a function foo like this: 
>> 
>> foo :: String -> IO () 
>> 
>> then it is guaranteed that there it takes a String and does some 
>> IO. Types does not say anything else about the program. So, I guess 
>> it depends what you mean by "correctness". 
>> 
>>> If this is correct, my contention is - it doesn't follow that it is 
>>> easier to write correct programs. 
>> 
>> I didn't quite follow that. Can you elaborate? 
> 
>Consider the example of date arithmetic. So adding 1 to 31 Jan gives 1 
>Feb. Adding 1 to 28 Feb gives 1 Mar for a non-leap year but 29 Feb for 
>a leap year. 
> 
>A correct program would be one that solves all these cases. Brian Hurt 
>defines this as 'working solution'. 
> 
>So my question is - how will the type system allow us to write 
>'correct/working' solutions faster? My contention is that, with a type 
>system, we can only reason about the correctness (to some extent). 
> 
>As you probably guessed, I just don't grok the point of static typing. 
> 
>-- 
>Pradip P Caulagi 
> 
>

Re: [bangalorehaskell] Static typing

From:
Ashok Gautham
Date:
2014-01-17 @ 22:34
---- On Fri, 17 Jan 2014 22:11:57 +0000 Ashok Gautham  wrote ---- 

>**NOTE** I did not completely grok who said what in the conversation I 
> ...

If that previous mail was as unreadable as it seemed to me (since all 
markdown indentation was flattened out while sending the mail), check out 
a hopefully better formatted version on my blog. 

http://blog.scriptdevil.in/why-i-adore-haskells-static-typing/

---
Ashok

Re: [bangalorehaskell] Static typing

From:
Pradip Caulagi
Date:
2014-01-18 @ 07:25
IMO, asking - can I send a message 'x' to an object - is the wrong
question.  For example, can I send reverse to this collection?  Tell, don't
ask. So just send the mesage. If the object doesn't understand the message,
it will fail.  These are simple problems that all unit tests will solve.

Like I mentioned earlier, there are other advantages of static typing that
I am missing. But I am pretty sure that the ability to tell at compile time
whether an object understands a message or not is *not* a significant
benefit.
On 18 Jan 2014 04:04, "Ashok Gautham" <scriptdevil@zoho.com> wrote:

>
> ---- On Fri, 17 Jan 2014 22:11:57 +0000 Ashok Gautham  wrote ----
>
> >**NOTE** I did not completely grok who said what in the conversation I
> > ...
>
> If that previous mail was as unreadable as it seemed to me (since all
> markdown indentation was flattened out while sending the mail), check out a
> hopefully better formatted version on my blog.
>
> http://blog.scriptdevil.in/why-i-adore-haskells-static-typing/
>
> ---
> Ashok
>
>

Re: [bangalorehaskell] Static typing

From:
Ashok Gautham
Date:
2014-01-20 @ 05:36
---- On Sat, 18 Jan 2014 07:25:11 +0000 Pradip Caulagi  wrote ----

> IMO, asking - can I send a message 'x' to an object - is the wrong
> question.  For example, can I send reverse to this collection?  Tell,
> don't ask. So just send the mesage. If the object doesn't understand
> the message, it will fail.  These are simple problems that all unit
> tests will solve.

Why do all the work when it is a solved problem? Unit-testing should
be used to test logic, not programming bugs. Things like 
`Object#respond_to?` of Ruby is leads to a lot of spaghetti code. 
Erlang's fail-but-handle-failure-elegantly model should only be used 
for the errors out of the programmer's control, like network-failures.
Quoting the old saying, "Exceptions are for exceptional cases"

Consider your example.

In a dynamically-typed language, you would start with

|        cabbage = my_collection.reverse

The first collection gets reversed correctly. Then it says,

|        `dict` type is not iterable

You say, aah that is easy... Let me add a defensive if

|        cleverCabbage = if my_collection.respond_to? :reverse
|           my_collection.reverse
|        else
|           some_complicated_workaround(my_collection)
|        end

Works for the next 20 collections then, BOOOM

|        NoneType does not respond to respond_to?
|
|        myGodWhyAreYouSoCabbage = if my_collection.null?
|           None
|        elif my_collection.respond_to? :reverse
|           my_collection.reverse
|        else
|           some_complicated_workaround(my_collection)

And then hope there is no object that doesn't fail in
`some_complicated_workaround`

In a statically-typed language,

|        my_collection.reverse

The compiler guarantees that this works (TM) on any program that 
compiles. 99% of the time in Haskell, if it compiles, it works.

The worst part about the dynamic solution is that you haven't really
solved the problem. You have only shifted the responsibility to
`some_complicated_workaround`. Now, that function needs to be able to
work on the entire universe of inputs.

Also, saying unit-testing solves the problem isn't correct. The
question is what are you going to unit-test with. If you have no
handle of what object could be passed on to the function, you would
have to test against the entire universe rather than testing
corner-cases for logical bugs.

> Like I mentioned earlier, there are other advantages of static
> typing that I am missing. But I am pretty sure that the ability to
> tell at compile time whether an object understands a message or not
> is *not* a significant benefit.

I think there is a fundamental difference in programming mindset
here. This is indispensible in my opinion. I would hate programming in
an environment where I would be unable to guarantee if some properties
hold or not without actually running the program. This is the reason I
provided the cyclomatic complexity example. The number of code-paths
you need to test is impossibly high for a significantly large
program. It is almost masochism to say, I don't mind runtime
errors. I will test all paths.

However, if you do want other benefits, I did point you to some in the
previous post as well

1. Optimization opportunities
2. Ease of use of libraries
3. Self-documenting function usage (from type signatures)
4. Lesser dependence on unit-testing
5. Automatic test generation

Without succumbing to the false lure of benchmarks, I would like to point 
out that the top 10 fastest languages in [1] are statically typed.

Compilers are around to help us. Why should one be so hesitant to take
help from it? I would agree the effort to annotate types would be much
higher in a primitive language like Java or C++. But in a language
like Scala or Haskell (especially Haskell), the type inference engine
is so strong, you don't really have to do too much.

Finally, I am currently reading TAPL [2] by Benjamin Pierce. I like the 
book, try it if and when free.

[1] 
http://benchmarksgame.alioth.debian.org/u64q/benchmark.php?test=all&lang=all&data=u64q
[2] http://www.cis.upenn.edu/~bcpierce/tapl/

Re: [bangalorehaskell] Static typing

From:
Pradip Caulagi
Date:
2014-01-23 @ 14:51
Ashok,

let me state upfront that my argument is because I don't grok static 
typing and its advantages rather than not believing in it.

> Why do all the work when it is a solved problem? Unit-testing should
> be used to test logic, not programming bugs. Things like
> `Object#respond_to?` of Ruby is leads to a lot of spaghetti code.
> Erlang's fail-but-handle-failure-elegantly model should only be used
> for the errors out of the programmer's control, like network-failures.
> Quoting the old saying, "Exceptions are for exceptional cases"
>
> Consider your example.
>
> In a dynamically-typed language, you would start with
>
> |        cabbage = my_collection.reverse
>
> The first collection gets reversed correctly. Then it says,
>
> |        `dict` type is not iterable
>
> You say, aah that is easy... Let me add a defensive if
>
> |        cleverCabbage = if my_collection.respond_to? :reverse
> |           my_collection.reverse
> |        else
> |           some_complicated_workaround(my_collection)
> |        end
>
> Works for the next 20 collections then, BOOOM
>
> |        NoneType does not respond to respond_to?
> |
> |        myGodWhyAreYouSoCabbage = if my_collection.null?
> |           None
> |        elif my_collection.respond_to? :reverse
> |           my_collection.reverse
> |        else
> |           some_complicated_workaround(my_collection)
>
> And then hope there is no object that doesn't fail in
> `some_complicated_workaround`
>
> In a statically-typed language,
>
> |        my_collection.reverse
>
> The compiler guarantees that this works (TM) on any program that
> compiles. 99% of the time in Haskell, if it compiles, it works.

Let me give my counter argument.  Consider again the example of date 
arithmetic.  I.e. we want to add or subtract 2 dates.

There are 2 checks that we need to do for a program - syntactic and 
semantic.  The syntactic checks validates we add dates.  This is what 
the compiler does.  It is also the least interesting of things.  The 
semantic checks will have validation of the form - 31 Jan + 1 = 1 Feb, 
28 Feb + 1 = 29 Feb for leap year and 1 Mar for non-leap year.  These 
checks are typically the business rules - the ones that matter.  The 
types in this case are useful but not to a great extent.  I would even 
think that types are an internal detail that shouldn't bother the 
developer.  More interesting are the methods/behavior the objects 
expose/have.
>
> The worst part about the dynamic solution is that you haven't really
> solved the problem. You have only shifted the responsibility to
> `some_complicated_workaround`. Now, that function needs to be able to
> work on the entire universe of inputs.
>
> Also, saying unit-testing solves the problem isn't correct. The
> question is what are you going to unit-test with. If you have no
> handle of what object could be passed on to the function, you would
> have to test against the entire universe rather than testing
> corner-cases for logical bugs.

I disagree.  In my experience, the inputs are very well defined.  I 
don't think having an add function with 2 inputs in a dynamically typed 
language implies it can add arbitrary objects.

> Compilers are around to help us. Why should one be so hesitant to take
> help from it? I would agree the effort to annotate types would be much
> higher in a primitive language like Java or C++. But in a language
> like Scala or Haskell (especially Haskell), the type inference engine
> is so strong, you don't really have to do too much.

This is the most interesting argument, IMO.  I want to understand how 
the type inference of Haskell is superior to what I have seen so far.
>
> Finally, I am currently reading TAPL [2] by Benjamin Pierce. I like the
> book, try it if and when free.

... of course, if it takes a book to argue about the type system, we can 
hardly hope to do better in a few posts.  But I would love to forward my 
understanding more with these arguments :)

--
Pradip P Caulagi
http://caulagi.com

Re: [bangalorehaskell] Static typing

From:
Ashok Gautham
Date:
2014-01-23 @ 18:58
---- On Thu, 23 Jan 2014 14:51:08 +0000 Pradip Caulagi  wrote ---- 

>Let me give my counter argument. Consider again the example of date 
>arithmetic. I.e. we want to add or subtract 2 dates. 
> 
>There are 2 checks that we need to do for a program - syntactic and 
>semantic. The syntactic checks validates we add dates. This is what 
>the compiler does. It is also the least interesting of things. The 
>semantic checks will have validation of the form - 31 Jan + 1 = 1 Feb, 
>28 Feb + 1 = 29 Feb for leap year and 1 Mar for non-leap year. These 
>checks are typically the business rules - the ones that matter. The 
>types in this case are useful but not to a great extent. I would even 
>think that types are an internal detail that shouldn't bother the 
>developer. More interesting are the methods/behavior the objects 
>expose/have. 
>> 

This is the fundamental point of difference. This is a great improvement.

Nothing prevents you from accidentally assigning a string like
"29-June-2012" to the date field in a dynamically typed language. You
aren't tripping until the point you actually end up using the variable
somewhere else. Further, what you are trying to encode can be achieved
by dependent types. Haskell isn't a dependently typed language, but
Agda is.  

Types aren't there to *bother* the programmer, they are around to
*help* him. You want "all-or-nothing" here. Think of it as some 
headache offloaded to the compiler. 
Is it a magical spell that lets him auto-generate all testing he ever has
to do? No. But does it eliminate worry about every single code path
for runtime type-errors? Yes.

>I disagree. In my experience, the inputs are very well defined. I 
>don't think having an add function with 2 inputs in a dynamically typed 
>language implies it can add arbitrary objects. 

True, but that is not a formal contract. That is my very point. For
instance, you have C++/Java where you have visibility modifiers like
private,protected,public etc. In Python, it is just an informal
contract. You can argue that it doesn't really matter if the
programmer/library developer is clever/careful enough to avoid any
erroneous updates directly to member variables. But, hiding the actual
implementation - as you might have encountered at some point - really
helps you write libraries that can grow better.

In other words, what prevents me from running into the following bug 3
days after executioin starts?

|    f = open("foo", 'w')
|    print("Writing to " + f)
|    f.write(someText)
|    f.close()

Yes, it is clear that the person shouldn't have printed a file object
and should have printed the file-name in retrospect. But then, humans
err.

>This is the most interesting argument, IMO. I want to understand how 
>the type inference of Haskell is superior to what I have seen so far. 

Compared to? If you do point out what languages enthuse you, I might
be able to give you better reasons why it is possibly finer. (It is a
HM-type system with constrained types). 

There is a difference between type inferencing in static languages and
dynamic languages. Static languages are often
variable-and-object-typed. The variable, once assigned a value of type
X, always has that type X. Most dynamic languages are
object-typed. i.e. it is possible for you to do

|    f = 11.22 # f is now pointing to a float object
|    f = ":-(" # f is now pointing to a string
|    f = lambda x: x+2 # f is now pointing to a function object

I hate this style of coding since I cannot have a mental model of what
some "f" is. Static typing prevents this. Dynamic typing does nothing
about it.

(This is not weak typing. I hope the difference is obvious)

>... of course, if it takes a book to argue about the type system, we can 
>hardly hope to do better in a few posts. But I would love to forward my 
>understanding more with these arguments :) 

It does not take a book to like type systems. But understanding it
completely would need study. But that is similar to the fact that you
use an interpreter with garbage collection, but don't really need to
know how the interpreter or garbage collector works.

---
Ashok