search

bennn / require-typed-scv

Typed Racket's `require/typed`, with soft contract verification
Other
1 stars 0 forks source link

recursive types #9

Closed bennn closed 7 years ago

bennn commented 7 years ago

Here's the beginning of zombie (soft contracts benchmark)

#lang typed/racket/base

(require
  require-typed-check
  "image-adapted.rkt"
)
(require/typed/check "zombie.rkt"
  (w0 World)
  (world-on-mouse (-> World (-> Real Real String World)))
  (world-on-tick (-> World (-> World)))
)

(define-type World
  (-> Symbol (U (Pairof 'on-mouse (-> Real Real String World))
                (Pairof 'on-tick (-> World))
                (Pairof 'to-draw (-> Image))
                (Pairof 'stop-when (-> Boolean)))))

We should be able to turn the recursive type into a recursive contract.

Maybe start with Rec types? But I think there's no such thing as anonymous recursive contracts.

bennn commented 7 years ago

Dear Ben, anonymous recursive contracts are easy. See http://docs.racket-lang.org/syntax-parse-example/index.html?q=syntax-parse-ex#%28part._rec_c%29

bennn commented 7 years ago

Probably fixed in https://github.com/bennn/require-typed-scv/commit/bd8c0343ef0da0af95f09350a4c0e903b3221f9d

At least the old programs still run, haven't gotten zombie to work (unbound type T).