[Feature Request] Tag Contract and Tag Type

Questions & Answers
1

Hello everyone, I want to share some thoughts I encountered when using Typed Racket. I don't have too deep theoretical foundation and knowledge accumulation, so it may be a little naive. :slight_smile:

Recently, I want to use mlist to modify the list data in some files. As a TR fan, I certainly hope to use TR to complete this job. However, it is not easy to use mutable type in TR. The difficulty comes from two problems:

  1. The current TR does not support the subtype relationship between mutable types (see Is it possible to make Mutable Types support subtype? 路 Discussion #1129 路 racket/typed-racket 路 GitHub),
  2. TR can't generate predicate for mutable type, nor can it generate contract for related operators to use by untyped racket.

For problem 1, I think Alex Knauth has already given a solution in that discussion. But how to solve the second problem?

I think the root of the second question is that when we convert the type A of the value x to its supertype B for processing, we lose some type information about x. After that, TR uses Occurrence Typing to retrieve x's' type information A by predicate.

And the key to the problem is that we can't define predicate for many types, which makes it difficult to retrieve the original type after we perform type conversion on the values.

I wonder if it is possible to retain the original type information during type conversion? For example, like this:

#lang typed/racket

(require typed/racket/unsafe)
(unsafe-require/typed compatibility/mlist
  [mlist (All (A) [-> A * (MListof A)])])

(define-type MList-Natural (Tag (MListof Natural)))
(define-type MList-Boolean (Tag (MListof Boolean)))

(define-predicate mlist-natural? MList-Natural)
(define-predicate mlist-boolean? MList-Boolean)

(define-type T (U Symbol String MList-Natural MList-Boolean))

(: sum [-> (MListof Natural) Natural])
(define sum (位 (mls) (if (null? mls) 0 (+ (mcar mls) (sum (mcdr mls))))))

(: f [-> T Number])
(define (f arg)
  (cond [(string? arg) (string-length arg)]
        [(symbol? arg) (string-length (symbol->string arg))]
        [(mlist-boolean? arg) -123]
        [(mlist-natural? arg) (sum arg)]))


(f (mlist))       ; -> (f '()) -> (sum '()) -> 0
(f (mlist #t))    ; -> -123
(f (mlist 1 2 3)) ; -> 6

When calculating (f'()) and converting the type of '() to tag type MList-Natural, TR adds a tag to '(), and then use mlist-natural? to check the tag for type inference.

Here is one way I simulated:

#lang typed/racket

(require typed/racket/unsafe)
(unsafe-require/typed compatibility/mlist
  [mlist (All (A) [-> A * (MListof A)])])

(struct mlist-natural ([value : (MListof Natural)]) #:type-name MList-Natural)
(struct mlist-boolean ([value : (MListof Boolean)]) #:type-name MList-Boolean)

(define-type T (U Symbol String MList-Natural MList-Boolean))

(: sum [-> (MListof Natural) Natural])
(define sum (位 (mls) (if (null? mls) 0 (+ (mcar mls) (sum (mcdr mls))))))

(: f [-> T Number])
(define (f arg)
  (cond [(string? arg) (string-length arg)]
        [(symbol? arg) (string-length (symbol->string arg))]
        [(mlist-boolean? arg) -123]
        [(mlist-natural? arg) (sum (mlist-natural-value arg))]))


(f (mlist-natural (mlist)))
(f (mlist-boolean (mlist #t)))
(f (mlist-natural (mlist 1 2 3)))

Recall that the reason I hope TR can support tag types is that we can't define predicates for all types. There is a similar dilemma in untyped racket -- we can't solve all problems with flat contract alone, so we need chaperone contract.

I wonder if we can also support tag contract?

#lang racket

(require compatibility/mlist)

(define mlist-natural/t (tag-contract (mlistof natural? #:flat? #f)))
(define mlist-boolean/t (tag-contract (mlistof boolean? #:flat? #f)))

(define mlist-natural? (tag-contract-predicate mlist-natural/t))
(define mlist-boolean? (tag-contract-predicate mlist-boolean/t))

(define T? (or/c symbol? string? mlist-natural/t mlist-boolean/t))

(define sum (位 (mls) (if (null? mls) 0 (+ (mcar mls) (sum (mcdr mls))))))

(define/contract (f arg)
  (-> T? number?)
  (cond [(string? arg) (string-length arg)]
        [(symbol? arg) (string-length (symbol->string arg))]
        [(mlist-boolean? arg) -123]
        [(mlist-natural? arg) (sum arg)]))


(f (mlist))       ; -> (f '()) -> (sum '()) -> 0
(f (mlist #t))    ; -> -123
(f (mlist 1 2 3)) ; -> 6
2

What does it mean to "add a tag" to a value? If what you mean is "wrap it in a struct" as in your simluation then it's easy to produce a macro that implements (define-tag-type MList-Natural (MListof Natural)) that would have a predicate. But that predicate would answer #f to (mlist 4), which I don't think is what you want.

The root of the problem is that there is not "original type information" that is not retained -- this information does not exist anywhere.

3

Before posting my thought, I didn鈥檛 know much about Racket鈥檚 contract. After that, I studied the impersonator from document and tried to write a simple implementation:
(I didn't find the chaperone contract for mlist, so I replaced the original mlist example with box)

main.rkt:

#lang racket/base

(require racket/contract racket/match)
(provide tag-contract tag-contract? tag-contract-recover)


(define-values (prop:tags prop:tags? prop:tags-get)
  (make-impersonator-property 'prop:tags))

(define/contract (tag-contract? arg)
  (-> any/c boolean?)
  (and (contract? arg)
       (match (contract-name arg)
         [`((tag-contract ,_) . ,(? symbol?)) #t]
         [_ #f])))

(define/contract (tag-contract base-contract)
  (-> chaperone-contract? tag-contract?)

  (define t (gensym))
  (make-contract #:name `((tag-contract ,(contract-name base-contract)) . ,t)
                 #:projection
                 (位 (b)
                   (define base-proj (contract-projection base-contract))
                   (define base (base-proj (blame-swap b)))
                   (位 (arg)
                     (match (base arg)
                       #;[(? procedure? p)]
                       #;[(? struct? s)]
                       #;[(? vector? v)]
                       [(? box? b)
                        (chaperone-box b
                                       (位 (b o) o)
                                       (位 (b i) i)
                                       prop:tags
                                       (if (prop:tags? b)
                                           (hash-set (prop:tags-get b) t b)
                                           (hasheq t b)))]
                       #;[(? hash? h)]
                       #;[(? channel? ch)]
                       #;[(? continuation-mark-key? cmk)])))))

(define/contract (tag-contract-recover tc)
  (-> tag-contract? (-> any/c any/c))

  (match-define `((tag-contract ,_) . ,t) (contract-name tc))
  (位 (arg)
    (and (prop:tags? arg)
         (hash-has-key? (prop:tags-get arg) t)
         (hash-ref (prop:tags-get arg) t))))

test-box.rkt:

#lang racket

(require "main.rkt")


(define box-number/t  (tag-contract (box/c number?)))
(define box-boolean/t (tag-contract (box/c boolean?)))

(define box-number/r  (tag-contract-recover box-number/t))
(define box-boolean/r (tag-contract-recover box-boolean/t))

(define T?
  (first-or/c symbol? string?
              (and/c (box/c number?  #:flat? #t) box-number/t)
              (and/c (box/c boolean? #:flat? #t) box-boolean/t)))


(define/contract (g arg)
  (-> (box/c none/c any/c) number?)

  (cond [(box-boolean/r arg)
         => (位 (arg)
              (set-box! arg (not (unbox arg)))
              (if (unbox arg) 1 -1))]
        [(box-number/r arg)
         => (位 (arg)
              (set-box! arg (- (unbox arg)))
              (unbox arg))]
        [else -123]))

(define/contract (f arg)
  (-> T? number?)

  (cond [(string? arg) (string-length arg)]
        [(symbol? arg) (string-length (symbol->string arg))]
        [else (g arg)]))


(f (box 10))    ; -10
(f (box #t))    ; -1
(f (box #f))    ;  1

This is the code I imagined in Typed Racket:

#lang typed/racket


(define-type Box-Number  (Tag (Boxof Number)))
(define-type Box-Boolean (Tag (Boxof Boolean)))

(define-recover box-number/r  Box-Number)
(define-recover box-boolean/r Box-Boolean)

(define-type T (U Symbol String Box-Number Box-Boolean))


(: g [-> (Boxof Nothing Any) Number])
(define (g arg)
  (cond [(box-boolean/r arg)
         => (位 (arg)
              (set-box! arg (not (unbox arg)))
              (if (unbox arg) 1 -1))]
        [(box-number/r arg)
         => (位 (arg)
              (set-box! arg (- (unbox arg)))
              (unbox arg))]
        [else -123]))

(: f [-> T Number])
(define (f arg)
  (cond [(string? arg) (string-length arg)]
        [(symbol? arg) (string-length (symbol->string arg))]
        [else (g arg)]))


(f (box 10))    ; -10
(f (box #t))    ; -1
(f (box #f))    ;  1