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].
>> * 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.
>
>> * unsafe/ops: unsafe-vector-* resisted a lot - until I just gave up and
>> require/typed it for my particular types. Maybe casting would help, but
>> the error messages were different to the classical problems of the
>> polymorphic functions in TR.
>
> Can you say more about what happened here?
I completely mixed things up. It was not unsafe/ops, actually there was
just a minor misunderstanding on my side and after I realized what's
wrong, it worked like a charm.
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.
>
>> * 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.
>
>> * 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.
>
> and `Path-String` is just the union of Path and String.
Turns out I must have some other error there as well. I cannot reproduce
it on its own and I wasn't tagging the whole tree when I encountered new
problems. Next time I am tagging the repository so that I can get back
to the exact bigger example of the problem and eventually see what
caused it.
>
>> * order of definitions matters. Not that this is unexpected, it is just
>> strange when working with larger code-base where it didn't matter.
>> Actually the error messages were helpful here.
>
> What do you mean by "order of definitions matters" here?
This one is completely lost. Again - it could have been something
different. The problem was that when I reordered the defines for some
functions and types, suddenly it started working.
>
>> * 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?
>
>> * More modules need to be required everywhere. If module A provides a
>> procedure that accepts a type from module B, all modules using that
>> procedure must also require the module B to know the type. In normal
>> Racket it does not matter as long as you just pass the opaque data along.
>
> Can you give an example?
I tried in the "modules" directory - but frankly, it works here as I
needed it to work. My problem was that when module B was not typed at
all, and modules A and C were, the type checks failed and I had to type
the whole module B. Of course the actual configuration contained way
more definitions and I didn't investigate what triggered the problem. I
assumed what I have written - that it is not possible. Yet my example
shows that it actually works. Let's see what I find when I encounter it
in the future.
>
>> * 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).
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).
I will definitely play with Typed Racket more now. But ultimately I want
to see the performance benefits from this venture. My usual approach is
to structure my modules in a way that there is always uncontracted
implementation and a wrapper module with contracts. Basically I use the
"design by contract" approach (not strictly, but most of the time).
Statically verified code should be in theory faster in the end - so I am
curious if (or more likely "when") it pays off performance-wise.
Cheers,
Dominik
[1] https://gitlab.com/racketeer/tr-mwe
--
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/4deede7e-5dd4-c86d-6638-f4bcbd4ee640%40trustica.cz.
