Python from Wise Guy's Viewpoint

[prunesquallor@comcast.net]

Re: Python from Wise Guy's Viewpoint

Ed Avis <ed@membled.com > writes:
[color=blue]
> prunesquallor@c omcast.net writes:
>[color=green]
>>What would you like to call those `syntactic constructs' that do not
>>currently type check in Haskell, yet *may* belong to a class of
>>syntactic constructs that *could* conceivably be type checked in a
>>successor to Haskell that has a better type inferencing engine?[/color]
>
> Well of course, if you program in a different language you'd need a
> different type checking system.[/color]

Obviously.

But let us suppose that someone improved the type system of Haskell
such that some useful complicated constructs that did not pass the
type checker were now able to be verified as correct. Didn't this
happen when Haskell was extended with second-order polymorphic types?
(when the restriction on forall was lifted?)

You could say that lifting this restriction created a `new' language
and refuse to admit the notion that two are related, or you might take
the viewpoint that some programs that were invalid before are now
valid. The former point becomes rather strained if you have some sort
of switch on the implementation.

For instance, OCaml allows recursive function types if you specify
that you want them. Most people seem to view this as

`OCaml with recursive function types'

instead of

`completely new language unrelated to OCaml, but sharing the exact
same syntax in all places except for declaration of recursive function
types.'

