Path: utzoo!utgpu!news-server.csri.toronto.edu!rpi!crdgw1!uunet!mcsun!ukc!ox-prg!msc13.comlab!mpj
From: mpj@prg.ox.ac.uk (Mark Jones)
Newsgroups: comp.lang.misc
Subject: Re: Dynamic typing (part 3)
Message-ID: <1558@culhua.prg.ox.ac.uk>
Date: 9 Apr 91 16:31:43 GMT
References: <1593@optima.cs.arizona.edu>
Sender: news@prg.ox.ac.uk
Reply-To: mpj@prg.ox.ac.uk (Mark Jones)
Organization: Oxford University Computing Laboratory, UK
Lines: 82

In article <1593@optima.cs.arizona.edu> David Gudeman writes:
| OK, try this.  
| [description of a map function which applies a given function to each
|  element of a sequence ... includes both a mathematical version and
|  an Icon version.]
|
|Try to write this function in a statically typed language so that it
|has all the generality of the math and Icon versions.

Well Haskell is a statically typed language and the map function can be
defined very neatly:    

                      map f xs = [ f x | x<-xs ]
 
That's it.  No need for any type declarations (although Haskell does
infer that map has type (a->b) -> [a] -> [b] for any types a and b).
 
As far as satisfying the mathematical definition that you gave:
|  If f is a function and s is a sequence, then map(f,s) is the
|  sequence t such that for all i . t[i] = f(s[i]).
 
In Haskell, the ith element of a sequence xs is written xs!!i.  So your
condition can be written as:   (map f xs)!!i = f (xs!!i).  This property
can be proved by simple structural induction (you will need to make the
assumption that xs has an ith element (i.e. that xs!!i exists); a point
which is implicit in your definition).
 
In other words, the Haskell definitions give you precisely the mathematical
behaviour that you've asked for!

|                                                       (Actually, the
|math version works for infinite sequences and the Icon one doesn't. 
|There are languages that fix that...) 
 
Haskell is one of them.  
 
|                                 In statically typed programming 
|languages the purpose of the types is to let the compiler generate 
|better code, and the nature of the declarations reflects that.  
 
In Haskell, you don't usually need to give any type declarations ...
perhaps some clever compilers will be able to use type declarations to 
generate better code ... but from my point of view, the main uses of 
type declarations are: 
 - documentation ... just knowing the type of a function can give you
   a lot of information about it.
 - consistency checking ... if I choose to give an explicit type 
   declaration, that reflects my intention as a programmer about how 
   an object will behave.  The Haskell type system will let me know 
   if the definition of the object does not agree with my intentions.

|                                                                For
|example, you cannot simply declare something as a "number", you have
|to decide whether you want it represented in floating point format or
|integer, and what size you want.
 
You can do this in (.. you guessed ..) Haskell.  In fact, even numeric
constants are treated as objects of type Num a => a meaning any type a
so long as a is a numeric type (which might be integers, floating points,
complex numbers ... even polynomials if you wanted).
 
Haskell takes this further ... in an expression of the form x+y one does
not have to insist that x,y are both Integers/Floats etc.  All that is
necessary is that they both have the same type a, and that a is a numeric
type.

This posting was not meant to be an advert for Haskell, but while I'm
on the subject, how would you use your Icon program to add one to a list
of lists of integers nss?  I'd be surprised if you could do it more naturally
than Haskell:
 
               map (map succ) nss where succ n = n+1
 
Which brings me onto a final point; if I can solve a problem P more naturally
in a language L1 than I can in a language L2, does that mean that L1 is
better than L2 (or that the type system of L1 is better than that of L2)?
I certainly wouldn't want to claim superiority of Haskell over Icon (or
anything else) in that way.
 
[Best quit now before we get back to first-class functions...]
 
Mark