Help: How to check a typed/racket type in an untyped Racket contract?

[James Geddes]

This is likely a typed-untyped interface newbie question.

Briefly, how can I write a contract that asserts that some value has a type that is defined in an imported typed/racket library?

In more detail, I am using the math/distributions library, which is written in typed/racket. My module is written in untyped Racket, and I'm figuring out how to use contacts:

#lang racket
(require math/distributions) ;; this is a typed/racket library

(define my-dist (discrete-dist '(thing-one thing-two)))

(provide (contract-out [my-dist ???]))


The question is: what should ??? be?. There is a distribution? predicate but I'd quite like to be more specific: namely, that my-dist is a discrete distribution. In the source of math/distributions, the following type is defined:

(define-type (Discrete-Dist A) (discrete-dist-struct A A))

but I don't know how this might translate into my untyped module.


Any help much appreciated!

James




-------------------------------
James Geddes

[Matthias Felleisen]

This is a great question. It suggests we should provide these generated contracts (or grant access them) via a modicum of reflection.

In the meantime, you want to look at the result type of discrete-dist, which is the type (Discrete-Dist A). This is turn is a subtype of (dist A A), which is opaque/undocumented/I can’t find it in the code base (on the fly). It’s not exported. So at the moment, your will have to take the fall if someone abuses it.

— Matthias

[Matthias Felleisen]

After some poking around, here is what I can offer:

#lang racket

(module predicates racket
(provide discrete-dist-thing?)

;; ---------------------------------
;; dependencies
(require math/distributions)

;; ---------------------------------
;; implementation
(define (discrete-dist-thing? x)
(define is-it-discrete-dist-values
(with-handlers ([exn:fail? (lambda (xn)
(define msg (exn-message xn))
(if (regexp-match? #rx"expected: discrete-dist-struct" msg)
#false
(raise xn)))])
(discrete-dist-values x)))
(and is-it-discrete-dist-values
(andmap symbol? is-it-discrete-dist-values)
(let ([probs (discrete-dist-probs x)])
(and (andmap flonum? probs) (andmap positive? probs))))))

(module server racket
(require (submod ".." predicates))
(provide
(contract-out
[d discrete-dist-thing?]))

;; ---------------------------------
;; dependencies
(require math/distributions)

;; ---------------------------------
;; implementation
(define d (discrete-dist '(one two))))

(require 'server)
d


Watch for symbol?. You want to abstract over that.

> --
> You received this message because you are subscribed to the Google Groups "Racket Users" group.
> To unsubscribe from this group and stop receiving emails from it, send an email to racket-users...@googlegroups.com.
> For more options, visit https://groups.google.com/d/optout.

[James Geddes]

Matthias,

Thank you, that's really helpful, both for letting me know I'm not being an idiot (always welcome!) and for the example code, which makes me realise I should learn about exceptions next.

Many thanks again,

James


-------------------------------
James Geddes

[Matthias Felleisen]

> On Jul 31, 2017, at 5:27 AM, James Geddes <jge...@turing.ac.uk> wrote:
>
>
> Matthias,
>
> Thank you, that's really helpful, both for letting me know I'm not being an idiot (always welcome!) and for the example code, which makes me realise I should learn about exceptions next.
>
> Many thanks again,
>
> James

Writing predicates via exceptions is a less than ideal situation.

The proper solution would be to change Typed Racket to provide
the contracts that come with exported identifiers or similar
solutions.

But knowing how exceptions work is a ‘good thing.’

[Sam Tobin-Hochstadt]

One other suggestion: you can use `define-predicate` in a Typed Racket
module to create a predicate for any type that can be checked
immediately. So

```
(define-predicate dist? (Discrete-Dist Your-Type-Here))
```

should define the predicate you want.

Sam

[bruno cuconato]

hi,

I'm trying to use a data structure defined in a typed racket module in my untyped code.

I'm want it to be accessible from a generic interface, so I'm using `define-generics`'s #:fast-defaults for

dispatching to the proper methods (this might not be the best practice though, and if so I welcome corrections).

to do this I need a predicate for the type of data structure, hence my replying to this thread.

would Matthias' suggestion be the best long-term solution here?

> It suggests we should provide these generated contracts (or grant access them) via a modicum of reflection.

I couldn't get Sam's solution to work, most likely because I haven't read much about typed racket yet. I tried

both

`(define-predicate RBTree? (All (A) (RedBlackTree A))) `

and

`(define-predicate RBTree? (RedBlackTree Any)) `

but none of them seem to work. even if I could get it to work,

I still like Matthias' suggestion because I wouldn't need to create

another module.

cheers,

-- bruno cuconato

> To unsubscribe from this group and stop receiving emails from it, send an email to racket...@googlegroups.com.

[Ben Greenman]

What happens if you provide the data structure from Typed Racket and
require it in an untyped module?

>> an email to racket...@googlegroups.com <javascript:>.

>> > For more options, visit https://groups.google.com/d/optout.
>>
>

> --
> You received this message because you are subscribed to the Google Groups
> "Racket Users" group.
> To unsubscribe from this group and stop receiving emails from it, send an

> email to racket-users...@googlegroups.com.
> To view this discussion on the web visit
> https://groups.google.com/d/msgid/racket-users/2f278821-a585-42c4-b7a4-1ade07a228f8%40googlegroups.com.