Re: Static vs Dynamic

From: Matthew Danish (mrd+nospam_at_cmu.edu)
Date: 10/24/04 

Date: 24 Oct 2004 17:40:08 -0400

pyedarren@hotmail.com (Darren) writes:
> If not, an example of how to do a similar polymorphic call in those
> languages would be appreciated.

This is how a functional statically typed language would do things
(Haskell, various MLs, but specifically Standard ML here):

The type system in SML has the notion of ``parametric polymorphism''
where it is possible to have types with unknowns, with variables. The
polymorphism comes into play when you define functions using these
parameterized types. Consider a basic type, the list.

list is defined to be either [], the empty list, or X::list, in Lisp
terms a cons.

Without parameterized types, you would have to define separately
an int_list, a char_list, etc, for example:

datatype int_list = INT_NIL | INT_CONS of int * int_list

This defines what is called a disjoint type that has two constructors.
INT_NIL constructs a value of type int_list. INT_CONS also constructs
a value of type int_list, for which it requires two constructor
parameters; an int, and an int_list. Then you could construct such an
int_list by doing this:

  INT_CONS(1, INT_CONS(2, INT_CONS(3, INT_NIL)))

The real definition of list looks something more like this:

(pseudo-code) datatype 'a list = [] | :: of int * 'a list

where 'a (pronounced: alpha) stands for the type parameter. This is
pseudo-code because you (the programmer) couldn't really define a
constructor named [] or the operator :: in SML, but other names would
be acceptable.

With such a system, it is easy to write statically-typed polymorphic
functions that operate on lists in general, or specific kinds of
lists.

fun length [] = 0
  | length (first::rest) = 1 + (length rest)

That is the simple recursive definition of the length function on
lists. It makes use of some pattern matching functionality of SML, as
you can see the arguments to the function are deconstructed
automatically. The type system of SML will determine that the type of
the above function is

  length : 'a list -> int

Which means that length is of the function type with parameter 'a list and
return value int. So

  length [1,2,3] (* translates to length (1::(2::(3::[]))) *)

is a valid call and so is

  length ["a","b","c"]

What the typechecker does is called Unification of types. In this
example, it would take the following types:

  length : 'a list -> int
  ["a","b","c"] : string list

and determine that

  length ["a","b","c"] : int

by substituting string for 'a and applying the function.

But suppose you wrote a function like this:

fun sum [] = 0
  | sum (first::rest) = first + (sum rest)

Now the unifier has to consider that you are using the + operator

  op+ : int * int -> int

Therefore, first must be an int, and rest must be an int list. So,

  sum : int list -> int

This makes

  sum [1,2,3]

a valid, well formed, typed expression (with result 6) and

  sum ["a","b","c"]

a static type error.

Standard ML's type system is based closely on what is called the
Hindley-Milner type system. It is designed for parametric
polymorphism, and for ease of type inference. SML adds a module
system. Other languages with similar goals include Objective CAML,
which adds an object system, and Haskell, which makes use of an
interesting category theory concept called Monads. [1]

As you can see, the goals of these languages are fundamentally
different from Common Lisp or Java. In Common Lisp, it is acceptable
for type errors to be found at run-time if they cannot be found by the
compiler, and there is a robust condition system for handling such
errors (and others). Java seems to be designed with the goal of being
simple, and thus leaves out both the rigor of a proper static type
system, and the robustness of a good condition system.

[1] More reading:
  http://www.standardml.org/ -- SML
  http://www.smlnj.org/ -- SML/NJ, an implementation with a top-level
  http://caml.inria.fr/ -- OCAML
  http://www.haskell.org/ -- Haskell 

-- 
;; Matthew Danish -- user: mrd domain: cmu.edu
;; OpenPGP public key: C24B6010 on keyring.debian.org

Relevant Pages

  • Re: EE Student, Edit, Proposal Masters, Help (concepts of functional programming, symbolic programmi
    ... A few comments on Symbolic and Functional Programming ... Symbolic programming languages fall under two categories, ... types, lists, expressions, primitives and variables. ... The assignment chain is not altered by evaluation. ...
    (sci.math.symbolic)
  • Re: Unix and OO Avoidance
    ... >> polymorphism except polymorphism based upon ... You are right, RCM has used managing dependencies as his definition of OO, ... << are managed through dynamic polymorphism. ... << that I would not consider OO languages. ...
    (comp.object)
  • Re: mot de passe root
    ... > poster's fellow nationals gently reminds them that it's an English ... Posts in other languages were historically entirely welcome, ... lists was because they were likely to get better results there, ... enough of a French posting to understand the problem and proposed ...
    (freebsd-questions)
  • Re: Reminder, blatant ad
    ... >>> a) The problem is naturally formulated in terms of named lists of items ... the programmig languages are many. ... What works for me is what I would call a di-graph of trees (a tree on ... I think declarative languages are ...
    (comp.databases.theory)