bennn / require-typed-scv

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

Can typed racket print contracts? #2

Open bennn opened 7 years ago

bennn commented 7 years ago

Can typed racket print the contracts it generated with require/typed? I think I remember Asumu showing me this.

bennn commented 7 years ago

Nothing stands out ... I asked on Slack, here's the conversation:

ben [4:23 PM] 
@asumu (or anyone) is there an easy way to print the contracts Typed Racket will make from a type?

[4:23] 
specifically from a `require/typed` ... I think I remember you showing me how to do this

samth [4:25 PM] 
@ben you probably want `value-contract` ... ?

[4:25] 
or do I misunderstand?

ben [4:27 PM] 
@samth yeah I tried that, but got `#f`. http://pasterack.org/pastes/85129

[4:29] 
a hard thing that worked: expand the typed module, copy/paste part of the `#%contract-defs` submodule

[4:30] 
so I'm now looking into what I can `require`` from that submodule, but was hoping there was something easier

samth [4:32 PM] 
I don't know of more than that to do

ben [4:32 PM] 
ok. Any idea why `value-contract` is returning `#f`?

samth [4:32 PM] 
no, but I'd try calling it not in the typed module

[4:34] 
maybe because of the contract on value-contract

ben [4:37 PM] 
yes that works, http://pasterack.org/pastes/22709

[4:38] 
(strange things: just providing `f` or doing a `rename-out` instead of `define` both give `#f` for the `value-contract`)
bennn commented 7 years ago

Code from the working paste:

#lang racket/base

(module u racket/base
  (define f (lambda (x) x))
  (provide f))

(module t typed/racket/base
  (require/typed (submod ".." u)
    (f (-> Symbol Symbol)))
  (define g f)
  (provide g))

(require 't)
(require racket/contract)

(value-contract g)
bennn commented 7 years ago

TODO try just printing the output of type->contract, whatever it is.

Like, have a file with a require/typed and print the contracts it makes.