And most people seem to think that my `black hole' `syntactic
construct', which does not type check under OCaml without the flag,
but *does* under OCaml with the flag, can be unambiguously called a
`program'.

[Ed Avis]

Re: Python from Wise Guy's Viewpoint

prunesquallor@c omcast.net writes:
[color=blue]
>But let us suppose that someone improved the type system of Haskell
>such that some useful complicated constructs that did not pass the
>type checker were now able to be verified as correct.[/color]

Wouldn't you need to define the semantics for these constructs too?
And perhaps extend the compiler to generate code for them?

My original point was that the type-checker won't reject programs
which are valid Haskell, so it makes no sense to talk about the
checker being too strict or not allowing enough flexibility. A
type-checker for some other language such as Lisp would obviously have
to not flag errors for any legal Lisp program. (That would probably
mean not checking anything at all, with the programmer having to
explicitly state 'yes I don't want to wait until runtime to catch this
error'.)

--
Ed Avis <ed@membled.com >

[prunesquallor@comcast.net]

Re: Python from Wise Guy's Viewpoint

Ed Avis <ed@membled.com > writes:
[color=blue]
> prunesquallor@c omcast.net writes:
>[color=green]
>>But let us suppose that someone improved the type system of Haskell
>>such that some useful complicated constructs that did not pass the
>>type checker were now able to be verified as correct.[/color]
>
> Wouldn't you need to define the semantics for these constructs too?
> And perhaps extend the compiler to generate code for them?
>
> My original point was that the type-checker won't reject programs
> which are valid Haskell, so it makes no sense to talk about the
> checker being too strict or not allowing enough flexibility.[/color]

So any program that currently runs on Haskell will run on the very
first version of Haskell? No? But Haskell won't reject programs that
are valid Haskell, so is the later version wrong?

[Fergus Henderson]

Re: Python from Wise Guy's Viewpoint

prunesquallor@c omcast.net writes:
[color=blue]
>Fergus Henderson <fjh@cs.mu.oz.a u> writes:
>[color=green]
>> But the difference between dynamically typed languages and
>> statically typed languages is that in dynamically typed languages, *every*
>> data access (other than just copying data around) involves a dynamic dispatch.
>> Sure, implementations can optimize a lot of them away. But generally you're
>> still left lots that your implementation can't optimize away, but which
>> would not be present in a statically typed language, such as the O(N)
>> dynamic type checks in the example above.[/color]
>
>That's what the type-checking hardware is for.[/color]

Did you forget a smiley?

In case not: type-checking hardware has been tried already, and failed.

(Anyway, type-checking hardware would only solve part of the problem, I think.
Dynamic type checking imposes two costs: one is the time cost of performing
the checks, and the other is the locality cost due to the code size increase.
Type-checking hardware avoids the code size increases, but I don't think it
helps with the time cost of performing the checks.)

--
Fergus Henderson <fjh@cs.mu.oz.a u> | "I have always known that the pursuit
The University of Melbourne | of excellence is a lethal habit"
WWW: <http://www.cs.mu.oz.au/~fjh> | -- the last words of T. S. Garp.

[Joachim Durchholz]

Re: Python from Wise Guy's Viewpoint

prunesquallor@c omcast.net wrote:[color=blue]
>
> And most people seem to think that my `black hole' `syntactic
> construct', which does not type check under OCaml without the flag,
> but *does* under OCaml with the flag, can be unambiguously called a
> `program'.[/color]

I'm still hoping for an explanation on the practical relevance of that
black hole device.
I don't insist that the black hole function as given does anything
useful; if the black-hole function was just a condensed example of a
general usage pattern, I'd like to know what that pattern is. It would
help me to find out where in the expressivity spectrum the various
languages lie.

Regards,
Jo

[prunesquallor@comcast.net]

Re: Python from Wise Guy's Viewpoint

Fergus Henderson <fjh@cs.mu.oz.a u> writes:
[color=blue]
> prunesquallor@c omcast.net writes:
>[color=green]
>>Fergus Henderson <fjh@cs.mu.oz.a u> writes:
>>[color=darkred]
>>> But the difference between dynamically typed languages and
>>> statically typed languages is that in dynamically typed languages, *every*
>>> data access (other than just copying data around) involves a dynamic dispatch.
>>> Sure, implementations can optimize a lot of them away. But generally you're
>>> still left lots that your implementation can't optimize away, but which
>>> would not be present in a statically typed language, such as the O(N)
>>> dynamic type checks in the example above.[/color]
>>
>>That's what the type-checking hardware is for.[/color]
>
> Did you forget a smiley?[/color]

No, I never use smileys.
[color=blue]
> In case not: type-checking hardware has been tried already, and failed.[/color]

News to me. I've used type checking hardware and it works like a charm.
[color=blue]
> (Anyway, type-checking hardware would only solve part of the problem, I think.
> Dynamic type checking imposes two costs: one is the time cost of performing
> the checks, and the other is the locality cost due to the code size increase.
> Type-checking hardware avoids the code size increases, but I don't think it
> helps with the time cost of performing the checks.)[/color]

Actually it works quite well with performing the checks. In general,
type checking is much quicker than computation, and in general it can
be performed in parallel with computation (you simply discard the
bogus result if it fails). You don't need very much hardware, either.

[prunesquallor@comcast.net]

Re: Python from Wise Guy's Viewpoint

Joachim Durchholz <joachim.durchh olz@web.de> writes:
[color=blue]
> prunesquallor@c omcast.net wrote:[color=green]
>> And most people seem to think that my `black hole' `syntactic
>> construct', which does not type check under OCaml without the flag,
>> but *does* under OCaml with the flag, can be unambiguously called a
>> `program'.[/color]
>
> I'm still hoping for an explanation on the practical relevance of that
> black hole device.[/color]

Neel Krishnaswami had a wonderful explanation in article
<slrnbplpv6.ikr .neelk@gs3106.s p.cs.cmu.edu>

[Ed Avis]

Re: Python from Wise Guy's Viewpoint

prunesquallor@c omcast.net writes:
[color=blue][color=green]
>>My original point was that the type-checker won't reject programs
>>which are valid Haskell, so it makes no sense to talk about the
>>checker being too strict or not allowing enough flexibility.[/color]
>
>So any program that currently runs on Haskell will run on the very
>first version of Haskell?[/color]

I should have said 'Haskell 98' and 'a type-checker in a working
Haskell 98 implementation' .

The same applies to any language, of course - Haskell 98 is just an
example. What I mean is don't shoot the messenger if the type checker
tells you your program is invalid. You might however want to change
to a different language (such as a later version of Haskell, or one
with nonstandard extensions) where your program is valid (and of
course the typechecker for that implementation will be happy).

--
Ed Avis <ed@membled.com >

[Greg Menke]

Re: Python from Wise Guy's Viewpoint


prunesquallor@c omcast.net writes:
[color=blue]
> Fergus Henderson <fjh@cs.mu.oz.a u> writes:
>[color=green]
> > prunesquallor@c omcast.net writes:
> >[color=darkred]
> >>Fergus Henderson <fjh@cs.mu.oz.a u> writes:
> >>[/color]
> > (Anyway, type-checking hardware would only solve part of the problem, I think.
> > Dynamic type checking imposes two costs: one is the time cost of performing
> > the checks, and the other is the locality cost due to the code size increase.
> > Type-checking hardware avoids the code size increases, but I don't think it
> > helps with the time cost of performing the checks.)[/color]
>
> Actually it works quite well with performing the checks. In general,
> type checking is much quicker than computation, and in general it can
> be performed in parallel with computation (you simply discard the
> bogus result if it fails). You don't need very much hardware, either.[/color]

As is also amply demonstrated by ECC hardware that operates right
alongside the memory- considerably easier than doing it in software.

Gregm

[Lex Spoon]

Re: Python from Wise Guy's Viewpoint

>>>It sounds unbelievable, but it really works.[color=blue][color=green]
>> I believe you. I have trouble swallowing claims like `It is never
>> wrong, always completes, and the resulting code never has a run-time
>> error.' or `You will never need to run the kind of code it doesn't allow.'[/color]
>
> This kind of claim comes is usually just a misunderstandin g.
> For example, the above claim indeed holds for HM typing - for the
> right definitions of "never wrong" and "never has an error".
>
> HM typing "is never wrong and never has a run-time error" in the
> following sense: the algorithm will never allow an ill-typed program
> to pass, and there will never be a type error at run-time. However,
> people tend to overlook the "type" bit in the "type error" term, at
> which point the discussion quickly degenerates into discourses of
> general correctness.[/color]


