[plt-scheme] Typed-Scheme, cond, match and wierd behaviour with non-disjoint types
Hi,
I met yet another issue. But to build up the context, lets define
something that works as expected.
#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