Allow definitions to be redefined with different type on top level (repl)?

[Inc0n]

What version of Racket are you using?

Racket 8.5 [cs]

What program did you run?

(define (a x) x)
(define (a x) (+ 1 x))

What should have happened?

(a 1) would evaluate to 2 now.

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

; :2593:14: Type Checker: No function domains matched in function application:
; Types: Number * -> Number
; Arguments: One Any
; Expected result: Any
;
; in: (+ 1 x)

The change in function signature cause a redefinition to fail, where as in untyped racket, this would succeed.

[sorawee]

This has nothing to do with redefinition. If you entered (define (a x) (+ 1 x)) first, it would fail too. As the error message suggested, x can be anything, e.g. a String, so (+ 1 x) doesn't type check.

By annotating that x must be a Number, it now works fine in the REPL:

> (: a (-> Number Number))
> (define (a x) x)
> (define (a x) (+ 1 x))

[racket-discourse-github-bot]

This issue has been mentioned on Racket Discussions. There might be relevant details there:

https://racket.discourse.group/t/how-can-i-redefine-defintions-in-typed-racket/1155/2

[Inc0n]

@sorawee, Thanks for the quick response, and the explanation.

But apology for the bad example, which doesn't fully express the issue I want to raise on this matter, since you have provided a workable solution.

I happen to do my racket work interactively in a repl (most probably do anyways), and if I had a procedure (definitions) defined already, and wishes to make changes to the definitions, which sometimes invovle changing the type signature also. As of now, I would restart my repl for the new changes to apply successfully, which I would like to avoid this.

And if definitions in typed racket can be redefined, then this would a great help this issue.

Then perhaps this next snippet could do the job better:

(: a (-> Number Number))
(define (a x) (1 + x))
(: a (-> Symbol Symbol))
(define (a x) x)

So my question is, how can I redefine a definition (binding) with different type?
In commonlisp, I know of unbound symbol, perhaps does racket provided something similar to that?

Many thanks, in advance.

[samth]

This is not possible in Typed Racket. If you have a definition of a, and then you change the type, then you've invalidated everything else that used that definition.

Effectively redefinition at the repl is just the same as set!, which also requires the type to stay the same.

[Inc0n]

I see there is a good reason for this not being possible. But it does take away the ability to interactively and iteratively to develop programs at the repl in Typed Racket. And what would be a workable solution to that of those who wishes to be able to leverage the power from Typed Racket and develop program interatively from the repl, which involves a lot of times modifing the type signatures of the definitions?

Perhaps there is some merits in that perspective too?

[rfindler]

I'm guessing the issue is that the optimizer is making the assumption that the types don't change to optimize uses of the identifiers. So this change would effectively disable all of TR's optimization capabilities.

[Inc0n]

Compiled Typed Racket code will still benefit from all optimization from TR I'm sure, and the change I would love seeing to be made to TR is to the top level REPL code, which doesn't have to be optimized in the whilst in development.

[samth]

The problem is not really about optimization. The fundamental problem is that the type checker relies on the types of things not changing out from under it. So if the type of some definition changed, then everything in the past that uses that definition would now be invalid.

GGenerally, it's not possible to make use of everything Racket does at the repl, in particular in the presence of sophisticated static features like type checking. Other typed languages also do not support this kind of redefinition, and in fact the repl in ML-family languages is typically even more limited in terms of redefinition than Typed Racket is.