[racket-dev] Motivation for polymorphic opaque types

On Sat, Jan 5, 2013 at 6:55 PM, Neil Toronto <neil.toronto at gmail.com> wrote:
>
> What if RAList could be exported as a polymorphic, opaque type?
>
> It seems the contract system could then exploit the fact that an RAList is
> always well-typed. What would it take? Tagging structs? A special chaperone?
> User-definable contracts for user struct types?
>
> If RAList were a polymorphic, opaque type, how could we put a contract on
> the following function, which instantiates it?
>
>   (: ralist-sum ((RAList Real) -> Real))
>   (define (ralist-sum lst)
>     (apply + (ralist->list lst)))
>
> Could exhaustively checking the structure of a polymorphic type be put off
> until such functions are called?
>
> Would it be impossible for mutable struct types to be opaque? Would having a
> type variable in positive position cause problems?
>
> I really don't want to write "Performance Warning: Using random-access lists
> in untyped Racket is currently 500x slower than using them in Typed Racket"
> at the top of the documentation for `data/ralist'.

There are two answers to the questions asked here.

1. Could we turn the structural checks into simpler constant-time
checks?  Answer: no.  The problem is that an untyped module can get
its hands on an (RAList Integer) and an (RAList String), and then
confuse them, say with `append`.  The only way to distinguish these
types is with structural checks of the implementation.

2. Could we delay some of these checks, so that `list-ref` could be
faster than O(N)? Answer: yes.  Robby has added the `#:lazy` variant
of structure contract checking, and you could try adding that to the
contract generation (in `typed-racket/private/type-contract.rkt`) and
see if that improves performance.  However, this may impose other
expensive overheads from chaperones and delayed checking, and thus may
not make you happy overall.  Also, this does not work for mutable
fields.

It may be that there's something clever here that I haven't thought
of, but I believe that polymorphic data structures and contract
boundaries involve substantial inherent costs, as you have discovered.

Sam