Racket v6.11 | Hacker News Reader

Racket v6.11

blog.racket-lang.org

154 pointsnickmain34 comments

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

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.

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.

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

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

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

What are refinement types and dependent function types?

A refinement type, is a value type with preconditions attached.

Simply put, instead of something being an Integer, you can say it is an Integer, but only between 1 and 6. In this case, this should be enforced at compile-time.

Dependent function types allow the return type of a function refer to the argument value of the function. The classic example is "vectors", which are like lists but have a statically-checked length. Here's an example function involving vectors:

    duplicate : (t : Type) -> t -> (n : Nat) -> (Vector n t)

This type signature says that `duplicate` is a function of 3 arguments: `a -> b` means a function from argument type `a` to return type `b`, and `a -> b -> c` can either be interpreted as "a function taking an `a` and returning a `b -> c`" or (equivalently) "a function taking an `a` and a `b` and returning a `c` (see https://wiki.haskell.org/Currying for why this is equivalent).

Argument types are written in one of two ways: if they're written like `a` (for example `Int` or `String`), then the type of the argument is `a`; if they're written `a : b` (for example `age : Int`) then the argument type is `b`, but later types can refer to the value as `a`.

So this signature says that the first argument of `duplicate` is called `t`, and it is a `Type`. The second argument has type `t`; this means the type of the second argument depends on the value of the first argument: if we call `duplicate` with `Bool : Type` as the first argument, then the second argument must be a `Bool`.

The third argument is called `n`, and has type `Nat` (natural numbers: i.e. the positive integers including zero). The return type is `Vector n t`, i.e. a list of length `n` containing elements of type `t`.

Note that we're referring to argument values by name, but we don't know what particular value they will be (i.e. which number `n` will be, or which type `t` will be). We can think of `a : b` as being `for all a of type b`.

If we think about functions returning lists, like `map` or `reverse`, we can "cheat" by having them always return an empty list; such functions satisfy their type signature (they return a list), but don't behave in the way we want.

In contrast, the "for all" nature of dependent function types can be used to prevent this sort of "cheating". The `duplicate` function can't just return an empty vector, since it must return a vector of length `n`, and the implementation must work for all values of `n`. We're forced to write a function which constructs a vector of the correct length: empty when `n` is zero, or non-empty otherwise.

To construct a non-empty vector, we need to put a value inside it. What value can we use? We can't "cheat" by using, say, the value `"hello"`, since that would give us a vector containing `String`, whilst our return type forces us to make a vector containing `t`. Whatever our function does, it must work for all values of `t` (`String`, `Bool`, `Int`, `Vector 5 (Int -> Bool)`, etc.).

Since we don't know what `t` will be, we can't "invent" a value of the right type. The only thing we can do is use an existing value which will always have type `t`. The only way something can have type `t` is if it appears in our type signature, since that's the scope of the name `t`. The only thing in our type signature which has type `t` is the second argument. Hence we must use the second argument as the elements of our vector (if it's non-empty).

