[racket] Typed Racket vs. Haskell

[thor...@lavabit.com]

Hi,

I'm a beginner, but I have some experience with Scheme and Haskell.

Haskell is famous for its strict type system. Is it possible to achieve
this in a Lisp-like language? Is Typed Racket as strict as Haskell?

I'd like to see a comparison between the two.

(Please don't refer me to the docs. Because I'm not very experienced it
might take too long to understand the type system of Typed Racket.)

P.S. I've also heard that Common Lisp supports static typing. I'll
appreciate an overview of its type system too (compared to the mentioned
languages), but it's not the main topic of this thread.


____________________
Racket Users list:
http://lists.racket-lang.org/users

[John Clements]

On Sep 18, 2012, at 8:30 AM, thor...@lavabit.com wrote:

> Hi,
>
> I'm a beginner, but I have some experience with Scheme and Haskell.
>
> Haskell is famous for its strict type system. Is it possible to achieve
> this in a Lisp-like language? Is Typed Racket as strict as Haskell?
>
> I'd like to see a comparison between the two.

Both Haskell and Typed Racket come from the Programming Languages community, and their type systems both arise from the same chain of research. They are both "type safe" systems (unlike, say, C), in that they produce proofs that some set of "bad things" can't happen.

With that said, Haskell and Typed Racket represent two different "attitudes" within that design space: Haskell takes the attitude that the type system is a fundamental part of the program design, and typed Racket takes the attitude that the program comes first, and the type system's job is to check that nothing is going to go wrong.

At a jargon level, you could say that Haskell has a Hindley-Milner type system, and that Racket uses "occurrence typing", if that's at all helpful.

When comparing type systems, it's extremely important to qualify opinions: the above two paragraphs (especially the first) are my opinion only.

John Clements

[Vincent St-Amour]

At Tue, 18 Sep 2012 09:55:36 -0700,

John Clements wrote:
> On Sep 18, 2012, at 8:30 AM, thor...@lavabit.com wrote:
>
> > Hi,
> >
> > I'm a beginner, but I have some experience with Scheme and Haskell.
> >
> > Haskell is famous for its strict type system. Is it possible to achieve
> > this in a Lisp-like language? Is Typed Racket as strict as Haskell?
> >
> > I'd like to see a comparison between the two.
>
> Both Haskell and Typed Racket come from the Programming Languages
> community, and their type systems both arise from the same chain of
> research. They are both "type safe" systems (unlike, say, C), in that
> they produce proofs that some set of "bad things" can't happen.

Common Lisp falls in roughly the same category as C here. The compiler
does some compile-time checking and can detect some type errors, but it
errs on the side of trusting the programmer, which can lead to type
errors that other type systems would prevent.

> With that said, Haskell and Typed Racket represent two different
> "attitudes" within that design space: Haskell takes the attitude that
> the type system is a fundamental part of the program design, and typed
> Racket takes the attitude that the program comes first, and the type
> system's job is to check that nothing is going to go wrong.

It's also possible to write Typed Racket programs "types first", like
one would in Haskell, and I sometimes do. The "sums-of-products"
programming style of Haskell and ML can be expressed easily with Typed
Racket's structs and union types. You can also mix and match between
"Haskell" and "Racket" styles of programming, and it will all work.

You can even take this "mix and match" approach even further, and mix
typed and untyped code. Typed Racket modules can interact with untyped
Racket modules and contract checks at the boundary will prevent untyped
code from breaking the typed code. This is very handy, and is probably
the Typed Racket feature I find myself missing the most when programming
in Haskell or ML.

Some Typed Racket features provide flexibility that Haskell cannot
express, while keeping everything safe. For example, Typed Racket
supports variable arity functions (like Racket's `+', `list', `map',
etc.), dynamic type checks, optional and keyword arguments, etc.

Of course, Haskell also provides type system features that Typed Racket
does not, such as type classes or type-level programming.

Vincent

[thor...@lavabit.com]