It is misleading to make this claim without a lot of qualification.
It requires careful, technical definitions of "type" and "type error"
that are different from what an unprepared audience will expect.


For example, it is not considered a type error if you get the wrong
branch of a datatype. So if you define:

datatype sexp = Atom of string | Cons of (sexp, sexp)

fun car (Cons (a,b)) = a

then the following would not be considered a "type error" :

car (Atom "hello")



To add to the situation, HM flags extra errors, too, that many people
would not consider "type errors" but which are for HM's purposes. For
example, it is considered a type error if two branches of an "if" do
not match, even if one branch is impossible or if the later code can
remember which branch was followed. For example:

val myint : int =
if true
then 0
else "hello"


or more interestingly:

val (tag, thingie) =
if (whatever)
then (0, 1)
else (1, 1.0)

val myotherstuff =
if tag = 0
then (tofloat thingie) + 1.5
else thingie + 1.5


In common parlance, as opposed to the formal definitions of "type
error", HM both overlooks some type errors and adds some others. It
is extremely misleading to claim, in a non-technical discussion, that
HM rejects precisely those programs that have a type error. The
statement is actually false if you use the expected meanings of "type
error" and "type".


All this said, I agree that HM type inference is a beautiful thing and
that it has significant benefits. But the benefit of removing type
errors is a red herring--both in practice and, as described in this
post, in theory as well.

-Lex

[Joachim Durchholz]

Re: Python from Wise Guy's Viewpoint

prunesquallor@c omcast.net wrote:[color=blue]
> Neel Krishnaswami had a wonderful explanation in article
> <slrnbplpv6.ikr .neelk@gs3106.s p.cs.cmu.edu>[/color]

Sorry, that link doesn't work for me, I don't know the proper syntax for
news: links, and I couldn't type one in even if I knew it.

Anybody got a full reference? This thread is too long for searching...

Regards,
Jo

[Emile van Sebille]

Re: Python from Wise Guy's Viewpoint

"Joachim Durchholz" asks:[color=blue]
> prunesquallor@c omcast.net wrote:[color=green]
> > Neel Krishnaswami had a wonderful explanation in article
> > <slrnbplpv6.ikr .neelk@gs3106.s p.cs.cmu.edu>[/color]
>
> Sorry, that link doesn't work for me, I don't know the proper syntax for
> news: links, and I couldn't type one in even if I knew it.
>[/color]

I prepend:

http://groups.google.com/groups?selm=

in this case yielding

http://groups.google.com/groups?selm=slrnbplpv6.ikr.neelk@gs3106.sp.cs.cmu.edu

Emile van Sebille
emile@fenx.com

[Dirk Thierbach]

Re: Python from Wise Guy's Viewpoint

Lex Spoon <lex@cc.gatech. edu> wrote:
[color=blue]
> To add to the situation, HM flags extra errors, too, that many people
> would not consider "type errors" but which are for HM's purposes. For
> example, it is considered a type error if two branches of an "if" do
> not match, even if one branch is impossible or if the later code can
> remember which branch was followed.[/color]
[...][color=blue]
> val (tag, thingie) =
> if (whatever)
> then (0, 1)
> else (1, 1.0)
>
> val myotherstuff =
> if tag = 0
> then (tofloat thingie) + 1.5
> else thingie + 1.5[/color]

