Re: Puzzled by Typed Racket

On Mar 3, 2016, at 12:47 PM, Sam Tobin-Hochstadt <[email protected]> wrote:

> On Thu, Mar 3, 2016 at 4:26 AM, Antonio Menezes Leitao
> <[email protected]> wrote:
>> Hi,
>> 
>> Here is a MWE for something that is puzzling me. In file testtyped.rkt, I have
>> 
>> #lang typed/racket
>> 
>> (provide foobar)
>> 
>> (struct (T) foo
>>  ([x : (T -> T)]))
>> 
>> (define (foobar [a : Boolean])
>>  (if a
>>      (foo (lambda ([x : Number]) x))
>>      (foo (lambda ([x : String]) x))))
>> 
>> In the REPL, I can test this file and it works fine:
>> 
>> Language: typed/racket; memory limit: 2048 MB.
>>> foobar
>> - : (-> Boolean (U (foo Number) (foo String)))
>> #<procedure:foobar>
>>> (foobar #t)
>> - : (U (foo Number) (foo String))
>> #<foo>
>>> (foobar #f)
>> - : (U (foo Number) (foo String))
>> #<foo>
>> 
>> 
>> However, using it from non-typed racket causes an error.  If, in file
>> test.rkt we have:
>> 
>> #lang racket
>> (require "testtyped.rkt")
>> 
>> ;;Note that this is _not_ typed/racket
>> 
>> Then the same example stops working:
>> 
>>> (foobar #t)
>> . . foobar: broke its own contract
>>  two of the clauses in the or/c might both match: (struct/c foo (->
>> Number any)) and (struct/c foo (-> String any))
>>  produced: #<foo>
>>  in: the range of
>>      (->
>>       (or/c #f #t)
>>       (or/c
>>        (struct/c foo (-> Number any))
>>        (struct/c foo (-> String any))))
>>  contract from:
>>      C:\Users\aml\Dropbox\AML\Projects\Rosetta\testtyped.rkt
>>  blaming: C:\Users\aml\Dropbox\AML\Projects\Rosetta\testtyped.rkt
>>   (assuming the contract is correct)
>>  at: C:\Users\aml\Dropbox\AML\Projects\Rosetta\testtyped.rkt:3.9
>> 
>> I know that Typed Racket has limitations in the generation of
>> contracts. Is this one of them? Is there a workaround?
> 
> Unfortunately, this is a real limitation. You end up with a union type
> in the result, and it's one that can't be decided immediately, since
> there are function contracts inside the struct contract.
> 
> In many cases, you can avoid a union of functions by pushing the union
> type inside the function type. But that's not the case here, because
> the type T appears in both the domain and the range of the function.
> 
> If you can say more about your actual use case, maybe I can be more helpful.


Sam, what bugs me about your explanation is that we could in principle
spell out the two types and stick them in Union and the problem would go 
away:


#lang racket

(module server typed/racket
  
  (provide foobar)
  
  (struct foo ([x : (U (Number  -> Number) (String -> String))]))

  (: foobar (Boolean -> foo))
  (define (foobar [a : Boolean])
    (if a
        (foo (lambda ([x : Number]) x))
        (foo (lambda ([x : String]) x)))))

(require 'server)

(foobar #t)

I think the explanation has to go back to polymorphism at export time. 

-- Matthias


-- 
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+unsubscribe-/JYPxA39Uh5TLH3MbocFF+G/[email protected]
For more options, visit https://groups.google.com/d/optout.