Typed/Untyped cost reduction and experience

[JCG]

Having just converted a server process of about 1800 lines of untyped Racket to 1900 lines of typed Racket, I'd like to make some comments

1) I highly suggest starting in Typed Racket if you are going to go end up there. I made the mistake of writing it untyped and then retrofitting which clearly is the more difficult path.

2) The conversion caught one likely-to-happen-sometime bug, thank you.

3) The end-product appears to be a 50%-performance hybrid due to boundary contracts, but ameliorated runtime-wise by utilizing the typed/racket/no-check language after it's all working in type checked mode.

4) I failed to create a valid new language with conditional inclusion of typed and no-check variants, but a command line or in-program conditional ability to disable types would permit an easy to accept morphing systems which need to gently attain 100% typed nature. At the moment, I use a Unix shell script to doctor the #lang lines. For instance 'raco -no-check exe ...' would really be nice after concluding that my slow hybrid is operating correctly.

5) When retrofitting, Dr Racket nicely points out errors, which in quantity should perhaps be limited to speed the retrofit cycle. Being familiar with G++ template errors, I was not too shocked. One thing that I learned was instead of attacking the first error which often was deeper in a function, it was more profitable to start at the outside, i.e. the function signature, and allow that information to imply further information. I found that otherwise, I ended up with correct but superfluous annotations.

6) A few missing typed versions of libraries were what caused me to not start there, notably the lack of typed/db.

Thanks,
JG

[Asumu Takikawa]

On 2015-12-26 15:52:38 -0800, JCG wrote:
> 3) The end-product appears to be a 50%-performance hybrid due to boundary
> contracts, but ameliorated runtime-wise by utilizing the
> typed/racket/no-check language after it's all working in type checked mode.

If you're using Racket v6.3, another way to get around this is to use the
`typed/racket/unsafe` library which allows you to selectively disable some
contracts:

http://docs.racket-lang.org/ts-reference/Unsafe_Typed_Racket_operations.html

That way at least your types won't bitrot as much. Note that as the name
indicates, this is potentially less safe than untyped Racket if the TR
optimizer is on.

(you could also write a wrapper macro that globally enables/disables the
use of the unsafe imports & exports)

Cheers,
Asumu

[JCG]

On Saturday, December 26, 2015 at 9:14:10 PM UTC-5, Asumu Takikawa wrote:
>
> That way at least your types won't bitrot as much. Note that as the name
> indicates, this is potentially less safe than untyped Racket if the TR
> optimizer is on.
>
> (you could also write a wrapper macro that globally enables/disables the
> use of the unsafe imports & exports)
>

Assuming that I'm reasonably sure from empirical tests that my contracts implied by the typed/untyped bridge are being satisfied, then this looks like a good idea.

Thanks for this addition to the system.

[Benjamin Greenman]

Is the server code online anywhere? I'd like to see what the boundary contracts are.

Let me know if starting typed works for a future project. So far, I've had the best experience starting untyped but keeping type annotations in comments -- basically like no-check, but without annotations on lambdas or for loops. The worst times I've had were hitting "dead-ends" while converting because I didn't understand Typed Racket, but after a little more experience it's nice to wait until the program works to enforce the types & catch edge cases.

--
You received this message because you are subscribed to the Google Groups "Racket Users" group.
To unsubscribe from this group and stop receiving emails from it, send an email to racket-users...@googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

[JCG]

Sorry, there's no publicly available code involved with the project.

Seeing all the options, I believe that my favorite one is to type only at the border of my code, leaving the implementation in untyped Racket. By dropping the contract cost, code still goes fast, and the borders are type-checked.

For the meantime, I'll be doing this on new code

#lang typed/racket[/unsafe maybe]

(module 'hundred-lines-of-untyped racket
...
(define (my-function A B C)
...)))

(require/typed/provide 'hundred-lines-of-untyped
[ my-function (-> NICE TYPED ARGS RESULT) ])

If I understand this correctly, the unsafe version will perform the same static checks on callers of the functions published by (provide) but not incur contract cost.

[Benjamin Greenman]

