[racket] Typed Racket has finally arrived!

[Neil Toronto]

Typed Racket has arrived: it is useful to write programs in it in which
types outnumber code. From my dissertation project:

(: make-rect-list-subtract-one
(All (N1 F1 E1 V1 N2 F2 E2 V2)
((set-sig N1 F1 E1 V1)
(set-sig N2 F2 E2 V2)
-> ((Listof (Nonextremal-Pair-Rect N1 F1 N2 F2))
(Nonextremal-Pair-Rect N1 F1 N2 F2)
-> (Listof (Nonextremal-Pair-Rect N1 F1 N2 F2))))))
(define (make-rect-list-subtract-one ops1 ops2)
(define pair-rect-subtract (make-pair-rect-subtract ops1 ops2))
(λ (As B)
(append* (map (λ: ([A : (Nonextremal-Pair-Rect N1 F1 N2 F2)])
(pair-rect-subtract A B))
As))))

FWIW, this is my fault for using `case->' types in other spots to have
TR prove extra stuff. Also, I'm manually doing generics. (Generic set
operations come bundled in a `set-sig' with type parameters for
*N*onextremal set, *F*ull (universal) set, *E*mpty set, and *V*alue.)

This is not a snarky complaint about lack of generics or too much typing
(pun intended). Rather, I'm impressed that I can get TR to typecheck a
"union of sets of pairs" function with this type:

(case-> ((Pair-Set N1 F1 N2 F2) (Nonempty-Pair-Set N1 F1 N2 F2)
-> (Nonempty-Pair-Set N1 F1 N2 F2))
((Nonempty-Pair-Set N1 F1 N2 F2) (Pair-Set N1 F1 N2 F2)
-> (Nonempty-Pair-Set N1 F1 N2 F2))
((Pair-Set N1 F1 N2 F2) (Pair-Set N1 F1 N2 F2)
-> (Pair-Set N1 F1 N2 F2)))

with only small changes to the function body. IOW, I can get it to prove
that a union of a nonempty product set and a possibly empty product set
is nonempty, mostly just by using more specific annotations.

I'm fine with large types that happen to be useful theorems. They've
caught errors, made many dynamic checks unnecessary, and taught me
things about the code I'm writing. Kudos to the TR team.

Also, it struck me as funny that I had written a useful function with
more type than code. :D

Neil ⊥
____________________
Racket Users list:
http://lists.racket-lang.org/users

[Raoul Duke]

> I'm fine with large types that happen to be useful theorems. They've caught
> errors, made many dynamic checks unnecessary, and taught me things about the
> code I'm writing. Kudos to the TR team.

i am curious to know what other statically typed + checked languages
you've used, and how you feel they compare with TR. i haven't gotten
into TR yet myself, unfortunately. i'm excited that it exists, and
that it is encouraging other originally-not-statically-typed languages
to maybe get the static option cf. typed-clojure. but i also wonder
how much of TR's features were already done in other languages which
started out with static typing from the get-go.

[Eli Barzilay]

Three hours ago, Neil Toronto wrote:
> Typed Racket has arrived: it is useful to write programs in it in
> which types outnumber code.

(...and therefore having types go through macro-expansion is even more
obviously missing...)

--
((lambda (x) (x x)) (lambda (x) (x x))) Eli Barzilay:
http://barzilay.org/ Maze is Life!

[Raoul Duke]

On Tue, May 21, 2013 at 2:36 PM, Eli Barzilay <e...@barzilay.org> wrote:
> (...and therefore having types go through macro-expansion is even more
> obviously missing...)

could the macros+types be something as strong as e.g. metaocaml?
http://stackoverflow.com/questions/3037643/typed-metaprogramming-languages

[Eli Barzilay]

Yesterday, Raoul Duke wrote:
> On Tue, May 21, 2013 at 2:36 PM, Eli Barzilay <e...@barzilay.org> wrote:
> > (...and therefore having types go through macro-expansion is even
> > more obviously missing...)
>
> could the macros+types be something as strong as e.g. metaocaml?
> http://stackoverflow.com/questions/3037643/typed-metaprogramming-languages

That would be some way to communicate type information to the macro
expansion. What I'm talking about is much simpler: just macro-expand
the types like all other syntax, which gets you something that is
"only" as strong as Racket macros. (Later on, it can be extended in a
compatible way to know about types via something like syntax
properties, or a syntax-time parameter.)

--
((lambda (x) (x x)) (lambda (x) (x x))) Eli Barzilay:
http://barzilay.org/ Maze is Life!