Typed Racket

[ntu...@googlemail.com]

For Racket (formely PLT Scheme), there exists a dialect called "Typed
Racket" [1], which allows for static type checking. I wonder if it is
feasible to port the typechecker to Clojure? Any ideas?

- nt

-----
[1] http://docs.racket-lang.org/ts-guide/index.html

[Mark Engelberg]

The nice thing about Racket is the way you can write different parts
of your program in different Racket languages. So you can write some
pieces in Typed Racket, and others in Lazy Racket, and others in
standard Racket.

It is my understanding that Typed Racket programs do not run any
faster than their dynamically-typed counterparts, and in fact commonly
run slower because there are a lot of additional runtime checks that
must be inserted to handle various types of unsafe calls that can
cross module boundaries or be executed at the REPL. Typed Racket is
purely about safety, not about speed. My guess is that the Clojure
community would have little interest in any version of static typing
that did not provide performance benefits.

[Raoul Duke]

On Wed, Jul 14, 2010 at 3:49 PM, Mark Engelberg
<mark.en...@gmail.com> wrote:
> purely about safety, not about speed.  My guess is that the Clojure
> community would have little interest in any version of static typing
> that did not provide performance benefits.

check out the approach Dialyzer takes for Erlang. would be fun to have
something like that for Clojure, i think.

[Laurent PETIT]

2010/7/15 Mark Engelberg <mark.en...@gmail.com>

Why so ?

Having the *option* to type the programs could be a big sell in the enterprise, and could be seen as a very pragmatic addition to the langage. I suppose here that the type system being pragmatic implies that it remains optional, allows mixed programs to be "composed" as usual, and is not "flawed".
My guess is that
a) it's not easy to come up with something "not flawed"
b) it's not easy to design a type system in such a way that "it does not get in your way" when you don't want to use it (in the REPL, when prototyping, etc.)
c) Even if points a) and b) are solved, it probably requires a vast amount of type to implement, and may not have been considered high priority yet (compared to alll that remains to be added). And also once introduced, it may be seen a potentially "getting in the way" of potential radical improvements.

?

[nickikt]

Hallo all,

Haveing the option of something like that would be nice but atm I
think we should not focus on that. Clojure is still a young language
and there is enought to do.

We should not confuse people with diffrent dialects of clojure
allready.


On Jul 15, 7:10 am, Laurent PETIT <laurent.pe...@gmail.com> wrote:
> 2010/7/15 Mark Engelberg <mark.engelb...@gmail.com>

[Nicolas Oury]

It's a hard problem. Most type-systems forbid the kind of program people write in Clojure

For example (if (keyword? x) ....using the fact that x is a keyword...

would not be typable in many languages. (Or there would be hundreds of special cases)

There is a category of type systems, that can handle this kind of thing: Dependant Types.

(But I am a bit biased, I am a researcher in Dependant Types)

With this kind of type systems, you can formalize something like 

"(keyword? x) = true => x : keyword" 

But they are still research projects, and most of them needs a lot of type annotations.

(Agda is nice, if yo want to try it, though)

It is not very hard to have a type-checker for a sub-cases of correct programs in Clojure.

(Something like ML + protocols, for example)

If other people want to do something, I would happily get involved.

But most programs won't be typable except with a very clever type-checker 

(more clever than the state of the art).

At least, it could be helpful in simple code, to put annotations.

Best,

Nicolas.

[Tomi Neste]

On Thu, Jul 15, 2010 at 10:55 AM, Nicolas Oury <nicola...@gmail.com> wrote:

It's a hard problem. Most type-systems forbid the kind of program people write in Clojure

For example (if (keyword? x) ....using the fact that x is a keyword...

would not be typable in many languages. (Or there would be hundreds of special cases)

Actually the previous example typechecks just fine with Typed Racket. Same with something like

(apply + (filter number? '(1 foo "bar" 2)))

Exactly these kind of cases make Typed Rackets occurrence typing system interesting ( www.ccs.neu.edu/scheme/pubs/popl08-thf.pdf for more details). But I don't think it would be easy to make it work with Clojure, given how polymorphic and dynamic the language is (IMHO Scheme is not too far from ML when it comes to type systems).

--
tomppa

[Nicolas Oury]

On Thu, Jul 15, 2010 at 7:16 PM, Tomi Neste <tomi....@gmail.com> wrote:

www.ccs.neu.edu/scheme/pubs/popl08-thf.pdf

Thanks for the link, I missed that. Looks very interesting.

The filter one is more impressive, because it means that there is no cheating involve, that would not be first-class.

But you're right Clojure is more dynamically used than Scheme.

But the Java interop orientation makes it more accessible to an interesting type system than, say, Ruby, IMHO.

[ntu...@googlemail.com]

On Jul 15, 8:16 pm, Tomi Neste <tomi.ne...@gmail.com> wrote:
> But I don't think it would be easy to make it work with Clojure,
> given how polymorphic and dynamic the language is (IMHO Scheme is not too
> far from ML when it comes to type systems).

Please expand.

- nt

[Frederick Polgardy]

A big part of it is that Clojure, being based on the JVM, has to deal with inheritance and polymorphism in the core type system. An algebraic type system like that of Haskell, OCaml, Scheme doesn't have to deal with inheritance. There is parametric polymorphism, but that's based on type classes, not inheritance.

-Fred

--
Science answers questions; philosophy questions answers.

> --
> You received this message because you are subscribed to the Google
> Groups "Clojure" group.
> To post to this group, send email to clo...@googlegroups.com
> Note that posts from new members are moderated - please be patient with your first post.
> To unsubscribe from this group, send email to
> clojure+u...@googlegroups.com
> For more options, visit this group at
> http://groups.google.com/group/clojure?hl=en

[Tomi Neste]

Compared to Clojure there are very few polymorphic functions in standard Scheme, for example, there are no generic sequence handling functions (instead you use list-ref, string-ref etc.). Usually defining a structure type creates getter and setter functions specific to the structure type. Most type errors are quickly caught during runtime, as opposed to more dynamic languages where 'type errors' can easily spread through program (common experience for me with Clojure has been that these errors aren't noticed until I hit Java level at some point).

Of course being a lisp Scheme is easily extended with more dynamic features but many 'regular' Scheme programs are well typed, some even under H-M style system and the rest with Typed Scheme/Racket.

There are different kinds of dynamic typing, Scheme being in the more strict end, at the other end you have languages like Clojure and Python. With Common Lisp some where in the middle. 

--
tomppa

[Eli Barzilay]

Mark Engelberg <mark.en...@gmail.com> writes:

> It is my understanding that Typed Racket programs do not run any
> faster than their dynamically-typed counterparts, and in fact
> commonly run slower because there are a lot of additional runtime
> checks that must be inserted to handle various types of unsafe calls
> that can cross module boundaries or be executed at the REPL. Typed

> Racket is purely about safety, not about speed. [...]

1. The dynamic type checks are contracts, which happen only on
interaction between typed and untyped code. The cost is therefore
not larger than the cost of contracts, and if you're talking about
code inside a single module, or involving several typed ones, then
there is no runtime cost at all.

2. Typed Racket used to be only about safety, but there's no intention
to avoid using it for speed. Recently there has been work invested
in making statically-typed code use unsafe operations, which can
make code run significantly faster. It's not publicly advertised,
yet, but it's not too far from it.

--
((lambda (x) (x x)) (lambda (x) (x x))) Eli Barzilay:
http://barzilay.org/ Maze is Life!