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.
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Reply via email to