🚀 go-pugleaf

In article <OLSON.91Apr9012119@lear.juliet.ll.mit.edu> olson@lear.juliet.ll.mit.edu ( Steve Olson) writes:
>
>I am aware that demanding detailed decisions about storage layout or machine
>data-types is not inherent to the concept of static typeing.  I would be 
>interested in hearing about a language where you could do something
>like declare x to be a "number".  Does such exist?  Efficiency aside, does
>there exist a language where a static type system catches lots of errors but
>dosen't get in your way the way current examples do?  I don't know myself
>-- thats why I read this list!


Ignoring, for just a moment, the always fascinating topic of 
lisp versus C, this seems to get at what I want to understand from this
discussion: namely, is there something inherent in "static" typing
and type checking that makes it so tedious and baroque? Is it not
possible to have a programming language in which types are used as in
mathematics to clarify, disambiguate, and catch errors? I do not
buy the argument that there is a real plus in being able to write
expressions that may not have any meaning. That is, if I write
$f(X)$ I should be able to ensure, during design time, that 
f is defined over all possible instantiations of X. Why, one would
find it reasonable to do otherwise is beyond me.
Sorry if this is just a result of ignorance.
On the other hand, the clumsy type hierarchies of the programming
languages that I am familiar with, are not that impressive either. 
It is not clear that "types" should form a "hierarchy" at all:
integers are not simply a stripped down version of reals, the
ring Z/3 is not just a smaller version of the ring Z/170, etc. etc.