[plt-scheme] Typed-Scheme, cond, match and wierd behaviour with non-disjoint types

On Tue, Apr 7, 2009 at 3:15 PM, Paulo J. Matos <pocmatos at gmail.com> wrote:
> Hi,
>
> I met yet another issue. But to build up the context, lets define
> something that works as expected.

Paulo,

It's not entirely clear what the issue is with the function that needs
a mytype2. Does the following do what you want?

#lang typed-scheme

(require scheme/match)

(define-type-alias mytype1 (U Integer Char))
(define-type-alias mytype2 (U Integer String))

(: test (mytype1 -> mytype2))
(define (test x)
  (cond
    ((integer? x) x)
    ((char? x) (make-string 1 x))))

(: test-alt (mytype1 -> mytype2))
(define (test-alt x)
  (match x
    ((? integer? x) x)
    ((? char? x) (make-string 1 x))))


(: test5 (mytype2 -> Boolean))
(define (test5 y)
  (cond
    ((integer? y) #t)
    ((and (string? y) (= (string-length y) 1)) #t)
    (else #f)))

(test5 (test 42))
(test5 (test #\a))
(test5 "yoyo")

(newline)
(test5 (test-alt 42))
(test5 (test-alt #\a))


Anthony
> #lang typed-scheme
>
> (require scheme/match)
>
> (define-type-alias mytype1 (U Integer Char))
> (define-type-alias mytype2 (U Integer String))
>
> (: test (case-lambda
>          [Integer -> Integer]
>          [Char -> String]
>          [mytype1 -> mytype2]))
> (define (test x)
>  (cond [(integer? x)
>         x]
>        [(char? x)
>         (make-string 1 x)]))
>
> You might be thinking... why the [mytype1 -> mytype2] in the typing
> but that will come quickly.
> I am however, using match in my program so I assumed the following
> would be equivalent:
> (: test2 (case-lambda
>          [Integer -> Integer]
>          [Char -> String]))
>          [mytype1 -> mytype2]))
> (define (test2 x)
>  (match x
>    ((? integer?)
>     x)
>    ((? char?)
>     (make-string 1 x))))
>
> However, it is not...
> . typecheck: No function domains matched in function application:
> Domains: Integer
>        Integer Char
> Arguments: Integer mytype1
>  in: (make-string 1 x)
> . typecheck: Expected mytype2, but got mytype1 in: x
>
> If I change the typing of test2 to remove the last line, it works... :)
> (: test2 (case-lambda
>          [Integer -> Integer]
>          [Char -> String]))
> (define (test2 x)
>  (match x
>    ((? integer?)
>     x)
>    ((? char?)
>     (make-string 1 x))))
>
> But then again, there's a reason why I need that line.... Because some
> functions expect a mytype2 as result and if it is not there explicitly
> it fails... For example:
> (: test3 (mytype1 -> mytype2))
> (define (test3 x)
>  (test2 x))
>
> with the last version of test2 gives:
> . typecheck: No function domains matched in function application:
> Domains: Integer
>        Char
> Arguments: mytype1
>  in: (test2 x)
>
> Now, I am not sure where the problem lies but the last error message
> is suspicious... if the domains are Integer or Char then a mytype1
> should do it since a mytype1 is exactly that... an Integer or a
> Char... Any workaround on something like this?
>
> Cheers,
>
> --
> Paulo Jorge Matos - pocmatos at gmail.com
> Webpage: http://www.personal.soton.ac.uk/pocm
> _________________________________________________
>  For list-related administrative tasks:
>  http://list.cs.brown.edu/mailman/listinfo/plt-scheme
>