[Haskell-cafe] Re: [Haskell] pros and cons of static typing and
side effects ?
Keean Schupke
k.schupke at imperial.ac.uk
Tue Aug 16 15:56:19 EDT 2005
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.
More information about the Haskell-Cafe
mailing list