typed-racket

typed-racket copied to clipboard

What version of Racket are you using?

v8.2

What program did you run?

Program 1:

#lang typed/racket

(: m0 (MPairof String Null))
(define m0 (mcons "world" '()))

(: m1 (MPairof Number (MPairof Symbol (MPairof String Null))))
(define m1 (mcons 123 (mcons 'hello m0)))


(displayln m0)
(displayln m1)

Program 2:

#lang typed/racket

(: m0 (MPairof String Null))
(define m0 (mcons "world" '()))

(: m1 (MPairof Symbol (MPairof String Null)))
(define m1 (mcons 'hello m0))

(: m2 (MPairof Symbol (MPairof String Null)))
(define m2 (mcons 'hello (mcons "world" '())))

(: m3 (MPairof Symbol (MPairof String Null)))
(define m3 (mcons 'hello (mcons "world" (ann '() Null))))

(: m4 (MPairof Symbol (MPairof String Null)))
(define m4 (mcons 'hello (ann (mcons "world" '()) (MPairof String Null))))


(displayln m0)
(displayln m1)
(displayln m2)
(displayln m3)

What should have happened?

Printing values.

If you got an error message, please include it here.

Program 1:

Type Checker: Polymorphic function `mcons' could not be applied to arguments:
Argument 1:
  Expected: a
  Given:    Positive-Byte
Argument 2:
  Expected: b
  Given:    (MPairof Symbol (MListof String))

Result type:     (MPairof a b)
Expected result: (MPairof Number (MPairof Symbol (MPairof String Null)))

  in: (mcons 123 (mcons (quote hello) m0))

(MPairof String Null) (m0's type) is regarded as a subtype of (MListof String).

> (: m0 (MPairof String Null))
> (define m0 (mcons "world" '()))
> m0
- : (MListof String) [more precisely: (MPairof String Null)]
(mcons "world" '())

> (: m1 (MListof String))
> (define m1 (mcons "world" '()))
> m1
- : (MListof String)
(mcons "world" '())

> (: m2 (MListof String))
> (define m2 (mcons "world" '()))
> m2
- : (MListof String)
(mcons "world" '())

> (set-mcdr! m1 m2)
> m1
- : (MListof String)
(mcons "world" (mcons "world" '()))

> (set-mcdr! m0 m2)
; Type Checker: Polymorphic function `set-mcdr!' could not
;   be applied to arguments:
; Domains: (MListof a) (MListof a)
;          (MPairof a b) b
; Arguments: (MPairof String Null) (MListof String)
;   in: (set-mcdr! m0 m2)
; [,bt for context]
> m0
- : (MListof String) [more precisely: (MPairof String Null)]
(mcons "world" '())

Program 2:

draft1.rkt:10:11: Type Checker: Polymorphic function `mcons' could not be applied to arguments:
Argument 1:
  Expected: a
  Given:    'hello
Argument 2:
  Expected: b
  Given:    (MPairof String (Listof Any))

Result type:     (MPairof a b)
Expected result: (MPairof Symbol (MPairof String Null))

  in: (mcons (quote hello) (mcons "world" (quote ())))
  location...:
   draft1.rkt:10:11
  context...:
   /usr/share/racket/pkgs/typed-racket-lib/typed-racket/utils/tc-utils.rkt:123:0: report-all-errors
   /usr/share/racket/pkgs/typed-racket-lib/typed-racket/typecheck/tc-toplevel.rkt:391:0: type-check
   /usr/share/racket/pkgs/typed-racket-lib/typed-racket/typecheck/tc-toplevel.rkt:635:0: tc-module
   /usr/share/racket/pkgs/typed-racket-lib/typed-racket/tc-setup.rkt:101:12
   /usr/share/racket/pkgs/typed-racket-lib/typed-racket/typed-racket.rkt:22:4
draft1.rkt:13:11: Type Checker: Polymorphic function `mcons' could not be applied to arguments:
Argument 1:
  Expected: a
  Given:    'hello
Argument 2:
  Expected: b
  Given:    (MPairof String (Listof Any))

Result type:     (MPairof a b)
Expected result: (MPairof Symbol (MPairof String Null))

  in: (mcons (quote hello) (mcons "world" (ann (quote ()) Null)))
  location...:
   draft1.rkt:13:11
  context...:
   /usr/share/racket/pkgs/typed-racket-lib/typed-racket/utils/tc-utils.rkt:123:0: report-all-errors
   /usr/share/racket/pkgs/typed-racket-lib/typed-racket/typecheck/tc-toplevel.rkt:391:0: type-check
   /usr/share/racket/pkgs/typed-racket-lib/typed-racket/typecheck/tc-toplevel.rkt:635:0: tc-module
   /usr/share/racket/pkgs/typed-racket-lib/typed-racket/tc-setup.rkt:101:12
   /usr/share/racket/pkgs/typed-racket-lib/typed-racket/typed-racket.rkt:22:4
Type Checker: Summary: 2 errors encountered
  location...:
   draft1.rkt:10:11
   draft1.rkt:13:11
  context...:
   /usr/share/racket/pkgs/typed-racket-lib/typed-racket/typecheck/tc-toplevel.rkt:391:0: type-check
   /usr/share/racket/pkgs/typed-racket-lib/typed-racket/typecheck/tc-toplevel.rkt:635:0: tc-module
   /usr/share/racket/pkgs/typed-racket-lib/typed-racket/tc-setup.rkt:101:12
   /usr/share/racket/pkgs/typed-racket-lib/typed-racket/typed-racket.rkt:22:4

I'm not sure why '()'s type is regarded as (Listof Any) instead of Null (even though I manually annotate its type).

For program A, the real issue here is that m0's type is incorrectly lifted to be (Mlistof String) during inference. I guess program B fails to type-check for a similar reason.

My initial investigation shows this issue has nothing to do with subtyping. Type generalization indeed promotes (MPair String Null) to(MList String) , but it is not the culprit. The real issue is probably the type checker is unable to check argument expressions using by-position type arguments in an expected type when it comes to checking nested polymorphic function application.

Here is another example:

(: a (Pairof String (Pairof String Null)))
(define a (cons "10" (cons "20" null)))

This problem also fails to check because the typechecker does not use (Pairof String Null) to check (cons "20" null). Instead, it treats (cons "20" null) as if it has no expected type and ends up generalizing the result type.

If we split up the two cons expression above, it will type-check correctly:

(: b (Pairof String Null))
(define b (cons "20" null))

(: a (Pairof String (Pairof String Null)))
(define a (cons "10" b))

My understanding is without a proper kind system, this would be very tricky to fix given the current Typed Racket infrastructure.

[I don't think you are the first person that has ever run into this problem. There should be some old similar issues, but I couldn't find one]