On Wed, Jan 20, 2021 at 5:16 PM Dominik Pantůček
<dominik.pantu...@trustica.cz> 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 racket-users+unsubscr...@googlegroups.com.
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.
