3 ms·

Well, typed racket is not racket with types,but a language that you will use differently than regular racket. I have stopped using for-loops for complex things

by bjoli 9y ago

Well, typed racket is not racket with types,but a language that you will use differently than regular racket. I have stopped using for-loops for complex things, since they expand to something that makes life hard for the type checker. With ML I never have the feeling that I am fighting the type checker, but with typed racket I have more problems than I'd like to admit. I am however no programmer and have no background in CS or even maths, and there are people that write a lot of code in typed racket. And last time I tried typed racket I had some weird slow downs when specifying types less generally (like: integer instead of real, positive-integer instead of integer). There is a bit of non-trivial code written in typed racket, and that is probably a good complementary reading to the typed racket guide.

neel_k 9y ago
> And last time I tried typed racket I had some weird slow downs when specifying types less generally (like: integer instead of real, positive-integer instead of integer). This is probably not your fault. Scheme (from which Racket descends) has a very intricate numeric hierarchy. Typed Racket models the numeric hierarchy very accurately, and the technique they use to do this (intersection types) has bad worst-case complexity -- you can encode arbitrary SAT problems in it pretty easily. So the numeric types are actually aliases for quite complicated formulae, and this can tip you over into bad cases for inference. Writing a more specific type gives you a smaller formula, which makes typechecking faster. In a clean-slate design, you would set things up to minimize the use of intersection types, but to get smooth access to the pre-existing Racket ecosystem, this is a price you have to pay. (Warning: my information is a few years old. Racket's type system could have changed in the meantime.)
- samth 9y ago
  This isn't quite right -- the parts where you can encode SAT and the parts where we model the numeric tower aren't the same parts. But the broader reason is accurate -- there are a lot of cases, and we model precisely by listing out a lot of possibilities, resulting in potentially longer type checking times.

by bjoli 9y ago

neel_k 9y ago

> And last time I tried typed racket I had some weird slow downs when specifying types less generally (like: integer instead of real, positive-integer instead of integer). This is probably not your fault. Scheme (from which Racket descends) has a very intricate numeric hierarchy. Typed Racket models the numeric hierarchy very accurately, and the technique they use to do this (intersection types) has bad worst-case complexity -- you can encode arbitrary SAT problems in it pretty easily. So the numeric types are actually aliases for quite complicated formulae, and this can tip you over into bad cases for inference. Writing a more specific type gives you a smaller formula, which makes typechecking faster. In a clean-slate design, you would set things up to minimize the use of intersection types, but to get smooth access to the pre-existing Racket ecosystem, this is a price you have to pay. (Warning: my information is a few years old. Racket's type system could have changed in the meantime.)

samth 9y ago
This isn't quite right -- the parts where you can encode SAT and the parts where we model the numeric tower aren't the same parts. But the broader reason is accurate -- there are a lot of cases, and we model precisely by listing out a lot of possibilities, resulting in potentially longer type checking times.