On Tue, Dec 29, 2015 at 7:05 PM, JCG <griff...@gmail.com> wrote:

If I understand this correctly, the unsafe version will perform the same static checks on callers of the functions published by (provide) but not incur contract cost.

Yep, that's right.

#lang typed/racket/base

(require typed/racket/unsafe)

(unsafe-require/typed racket/base (values (-> String Integer)))

(string-append (values "foo") "bar")  ;; Type Error

(+ (values "foo") 1)  ;; Runtime Error, because annotation on `values` is incorrect

[Robby Findler]

Just as a word of caution here: with a different set of type
annotations, that program could go from a runtime error to a segfault.
You probably also want to at least disable TR's optimizations when you
do this.

Robby

[Matthias Felleisen]

Late but I want to record principles and experiences in this thread:

On Dec 26, 2015, at 6:52 PM, JCG <griff...@gmail.com> wrote:

> Having just converted a server process of about 1800 lines of untyped Racket to 1900 lines of typed Racket, I'd like to make some comments
>
> 1) I highly suggest starting in Typed Racket if you are going to go end up there. I made the mistake of writing it untyped and then retrofitting which clearly is the more difficult path.
>

TR is intended for people who wish to add types retroactively.

My own experience doing so is highly favorable, and I have ported 1000s of lines and I have asked some of my students to port many more of my lines. But yes, TR and its tool support is work in progress, and I am sure we can do better.

> 2) The conversion caught one likely-to-happen-sometime bug, thank you.

That's a nice side effect. I rarely find mistakes, but I follow the HtDP approach to an extreme with tons of type comments.

The actual purpose is to record with sound, checked types what the designer had in his head retroactively so that developers can benefit from this type information and so that the creation of *new code* can benefit from the (shallow but large) advantages of types and type checking.

> 3) The end-product appears to be a 50%-performance hybrid due to boundary contracts, but ameliorated runtime-wise by utilizing the typed/racket/no-check language after it's all working in type checked mode.

I don't understand this bullet. Bullet 1 says your code is now completely typed. Our experience is that completely typed versions are about as fast and on many occasions (eg., numeric) faster than completely untyped versions.

But, we are perfectly aware that many hybrid versions are slower than the untyped version by several factors. Many of people in PLT (everyone?) are working on this problem right now.


Thanks -- Matthias

[Emmanuel Oga]

On Tuesday, January 5, 2016 at 11:12:44 AM UTC-8, Matthias Felleisen wrote:
> TR is intended for people who wish to add types retroactively.

Not sure I understand this stance:

* Does this mean if I want to use types proactively, TR is not a recommended PL?

* Or maybe it means adding types proactively is just not a recommended way to go in general, and types should only be added when the code base reaches certain trigger conditions?

> The actual purpose is to record with sound, checked types what the designer had in his head retroactively so that developers can benefit from this type information and so that the creation of *new code* can benefit from the (shallow but large) advantages of types and type checking.

BTW I did read this "actual purpose" paragraph. I'm just not sure how this answers my comments above :-).

[Hendrik Boom]

Using types proactively is, if I understand you, deciding the types
before you write the code. Or at the latest, at the same time. So I
this will be new code.

I think the following part of the quoted text answers your question:
\
+ the creation of *new code* can benefit from the
+ (shallow but large) advantages of types and type checking.

That's certainly how I use types when writing new Racket code.

-- hendrik

[JCG]

On Tuesday, January 5, 2016 at 2:12:44 PM UTC-5, Matthias Felleisen wrote:
> Late but I want to record principles and experiences in this thread:
>

> I don't understand this bullet. Bullet 1 says your code is now completely typed. Our experience is that completely typed versions are about as fast and on many occasions (eg., numeric) faster than completely untyped versions.
>

Yes, it was hybrid and is still, although today I made quite a few conversions where the cost/benefit (all mental cost/benefit, not speed) was conducive. This project is 40 files, 17 of which are hybrid with untyped code in submodules.

I started this Typed Racket in mid-December, but I'm getting there. My feeling is that I rather like making small modules with typed borders but sometimes untyped implementations. I look forward to seeing future performance improvements in these hybrids.

