expressiveness and strong type system? 
Author Message
 expressiveness and strong type system?


Quote:

> somewhere in the current discussion jeff dalton repeats an occasionally
> heard claim that stronger type systems result in "less expressive" languages.
> this is an interesting claim, but it occasionally gets stuck like a fuzzball
> in the throat of further inquiry. perhaps people who have thought about this
> issue can provide some examples? references to any formal work? is there any
> support for felleisen's neat "conciseness conjecture" for example?

I presume that by 'stronger type systems', you mean statically typable systems.

The problem with most type systems is that they insist on going it alone, with
no help from the programmer.  Since this choice results in type systems that
have recursive algorithms, it necessarily restricts the expressiveness of
the language.

One can conceive of type systems which can be given help by the programmer,
and therefore allow a much greater degree of expressiveness, while allowing
the type check to run in some reasonable amount of time.

Many of the proposals for 'run-time' typing are 'really' a mechanism for
the programmer to help the (static) type system.

A concrete example --
I contend that a type system that cannot type implementations of the Y
combinator restrict the expressiveness of the language.

--
www/ftp directory:
ftp://ftp.netcom.com/pub/hb/hbaker/home.html



Mon, 31 Aug 1998 03:00:00 GMT  
 expressiveness and strong type system?

Quote:

> somewhere in the current discussion jeff dalton repeats an occasionally
> heard claim that stronger type systems result in "less expressive" languages.
> this is an interesting claim, but it occasionally gets stuck like a fuzzball
> in the throat of further inquiry. perhaps people who have thought about this
> issue can provide some examples? references to any formal work? is there any
> support for felleisen's neat "conciseness conjecture" for example?

A type system is a structure imposed on the sets of values
representable by a language.  No type system will always
be appropriate in all situations.

Examples:

The lack of a discriminated union in C++ has caused me no
end of grief.  Every time I add a new type to my hand-built
discriminated unions, I have to go changing case statements
all over the place.  A side note to this is that C and C++
programmers have unknowingly invented their own ad-hoc
pseudo-discriminated union by overloading the meaning of a
pointer when its value is null.

The yuckiness of `=' in SML has been taken as testimony to an
incompleteness in the language's type system (or an argument
about the semantics of equality, depending on who you talk to).  
And the type of `eval' can't be represented in SML either if
I'm not mistaken.

I'm all gung-ho about how cool generic functions are, and I've
built my own type system in Scheme around them.  It's great
that Scheme allowed me to built a type system appropriate to
my task, but I pay for that flexibility in performance.

I'm eager to do something serious in SML to see how well I get
along without generic functions.

One might argue that these are examples of how incomplete or
bad type systems are what make a language less expressive,
but the lesson I gather is that type systems themselves will
never be complete (which is a big-duh when you think about it).

Thant Tessman



Mon, 31 Aug 1998 03:00:00 GMT  
 expressiveness and strong type system?
somewhere in the current discussion jeff dalton repeats an occasionally
heard claim that stronger type systems result in "less expressive" languages.
this is an interesting claim, but it occasionally gets stuck like a fuzzball
in the throat of further inquiry. perhaps people who have thought about this
issue can provide some examples? references to any formal work? is there any
support for felleisen's neat "conciseness conjecture" for example?

oz
---




Mon, 31 Aug 1998 03:00:00 GMT  
 expressiveness and strong type system?

   A concrete example --
   I contend that a type system that cannot type implementations of the Y
   combinator restrict the expressiveness of the language.

I assume you refer to type systems that cannot type self-application...

Anyway, I am perfectly happy with a language and a decidable type
system, if it comes with a built-in Y combinator.

--
-Matthias



Mon, 31 Aug 1998 03:00:00 GMT  
 expressiveness and strong type system?
Look, Scheme is dynamically typed.  What this really means is that you
have no useful information to reason about a term at compile time.  In
other words, the only useful approximation of the term's behavior is
the term itself -- And of course, to reason about some non-trivial
property of the term is in general undecidable.  Where's the big
surprise in this?