> It's also possible to write Typed Racket programs "types first", like
> one would in Haskell, and I sometimes do. The "sums-of-products"
> programming style of Haskell and ML can be expressed easily with Typed
> Racket's structs and union types. You can also mix and match between
> "Haskell" and "Racket" styles of programming, and it will all work.

Are you talking about this?

We have already seen the : type annotation form. This is useful for
definitions, at both the top level of a module

(: x Number)
(define x 7)

and in an internal definition

(let ()
  (: x Number)
  (define x 7)
  (add1 x))

http://docs.racket-lang.org/ts-guide/more.html#(part._.Annotating_.Definitions)

> You can even take this "mix and match" approach even further, and mix
> typed and untyped code. Typed Racket modules can interact with untyped
> Racket modules and contract checks at the boundary will prevent untyped
> code from breaking the typed code. This is very handy, and is probably
> the Typed Racket feature I find myself missing the most when programming
> in Haskell or ML.

Very interesting.
I'm going to write a library. I want it to be available for the largest
number of people.
Can other Lisp-like languages (e.g. Guile) use libraries written in Typed
Racket?

> Of course, Haskell also provides type system features that Typed Racket
> does not, such as type classes or type-level programming.

Is there a need for such features in Typed Racket?
Is it possible to implement them?
Is there a plan to implement them?

[thor...@lavabit.com]

I forgot to ask about performance.
I know that all benchmarks lie, but which one is faster: Haskell or Typed
Racket?

[Raoul Duke]

http://shootout.alioth.debian.org/u32/benchmark.php?test=all&lang=racket&lang2=ghc

[Matthias Felleisen]

Haskell is a mature, 20-year old compiler.

Typed Racket is an evolving, 3-year old language for which we have only recently turned to performance issues. Also it runs atop a jit compiler that does not know anything about types. We need to develop new and different ways to perform optimizations. Nevertheless, the performance of TR programs is quite decent and may beat Haskell on occasion.

;; ---

Typed Racket is designed for Racket. One day Guile will have a Typed Guile companion, and Chez Scheme may have a Typed Chez companion but until then TR is for Racket.

[Vincent St-Amour]

At Tue, 18 Sep 2012 16:08:29 -0400 (EDT),

thor...@lavabit.com wrote:
>
> > It's also possible to write Typed Racket programs "types first", like
> > one would in Haskell, and I sometimes do. The "sums-of-products"
> > programming style of Haskell and ML can be expressed easily with Typed
> > Racket's structs and union types. You can also mix and match between
> > "Haskell" and "Racket" styles of programming, and it will all work.
>
> Are you talking about this?

I'm mostly talking about different ways to structure data.

In Haskell, you would structure data like this:

data Tree = Branch Tree Tree
| Leaf Integer

A direct Typed Racket translation is:

(define-type Tree (U Branch Leaf))
(struct: Branch ([left : Tree] [right : Tree]))
(struct: Leaf ([val : Integer]))

The same program, written "Racket-style":

(define-type Tree (U Branch Integer))
(struct: Branch ([left : Tree] [right : Tree]))

Typed Racket's union types makes it possible to write this program
without the extra constructor. In this example, the savings are small,
but it can simplify code a lot in larger cases.

> > You can even take this "mix and match" approach even further, and mix
> > typed and untyped code. Typed Racket modules can interact with untyped
> > Racket modules and contract checks at the boundary will prevent untyped
> > code from breaking the typed code. This is very handy, and is probably
> > the Typed Racket feature I find myself missing the most when programming
> > in Haskell or ML.
>
> Very interesting.
> I'm going to write a library. I want it to be available for the largest
> number of people.
> Can other Lisp-like languages (e.g. Guile) use libraries written in Typed
> Racket?

Typed Racket can interact with other languages in the Racket ecosystem.
This does not include Guile.

> > Of course, Haskell also provides type system features that Typed Racket
> > does not, such as type classes or type-level programming.
>
> Is there a need for such features in Typed Racket?
> Is it possible to implement them?
> Is there a plan to implement them?

As John said, Typed Racket has a different philosophy than Haskell. Some
of Haskell's features would not make sense in Typed Racket. Others
provide functionality that would be nice to have (e.g. type classes),
but it's unclear whether Haskell's solutions would be appropriate in our
case. Feature parity with Haskell is explicitly not a goal for Typed
Racket.