[Matthias Felleisen]

I will say this as the first Racketeer and Typed Racketeer: if you just want to program in an explicitly-statically typed language (possibly with inference), you might wish to broaden your scope of search. There are other expressively typed languages that come with good libraries. Most of these languages are much more mature than TR and probably more reliable and stable (in this sense).

I am not sending you away. I am a scientist-designer who wants user-developers to be highly informed.

-- In this spirit, TR is explicitly designed to help developers move from untyped code to [explicitly-statically and sound] typed cpde in an incremental, module-by-module manner [*]. This is spelled out in the DSL 2006 vision paper. As such, TR's type system *must* accommodate many of the programming idioms that developed in Racket/Scheme/Lisp over the past six decades. This makes the type system unusual and a bit quirky. For example, we do not support abstract types to the point where one new member of the team said "but TR doesn't have types" (thinking of Reynolds's slogan).

-- At the same time, our experiments with 10s of thousands of lines suggest that it is possible to port lots of code without changing much about the structure of the code. That increases the likelihood that the code remains functioning as developers convert. Naturally we expect a test suite to confirm the validity of these intermediate conversion points.

-- Having said that, you also need to know that I advertise the use of explicit types even when your chosen language does not have a static type system. See "how to design programs" for the underlying philosophy. The basic reason is that types exist whether your language allows you to write them down or not. If it doesn't, use comments to develop them before you code because doing so will help you very much develop well-organized most-likely-pretty-much-working code. You won't have the advantages of type systems, which (mostly) check shallow properties and violations of those. But you do have the deeper advantage of organizing your thoughts. I have followed this philosophy since 1986 and co-authored (rewrote) my first book on this idea back them. It works :-)


[*] Let's ignore why we are doing this for now. The 'actual purpose' paragraph sketched this out in a hyper-concise manner.

[Matthias Felleisen]

You are exactly the kind of user-developer that we imagined. Please keep us informed about your progress. If we can assist, don't hesitate to ask. If TR and its type system get in your way, let us know.

Good luck and thanks for these first reports -- Matthias

[JCG]

> I will say this as the first Racketeer and Typed Racketeer: if you just want to program in an explicitly-statically typed language (possibly with inference), you might wish to broaden your scope of search. There are other expressively typed languages that come with good libraries. Most of these languages are much more mature than TR and probably more reliable and stable (in this sense).
>
> I am not sending you away. I am a scientist-designer who wants user-developers to be highly informed.

I'm looking for a middle ground between Python and C++, the two basic language tools in use at the office. I like typing fast with my fingers and typing loose with my data, until it passes 100 lines of Python, the point at which my opinion flips 180 degrees. After 100 lines, my option is to go to C++ or put another tool in the mix. Here are my constraints for a potential middle ground tool:

1) It must run on command-line non-X11 Linux, (and OSX as well if possible)
2) It must have a reasonable FFI to use our proprietary C++ libraries and allow foreign controlled data structures. There are pointers to substantial C++ side heap allocations requiring execution of C++ destructors at disposal time.
3) The nature of our library calls is that a language permitting optional named arguments
is almost a requirement to harness the capabilities of our library.
4) It must be considerably more productive than C++, otherwise it's C++
5) I've had enough uncaught flaws in Python that I'm now convinced that I need types.
6) It needs pattern matching, otherwise I'm back to C++, flex and bison or I have to figure out Stroustrup's Mach 7 which does not yet seem settled.
7) A reasonable size, polite, and intelligent group driving the technology.

My preferences include:

1) reasonably fast executables
2) Lightweight threads
3) Reasonable ability to use multiple cores safely.
4) Reliable environment generating reliable JavaScript
5) Immutability of data
6) Weighted more towards functions than objects

So, two things come to mind, Racket and SBCL because I've used them before, and the ML family - Haskell, OCaml, and Scala. Having tried Scala, I like the language but the associated environmental baggage appeared heavy and brittle from build dependencies. Both Haskell and OCaml seem quite plausible. Having types potentially in Racket keeps it in the running.

