I am posting this here because perhaps this is more suited for the beginners channel

It seems that in #general no one was able to provide an answer to these questions, or a pointer to some good reference where these questions can be answered

Is the goal of Typed Racket to have a statically typed language in the generally dynamically typed ecosystem of Racket, along with other languages, thus being another showcase of what the language-oriented Racket system can do?

Or does it go beyond that and brings new type machinery not present in OCaml or Haskell?

Is there anyone here from Racket’s core team able to answer these questions?

I’m not from the core team, but I think the goal is to be able to transition from a dynamically-typed program to a typed program incrementally, and have the typed parts interoperate with the “untyped” parts

in Racket there is a continuum, you can start without any verification, then add contracts, then add types. contracts are checked dynamically and can express stronger properties than most type systems

Thanks @andreiformiga, that is something different from the other languages I mentioned, makes sense

As I understand it (I am horribly unqualified to really answer this question), Typed Racket does do some kind of type inference that OCaml and Haskell can’t, particularly occurrence typing. (I believe there are other things OCaml and Haskell do that Typed Racket doesn’t: it is a different approach. @samth could give you a definitive answer.

You might also be interested in @lexi.lambda’s Hackett: https://www.thestrangeloop.com/2018/hackett-a-metaprogrammable-haskell.html

I think it’s maybe less that OCaml/Haskell can’t do those things and more that they consciously choose not to. Type systems are a big design space. TR has anonymous unions with subtyping, which are pretty useful, but they also make type inference a lot worse, so it’s a tradeoff.

TR’s type system is designed primarily with the “migratory typing” idea that @andreiformiga mentioned, but even looking at its type system in isolation (ignoring the gradual typing aspect) I’d say it has pros and cons.

TR does, however, have a design goal of no new dynamic semantics, so type erasure is morally a simple process of throwing the type annotations away. TR will never have anything like typeclasses or implicits because of that.

(At least, unless that design goal changes.)

Hi, I’m looking at a contract for a function that takes no arguments. As an aside, it’s an exercism exercise so there’s no production costs to be wary of. The interface is two functions, a function with one argument and a function with none. So you get something that looks like: (provide (contract-out [a ((integer-in 1 64) . -> . exact-positive-integer?)] [b (->* () () exact-positive-integer?)])) So given that: 1) can I define a better contract for the b function? 2) for functions with no input but only output would it be better to opt out of the contract? Can I do that inside the provide?

@robert.postill what do you mean by a “better contract for the b function”? You could write it as (-> exact-positive-integer?) instead, but that’s just simpler syntax for the same contract. Contracts can still make sense for functions that take no arguments, but if you want to leave it out you can replace the [b ...] with just b

Thanks @dan I was indeed going for a more succinct form so that’s spot on.

I also didn’t know you could just say b without the attending contract. Which is again a win for brevity

@mario.luis.guimaraes The other big important idea of Typed Racket is that it’s not a separate compiler or runtime from Racket. It’s a library that uses the standard Racket macro system. So all of the Racket toolchain works with TR, including the Racket compiler, module system, package system, documentation system, and editor. TR is basically proof that entire static type systems can be a “derived concept” that don’t require special compiler support to build. You could make TR yourself if you wanted to (and had a lot of time on your hands).

@robert.postill In general you can use -> as long as you don’t have optional arguments.

or dependent contracts (which requires ->i), but those are rare

@mario.luis.guimaraes Another approach to type systems in Racket-land is Turnstyle: https://docs.racket-lang.org/turnstile/