[plt-scheme] More fun with typed scheme: attempt to write vector-join and a minor rant

On Mon, Nov 2, 2009 at 1:17 AM, Scott McLoughlin <scott at adrenaline.com> wrote:
> Or vector-append - but in any case, just a function that creates
> a single (Vectorof a) out a bunch of other (Vectorof a) arguments
> passed as rest arguments.

Like I said, I'll have better support for vectors in Typed Scheme,
hopefully today or tomorrow.

> So the signature is.
>
> (define: (a) (vector-join . [vecs : (Vectorof a) *]) : (Vectorof a)
>
> A blow by blow of the type errors is impossible at this point (unless Dr.
> Scheme has a logging feature of which I'm not aware.)
>
> But futzing around, (1) I first recalled from previous emails that some
> vector routines weren't "type-schemed" yet, so I wrote my own vector->list
> called tvector->list. Lovely routine, but that didn't do the trick.

`vector->list' has a type in Typed Scheme, so your function shouldn't
be necessary.

> Then I recalled reading the cool paper on the typed-scheme type system
> and how it handled, with near pure genius, higher order variable arity
> routines such as "map."  So, hmmm, I thought, and wrote my own nicely
> type-schemed "map1" which just did the job for a single list and nothing
> else fancy. That works lovely too, as it well should.
>
> ;;; tvector->list isn't a challenge
> (tvector->list #(2 3))
> (2 3)
>
>
> ;;; No general problem with map1
> (map1 string->symbol (list "ffdsaf" "d"))
> (ffdsaf d)
>
> Nevertheless, combining map or map1 with vector->list or tvector->list give
> nearly
> identical error messages.
>
> ;;; Original map type check error
> (map vector->list   (list #(2) #(1)))
> typecheck: Polymorphic function map could not be applied to arguments:
> Domain: (a b ... b -> c) (Listof a) (Listof b) ... b
> Arguments: (All (a) ((Vectorof a) -> (Listof a))) (List (Vectorof Integer)
> (Vectorof Integer))
> in: (#%app map vector->list (#%app list (quote #(2)) (quote #(1))))
>
> ;;; My map1 type check error, this type using tvector->list
> (map1 vector->list   (list #(2) #(1)))
> typecheck: Polymorphic function map1 could not be applied to arguments:
> Domain: (a -> b) (Listof a)
> Arguments: (All (a) ((Vectorof a) -> (Listof a))) (List (Vectorof Integer)
> (Vectorof Integer))
> in: (#%app map1 tvector->list (#%app list (quote #(2)) (quote #(1))))

This is because Typed Scheme, in general, can't infer the types when
you apply a polymorphic function (like `map') to a polymorphic
argument (like `vector->list').  I will improve the error message so
this is clear.

> So anyway, imagine lots of futzing and testing, breaking down each little
> part, of an already really short function to begin with, and making sure it
> works.  But alas, unless I'm terribly distracted by Next Iron Chef, I think
> there's
> some other reason I'm coming up empty handed.
>
> So any guidance, greatly appreciated.

Here's a solution:

(map #{vector->list @ Integer}  (list #(1) #(2)))

What that funny syntax does is explicitly instantiate the
`vector->list' function at the type Integer, so it no longer runs into
the problem described above.  If you don't like funny syntax, you can
also write this:

(map (inst vector->list Integer)  (list #(1) #(2)))

which does the same thing.

>
> OH OH OH OH - One last little thing that actually does tick off my normally
> serene demeanor.  As I understand it, (List a b c) is basically a tuple and
> (Listof a) is a list of type a.
> Well, unless I'm missing something, and yes, I certainly might be, the error
> messages
> you'll see above report rest arguments as if they were tuples: (List
> (Vec...) (Vec...)).
>
> Maybe there's some great reason for this, but it's yet another "undocumented
> feature"
> of typed-scheme that caused untold amounts of unnecessary staring at the
> screen and drooling
> on the keyboard on my part.

This isn't particular to rest arguments.  Typed Scheme knows that an
expression like (list #(2) #(1)) produces a fixed length list, and so
it reports that type in the expression.  There's really not much
difference between the two, so I'm not sure what caused your
confusion.  Can you clarify?

> Anyway, I LOVE the idea of typed scheme, and could even imagine loving
> WORKING with it, but given
> that nearly every time I've touched it I've had to post to this list and
> retrieved a response akin
> to, "Oh yeah, sorry, that's not really 100% yet," maybe it would be kinder
> to those whose
> time is actually worth something to actually pull the plug on the beloved
> feature until it gets
> the 1000's of test cases, ~50 pages of introductory tutorial and ~200+ pages
> of detailed
> documentation that the (otherwise nifty) language deserves.

First, people are using Typed Scheme for real. We've used it even in
undergraduate classes here at Northeastern.  But we could never have
the success we've had in PLT of making academic research software
useful to real people if we never showed it to anyone before it was
completely polished.  Even apart from academia, that isn't how any
free software project works.

> And neither of *those* teeny weeny tiny little languages have typed-scheme's
> complex manifest type
> system to fully describe, shine blindingly bright illumination on every
> corner case, and so on and
> so forth.
> Anyway, I'd MUCH rather just have typed-scheme work 95++ % of the time or at
> least see a
> carefully constructed and published road map regarding both HOW and WHEN
> type-scheme might
> finally achieve this level of ready for "prime time" status.

There's a few answers as to when.  First, it is, as the Beatles say,
getting better all the time.  Second, it gets better when people use
it, and complain about things they don't like, as you're doing, and
more help is always appreciated [1].  But the real answer is that
Typed Scheme is still a research project, and it would be foolish to
try to predict the schedule on which research will be successful.
That doesn't mean that more documentation and libraries and such won't
happen sooner, but problems like the one you describe in this email
are open research areas.

-- 
sam th
samth at ccs.neu.edu