One implementation which satisfies this type is the following (assuming that `Nat` is encoded as Peano numerals https://en.wikipedia.org/wiki/Successor_function ):

    duplicate t x n = case n of
                           zero   -> vectorNil t
                           succ m -> vectorCons t x (duplicate t x m)

This isn't the only possible implementation, for example we might choose to send the recursive call through a `vectorReverse` function (although it would be pointless), but such differences cannot alter the input/output behaviour of the function.

Of course, we don't have to use dependent function types to restrict all of a function's behaviour. If we think back to the `map` example, we take a function of type `a -> b`, a `List a` and must return a `List b`: the easiest thing to do is return an empty list, which satisfies the type but isn't what we want.

If we instead make a `vectorMap` function, where `List` is replaced with `Vector n`, then that "cheat" no longer works (since an empty vector doesn't always have length `n`). We could still mess around with the contents, like reversing it or doing some other permutation, but that's harder than just doing the right thing. The path of least resistance is to write a correct implementation!

I like the way Edwin Brady talks about this: a dependently typed language is one in which types are first class. That is, you can use them as values in computations and return them.

"First class types" and "dependent types" are actually two different things. We can have first class types without any dependencies. For example:

    isEven : Nat -> Type
    isEven  zero           = Unit
    isEven (succ zero)     = Empty
    isEven (succ (succ n)) = isEven n

    fortyTwoEven : isEven 42
    fortyTwoEven = unit

Here the `isEven` function calculates a type based on the given number: if the number's even, it returns the `Unit` type, of which there is a value `unit`; if the number's odd, it returns the `Empty` type, of which there are no values.

The value `fortyTwoEven` is a "proof" that the number `42` (which would actually be `succ (succ (succ ...))` nested 42 times) is even. The proof is the value `unit`, which will only work if `isEven 42` returns `Unit`, which will only happen if 42 is even, so everything works out. We can write a type like `isEven 43`, but that will return the type `Empty`, which there's no way to satisfy.

We can use this sort of thing to do static checks of reasonably simple data; for example, if we have a bunch of config parameters which need to be related in some way.

Dependent types add the "naming" part, which we can use in functions (as explained above), but also in other "compound" datastructures like tuples `(n : Nat, isEven n)` and records `{ n : Nat, evenProof : isEven n }`

The annoying thing is that few languages seem to have first class types at all, so every explanation of dependent types has to start by introducing first class types, and then explaining the "dependent" parts.

It's like trying to explain something like interfaces, if all mainstream languages were dynamically typed. We'd have to begin by explaining what types are, and then go on to explain interfaces. Readers might easily confuse features of types with features of interfaces, which would lead to much confusion.

I think that's kind of happened with "dependent types" and "first class types", although I haven't seen any/many systems which have one without the other, so maybe it's not too bad :)

That was some of the clearest technical writing I've ever read. I hope you write a book, if you haven't already.

As someone who only has a fuzzy understanding of these concepts, this reply was enlightening. Thanks!

Please forgive some ignorance here, but I thought that LISP couldn't have a proper type system since it would muck with homoiconicity. Clearly I'm wrong about this, but now I'm curious why more LISPs aren't typed.

Can anyone here enlighten me?

What do you mean by a "proper type system"?

In SBCL, if you set the optimization (SAFETY 3) then the system can catch many type errors in advance.

Finally, homoiconicity simply means that the text of a program generally resembles the AST of the language. Adding type annotations (which you can do in CL, clojure, and typed racket) is therefore not incompatible with the principle of homoiconicity.

I think that I got confused based on some post talking about difficulties of implementing a Hindley Milner type system in Lisp. So much for relying on three-year-old memories.

Homoiconicity is a weak concept; it refers to programs being stored in the original textual representation.

A very good example of this that is in widespread use today is the POSIX shell, which is homoiconic because you can run "set" to see function definitions that can be copy and pasted.

This is not valued in the Lisp world at all; Lisp implementations throw away the text and compile the code into another representation.

Common Lisp has optional support for homoiconicity. There is a function called ed which can recall a function definition for editing. http://clhs.lisp.se/Body/f_ed.htm

Representing source code as a data structure (and allowing user-defined code to intercept and transform it at compile time) isn't homoiconicity.

Your definition of homoiconicity is different than any I've ever seen, which is something like "the language's own code is a first-class data type" (see the discussion on the C2 wiki, for example: http://wiki.c2.com/?DefinitionOfHomoiconicDiscussion)

https://en.wikipedia.org/wiki/Homoiconicity uncovers where the term came from: the paper describing a text processing language called TRAC. Nothing about a fist-class data type other beyond the character string. It seems to have been contrived by sticking the greek prefix "homo" (same) onto "iconic", which is derived from "ikonos" (image). The code in the machine has the same (homo) image (ikonos) as what came from the keyboard.

The Lisp example in that page is irrelevant. eval is not required, in fact, to walk the nested list data structure; some Lisps have an eval which compiles to native code, then calls the resulting function. Lisp data is somewhat homoiconic in that it has a representation which converts back to text. It's not exactly the original text, but there is an important concept at play called "read/print consistency". It is weaker than homoiconicity, which preserves the exact character spelling, more or less.

There are statically typed variants of Lisp. Shen springs to mind. The homepage for Shen has more details about the type system it uses, but just to warn you the site jumps in at the deep end:

http://shenlanguage.org/

Perhaps there's a gentler introduction elsewhere.

My money would be on cost of implementation. Specifically, implementing a full type system takes a large effort.

Now, it should come as no surprise that many Common Lisp implementations do give what is equivalent to compile time warnings when things are done incorrectly. What throws most people off, I think, is that compile/runtime are easy to mix in a lisp language. Such that you can go between the phases more naturally than you can in other languages.

Reply on news.ycombinator.com