Hacker News Reader

Comment by Buttons840 | Hacker News Reader

> Typed Racket supports refinement types and dependent function types. Previously an experimental feature, refinement types allow types to describe more interesting properties of values, especially integers. For example, this type shows that the max function always produces a number at least as big as its inputs: (-> [x : Integer] [y : Integer] (Refine [z : Integer] (and (>= z x) (>= z y))))

Did Racket become a better Haskell while I wasn't looking? What's the catch? Those look like some powerful type system features.

View on HN

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.

> 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.)

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.

There's a few caveats [0] compared to untyped Racket, optimisation can be a little trickier, type generalisations can be somewhat unexpected. Typed/untyped boundaries can be unexpectedly expensive at times.

But the big one compared to Haskell is:

> Typed Racket will type-check all expressions at the run-time phase of the given module and will prevent errors that would occur at run-time. However, expressions at compile-time—including computations that occur inside macros—are not checked.

[0] https://docs.racket-lang.org/ts-guide/caveats.html

I misread this sentence the first couple times. Note that it isn't saying that Typed Racket only catches type errors at runtime, i.e. that it's a runtime type checker or a "contracts" implementation; it's saying that it—statically, and ahead of time—checks that expressions that would be evaluated at runtime have the correct types. (NB: as the caveats section notes, macro expansions are still statically type checked in Typed Racket)

What makes you see this as a caveat relative to Haskell? I can't imagine most Racket users typically deal with macros at such a low level; don't Schemers tend to use syntax-rules?

https://docs.racket-lang.org/guide/proc-macros.html

Using things like begin-for-syntax for compile-time evaluation isn't unusual for things like optimisation, but it'd bypass Typed Racket's safety here.

And usually, you don't need to care if what you're calling is a macro or a procedure. Now you do.

> but it'd bypass Typed Racket's safety here.

Sort of, but the expansion of any macros is still type-checked.

It doesn't bypass safety -- all code that's actually run is typechecked. It's just that we don't enforce anything about the macro itself, so the macro might error or produce code that results in a type error.

Look at Hackett which has Haskell’s type system and Racket’s macros. It is being developed by a Racket contributor who works full time as a Haskell developer.

https://lexi-lambda.github.io/blog/2017/05/27/realizing-hack...

Typed Racket is defined as:

> Typed Racket is Racket’s gradually-typed sister language which allows the incremental addition of statically-checked type annotations. https://docs.racket-lang.org/ts-guide/

> One of the key features of Typed Racket is that it allows the combination of both typed and untyped code in a single program. https://docs.racket-lang.org/ts-guide/typed-untyped-interact...

I was thinking the same thing, that's a really cool feature.

Using Typed Racket adds 7+ MiB to the binary.

Let’s assume Typed Racket’s system is perfect (others have already established it isn’t). There are still things a bolt-on type system can’t do. It can’t be used to compile more efficient code (which GHC does all the time) and you can’t get any more polymorphism than the language already offers, so forget typeclasses, return type polymorphism and usable monads.

Typed Racket does offer more efficient byte-code in a lot of situations, particularly if it isn't interacting with untyped Racket, or another racketlang.

Typed Racket offers parametric polymorphism, the Typed Racket guide shows how to implement Haskell's Maybe type as their first example. It still handles lexical scope and variable arity, as well.

Lastly, Typed Racket is hardly a "bolt-on" type system. It's a language with it's own parser and lexer. It just happens to be capable of interacting with every language also running on the Racket backend. That's like calling GHC a bolt-on, because it's part of GCC.

> That's like calling GHC a bolt-on, because it's part of GCC.

Eh? AFAIK, GHC has absolutely nothing to do with GCC.

Badly worded, but GHC has GCC as a backend, the Windows dist uses it.

I got my information from [1] and it only mentions gcc for the backend meant for porting, so I just kind of assumed that it would be using the native backend for all platforms. (Admittedly [1] is perhaps a bit out of date, thought.)

Certainly, it was just nitpicking, regardless.

[1] https://downloads.haskell.org/~ghc/7.8.3/docs/html/users_gui...

If you read this document on Racket optimizers you will see that they have actually put a lot of thought and tools for exactly your concerns. The collective Lisp academic might behind Racket is big but there is also a lot of general computing work getting added to Racket for years. I certainly wouldn't say it is a "bolt-on type system" Racket Typed is defined as

> Typed Racket is Racket’s gradually-typed sister language which allows the incremental addition of statically-checked type annotations. https://docs.racket-lang.org/ts-guide/index.html

> This package provides optimization coaching support to help you get the most of the Racket and Typed Racket optimizers. https://docs.racket-lang.org/optimization-coach/index.html

Reply on news.ycombinator.com