Re: What is Expressiveness in a Computer Language [correction]

[rossberg]

Joe Marshall wrote:
> Andreas Rossberg wrote:
> >
> > Which is why this actually is a very bad example to chose for dynamic
> > typing advocacy... ;-)
>
> Actually, this seems a *good* example.  The problem seems to be that
> you end up throwing the baby out with the bathwater:  your static type
> system stops catching the errors you want once you make it powerful
> enough to express certain programs.

That is not the case: you can still express these programs, you just
need to do an indirection through a datatype.

- Andreas

-- 
http://mail.python.org/mailman/listinfo/python-list

Re: What is Expressiveness in a Computer Language [correction]

[Joe Marshall]

Andreas Rossberg wrote:
>
>~/> ocaml -rectypes
>  Objective Caml version 3.08.3
>
># let rec blackhole x = blackhole;;
>val blackhole : 'b -> 'a as 'a = 
>
> The problem is, though, that almost everything can be typed once you
> have unrestricted recursive types (e.g. missing arguments etc), and
> consequently many actual errors remain unflagged (which clearly shows
> that typing is not only about potential value class mismatches).
> Moreover, there are very few practical uses of such a feature, and they
> can always be coded easily with recursive datatypes.
>
> It is a pragmatic decision born from experience that you simply do *not
> want* to have this, even though you easily could. E.g. for OCaml,
> unrestricted recursive typing was removed as default because of frequent
> user complaints.
>
> Which is why this actually is a very bad example to chose for dynamic
> typing advocacy... ;-)

Actually, this seems a *good* example.  The problem seems to be that
you end up throwing the baby out with the bathwater:  your static type
system stops catching the errors you want once you make it powerful
enough to express certain programs.

So now it seems to come down to a matter of taste:  use a restricted
language and catch certain errors early or use an unrestricted language
and miss certain errors.  It is interesting that the PLT people have
made this tradeoff as well.  In the DrScheme system, there are
different `language levels' that provide a restricted subset of Scheme.
 At the beginner level, first-class procedures are not allowed.  This
is obviously restrictive, but it has the advantage that extraneous
parenthesis (a common beginner mistake) cannot be misinterpreted as the
intent to invoke a first-class procedure.

-- 
http://mail.python.org/mailman/listinfo/python-list

Re: What is Expressiveness in a Computer Language [correction]

[Andreas Rossberg]

David Hopwood wrote:
>>
>>>(defun blackhole (argument)
>>> (declare (ignore argument))
>>> #'blackhole)

> I believe this example requires recursive types. It can also be expressed
> in a gradual typing system, but possibly only using an unknown ('?') type.
> 
> ISTR that O'Caml at one point (before version 1.06) supported general
> recursive types, although I don't know whether it would have supported
> this particular example.

No problem at all. It still is possible today if you really want:

   ~/> ocaml -rectypes
 Objective Caml version 3.08.3

   # let rec blackhole x = blackhole;;
   val blackhole : 'b -> 'a as 'a = 

The problem is, though, that almost everything can be typed once you 
have unrestricted recursive types (e.g. missing arguments etc), and 
consequently many actual errors remain unflagged (which clearly shows 
that typing is not only about potential value class mismatches). 
Moreover, there are very few practical uses of such a feature, and they 
can always be coded easily with recursive datatypes.

It is a pragmatic decision born from experience that you simply do *not 
want* to have this, even though you easily could. E.g. for OCaml, 
unrestricted recursive typing was removed as default because of frequent 
user complaints.

Which is why this actually is a very bad example to chose for dynamic 
typing advocacy... ;-)

- Andreas
-- 
http://mail.python.org/mailman/listinfo/python-list

Re: What is Expressiveness in a Computer Language [correction]

[David Hopwood]

David Hopwood wrote:
> Joe Marshall wrote:
> 
>>(defun blackhole (argument)
>>  (declare (ignore argument))
>>  #'blackhole)
> 
> This is typeable in any system with universally quantified types (including
> most practical systems with parametric polymorphism); it has type
> "forall a . a -> #'blackhole".

Ignore this answer; I misinterpreted the code.

I believe this example requires recursive types. It can also be expressed
in a gradual typing system, but possibly only using an unknown ('?') type.

ISTR that O'Caml at one point (before version 1.06) supported general
recursive types, although I don't know whether it would have supported
this particular example.

-- 
David Hopwood <[EMAIL PROTECTED]>
-- 
http://mail.python.org/mailman/listinfo/python-list

Re: What is Expressiveness in a Computer Language [correction]

[David Hopwood]

David Hopwood wrote:
> Marshall wrote:
>>David Hopwood wrote:
>>>Marshall wrote:
>>>
The real question is, are there some programs that we
can't write *at all* in a statically typed language, because
they'll *never* be typable?
>>>
>>>In a statically typed language that has a "dynamic" type, all
>>>dynamically typed programs are straightforwardly expressible.

Correction: as the paper on gradual typing referenced below points
out in section 5, something like the "typerec" construct of
 would be
needed, in order for a system with a "dynamic" type to be equivalent
in expressiveness to dynamic typing or gradual typing.

("typerec" can be used to implement "dynamic"; it is more general.)

>>So, how does this "dynamic" type work?
> 
> 
> 
>>It can't simply be the "any" type, because that type has no/few
>>functions defined on it.
> 
> It isn't. From the abstract of the above paper:
> 
>   [...] even in statically typed languages, there is often the need to
>   deal with data whose type cannot be determined at compile time. To handle
>   such situations safely, we propose to add a type Dynamic whose values are
>   pairs of a value v and a type tag T where v has the type denoted by T.
>   Instances of Dynamic are built with an explicit tagging construct and
>   inspected with a type safe typecase construct.
> 
> "Gradual typing" as described in
>  is
> another alternative. The difference between gradual typing and a
> "dynamic" type

This should be: the difference between gradual typing and a system with
"typerec"...

> is one of convenience rather than expressiveness --
> gradual typing does not require explicit tagging and typecase constructs.

-- 
David Hopwood <[EMAIL PROTECTED]>
-- 
http://mail.python.org/mailman/listinfo/python-list