Typed code from untyped code

[Bertrand Augereau]

Hello everybody,
I'm trying to gradually type my script to make it a proper app (yes
I'm a static-ish guy) and I have an issue (Racket 7.6 CS).

===================================================
racket_mod.rkt:
#lang racket

(provide (struct-out s))
(provide list-of-s)
(provide set-list-of-s!)

(struct s (a))
(define list-of-s '())
(define (set-list-of-s! los)
(set! list-of-s los))
===================================================

racket_mod_typed.rkt:
#lang typed/racket

(provide (struct-out s2))
(provide list-of-s2)
(provide set-list-of-s2!)

(struct s2 ([a : Natural]))
(define list-of-s2 '())
(define (set-list-of-s2! [los : (Listof s2)])
(set! list-of-s2 los))
===================================================
racket_main.rkt:
#lang racket

(require "racket_mod.rkt")
(require "racket_mod_typed.rkt")

(define los (list (s 1) (s 2)))
(set-list-of-s! los)
(displayln list-of-s)

(define los2 (list (s2 1) (s2 2)))
(set-list-of-s2! los2)
(displayln list-of-s2)
===================================================

list-of-s2 is empty and list-of-s is not, the only difference seems to
be the type annotations.
Can someone help me ? :)

Cheers and thanks,
Bertrand

[Ben Greenman]

If you export a "getter" function instead of the list, both modules
have the same behavior:

```
#lang racket/base

(module racket_mod racket
(provide (struct-out s))
(provide get-s)

(provide set-list-of-s!)

(struct s (a))
(define list-of-s '())

(define (get-s) list-of-s)
(define (set-list-of-s! los)
(set! list-of-s los)))

(module racket_mod_typed typed/racket
(provide (struct-out s2))
(provide get-s2)

(provide set-list-of-s2!)

(struct s2 ([a : Natural]))

(define list-of-s2 : (Listof s2) '())
(define (get-s2) : (Listof s2) list-of-s2)

(define (set-list-of-s2! [los : (Listof s2)])

(set! list-of-s2 los)))

(require 'racket_mod)
(require 'racket_mod_typed)

(define los (list (s 1) (s 2)))
(set-list-of-s! los)

(displayln (get-s))
;; (#<s> #<s>)

(define los2 (list (s2 1) (s2 2)))
(set-list-of-s2! los2)

(displayln (get-s2))
;; (#<s2> #<s2>)
```

- - -

The issue in the original code comes from Typed Racket's internals.
When you write `(provide x)` in a TR module, the compiler makes 2
kinds of `x`: a plain `x` for typed clients and a contract-protected
`x` for untyped clients.

```
;; source code
(provide x)
(define x : (Listof s2) '())
```

```
;; complied code, approximately
(provide (rename-out safe-x x))
(define-typed/untyped-identifier safe-x typed-x untyped-x)

(define typed-x : (Listof s2) '())
(define untyped-x (contract (listof s2?) typed-x))
```

The contracts make sure that untyped code respects TR types, and
normally nothing else. But your example shows one way that the current
strategy can end up with different behavior. This is unfortunate, but
I'm not sure how TR could do better ... every new element that gets
added to the list needs protection.

- - -

fwiw, you can also see equal behavior from a typed main module:

```
#lang typed/racket
;; typed_racket_main.rkt

(require/typed "racket_mod.rkt"
(#:struct s ((a : Natural)))
(set-list-of-s! (-> (Listof s) Void))
(list-of-s (Listof s)))

(require "racket_mod_typed.rkt")

(define los (list (s 1) (s 2)))
(set-list-of-s! los)
(displayln list-of-s)

(define los2 (list (s2 1) (s2 2)))
(set-list-of-s2! los2)
(displayln list-of-s2)

```

If you were planning to add types everywhere, then maybe its best to
go ahead with that instead of adding getter functions.

[Bertrand Augereau]

Hello and thank you Ben for the explanation,

I had already implemented the workaround, I'll keep it :)
It seems that wrapping every binding access in a function is seen as
unnecessary in Scheme and Common Lisp ("Reference needed" :) ) but
it's a tool I use a lot in my favorite statically typed languages
usually so I'll keep at it because it just eases refactoring... for
instance in this case :)
Maybe the documentation should warn about this ?
Cheers,
Bertrand

Le lun. 17 févr. 2020 à 16:46, Ben Greenman
<benjamin...@gmail.com> a écrit :

> --
> You received this message because you are subscribed to the Google Groups "Racket Users" group.
> To unsubscribe from this group and stop receiving emails from it, send an email to racket-users...@googlegroups.com.
> To view this discussion on the web visit https://groups.google.com/d/msgid/racket-users/CAFUu9R5fDBYWMPH%3DLsRe1VXnVmdncdrRY%3DLODGYtGhuhsmSZ-A%40mail.gmail.com.

[Ben Greenman]

On 2/17/20, Bertrand Augereau <bertrand...@gmail.com> wrote:
> Hello and thank you Ben for the explanation,
>
> I had already implemented the workaround, I'll keep it :)
> It seems that wrapping every binding access in a function is seen as
> unnecessary in Scheme and Common Lisp ("Reference needed" :) ) but
> it's a tool I use a lot in my favorite statically typed languages
> usually so I'll keep at it because it just eases refactoring... for
> instance in this case :)
> Maybe the documentation should warn about this ?
> Cheers,
> Bertrand

Yes, a note in the docs would be good.

Another idea:* TR could fix the issue by protecting set!'d identifiers
lazily. Instead of applying a contract in the typed module, export a
macro that applies the contract at each untyped use-site.

* Thanks to Alex Knauth

[Alex Knauth]

The way I we imagined it, it would be implemented like the workaround of a getter function, but with an identifier macro to hide the function from the person using the mutable identifier.

Alex Knauth (mobile)

> On Feb 17, 2020, at 7:22 PM, Ben Greenman <benjamin...@gmail.com> wrote:

> --
> You received this message because you are subscribed to the Google Groups "Racket Users" group.
> To unsubscribe from this group and stop receiving emails from it, send an email to racket-users...@googlegroups.com.

> To view this discussion on the web visit https://groups.google.com/d/msgid/racket-users/CAFUu9R7f3tRawUp76L9qa%3DEUWL_FNjgysCaJ%3D%3Df%3DS8rAJ41ZXA%40mail.gmail.com.

[Bertrand Augereau]

That's the way I expected it to work somehow, though I'm a Racket beginner and don't know how to check this kind of assumptions :)

Thanks for the answers,

Bertrand

To view this discussion on the web visit https://groups.google.com/d/msgid/racket-users/AE5BC9AE-6FE2-405E-B4D2-6178F0F91532%40knauth.org.