Typed Racket: Casting to types containing type variables

[unlimitedscolobb]

Hello,

I'm trying to get something similar to the following code working:

#lang typed/racket

(: f (-> Integer Any))
(define (f x) (+ 1 x))

(: g (All (a) (-> Integer a)))
(define (g x) (f x))

Of course, this gets me a type error:

;Type Checker: type mismatch
;   expected: a
;   given: Any
;   in: (f x)

Now, I try to throw a cast into g:

(: g (All (a) (-> Integer a)))
(define (g x) (cast (f x) a))

This gives the following type error:

;Type Checker: Type a could not be converted to a contract because it contains free variables.
;   in: a

Does this mean that I can never cast to types containing type variables?

My original problem comes from playing around with eval, which returns AnyValues.  Ideally, I would like to be able to retrieve the first returned value (done), and then convert it to a type variable bound by one of the arguments:

(: my-super-func (All (a) (-> (Type1 a) a)))
(define (my-super-func arg)
  ...
  (get-first-value (eval some-stuff))) ; how to cast to a ?

-

Sergiu

[Ben Greenman]

On 2/19/20, unlimitedscolobb <unlimite...@gmail.com> wrote:
>
> [....]

>
> ;Type Checker: Type a could not be converted to a contract because it
> contains free variables.
> ; in: a
>
> Does this mean that I can never cast to types containing type variables?

Yes

> My original problem comes from playing around with eval, which returns
> AnyValues. Ideally, I would like to be able to retrieve the first returned
>
> value (done), and then convert it to a type variable bound by one of the
> arguments:
>
> (: my-super-func (All (a) (-> (Type1 a) a)))
> (define (my-super-func arg)
> ...
> (get-first-value (eval some-stuff))) ; how to cast to a ?

You can ask the caller to supply a cast function that turns an Any to an A.

But depending on what you want to cast to, occurrence typing may be
more convenient. For example:

#lang typed/racket

(: my-super-func (All (a) (-> (-> Any) (-> Any Boolean : #:+ a) a)))
(define (my-super-func get-v check-v)
(assert (get-v) check-v))

(ann (my-super-func (lambda () 42) exact-integer?) Integer);
;; 42
(ann (my-super-func (lambda () '(A)) (lambda (x) (and (list? x)
(andmap symbol? x)))) (Listof Symbol))
;; '(A)

[unlimitedscolobb]

Hi Ben,

Thank you for your answer.

On Thursday, February 20, 2020 at 3:29:15 AM UTC+1, Ben Greenman wrote:

On 2/19/20, unlimitedscolobb <unlimite...@gmail.com> wrote:
>
> [....]
>
> ;Type Checker: Type a could not be converted to a contract because it
> contains free variables.
> ;   in: a
>
> Does this mean that I can never cast to types containing type variables?

Yes

Ah, okay, got it.

 

> My original problem comes from playing around with eval, which returns
> AnyValues.  Ideally, I would like to be able to retrieve the first returned
>
> value (done), and then convert it to a type variable bound by one of the
> arguments:
>
> (: my-super-func (All (a) (-> (Type1 a) a)))
> (define (my-super-func arg)
>   ...
>   (get-first-value (eval some-stuff))) ; how to cast to a ?

You can ask the caller to supply a cast function that turns an Any to an A.

Ahaa, that's a clever idea!

But depending on what you want to cast to, occurrence typing may be
more convenient. For example:

#lang typed/racket

(: my-super-func (All (a) (-> (-> Any) (-> Any Boolean : #:+ a) a)))
(define (my-super-func get-v check-v)
  (assert (get-v) check-v))

(ann (my-super-func (lambda () 42) exact-integer?) Integer);
;; 42
(ann (my-super-func (lambda () '(A)) (lambda (x) (and (list? x)
(andmap symbol? x)))) (Listof Symbol))
;; '(A)

This does look quite a bit like lifting contracts to types, very nice.

Thank you very much for clarifying and giving a detailed example.  I'm coming over from Haskell, so I'm still in process of wrapping my head around types and contracts in Racket.

-

Sergiu