[racket-dev] type-case + typed racket yet?

7 hours ago, Shriram Krishnamurthi wrote:
> My understanding is that Eli has all these things for his PL course,
> right?

I do.


> So it's just a matter of making them more widely accessible?

But I don't want to do this... instead, I'd like TR to have some
better support for this.  The main thing that is bad about my thing is
that you need to know `match' and `cases', and they look very similar
(esp. now that `match' mostly caught up with handling struct names
easily) -- but you can't mix them.  So I'd really love to just get rid
of all my `cases' and replace them with `match' if it would do the
same.

The thing is that last time we talked about it, it wasn't clear what's
the best way to do so.  One rough sketch I had was:

  (define-type FOO (Bar String) (Baz Integer))

translates to (pseudo syntax, I can never remember the TR syntax
without looking at the docs):

  (struct: Bar (gensym123 String))   ; the slot names are
  (struct: Baz (gensym876 Integer))  ; not important
  (declare-disjoint-union FOO Bar Baz)

where that last imaginary thing defines FOO as (U Bar Baz), and tells
TR that if it sees Bar or Baz by themselves, then it should throw an
error.  This way you could only write a function that uses both as an
input, and never produce both as an output.

But now I wonder if it's enough to just avoid Bar and Baz from being
bound type names, so they can't be used directly -- in the above, you
won't be able to use `Bar' by itself, only `FOO', which will force you
to always consider the `Baz' case too.

Clearly, one missing link is a `match' form that can throw a type
error if the matched value has some non `None' type at the end.

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