6 ms·

> Typed Racket supports refinement types and dependent function types. Previously an experimental feature, refinement types allow types to describe more interes

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

swlkr 9y ago
I was thinking the same thing, that's a really cool feature.
- deleted 9y ago
  [deleted]
  - deleted 9y ago
    [deleted]
    - deleted 9y ago
      [deleted]
      - deleted 9y ago
        [deleted]
        deleted 9y ago
        [deleted]
        deleted 9y ago
        [deleted]
        deleted 9y ago
        [deleted]
- deleted 9y ago
  [deleted]
shakna 9y ago
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 https://docs.racket-lang.org/ts-guide/caveats.html
- tomjakubowski 9y ago
  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 https://docs.racket-lang.org/guide/proc-macros.html
  - shakna 9y ago
    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.
    - alphaalpha101 9y ago
      >And usually, you don't need to care if what you're calling is a macro or a procedure. Now you do. You always do, because macros can change evaluation semantics and procedures cannot.
    - wtetzner 9y ago
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.
moomin 9y ago
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.
- shakna 9y ago
  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.
  - lomnakkus 9y ago
    > That's like calling GHC a bolt-on, because it's part of GCC. Eh? AFAIK, GHC has absolutely nothing to do with GCC.
    - shakna 9y ago
      Badly worded, but GHC has GCC as a backend, the Windows dist uses it.
      - lomnakkus 9y ago
        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_guide/code-generators.html https://downloads.haskell.org/~ghc/7.8.3/docs/html/users_gui...
baldfat 9y ago
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/ 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-interaction.html https://docs.racket-lang.org/ts-guide/typed-untyped-interact...
glebm 9y ago
Using Typed Racket adds 7+ MiB to the binary.
baldfat 9y ago
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-hackett-a-metaprogrammable-haskell/ https://lexi-lambda.github.io/blog/2017/05/27/realizing-hack...

swlkr 9y ago

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

deleted 9y ago
[deleted]
- deleted 9y ago
  [deleted]
  - deleted 9y ago
    [deleted]
    - deleted 9y ago
      [deleted]
      - deleted 9y ago
        [deleted]
        deleted 9y ago
        [deleted]
        deleted 9y ago
        [deleted]
deleted 9y ago
[deleted]

shakna 9y ago

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 https://docs.racket-lang.org/ts-guide/caveats.html

tomjakubowski 9y ago
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 https://docs.racket-lang.org/guide/proc-macros.html
- shakna 9y ago
  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.
  - alphaalpha101 9y ago
    >And usually, you don't need to care if what you're calling is a macro or a procedure. Now you do. You always do, because macros can change evaluation semantics and procedures cannot.
  - wtetzner 9y ago

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.

moomin 9y ago

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.

shakna 9y ago
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.
- lomnakkus 9y ago
  > That's like calling GHC a bolt-on, because it's part of GCC. Eh? AFAIK, GHC has absolutely nothing to do with GCC.
  - shakna 9y ago
    Badly worded, but GHC has GCC as a backend, the Windows dist uses it.
    - lomnakkus 9y ago
      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_guide/code-generators.html https://downloads.haskell.org/~ghc/7.8.3/docs/html/users_gui...

baldfat 9y ago

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/ 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-interaction.html https://docs.racket-lang.org/ts-guide/typed-untyped-interact...

glebm 9y ago

Using Typed Racket adds 7+ MiB to the binary.

baldfat 9y ago

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-hackett-a-metaprogrammable-haskell/ https://lexi-lambda.github.io/blog/2017/05/27/realizing-hack...