Anyway, Racket floated first to the top because I reimplemented a network service that really needed pattern matching to combat the growing complexity of patterns. I grabbed a familar (untyped) Racket and made a prototype. Unfortunately, the prototype worked so well that I'm using it now for real. Nevetheless, it has the smell of something that might be easier to maintain long-term with compiler-checked type annotations. Typed Racket has improved or at least my utilization of it considerably since I looked at it about 4 years back. Likewise, the places module which had previously been for me ungrokkable and lethargic was now easy and fast enough.

While those MLs are definitely still in mind, I'm going to get more comfortable with Typed Racket first.

[Sam Tobin-Hochstadt]

On Wed, Jan 6, 2016 at 2:01 PM, JCG <griff...@gmail.com> wrote:
>
> So, two things come to mind, Racket and SBCL because I've used them before, and the ML family - Haskell, OCaml, and Scala. Having tried Scala, I like the language but the associated environmental baggage appeared heavy and brittle from build dependencies. Both Haskell and OCaml seem quite plausible. Having types potentially in Racket keeps it in the running.
>
> Anyway, Racket floated first to the top because I reimplemented a network service that really needed pattern matching to combat the growing complexity of patterns. I grabbed a familar (untyped) Racket and made a prototype. Unfortunately, the prototype worked so well that I'm using it now for real. Nevetheless, it has the smell of something that might be easier to maintain long-term with compiler-checked type annotations. Typed Racket has improved or at least my utilization of it considerably since I looked at it about 4 years back. Likewise, the places module which had previously been for me ungrokkable and lethargic was now easy and fast enough.
>
> While those MLs are definitely still in mind, I'm going to get more comfortable with Typed Racket first.

I'm glad you're enjoying using Typed Racket.

While our original goal with Typed Racket was to support the porting
process from Racket to Typed Racket, it's become clear in the 10 years
of Typed Racket development that many people prefer to start with
Typed Racket. That's a fully-supported way of using Typed Racket, and
plenty of excellent software has been written that way at this point.

Either way, I encourage you to keep using Typed Racket, and thanks for
the kind words -- we've put lots of effort into improving it in the
last 4 years, and hopefully we'll be able to address more of the
issues you've run into in the future.

Sam

[Emmanuel Oga]

On Wednesday, January 6, 2016 at 11:01:56 AM UTC-8, JCG wrote:
> > I will say this as the first Racketeer and Typed Racketeer: if you just want to program in an explicitly-statically typed language (possibly with inference), you might wish to broaden your scope of search. There are other expressively typed languages that come with good libraries. Most of these languages are much more mature than TR and probably more reliable and stable (in this sense).
> >
> > I am not sending you away. I am a scientist-designer who wants user-developers to be highly informed.
>
> I'm looking for a middle ground between Python and C++, the two basic language tools in use at the office. I like typing fast with my fingers and typing loose with my data, until it passes 100 lines of Python, the point at which my opinion flips 180 degrees. After 100 lines, my option is to go to C++ or put another tool in the mix. Here are my constraints for a potential middle ground tool:
>
> 1) It must run on command-line non-X11 Linux, (and OSX as well if possible)
> 2) It must have a reasonable FFI to use our proprietary C++ libraries and allow foreign controlled data structures. There are pointers to substantial C++ side heap allocations requiring execution of C++ destructors at disposal time.
> 3) The nature of our library calls is that a language permitting optional named arguments
> is almost a requirement to harness the capabilities of our library.
> 4) It must be considerably more productive than C++, otherwise it's C++
> 5) I've had enough uncaught flaws in Python that I'm now convinced that I need types.
> 6) It needs pattern matching, otherwise I'm back to C++, flex and bison or I have to figure out Stroustrup's Mach 7 which does not yet seem settled.
> 7) A reasonable size, polite, and intelligent group driving the technology.
>

With these constraints seems like http://extempore.moso.com.au/ could be interesting to you. It implements this http://extempore.moso.com.au/temporal_recursion.html model that I had not heard about before.