The ability to encode invariants which are decidable is extremely
useful.  If I know that e has type float, then I can evaluate e and
place it in a floating-point register instead of having to box and/or
tag the value to place it in a GP register.  Likewise, knowledge that
e has type tau1->tau2 and e' has type tau1, means that I don't have to
check at runtime that the application e (e') won't cause a core dump.
If e has type my_capability, and the only way to create a
my_capability object is through my interface, then I don't have to
check at runtime whether e is a forged capability or not.  Thus,
strictly from a performance point of view, static types buy you
information that other programmers, an optimizer, and/or a runtime
system can put to very good use.  

And before you go claiming that this ability can be done for
dynamically typed languages like Scheme, consider the issues
of separate and dynamic compilation -- most, if not all, program
analyses (such as so-called soft type systems) fail at module boundaries
because there is no constraint on how an exported object may be used.  
The result is that at module boundaries, every object is promoted
to type "dynamic" (i.e. no useful static information).  In contrast,
when modules can be labelled with type information to constrain
their components' uses, and these constraints can be enforced at compile time,
this useful information can flow across module boundaries providing
enhanced modularity without sacrificing separate compilation.
In contrast, soft-type systems must do whole program analysis
to get suitable performance, yet this sacrifices separate compilation,
dynamic linking, etc.

Projects like SPIN at the University of Washington have taken the good
ideas of type systems and put them to use, building an entirely extensible
OS kernel around a statically typed language, Modula-3.  The result is
far fewer "capability" checks when arguments are passed from
user-level routines to kernel-level routines.  Not only does this
enhance performance (no need for costly run-time checks either in
hardware or in software, no need for costly context switching, etc.),
but it also enhances extensibility because modules can be separately
compiled, linked, and loaded into the kernel dynamically without
sacrificing security or performance.

The SPIN project, among others, is a striking example of why many
people in the ML consider the ability to add constraints (e.g.
typing information) as leading to a more expressive language.  

Having said all of this, it is easily possible to add dynamic
types to statically typed languages like Modula-3 and ML
(see the ref any type for M3 and various dynamic proposals
put forth by people in the ML community.)  In the ML community,
the implementors just haven't heard enough clamoring from
the users to provide this feature...

-Greg Morrisett



Tue, 01 Sep 1998 03:00:00 GMT  
 expressiveness and strong type system?

This was a very nice post. Thanks for sharing it with us.

I'd like to add to it by offering some insight into the dynamic approaches
that are being taken to deal with the same set of issues you raised.

I'm not arguing with you are trying to say that anything you said is wrong
or misleading.  I'm just offering a complementary view of the same issues
from the viewpoint of a different but related research sub-community.

In fact, the first step in working towards a dynamic approach is to steal
all the good ideas you can from the static community ;-)

---

   Look, Scheme is dynamically typed.  What this really means is that you
   have no useful information to reason about a term at compile time.

It is common to use the term ``compile time'' to describe a static phase of
program processing completely separate from the program's actual execution
on any data set (the ``running time'' or just ``run time'').

But there is a growing body of work in dynamic re-compilation and run-time
code generation.  See for example:

  http://www.cs.washington.edu/homes/pardo/rtcg.d/index.html

This blurs the distinction between ``compile time'' and ``run time'' since
some amount of compilation (in some cases, _all_ compilation) can take
place dynamically, as the program runs.

In such systems, there is plenty of useful information to reason about.

   And before you go claiming that this ability can be done for
   dynamically typed languages like Scheme, consider the issues
   of separate and dynamic compilation -- most, if not all, program
   analyses (such as so-called soft type systems) fail at module boundaries
   because there is no constraint on how an exported object may be used.  
   The result is that at module boundaries, every object is promoted
   to type "dynamic" (i.e. no useful static information).  In contrast,
   when modules can be labeled with type information to constrain
   their components' uses, and these constraints can be enforced at compile time,
   this useful information can flow across module boundaries providing
   enhanced modularity without sacrificing separate compilation.

But with dynamic re-linking and on-the-fly per-call-site specialization,
these artificial module boundaries can be crossed with _dynamic_
information through dynamic flow analysis, resulting in better code than
mere static analysis alone can achieve.  For instance, in a system with
disjoint union types, like ``INT or FLOAT'', dynamic polyvariant partial
evaluation gives you this incremental on-the-fly per-call-site
specialization.

