I think this "specific case" covers pretty much every abstract data type
written in Typed Racket, including all those exported by PFDS and
math/array. (Well, the RAList type in PFDS would have to wrap its lists
of roots in a struct to get great performance in untyped Racket instead
of just good performance.) In math/array, in particular, there are only
a few instances in which the typed code instantiates the Array type, all
having to do with conversions to and from FlArray and FCArray.
Yes, this would make me very happy. :)
Neil ⊥
On 01/06/2013 03:36 PM, Sam Tobin-Hochstadt wrote:
Right -- if we (the typed code) are picking the instantiation, then we
have to check structurally, to make sure that it's really got integers
everywhere.
But if it's a plain type parameter, then the untyped side gets to pick
it, and WLOG they could pick `Any`, meaning that there's no wrong
values they could supply. That means that as long as they supply a
`kons`, it must meet the contract of `(Kons A)`. So I think the
contract can be much cheaper in this one specific case, which
fortunately is the case that Neil cares about, I think.
Sam
On Sun, Jan 6, 2013 at 5:28 PM, Robby Findler
<ro...@eecs.northwestern.edu> wrote:
Oh-- I think you're right that the type parameter can matter (it could go
over to R as an Integer list and come back as a Boolean list or something).
Robby
On Sun, Jan 6, 2013 at 4:08 PM, Sam Tobin-Hochstadt <sa...@ccs.neu.edu>
wrote:
Sorry, that was very silly of me. That isn't what's happening at all,
because type soundness means we don't need to enforce the
parametricity at all.
The actual relevant program is:
(module m racket
(struct kons (a d))
(struct mt ())
(define MT (mt))
(define (FST v)
(when (eq? MT v) (error 'empty))
(kons-a v))
(define (RST v)
(when (eq? MT v) (error 'empty))
(kons-d v))
(define (LST . x)
(if (empty? x)
MT
(kons (first x) (apply LST (rest x)))))
(define (LST/C elem/c)
(define C (recursive-contract
(or/c (λ (v) (eq? v MT))
(struct/dc kons [a elem/c] [d C]))))
C)
(provide/contract
[LST (->* () #:rest any/c (LST/C any/c))]
[FST (-> (LST/C any/c) any/c)]
[RST (-> (LST/C any/c) (LST/C any/c))])
)
However, thinking about this more, it's an invariant that `kons`
structures are always correctly constructed, and we can rely on them
to have *some* instantiation that typechecks -- that's why the `any/c`
is ok. That suggests to me that contract generation for a struct type
applied to simple type variables can always be just the predicate for
that type, which would make Neil very happy. I want to think about
this more before I'm sure, though.
Thanks for being patient while I get this wrong in various ways ...
Sam
On Sun, Jan 6, 2013 at 4:13 PM, Robby Findler
<ro...@eecs.northwestern.edu> wrote:
This has a non-chaperone contract being used in a struct/c, I think?
(FST (LST 1 2 3)) => struct/dc: expected chaperone contracts, but field
a
has #<barrier-contract>
Robby
On Sun, Jan 6, 2013 at 2:40 PM, Sam Tobin-Hochstadt <sa...@ccs.neu.edu>
wrote:
On Sun, Jan 6, 2013 at 3:23 PM, Robby Findler
<ro...@eecs.northwestern.edu> wrote:
On Sun, Jan 6, 2013 at 2:18 PM, Sam Tobin-Hochstadt
<sa...@ccs.neu.edu>
wrote:
The boundaries have the information; that's how the contracts got
inserted
in the first place.
No, the contracts are parametric contracts using `parametric->/c`,
and
thus don't have any information about the types used at all.
I don't see why you can't tag them when something at a boundary and
then
check that something at another boundary instead of doing some deep
check.
The problem is that I don't know what to tag them *with*.
Consider the following program:
#lang racket
(struct kons (a d))
(struct mt ())
(define MT (mt))
(define (FST v)
(when (eq? MT v) (error 'empty))
(kons-a v))
(define (RST v)
(when (eq? MT v) (error 'empty))
(kons-d v))
(define (LST . x)
(if (empty? x)
MT
(kons (first x) (apply LST (rest x)))))
(define (LST/C elem/c)
(define C (recursive-contract
(or/c (λ (v) (eq? v MT))
(struct/c kons elem/c C))))
C)
(provide/contract
[LST (parametric->/c (A) (->* () #:rest A (LST/C A)))]
[FST (parametric->/c (A) (-> (LST/C A) A))]
[RST (parametric->/c (A) (-> (LST/C A) (LST/C A)))])
This is the essence of Neil's polymorphic list program, as implemented
by Typed Racket. I don't know how to change those contracts to not be
really expensive, because I can't pick the instantiation of A at
runtime to tag the structure instances with.
Sam
_________________________
Racket Developers list:
http://lists.racket-lang.org/dev