> My preferences include:
>
> 1) reasonably fast executables
> 2) Lightweight threads
> 3) Reasonable ability to use multiple cores safely.
> 4) Reliable environment generating reliable JavaScript
> 5) Immutability of data
> 6) Weighted more towards functions than objects
>
>
> So, two things come to mind, Racket and SBCL because I've used them before, and the ML family - Haskell, OCaml, and Scala. Having tried Scala, I like the language but the associated environmental baggage appeared heavy and brittle from build dependencies. Both Haskell and OCaml seem quite plausible. Having types potentially in Racket keeps it in the running.
>

I really like ML like languages, but the reason I enjoy racket more is... basically s-expressions :-).

In both Haskell and OCaml simply printing or inspecting a value of a custom data type is a bit convoluted when you compare it to more dynamic language like racket.

For a long while OCaml had some ambiguities about which macro processor was the go-to one... now there's something new that is also nothing as easy as s-expression manipulation (ppx something...). In Haskell I don't even know how I'd write some macro-like behavior.

If I could have built-in ADTs, pattern matching and s-expressions on a single language, I'd be a happy programmer :).

[Matthias Felleisen]

On Jan 6, 2016, at 2:01 PM, JCG <griff...@gmail.com> wrote:

>
>> I will say this as the first Racketeer and Typed Racketeer: if you just want to program in an explicitly-statically typed language (possibly with inference), you might wish to broaden your scope of search. There are other expressively typed languages that come with good libraries. Most of these languages are much more mature than TR and probably more reliable and stable (in this sense).
>>
>> I am not sending you away. I am a scientist-designer who wants user-developers to be highly informed.
>
> I'm looking for a middle ground between Python and C++, the two basic language tools in use at the office. I like typing fast with my fingers and typing loose with my data, until it passes 100 lines of Python, the point at which my opinion flips 180 degrees. After 100 lines, my option is to go to C++ or put another tool in the mix. Here are my constraints for a potential middle ground tool:
>
> 1) It must run on command-line non-X11 Linux, (and OSX as well if possible)
> 2) It must have a reasonable FFI to use our proprietary C++ libraries and allow foreign controlled data structures. There are pointers to substantial C++ side heap allocations requiring execution of C++ destructors at disposal time.
> 3) The nature of our library calls is that a language permitting optional named arguments
> is almost a requirement to harness the capabilities of our library.
> 4) It must be considerably more productive than C++, otherwise it's C++
> 5) I've had enough uncaught flaws in Python that I'm now convinced that I need types.
> 6) It needs pattern matching, otherwise I'm back to C++, flex and bison or I have to figure out Stroustrup's Mach 7 which does not yet seem settled.
> 7) A reasonable size, polite, and intelligent group driving the technology.
>
> My preferences include:
>
> 1) reasonably fast executables
> 2) Lightweight threads
> 3) Reasonable ability to use multiple cores safely.
> 4) Reliable environment generating reliable JavaScript

Hmph.

> 5) Immutability of data
> 6) Weighted more towards functions than objects
>
>
> So, two things come to mind, Racket and SBCL because I've used them before, and the ML family - Haskell, OCaml, and Scala. Having tried Scala, I like the language but the associated environmental baggage appeared heavy and brittle from build dependencies. Both Haskell and OCaml seem quite plausible. Having types potentially in Racket keeps it in the running.
>
> Anyway, Racket floated first to the top because I reimplemented a network service that really needed pattern matching to combat the growing complexity of patterns. I grabbed a familar (untyped) Racket and made a prototype. Unfortunately, the prototype worked so well that I'm using it now for real.

This makes you the normal Racket developer and (as I have said) an ideal candidate for TR.

> Nevetheless, it has the smell of something that might be easier to maintain long-term with compiler-checked type annotations. Typed Racket has improved or at least my utilization of it considerably since I looked at it about 4 years back. Likewise, the places module which had previously been for me ungrokkable and lethargic was now easy and fast enough.
>
> While those MLs are definitely still in mind, I'm going to get more comfortable with Typed Racket first.

Great. Keep pushing, we'll keep improving -- Matthias