The point here is of course that you "glue together" the tag
and the value, with the additional side effect that this documents
your intention. So you would write in this case

data Thingie = Tag0 Integer | Tag1 Float

and then you can write

myfirststuff whatever = if whatever then Tag0 1 else Tag1 1.0

myotherstuff (Tag0 thingie) = (fromInteger thingie) + 1.5
myotherstuff (Tag1 thingie) = thingie + 1.5

Then the type checker will happily infer that

myfirststuff :: Bool -> Thingie and
myotherstuff :: Thingie -> Float

So you indeed have to express your tags a bit differently. Is this
asking too much? Is that so inconvient, especially when you get a
good documention of your intentions for free?

- Dirk

[Joachim Durchholz]

Re: Python from Wise Guy's Viewpoint

Emile van Sebille wrote:[color=blue]
> "Joachim Durchholz" asks:
>[color=green]
>>prunesquallor @comcast.net wrote:
>>[color=darkred]
>>>Neel Krishnaswami had a wonderful explanation in article
>>> <slrnbplpv6.ikr .neelk@gs3106.s p.cs.cmu.edu>[/color]
>>
>>Sorry, that link doesn't work for me, I don't know the proper syntax for
>>news: links, and I couldn't type one in even if I knew it.
>>[/color]
>
>
> I prepend:
>
> http://groups.google.com/groups?selm=[/color]

Got it - thanks!

Regards,
Jo

[Fergus Henderson]

Re: Python from Wise Guy's Viewpoint

Pascal Costanza <costanza@web.d e> writes:
[color=blue]
>- The important thing here is that the EMLOYED mixin works on any class,
>even one that is added later on to a running program. So even if you
>want to hire martians some time in the future you can still do this.[/color]

What happens if the existing class defines a slot named "salary" or "company",
but with a different meaning? Are slot names global, or is there some sort
of namespace control to prevent this kind of accidental name capture?

Anyway, regarding how to write this example in a statically typed
language: you can do this in a quite straight-forward manner,
by just keeping a separate table of employees.
For example, here it is in Java.

import java.util.*;
public class Employed {
static String default_company = "constanz-inc";

static class Employee {
public Object obj;
public String company;
public int salary;
public Employee(Object o, String c, int s) {
company = c;
salary = s;
obj = o;
}
}

static Hashtable employees = new Hashtable();

static void hire(Object obj, int salary) {
hire(obj, salary, default_company );
}
static void hire(Object obj, int salary, String company) {
employees.put(o bj, new Employee(obj, company, salary));
}
static void fire(Object obj) {
employees.remov e(obj);
}

static void test_employed() {
class Person {
public String name;
Person(String n) { name = n; }
};
Person joe = new Person("joe");
System.out.prin tln("-> hire joe");
hire(joe, 60000);
System.out.prin tln("name: " + joe.name);
System.out.prin tln("class: "
+ joe.getClass(). getName());
Employee e = (Employee) employees.get(j oe);
System.out.prin tln("employed: " +
(e != null ? "yes" : "no"));
System.out.prin tln("company: " + e.company);
System.out.prin tln("salary: " + e.salary);
System.out.prin tln("-> fire joe");
fire(joe);
if (employees.cont ains(joe)) {
System.out.prin tln("joe is still employed.");
} else {
System.out.prin tln(
"joe is not employed anymore.");
}
}

public static void main(String args[]) {
test_employed() ;
}
}

As you can see, there's no need here for dynamically changing the types of
objects at runtime or for creating classes at runtime. But you can employ
Martians or any other object.

This example makes use of one dynamic cast; that's because the Java
type system doesn't support generics / parametric polymorphism. It would
be a little nicer to do this in a language which supported generics, then
we could use `Hashtable<Obje ct, Employee>' rather than just `Hashtable',
and there wouldn't be any need for the dynamic cast to `(Employee)'.

--
Fergus Henderson <fjh@cs.mu.oz.a u> | "I have always known that the pursuit
The University of Melbourne | of excellence is a lethal habit"
WWW: <http://www.cs.mu.oz.au/~fjh> | -- the last words of T. S. Garp.