See for example the body of work by Chambers and Ungar on Self, a Dynamic
OOPS system:

 http://self.smli.com/

One of the major ideas of the Self project was the dynamic in-lining and
specialization of method dispatch in an OOPS system.  The encapsulation
properties of OOPS classes, for example, have much in common with those of
static module systems.

The overhead of such on-the-fly incremental code improvement can be offset
both by amortizing it over the lifetime of the code and by factoring in the
speed up gained from the incremental performance improvements.

----

   Projects like SPIN at the University of Washington have taken the good
   ideas of type systems and put them to use, building an entirely extensible
   OS kernel around a statically typed language, Modula-3.

This is a great project.  Another great project at UW is the Cecil/Cortex
project. From their project home page:

  CECIL is a purely object-oriented language intended to support rapid
  construction of high-quality, extensible software.  Cecil incorporates
  multi-methods, a simple prototype-based object model, a mechanism to
  support a structured form of computed inheritance, module-based
  encapsulation, and a flexible static type system which allows
* statically- and dynamically-typed code to mix freely.

  VORTEX is an optimizing compiler infrastructure for
  object-oriented and other high-level languages.  It targets both pure
  object-oriented languages like Cecil and hybrid object-oriented
  languages like C++ and Modula-3.  Vortex currently incorporates
  high-level optimizations such as static class analysis, class hierarchy
* analysis, profile-guided receiver class prediction, profile-guided
* selective procedure specialization, intraprocedural message splitting,
* automatic inlining, and static closure analyses.  It also includes a
  collection of standard intraprocedural analyses such as common
  subexpression elimination and dead assignment elimination.  The Vortex
  compiler is written entirely in Cecil.

Their project home page is at:

  http://www.cs.washington.edu/research/projects/cecil/www/cecil-home.html

---

I see SPIN and Cecil/Vortex not as competing projects so much as they are
complementary projects with similar long-term goals.  It is a credit to UW
that they have so hearty a research environment to support these
alternative approaches.  In many ways, I envy them.  I wonder if their
looking for any post-docs ;-)

   The SPIN project, among others, is a striking example of why many
   people in the ML consider the ability to add constraints (e.g.
   typing information) as leading to a more expressive language.  

Well said.

And the Cecil/Vortex project, among others, is a striking example of why
many people in the dynamic languages/systems community consider the ability
to add constraints (e.g. both static _and_ dynamic typing information) as
leading to a more expressive language and a more effective runtime system.
--
------------------------------------------------------------------------------


,,Lambda Calculus...   /\\_ ...uber alles!'' | 545 Technology Square--Room 439
http://www-swiss.ai.mit.edu/~ziggy/ziggy.html| Cambridge,  MA USA   02139-3594



Wed, 02 Sep 1998 03:00:00 GMT  
 expressiveness and strong type system?

ziggy> But there is a growing body of work in dynamic re-compilation
ziggy> and run-time code generation.  ...  This blurs the distinction
ziggy> between ``compile time'' and ``run time'' since some amount of
ziggy> compilation (in some cases, _all_ compilation) can take place
ziggy> dynamically, as the program runs.  In such systems, there is
ziggy> plenty of useful information to reason about.

in my work on run-time code generation (and i'm sure Mark Leone and
Peter Lee have has well) i've found a that well-typed source programs
are *exactly* what are needed for efficient RTCG.  The reason is that
the types are what you need in order to produce fast code generators.
see:

http://www.cs.cmu.edu/~spot/nitrous.html
Compiler Generation for Interactive Graphics using Intermediate Code
by Scott Draves

http://www.cs.cmu.edu/~mleone/papers/ml-rtcg.ps
Optimizing ML with Run-Time Code Generation by Mark Leone and Peter
Lee

for those who *still* aren't convinced, see

ftp://ftp.daimi.aau.dk/pub/danvy/Papers/danvy-popl96.ps.gz
Type-Directed Partial Evaluation by Olivier Danvy

--
                                balance
                                equilibrium
                                death

http://www.cs.cmu.edu/~spot



