[Haskell-cafe] Re: [Haskell] pros and cons of static typing and side effects ?

[Keean Schupke]

My 2-pence worth on static typing.

Static typing to me seems to be a simplified form of design by contract. 
There are some things about a program that can be proved "true for all 
time". Types are an example of such a thing. We can use type systems to 
make assertions about properties that must be true for all time, and 
then reject programs that break these rules.

One of the easyest things to prove about a program is that all values 
and references are handled correctly - hence you will never see a 
"segmentation fault" due to bad programming, it is just impossible (of 
course the run-time-system which is written in C may cause one, but that 
cannot be due to a bug in your program).


Taking one of your points in more detail:The single type property for 
lists is not a problem due to the presence of algebraic datatypes, for 
example want a list of strings and ints:

    data StringOrInt = IsString String | IsInt Int
    type ListOfStringOrInt = [StringOrInt]

You can also have lists of records... Think about it for a bit and you 
will see there are very  few cases where you need to have a list of 
'general types'...

You can even use existential types to create lists of things with a 
common interface, where you do not know in advance what types you may need:

    data XWrap = XWrap (forall a . Show a => a)
    type ListXWrap = [XWrap]

This creates a list where the items can be any type, provided they are a 
member of the class Show. Also the only functions you can call on the 
items in the list are the methods of the Show class... Of course you can 
have multiple type constraints (forall a . (Show a,Num a) => a).

This is not the limit of how far we can go with static typing. We can 
choose any provable property about a program... for example we could ask 
that the compiler prove that the heap size of the program never exceeds 
10M (not possible in any current language - but is an extension of the 
concept).

Other things we can do ... with dependant types we can ask the compiler 
to prove the correctness of sorting algorithms. If we define an ordered 
list tgo be one where each element must be larger than the preceding one:

    data OrderedIntList = Cons (a::Int) (l::OrderedList) | Nil {- where 
a <= head l -}
    data IntList = [Int]

We can now define our sorting function:

    quicksort :: IntList -> OrderedIntList

By this we are asking the compiler to prove (by induction) that the 
function provided can only result in
correctly ordered lists - irrespective of what arguments it is given (ie 
proved true for any input)... This would have to be done symbolically 
but is not beyond what can be achieved using logic programming.
To implement this, a Prolog program containing all the type constraints 
of the function definition and
the "proposed" type would be evaluated... Prolog will say "yes" or "no" 
to the function.

    Regards,
    Keean.