If you're looking for a cool typed language with interesting new ideas
that bring the best of typed and untyped languages together, then you'll
love Typed Racket. If you're looking for a Haskell relative, Typed
Racket may not be for you.

Vincent

[David Van Horn]

On 9/18/12 4:08 PM, thor...@lavabit.com wrote:
>> It's also possible to write Typed Racket programs "types first", like
>> one would in Haskell, and I sometimes do. The "sums-of-products"
>> programming style of Haskell and ML can be expressed easily with Typed
>> Racket's structs and union types. You can also mix and match between
>> "Haskell" and "Racket" styles of programming, and it will all work.
>
> Are you talking about this?
>
> We have already seen the : type annotation form. This is useful for
> definitions, at both the top level of a module
>
> (: x Number)
> (define x 7)
>
> and in an internal definition
>
> (let ()
> (: x Number)
> (define x 7)
> (add1 x))
>
> http://docs.racket-lang.org/ts-guide/more.html#(part._.Annotating_.Definitions)

No, by "types first" I think John and Vincent are talking about a
conceptual order. I would phrase it a little more subtly: an ML (or
Haskell) programmer writes their types, then their programs (as you
must); a TR programmer thinks about their data, writes down a program,
then writes down the types (describing the data) they had in mind in the
first place (and often were written down as comments). Vincent is
pointing out that writing TR programs in the other order works just
fine, too. The flexibility is one of the best things about TR: you get
to choose how much of your program is typed and this can evolve over time.

There's also a style to types that's different. Since Racket
programmers often think in terms of union types, it was really important
TR supported union types. It was also important to support the kind of
control flow based on predicates that discriminate between members of a
union, hence the occurrence typing features. In ML or Haskell, you
would instead use _disjoint_ unions and pattern matching against
constructors. As Vincent said, you can program in that style in TR,
too, but that style is often not what you would have written in Racket
in the first place.

A good exercise to get the feel of both styles is to develop a data
definition for XML expressions or something similar. Try it out first
in Racket, then TR. Then re-develop the program in Haskell. You'll
notice that in one, you probably have something like

;; A XExpr is one of
;; - String
;; - Number
;; - ...

and programs look like:

(define (xexpr-function x)
(cond [(string? x) ... x is a string]
[(number? x) ... x is a number]
...))

And in the other you'll have (OK, ML since I know it better):

datatype XExpr = Str of string | Num of real | ...

and programs:

fun xexprfunction Str(s) = ... s is a string
| xexprfunction Num(n) = ... n is a real
| ...

The latter style you can always recreate in TR using structs and match,
but the other direction won't work.

David

[Raoul Duke]

> No, by "types first" I think John and Vincent are talking about a conceptual
> order. I would phrase it a little more subtly: an ML (or Haskell)
> programmer writes their types, then their programs (as you must); a TR
> programmer thinks about their data, writes down a program, then writes down
> the types (describing the data) they had in mind in the first place (and
> often were written down as comments).

i don't fully grok this but i'd guess there are other things going on as well.

i'm not sure what you mean by "as you must" since ml/haskell have type
inference.

i think it could be more that in non T Racket, you *cannot* use types
to do the work, so you have to "manually" do it with predicates.
whereas in typed languages, presumably you *want* to make use of the
types, because then you are getting static checking e.g. that you've
tested all constructors or whatever (not sure if/how that in
particular would work in ml/haskell, but in e.g. haxe the switch will
warn you if you miss a case).

?

[David Van Horn]

On 9/18/12 4:59 PM, Raoul Duke wrote:
>> No, by "types first" I think John and Vincent are talking about a conceptual
>> order. I would phrase it a little more subtly: an ML (or Haskell)
>> programmer writes their types, then their programs (as you must); a TR
>> programmer thinks about their data, writes down a program, then writes down
>> the types (describing the data) they had in mind in the first place (and
>> often were written down as comments).
>
> i don't fully grok this but i'd guess there are other things going on as well.
>
> i'm not sure what you mean by "as you must" since ml/haskell have type
> inference.