Wed, 02 Sep 1998 03:00:00 GMT  
 expressiveness and strong type system?

[many interesting things omitted...]

SD> for those who *still* aren't convinced, see
SD> ftp://ftp.daimi.aau.dk/pub/danvy/Papers/danvy-popl96.ps.gz
SD> Type-Directed Partial Evaluation by Olivier Danvy

Hmm. I understand that Dan Friedman and/or Kent Dybvig have subsequently
shown how to take Olivier's idea and do it in a dynamically typed system.

No great morals intended; just a data point.

--Mitch


College of Computer Science, Northeastern University
360 Huntington Avenue #161CN, Boston, MA 02115     Phone: (617) 373 2072
World Wide Web: http://www.ccs.neu.edu/home/wand   Fax:   (617) 373 5121



Sat, 05 Sep 1998 03:00:00 GMT  
 expressiveness and strong type system?


|
|      A concrete example --
|      I contend that a type system that cannot type implementations of the Y
|      combinator restrict the expressiveness of the language.
|
|   I assume you refer to type systems that cannot type self-application...
|
|   Anyway, I am perfectly happy with a language and a decidable type
|   system, if it comes with a built-in Y combinator.

In my case I am more concerned with type systems that disallow
heterogenous lists, vectors, and other arbitrarily-sized "indexed"
data structures (not records) where the elements are of different
types.



Sun, 06 Sep 1998 03:00:00 GMT  
 expressiveness and strong type system?

   In my case I am more concerned with type systems that disallow
   heterogenous lists, vectors, and other arbitrarily-sized "indexed"
   data structures (not records) where the elements are of different
   types.

I think 99% of the cases where people take advantage of this in Scheme
is when the size is actually fixed and lists serve as a kludge to make
up for the missing record types.

