Promise for absense of side effects

[André Thieme]

I like that Clojure is a dynamically typed language.
Even in dynamic languages it is possible to find out a lot more
about the code itself than one may think on a first glance.
Clojure already supports type hints that can make code run
faster. But what if we could add a soft layer of static typing
into the compiler, by making promises to it, which can then be
enforced?
For example, we could promise that foo will always be a string:
(def+ foo "Hello Clojure")

Same for functions, about its parameters and return values.
Note that I am not proposing a concrete syntax here, this is just
a sketch, so we can talk about it:
(defn reverse
"Returns a seq of the items in coll in reverse order. Not lazy."
[#^Collection coll]
(reduce conj () coll))

For all functions in the core.clj which don’t have side effects we
could make this promise. In that case the compiler could check
if foo is ever used in a position where not a string is expected.
And it could check if the return value of a function is an argument
to another function, and then see if those match:

(+ (count foo) 15) ==> 28

(dec foo) ==> compile time error, can't subtract 1 from a String.

(count (count foo)) ==> compile time error, as count returns a
number, not a collection.

This would keep Clojure still extremly dynamic. One exception is:
functions and vars for which we gave promises can’t be changed
anymore during runtime. But these compiler checks would only
be made when in a form there only occur vars/functions which all
made promises about their types. These types can be inferred by
Clojure. For example in (def+ foo "Hi") we see that foo refers to a
string. As Clojure is mostly a functional language anyway it will
not cause much harm that foo can’t be changed anymore.
In principle each var that was def’ed should be seen as a constant.
As long we are debugging our code it can of course make sense
to change those vars.

Anyway, with this proposal a good bit of code can be checked for
type correctness and there is another positive aspect:
the Clojure editors could make use of it.
When we write
(count<space>
the editor will not offer us auto-completion for vars that we promised
to be numbers or microwave objects. This feature would allow the
IDE to do more refactoring and more code completion at edit time.

I am proposing a complete optional mode. Into the metadata one could
add a promise and state the explicit types, or add just an empty
promise
and have the Clojure compiler then to infer the correct times (it
could
give warnings if this were not possible).
This way only people who like these features could use them.
Even if the core.clj and the whole load of clojure-contrib changed in
a
way to fully support soft static typing, then still a user can decides
to
never put promises into his code, and so he wouldn’t even notice that
there is some (soft) mechanism for static typing.

Opinions?

[Raoul Duke]

[Raoul Duke]

ok oops that didn't work, sorry -- i mean to send this link:

http://www.ccs.neu.edu/home/samth/typed-scheme/manual/

[André Thieme]

On 9 Mrz., 20:42, Raoul Duke <rao...@gmail.com> wrote:
> ok oops that didn't work, sorry -- i mean to send this link:
>
> http://www.ccs.neu.edu/home/samth/typed-scheme/manual/

That is not too far away of what I had in mind.
What I would like is if it were even a bit more optional.
Typed Scheme allows to have a specific module statically
typed without having to touch the others. I would like to
go even further, by allowing in the same file/module to
have code as we have it today, and code for which the
compiler can give us support by doing compile time checks.

At two places we would need a hook to add typing
information. This could happen via metadata. Those places
are: variable binding (such as def, let or function
parameters), and the return values of functions.
A global or namespace based switch would be also a nice
thing to have.

[Meikel Brandmeyer]

Hi,

Am 14.03.2009 um 12:38 schrieb André Thieme:

> At two places we would need a hook to add typing
> information. This could happen via metadata. Those places
> are: variable binding (such as def, let or function
> parameters), and the return values of functions.
> A global or namespace based switch would be also a nice
> thing to have.

I remember some presentation of someone doing this for,
I think, Python. There you hint things, where the type is
known and the compiler inferred the rest as far as possible.
What cannot be inferred was cast to a special type called
"dynamic". So this roughly worked like type hints in Clojure.
Just with a bit more inference and "dynamic" meaning
"reflection".

However, I can't seem to find the video anymore. I think
it was a Google techtalk....

How something like this could be implemented, where
some types life in the Java class space while others
exist in the Clojure map space.... I'm not that of a specialist
for language implementation. :)

Sincerely
Meikel

[pmf]

On Mar 14, 1:08 pm, Meikel Brandmeyer <m...@kotka.de> wrote:
> I remember some presentation of someone doing this for,
> I think, Python. There you hint things, where the type is
> known and the compiler inferred the rest as far as possible.
> What cannot be inferred was cast to a special type called
> "dynamic". So this roughly worked like type hints in Clojure.
> Just with a bit more inference and "dynamic" meaning
> "reflection".

Something like that would probably play nice with the JVM's future
invokedynamic-instruction (or the .NET CLI's forthcoming dynamic vars).

[Robert Pfeiffer]

Meikel Brandmeyer schrieb:

> I remember some presentation of someone doing this for,
> I think, Python. There you hint things, where the type is
> known and the compiler inferred the rest as far as possible.
> What cannot be inferred was cast to a special type called
> "dynamic". So this roughly worked like type hints in Clojure.
> Just with a bit more inference and "dynamic" meaning
> "reflection".

Did you mean this:

http://wiki.jvmlangsummit.com/pdf/28_Siek_gradual.pdf

It was presented at the JVM Summit, so Rich may already have given a
thought to this.

[Meikel Brandmeyer]

Hi,

Am 16.03.2009 um 12:26 schrieb Robert Pfeiffer:

> Did you mean this:
>
> http://wiki.jvmlangsummit.com/pdf/28_Siek_gradual.pdf
>
> It was presented at the JVM Summit, so Rich may already have given a
> thought to this.

Argh.. "Gradual Typing" that was term I was missing.

Here some more information.

The Paper (and a unsurprisingly negative discussion) on LtU:
http://lambda-the-ultimate.org/node/1707

And the video of the talk from the above link.
http://video.google.com/videoplay?docid=21835070615692553

I don't know, whether this is useful or not, but if we really want
an optional type system, we should investigate the possibilities,
I think.

Sincerely
Meikel

[André Thieme]

On 16 Mrz., 19:43, Meikel Brandmeyer <m...@kotka.de> wrote:

> Am 16.03.2009 um 12:26 schrieb Robert Pfeiffer:
>
> > Did you mean this:
>
> >http://wiki.jvmlangsummit.com/pdf/28_Siek_gradual.pdf
>
> > It was presented at the JVM Summit, so Rich may already have given a
> > thought to this.
>
> Argh.. "Gradual Typing" that was term I was missing.
>
> Here some more information.
>
> The Paper (and a unsurprisingly negative discussion) on LtU:http://lambda-the-ultimate.org/node/1707
>

> And the video of the talk from the above link.http://video.google.com/videoplay?docid=21835070615692553

>
> I don't know, whether this is useful or not, but if we really want
> an optional type system, we should investigate the possibilities,
> I think.

Oh, that sounds really useful. This is in principle very close
to what I was had in mind in the past years.
The paper says:
“The type system and semantics should place a minimal
implementation burden on language implementors.”

And that also sounds like a good thing.
What I would love to see is an optional system.
With such even hardcore fans of dynamic typing should not have
any problem with it, if Clojure is going to have one.

A thing that should be easy to add is a on/off switch.
Maybe a global one, and a file based one.
Perhaps this gradual typing even allows a gradual implementation.

Would be a nice productivity boost to have the compiler checking
parts of our code during some phases of development.

[Raoul Duke]

please, for those who aren't Erlang nerds, also see Dialyzer.

http://www.it.uu.se/research/group/hipe/dialyzer

[André Thieme]

On 16 Mrz., 23:36, Raoul Duke <rao...@gmail.com> wrote:
> please, for those who aren't Erlang nerds, also see Dialyzer.
>
> http://www.it.uu.se/research/group/hipe/dialyzer

Funny, I just wanted to post exactly that link.
It is very impressive what that tool did:
"Dialyzer has been applied to large code bases,
for example the entire code base of AXD301
consisting of about 2,000,000 lines of Erlang code,
and has identified a significant number of software
defects that have gone unnoticed after years of
extensive testing."

In fact, it is this very tool, the Erlang Dialyzer
that made me start thinking about this whole thing.
The Dialyzer will infer the types from the sources,
without hints of the developers. This means that it
can not find all bugs. But it uses the information
that exists even in a dynamically typed language to
spit out warnings about type problems, but also
about other discrepancies.

If you follow the link, also read the pdfs they put
online, such as:
http://user.it.uu.se/~kostis/Papers/bugs05.pdf
It's just five pages, and written not only for
experts of static type systems.

If the Dialyzer can do all this without having an
optional type system in Erlang, then it should be
obvious what would be possible, if Rich agrees and
finds the time/resources to add one in Clojure.

[Raoul Duke]

> If the Dialyzer can do all this without having an
> optional type system in Erlang, then it should be
> obvious what would be possible, if Rich agrees and
> finds the time/resources to add one in Clojure.

maybe this is a bad/crazy idea, but could one make a pluggable
Dialyzer, which could then be customized to work on any dynamic
language? that could be pretty awesome.

sincerely.

[André Thieme]

Another link that gives an easy understandable intro into
gradual typing:
http://ece-www.colorado.edu/~siek/gradualtyping.html

By adding local and global switches this behaviour could
be made completely optional, allowing everyone to have
as much typing as one wants to have in the code.

Btw, is anyone currently working on any code analysis
tools for Clojure?
Something like the Erlang Dialyzer, or gradual typing?