Yes, but you can't infer the _definitions_ of types. So what I meant
was, you must define your types before writing programs. In Racket, you
can just think about a class of data (e.g. "all the numbers and
strings") and write a program that operates on that data without having
to first define the type that means either a number or a string. If you
want to come back to that program later and make a TR program by writing
defining the type.

> i think it could be more that in non T Racket, you *cannot* use types
> to do the work, so you have to "manually" do it with predicates.
> whereas in typed languages, presumably you *want* to make use of the
> types, because then you are getting static checking e.g. that you've
> tested all constructors or whatever (not sure if/how that in
> particular would work in ml/haskell, but in e.g. haxe the switch will
> warn you if you miss a case).

I'm not sure what you mean. You get a similar guarantee in TR.

#lang typed/racket
(: f ((U String Number) -> String))
(define (f a)
(cond [(string? a) a]))

This doesn't type check because it's missing a case for numbers.

David

[Raoul Duke]

> Yes, but you can't infer the _definitions_ of types. So what I meant was,
> you must define your types before writing programs. In Racket, you can just
> think about a class of data (e.g. "all the numbers and strings") and write a

not sure this is a black and white situation; seems like haskell/ml
have some pre-defined types that would already be covered, have
operations, be inferrable from the operations used.

>> i think it could be more that in non T Racket, you *cannot* use types

> I'm not sure what you mean. You get a similar guarantee in TR.

i didn't write it well enough, apologies -- "non T Racket" meaning
"non-Typed Racket" as in old-school Racket, before TR existed.

sincerely.

[Eli Barzilay]

Yesterday, thor...@lavabit.com wrote:
>
> I'm going to write a library. I want it to be available for the
> largest number of people. Can other Lisp-like languages
> (e.g. Guile) use libraries written in Typed Racket?

And Matthias Felleisen replied:

>
> Typed Racket is designed for Racket. One day Guile will have a Typed
> Guile companion, and Chez Scheme may have a Typed Chez companion but
> until then TR is for Racket.

I see on the Guile list that you (thorsopia) took the above the wrong
way. Developing statically typed code in TR and making it work later
on other Scheme implementations should be easy, since the TR type
system is intended to allow the same style of code that is used in
Racket, which is also similar to the style in other scheme
implementations. The required "translation" step will be mostly
removing the type declarations. Doing the same with Haskell etc would
most likely be much harder.

[The big caveat in the above is independent of TR: it's the usual one
about "Scheme" being a kind of a shrunked skeleton of a language core,
vs Racket being a practical tool. The effort of writing some
"portable Scheme" can get to the point where you'd just as well go
with Haskell or raw machine code...]

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

[thor...@lavabit.com]

> Developing statically typed code in TR and making it work later
> on other Scheme implementations should be easy, since the TR type
> system is intended to allow the same style of code that is used in
> Racket, which is also similar to the style in other scheme
> implementations.

Actually, this is what I was asking about.
(Guile people told me to use C or bins, but I don't want to go that deep.)

> The required "translation" step will be mostly
> removing the type declarations. Doing the same with Haskell etc would
> most likely be much harder.

Is it possible not to remove types?
Vincent told me that one can "mix typed and untyped code" in Racket.
How it's done in Racket (the implementation details)? How these modules
interact? Could you give me some pointers?
Why it's not possible in other Lisp-like languages (e.g. Guile)?

[Matthias Felleisen]

On Sep 20, 2012, at 2:41 AM, thor...@lavabit.com wrote:

> Is it possible not to remove types?
> Vincent told me that one can "mix typed and untyped code" in Racket.
> How it's done in Racket (the implementation details)? How these modules interact? Could you give me some pointers?

1. Typed Racket programs do not rely on their types for semantics. Types are syntactic entities (as they should be) and they do not play a role for the execution of completely typed TR programs.

2. You can turn type checking off for TR programs, and then types are just comments. [I do not know whether their syntax is checked.]

3. You can also remove type annotations quite easily and get a Racket program out of it.

[**] A TR module can call functions from an R module and vice versa. The key to our work is that this mutual calling mechanism is TYPE-SAFE (meaning we proved a type soundness theorem for the mix, and if you find a program that crashes, it is a bug in our implementation. In the limit, we will eliminate all such bugs.) -- The mechanism for accomplishing type safety is to translate types (which are merely syntax) into run-time assertions. The latter ensure that when an R module calls an (Int -> Int) function from an R module, the argument is an integer. Or when it is an ((Int -> Int) -> String) function, it checks that the argument is an (Int -> Int) function. This part is quite novel and based on reasonably recent research.

> Why it's not possible in other Lisp-like languages (e.g. Guile)?

All of the above is possible in all other Lisp-like languages, e.g., Guile, Python, Perl, Clojure to name a few.

It will take some work to reach the soundness level explained in [**]. For example, Common Lisp has the first three properties [1-3], it doesn't have [**]. At this point I am not aware of any Lisp-y language that accomplishes [1-3] + [**].

[Vincent St-Amour]

At Thu, 20 Sep 2012 02:41:02 -0400 (EDT),

thor...@lavabit.com wrote:
> > The required "translation" step will be mostly
> > removing the type declarations. Doing the same with Haskell etc would
> > most likely be much harder.
>
> Is it possible not to remove types?

Yes. A Typed Racket is a Racket program, so Racket can run it just fine.

What Eli was saying is that if you want to port it to, say, Guile, part
of the work will be removing the types, and part of it will be porting
the resulting Racket program to Guile.

> Vincent told me that one can "mix typed and untyped code" in Racket.

Here's a simple example:

;; in file typed.rkt
#lang typed/racket
(provide louder)
(: louder : String -> String)
(define (louder s) (string-append s "!"))

;; in file untyped.rkt
#lang racket
(require "typed.rkt")
(displayln (louder "I can call typed code"))

The first module is written in Typed Racket, and the second in untyped
Racket. If you run "untyped.rkt", it prints "I can call typed code!", as
expected.

You can also require untyped code from typed code using `require/typed'.

> How it's done in Racket (the implementation details)? How these modules
> interact? Could you give me some pointers?

Typed Racket modules compile to Racket modules, which interact with
other Racket modules via the module system. To make sure that typed
functions don't get invalid inputs from untyped code, the Racket
contract system checks everything that goes from untyped to typed code.

For example, if the untyped module above tried to do

(louder 3)

this would raise an error, since `louder' only accepts strings.

For more details about how contracts are used for typed-untyped
interaction, you can read
http://www.ccs.neu.edu/racket/pubs/dls06-tf.pdf

> Why it's not possible in other Lisp-like languages (e.g. Guile)?

Typed Racket relies on several important pieces of infrastructure that
Racket provides: the module system, the contract system, and Racket's
language extension facilities (including, but not limited to the macro
system), among others.

For more information about how the Typed Racket implementation uses
these mechanisms, you can read
http://www.ccs.neu.edu/racket/pubs/pldi11-thacff.pdf

Other systems that provide similar infrastructure could build their own
Typed Racket-like systems, too. Typed Clojure and Typed Ironscheme are
two such projects. IIUC, Guile has most of the necessary puzzle pieces,
too. But even with the necessary infrastructure, building such a system
remains a large engineering undertaking.

Vincent

[thor...@lavabit.com]

Thank you all for the replies.

I'll give it a try.

[Patrick Mahoney]

Hey all,

One feature of typed racket that makes translation between untyped and typed code somewhat less simple than adding or removing type signatures is that certain forms require rewriting/alteration of the untyped form itself. Others allow stand-alone declaration of the types prior to the form.

  #lang racket

(define (louder s) (string-append s "!"))

becomes
#lang typed/racket

(: louder : String -> String)
(define (louder s) (string-append s "!"))

but

#lang racket
(struct arrow (dom cod))

becomes
#lang typed/racket
(struct: arrow ([dom : Any] [cod : Any]))

or a stricter
#lang typed/racket
(struct: (A B) arrow ([dom : A] [cod : B]))

I tend to prefer the former case, as moving to untyped code just requires removal of the (: louder ...) type declaration.

I'd really dig the addition of an alternate way to declare types on structs in particular:

#lang typed/racket
(: arrow (ForAll (A B) (StructOf A B)))
(struct arrow (a b))

This allows me to reuse my mental untyped code parser for struct forms, while the struct: form requires an additional rule. It also makes declaration of types more uniform. Not sure whether this is possible.

Thanks all,
-Patrick

[Matthias Felleisen]

Technically this should be possible and conceptually preferable.

However, it does come with redundancies that conventional type annotations avoid and I am not sure how much of this redundancy we should push on programmers.

[Eli Barzilay]

Yesterday, thor...@lavabit.com wrote:
> > Developing statically typed code in TR and making it work later on
> > other Scheme implementations should be easy, since the TR type
> > system is intended to allow the same style of code that is used in
> > Racket, which is also similar to the style in other scheme
> > implementations.
>
> Actually, this is what I was asking about. (Guile people told me to
> use C or bins, but I don't want to go that deep.)

[That's what I thought, and I posted yet another reply because it
sounded like you were headed that way...]

Yesterday, Vincent St-Amour wrote:
>
> What Eli was saying is that if you want to port it to, say, Guile,
> part of the work will be removing the types, and part of it will be
> porting the resulting Racket program to Guile.

Exactly -- and if you stick to code that is "mostly basic scheme" then
the latter might not be too bad. (And in any case it is probably much
easier than writing haskell code and using a compiled binary from
guile.)

> > Why it's not possible in other Lisp-like languages (e.g. Guile)?
>
> Typed Racket relies on several important pieces of infrastructure

> that Racket provides [...]

(You should view Matthias's reply that it's possible *given* what
Vincent says above -- it's possible, but will require a ton of work.
AFAICT, Guile is getting to be the implementation where the needed
delta is smaller, but getting to a working TR-like would still be a
huge project.)

Yesterday, Patrick Mahoney wrote:
> One feature of typed racket that makes translation between untyped
> and typed code somewhat less simple than adding or removing type
> signatures

In case some people miss the obvious here: "removing type signatures"
is easy in any scheme -- you just need to define `:' as a macro that
ignores its contents.

> is that certain forms require rewriting/alteration of the untyped
> form itself. Others allow stand-alone declaration of the types prior
> to the form.

Right, but for thorsopia's case many of them (like the `for*:' forms)
are not important since they're Racket-specific anyway. The `struct:'
form is probably still relevant though -- since doing any serious work
without the ability to define new structs is an insane step back to
the dark SICP days.

> I'd really dig the addition of an alternate way to declare types on
> structs in particular:
>
> #lang typed/racket
> (: arrow (ForAll (A B) (StructOf A B)))
> (struct arrow (a b))
>
> This allows me to reuse my mental untyped code parser for struct
> forms, while the struct: form requires an additional rule. It also
> makes declaration of types more uniform. Not sure whether this is
> possible.

+1 for the sentiment, but the above makes `StructOf' a weird meta
thing which can be confusing in itself. Also, there are still other
`foo:'s and there's the identifier syntax that I think is mostly
obscure...

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

[thor...@lavabit.com]

One more question.

I've been told that there are no typeclasses in TR.
How would you handle this?

foo :: (Ord a) => a -> a -> a

(I haven't checked the docs yet. Maybe this is not needed in TR.)

[Sam Tobin-Hochstadt]

On Fri, Sep 21, 2012 at 2:29 PM, <thor...@lavabit.com> wrote:
> One more question.
>
> I've been told that there are no typeclasses in TR.
> How would you handle this?
>
> foo :: (Ord a) => a -> a -> a

Racket doesn't have a general notion of ordering, so we'd probably
write this function like this:

(: foo : (All (A) (A A -> Boolean) A A -> A))
(define (foo cmp left right) ...)

On the more general question, Racket has struct properties and the
generics system built on them. We would like to integrate Typed
Racket with these facilities, but that has not happened yet.
--
sam th
sa...@ccs.neu.edu