The data-lib library has many useful data structures that are missing from the typed racket standard library. Following the documentation on interacting with untyped code, I was able to use the #:opaque type to import the untyped queue implementation from data-lib to typed code as follows:
The problem here is that Heap is specialized to contain only Integer. Ideally, I'd like to introduce a Heap type constructor and make the associated functions polymorphic over the element type. (It makes sense why you can't do that, because there's no way a single heap? predicate would be able to tell apart Heap Integer and Heap String.)
I'd be happy to either have a nice way of manually requiring untyped code into different types (IntQueue and StringQueue) or a way to ascribe and trust the polymorphic signatures. Just wanna make sure I'm not missing anything from the documentation.
The data-lib library contains many mutable data structures, which necessitate distinguishing between read types and write types. While current Typed Racket doesn't provide a built-in way to define such types, we can achieve this through some clever techniques.
Thank you! My understanding is that if I'm content with invariant type constructors, then I can use a dummy mutable struct to type the functions. However, it seems that the resulting typed code from the repositories you linked can only be used with typed/racket/optional to prevent racket from dynamically checking the queue is an instance of the dummy struct. Is there a way to work around that and make the code importable by typed/racket?
When typed/racket uses require/typed, it generates contracts. However, some types cannot generate corresponding contracts. Besides using typed/racket/optional, you can also use unsafe-require/typed as an alternative approach.
That's really helpful! Another question I have is how does the typed racket standard library introduce container types like Vectorof and Listof? My main concern with unsafe-require/typed is that I don't understand how the optimizations interact with the dummy struct trick. Conceptually it's safe if the Queue struct is sealed, but the documentation is worded in a way that sounds like any use of unsafe-require + optimization immediately takes us to the undefined behavior territory.
My guess is that the standard library can't possibly do anything smarter besides the developers know the inner workings of the optimization passes well enough to ascribe type signatures.
I do wonder if there's a way to use macros to automate the process and avoid duplication, but modules don't seem to be first-class in racket (maybe typed unit is what I should be looking for?). Either way, for my purpose of leetcoding with a statically typed functional language that's not scala, the monomorphisized modules seem to work quite well
This is a useful approach (especially abstracted into a macro, as @EmEf demonstrated), but one caveat is that, while the require/typed declarations claim that I:heap? and S:heap? recognize specifically I:Heap and S:Heap, respectively, both will actually answer #t for any heap, regardless of its contents. Thus, this program typechecks:
#lang typed/racket
(require (for-syntax syntax/parse))
(define-syntax (heap-module stx)
(syntax-parse stx
[(_ Name Type)
(syntax-local-introduce
#`(module Name typed/racket
(provide Heap heap? make-heap heap-add! heap-min heap-count)
(require/typed data/heap
[#:opaque Heap heap?]
[make-heap (-> (-> Type Type Boolean) Heap)]
[heap-add! (-> Heap Type Void)]
[heap-min (-> Heap Type)]
[heap-count (-> Heap Natural)])))]))
(heap-module IntHeap Integer)
(heap-module StringHeap String)
(require (prefix-in I: 'IntHeap))
(require (prefix-in S: 'StringHeap))
(: does-not-work (-> (U I:Heap S:Heap) String))
(define (does-not-work h)
(if (and (I:heap? h)
(not (= 0 (I:heap-count h))))
(number->string (I:heap-min h))
"other"))
(module+ main
(define sh (S:make-heap string<=?))
(S:heap-add! sh "this is a string")
(does-not-work sh))
but fails with the following runtime error:
heap-min: broke its own contract
promised: exact-integer?
produced: "this is a string"
in: (-> any/c exact-integer?)
contract from: (interface for heap-min)
blaming: (interface for heap-min)
(assuming the contract is correct)
at: 3-unsaved-editor:13:26
If this is a problem for you in practice (often it is not!), you can have the adapter module introduce a wrapper struct around the underlying heap.
Finally, at the risk of stating the obvious, you might consider a library that implements the data structure you want in Typed Racket directly, e.g. pfds/heap/pairing in this case (among many others).
