Open Fyrbll opened 1 year ago
v8.7.0.6
#lang typed/racket #:no-optimize #:with-refinements ;; `theorem_1` is accepted by the typechecker. Good. (: theorem_1 ((Refine (x : Integer) (= x 0)) -> Zero)) (define theorem_1 identity) ;; `theorem_2` is accepted by the typechecker. Good. (: theorem_2 (Zero -> (Refine (x : Integer) (= x 0)))) (define theorem_2 identity) ;; Contrary to my intuition, the typechecker rejects `theorem_3`. ;; (: theorem_3 ((Refine (x : Integer) (= x 2)) -> 2)) ;; (define theorem_3 identity) ;; Contrary to my intuition, the typechecker accepts `theorem_4` (: theorem_4 (Refine (x : 1) (= x 2))) (define theorem_4 1) ;; Contrary to my intuition, the typechecker accepts `theorem_5` (: theorem_5 ((Refine (x : Integer) (= x 1)) (Refine (x : Integer) (= x 3)) -> (Refine (x : Integer) (= x 5)))) (define (theorem_5 m n) (+ m n)) ;; The typechecker rejects `theorem_6` with the message ;; "Expected result: Nothing". Good. ;; (: theorem_6 (Refine (x : (Pairof Integer Integer)) ;; (and (= (car x) 1) (= (cdr x) 3) ;; (= (+ (car x) (cdr x)) 5)))) ;; (define theorem_6 (cons 1 3)) ;; Contrary to my intuition, the typechecker rejects `theorem_7`. ;; (: theorem_7 (Refine (x : (Pairof 1 3)) (= (+ (car x) (cdr x)) 4))) ;; (define theorem_7 (cons 1 3)) ;; Contrary to my intuition, the typechecker accepts `theorem_8`. (: theorem_8 (Refine (x : (Pairof 1 1)) (= (+ (car x) (cdr x)) 4))) (define theorem_8 (cons 1 1))
Please check the comments in the code above. I think the intuitive behavior should be evident, but I could be mistaken.
In some situations, I get an error when I think I should not. In other situations, the typechecker accepts a definition that should not work.
What version of Racket are you using?
v8.7.0.6
What program did you run?
What should have happened?
Please check the comments in the code above. I think the intuitive behavior should be evident, but I could be mistaken.
If you got an error message, please include it here.
In some situations, I get an error when I think I should not. In other situations, the typechecker accepts a definition that should not work.