The remaining 1% cases where objects of different type go into the
same list can easily be dealt with using explicit sum types
(`datatypes' in ML).  In this case you even get some extra help from
the compiler, who will make sure you don't put things into the list
you didn't think of before, and who will warn you if you handle only a
subset of all possible cases...

After all, Scheme's "type" system can be viewed as just one big ML
`datatype'.

--
-Matthias



Sun, 06 Sep 1998 03:00:00 GMT  
 expressiveness and strong type system?


      In my case I am more concerned with type systems that disallow
      heterogenous lists, vectors, and other arbitrarily-sized "indexed"
      data structures (not records) where the elements are of different
      types.

   I think 99% of the cases where people take advantage of this in Scheme
   is when the size is actually fixed and lists serve as a kludge to make
   up for the missing record types.

   The remaining 1% cases where objects of different type go into the
   same list can easily be dealt with using explicit sum types
   (`datatypes' in ML).  In this case you even get some extra help from
   the compiler, who will make sure you don't put things into the list
   you didn't think of before, and who will warn you if you handle only a
   subset of all possible cases...

I just would add that there are still some % missing. Notably when you
are going to implement an object oriented system in Scheme. In that
case you might not only want to add objects of a base type to the list
but also of its extensions. This actually is not easy to implement with
ML's type system. There has been some research on that, but the
solutions presented in the papers I've read either look like some
kludgery (if they rely on ML's type system) or require extensions to
the type system.

But besides that, I share your view.

   After all, Scheme's "type" system can be viewed as just one big ML
   `datatype'.

From the above remark I would say "can roughly be viewed" :-)

   --
   -Matthias

Wolfgang

--
----
Wolfgang Lux

+49-6221-59-4546                        VNET:     LUX at HEIDELBG
+49-6221-59-3500 (fax)                  EARN:     LUX at DHDIBMIP



Mon, 07 Sep 1998 03:00:00 GMT  
 expressiveness and strong type system?


|
|      In my case I am more concerned with type systems that disallow
|      heterogenous lists, vectors, and other arbitrarily-sized "indexed"
|      data structures (not records) where the elements are of different
|      types.
|
|   I think 99% of the cases where people take advantage of this in Scheme
|   is when the size is actually fixed and lists serve as a kludge to make
|   up for the missing record types.

Perhaps, but none of my uses fall here, since the version of Scheme
that I use has record types.

|   The remaining 1% cases where objects of different type go into the
|   same list can easily be dealt with using explicit sum types
|   (`datatypes' in ML).  In this case you even get some extra help from
|   the compiler, who will make sure you don't put things into the list
|   you didn't think of before, and who will warn you if you handle only a
|   subset of all possible cases...

I don't agree.  I often write "system level" code.  I write generic
object finalization code.  I write generic hash tables.  I write
generic parsers, unparsers, inspectors, de{*filter*}s, etc.

In all of these cases, the code must be ready to deal simultaneously
with types that it has never encountered before, which is precisely
why I depend on this ability.

Sum types do not cut it because the types must be pre-specified.



Mon, 07 Sep 1998 03:00:00 GMT  
 expressiveness and strong type system?


Quote:
>In all of these cases, the code must be ready to deal simultaneously
>with types that it has never encountered before, which is precisely
>why I depend on this ability.

>Sum types do not cut it because the types must be pre-specified.

But Scheme does not allow you to define new types!  It's just one
big ML datatype, such as:

        datatype dynamic = Dynamic of ref value
        and Int of int | Real of real | Function of dynamic list -> dynamic
        | Cons of dynamic * dynamic | Vector of dynamic | Null

-Greg



Mon, 07 Sep 1998 03:00:00 GMT  
 expressiveness and strong type system?

   |   The remaining 1% cases where objects of different type go into the
   |   same list can easily be dealt with using explicit sum types
   |   (`datatypes' in ML).  In this case you even get some extra help from
   |   the compiler, who will make sure you don't put things into the list
   |   you didn't think of before, and who will warn you if you handle only a
   |   subset of all possible cases...

   I don't agree.  I often write "system level" code.  I write generic
   object finalization code.  I write generic hash tables.  I write
   generic parsers, unparsers, inspectors, de{*filter*}s, etc.

   In all of these cases, the code must be ready to deal simultaneously
   with types that it has never encountered before, which is precisely
   why I depend on this ability.

   Sum types do not cut it because the types must be pre-specified.

Well, looks like what you need is polymorphism (type variables)...
(No, I won't mention the name of the language I am thinking of and
which offers those too... :)

--
-Matthias



Mon, 07 Sep 1998 03:00:00 GMT  
 expressiveness and strong type system?

   I just would add that there are still some % missing. Notably when you
   are going to implement an object oriented system in Scheme.
   [ ... ]

I was almost expecting such a reply.  Incidentally, I don't believe in
OO-ness.  At least not in the subtyping- and inheritance aspects of it.

      After all, Scheme's "type" system can be viewed as just one big ML
      `datatype'.

   From the above remark I would say "can roughly be viewed" :-)

Actually, the Scheme "type" system is *exactly* just one big ML
datatype, as can trivially be seen by looking at existing Scheme
implementations in ML.  Here is one I was using for an experimental
system (which is not 100% Scheme):

    datatype t =
        INTEGER of int
      | STRING of string
      | SYMBOL of Symbol.t
      | IDENT of Names.ident
      | PRIMOP of Primop.t
      | HOOK of t list -> t
      | NIL
      | TRUE
      | FALSE
      | EOF
      | CELL of t ref
      | CONS of t ref * t ref
      | VECTOR of unit ref * t Array.array
      | PROC of t LExp.env * t LExp.exp
      | IPORT of TextIO.instream
      | OPORT of TextIO.outstream
      | CONT of t SMLofNJ.cont

--
-Matthias



Mon, 07 Sep 1998 03:00:00 GMT  
 
 [ 25 post ]  Go to page: [1] [2]

 Relevant Pages 

1. Flying With Python (Strong versus Weak Typing) [actually, Static vs Dynamic typing]

2. Static typing and expressiveness

3. Difference between a type system and a type constraint system

4. Difference between a type system and a type constraint system

5. Strong static typing does not work

6. Strong type checking...

7. Strong type checking ... (not really)

8. Strong type checking + Heterogenous con

9. Strong typed variables

10. Strong typing header needed

11. Strong type checking is good, but...

12. Strong Typing

 

 
Powered by phpBB® Forum Software