On Wed, Jan 20, 2021 at 5:16 PM Dominik Pantůček
<[email protected]> wrote:
>
> Hi Sam,
>
> I went through all my notes and prepared minimal (sometimes) working
> examples for most of the issues I mentioned. Let's go through it one by
> one. I assume that some of the complications I encountered were because
> my lack of experience with Typed Racket. I hope some of these examples
> will be useful anyway.
>
> All the examples are in a git repository on Gitlab [1].
This is great, thanks! I've opened several issues for fixing some of
these problems.
> >> * Higher-order procedures and polymorphic functions in all imaginable
> >> combinations. That was a total disaster. Yes, the documentation clearly
> >> states that - but typing any code using these is like trying to break a
> >> badly designed cipher. Irregularities here and there. Sometimes simple
> >> `inst' was enough. Sometimes casting both the function and the arguments
> >> was necessary. The biggest trouble is that the error messages are very
> >> cryptic and sometimes even do not point to the offending construct but
> >> only the module file. I will provide MWE to show this if someone wants
> >> to look into it.
> >
> > An example would be great here. In general you should only need one
> > use of `inst` in any of these cases, and you shouldn't ever need a
> > `cast`.
>
> Directory "polymorph". In my use-case, there is a lot of structured
> S-expression data in the format:
>
> (define tagged-data-example
> '(data-2D
> ((B B B B)
> (B B B))))
>
> 9 steps of typing the procedure to calculate the maximum length of the
> 2D matrix are in this directory. All the errors are documented there.
> Yes, many of the intermediate constructs are wrong. The error in
> polymorph4.rkt shows the biggest problem I've seen so far. As a separate
> example, it is pretty easy to fix - but finding the source of the
> problem in a bigger module was not easy at all. Basically I ended up
> bi-partitioning the whole source code with procedure granularity and
> once I found the offending procedure a linear trial-and-error approach
> was the only option that allowed me to find the offending expression.
>
> Yes, the final polymorph9.rkt contains the approach that I actually used
> for resolving the issue.
Yikes, this is pretty terrible. Here's a nice simple version that works, though:
(define (typed-extract-data (tagged-data : (Pairof Symbol (Listof
(Listof (Listof Symbol)))))) : Number
(define data (car (cdr tagged-data)))
(define lengths (map (inst length Symbol) data))
1)
What's going on here is:
1. The type for `cadr` is not quite smart enough -- if it knows that
you have an at-least two element list, then it will produce the second
element type. Otherwise, if you have a (Listof T), it produces T. But
if you have a pair of a T and (Listof S), that ends up with (Union S
T).
2. I think there's a missing `syntax/loc` in the implementation of
`cast`, which resulted in the bad error message you saw.
I also think you're jumping too quickly to use `cast` -- before you do
that, you should try `ann`, for example, with the types of `length`
that you tried, which would have accomplished the same thing and
doesn't hide type errors or impose runtime costs.
> The actual problem I was referring to here is nicely shown in the
> "union" directory and it is about typing hash-union procedure.
>
> I do not know what solution should be considered correct if there were
> multiple differently-typed hash-tables in the same module. The explicit
> type information in require/typed is definitely not a good idea - but I
> found no better way.
Well, first we should make `racket/hash`'s exports work automatically.
But absent that, there are a few things going on here:
First, using `Any` is forgetting information, which is why the version
with `Any` everywhere produced an unsatisfactory result. In general,
one misconception I see regularly with Typed Racket users is using a
general type (such as `Any`) and then expecting Typed Racket to
specialize it when it's used. If you want that, you'd need to write a
polymorphic type, like this:
(hash-union (All (a b)
(-> (Immutable-HashTable a b)
(Immutable-HashTable a b)
(Immutable-HashTable a b)))))
Unfortunately, while this is the type you want, it can't work here
because contracts for hashes are limited in various ways. There are a
couple options to work around that.
1. Use `unsafe-require/typed` from `typed/racket/unsafe`. This works
with the type as written, but obviously if you make a mistake things
can go poorly.
2. Use a more restrictive type, such as `Any` or `Symbol` for the keys.
> >> * Classes: My notes say "AAAAAAAAAAAAAAAAAAAA". Which roughly says it
> >> all. Although I managed to back down to only using bitmap% class,
> >> properly typing all procedures using it was a nightmare. By properly I
> >> mean "it compiles and runs".
> >
> > More detail here would be helpful as well.
>
> The task was so simple and the solution so ugly. See the "classes"
> directory with 4 steps of typing a simple program to load a bitmap.
>
> Yes, normally I use (make-object bitmap% filename 'unknown/alpha) and it
> just works (racket/draw hides all the problems from the programmer). But
> I failed to require/typed it correctly. With explicit specification of
> object interface that is used, it worked. The bitmap4.rkt contains the
> code that I actually used.
Fortunately, this one has an easy solution: if you require
`typed/racket/draw`, then everything just works. Libraries that are
available like this are described here:
https://docs.racket-lang.org/ts-reference/Libraries_Provided_With_Typed_Racket.html
> >> * with-input-from-file does not accept Path or String, only Path-String
> >> and the conversion rules are either missing or strange at best.
> >> Basically I ended up with just converting to String and casting to
> >> Path-String to make everything work.
> >>
> >> * with-input-from-file also revealed that procedure signatures as types
> >> can be very tricky - just passing `read' was not possible, because it
> >> accepts some optional arguments. Wrapping it in thunk helped though.
> >
> > I don't understand what the problem was here; for example this works for me:
> >
> > #lang typed/racket
> > (with-input-from-file "/tmp/x.rkt" read)
>
> Yes, this works. The example in "input" directory shows the problem I
> had. Again, the trouble was I was working with a list where the first
> element is different from the rest of elements and I wanted to ensure
> type consistency for the rest of the code.
This, unfortunately, is just a case where Typed Racket is making you
face some potential problems that you might want to ignore. `read` can
produce anything, and you have to deal with that in Typed Racket.
That said, I might do things a bit differently than you ended up doing.
For example, you wrote `(with-input-from-file ... (cast read (->
DataDef)))` but I would probably do `(cast (with-input-from-file ...
read) DataDef)` because first-order checks are faster than
higher-order ones, and I also mostly try to use `assert` together with
predicates if you have them, because plain functions are usually
faster than contract system-generated ones.
> >> * Type annotations of procedures with variadic arguments. The only place
> >> where I had to put annotations outside of the procedure definition. It
> >> is nothing super-problematic, but it feels inconsistent with the rest.
> >
> > I would encourage type annotations before the procedure definition in
> > all cases -- the `define` form doesn't really have the right places to
> > put everything that can go in a function type.
>
> And what about procedures created with lambda? I thought the (define
> (proc args ...) body ...) is just a syntactic sugar around (define proc
> (lambda (args ...) body ...)) - so I thought the type annotations are
> the same as well. Or do I miss something here?
Indeed, using the (proc args ...) style is most a simple shortcut (but
see exceptions wrt keyword/optional arguments). This is true for Typed
Racket too. For annotating `lambda`s directly, usually the trickier
cases are less significant. If you run into them, then using `ann`
will produce the same results as the top-level annotation.
> >> * Syntax macros are extra hard. As I use some syntax trickery to convert
> >> semi-regular code to "futurized" one, I basically gave up and just ran
> >> everything single-threaded. The main issue is passing type information
> >> from the module that uses the macro to the macro and matching it on both
> >> sides. Also the macro must split the type annotation from argument names
> >> in the syntax pattern when it defines new procedures - I did some ugly
> >> hacks to get through it but in the end I just refrained from using them
> >> when possible (except for the unsafe-struct macro, of course).
> >> commits, 2292-line diff!) and genuinely (it really helped).
> >
> > An example here would be great too.
>
> Two examples are in the "syntax" directory. First one with the three
> stages of typing a struct. The need for explicitly extracting the field
> names differently than without TR is not very convenient. When I tried
> to make a "universal" macro that would handle both typed and untyped
> variants, I failed (but I bailed out quickly as that was not my goal).
Note that just handling all cases of `struct`, even in untyped Racket,
will require the same thing.
> The second example is my common define-futurized syntax macro. The TS
> version shows the :1, :2 and ::: as non-validating syntax template
> placeholders (just something that matches the expression but does not do
> any actual syntax checking). Is there a better way? (I would think so).
Yes, you want to use the "literals" feature in `syntax-case`. In other
words, you'd write:
(define-syntax (define-futurized stx)
(syntax-case stx (:)
((_ (proc (start : stype) (end : etype)) : RetType body ...)
.....)))
--
You received this message because you are subscribed to the Google Groups
"Racket Users" group.
To unsubscribe from this group and stop receiving emails from it, send an email
to [email protected].
To view this discussion on the web visit
https://groups.google.com/d/msgid/racket-users/CAK%3DHD%2BZasYSVtV8A0iY7GR4BG_-QSPGZ9zgmAFHew-fjK-3h-g%40mail.gmail.com.
