TR dependent types cannot check equality of symbols

[Marc Kaufmann]

Hi,

I worked my way through the blog posts on refinement types (https://blog.racket-lang.org/2017/11/adding-refinement-types.html) and through the docs (https://docs.racket-lang.org/ts-reference/Experimental_Features.html#%28form._%28%28lib._typed-racket%2Fbase-env%2Fbase-types-extra..rkt%29._.Refine%29%29). The problem I wanted to solve is as follows: I have some code that gets values from a hash that can be Integers or Symbols, but I sometimes need to know that the returned value is exactly an integer in order to use it. Currently my code uses lots of `(if (number? x) ...)` to deal with this, but I was wondering if I could use refinement types to do the same, since I know which columns are of which types.

It turns out that I can solve the problem by rewriting my code to use hashes that return a struct `person`, and the fields of the struct are easy to type check via `(person-age ...)` and `(person-name ...)` -- but I am still wondering if this kind of dependent typing is possible with typed racket right now or not.

Below is the code, which does *not* type check, it says: "terms in linear constraints must be integers, got Symbol for var". I thought that from the docs one could also use `id`s in the proposition constraints, but I guess by id it means the id of some argument, not the id of a variable? Is there a way to make this code work such that my function `get-user-var` always returns *either* type Integer *or* type Symbol, but not both - and hence the code would type check? The last line won't type check if I get rid of the refinement, since then the type is clearly (U Integer Symbol).

#lang typed/racket

(struct person ([name : Symbol] [age : Integer]) #:transparent)

(define bob (person 'bob 15))
(define sally (person 'sally 30))

(: people (HashTable Integer person))
(define people (hash 1 bob
                     2 sally))

(: get-user-var (-> ([uid : Integer]
                    [var : Symbol])
                    (Refine [res : (U Symbol Integer)]
                            (if  (= var 'age)
                              (: res Integer)
                              (: res Symbol)))))
(define (get-user-var uid var)
  (cond [(eq? var 'name) (person-name (hash-ref people uid))]
        [(eq? var 'age) (person-age (hash-ref people uid))]
        [else
          (error "No such variable: " var)]))

(get-user-var 1 'age)
(get-user-var 1 'name)
(add1 (get-user-var 1 'age))

[Ben Greenman]

Try this case-> type instead:

(case->
(-> Integer 'name Symbol)
(-> Integer 'age Integer)
(-> Integer Symbol (U Symbol Integer)))


I don't know what it would take to add refinements for symbols, but
that might be useful. Andrew Kent's dissertation may have some
pointers:

https://pnwamk.github.io/docs/dissertation.pdf

[Marc Kaufmann]

Very nice, adding

(: get-user-var (case-> ...))

indeed does the trick. So I can use `case->` to do overloading (if that's what it is called), by defining different functions for different type signatures, and then put them together into a single function via a cond. E.g.:

(: int-add (-> Integer Integer Integer))
(define (int-add x y)
  (+ x y))

(: string-add (-> String String String))
(define (string-add x y)
  (string-append x y))

(: int-string-add (case->
                    (-> Integer Integer Integer)
                    (-> String String String)))
(define (int-string-add x y)
  (cond [(integer? x) (int-add x y)]
        [(string? x) (string-add x y)]
        [else
          (error "Not a string or int" x)]))

I am wondering if there is a way to avoid the final definition of `int-string-add`, by simply defining the same function twice (or more) with different type signatures, and then when I call the function, which code gets called depends on the type signature? I would be surprised if this existed in Typed Racket right now, but it would be neat and good to know if there is a more idiomatic/built-in way than what I do above, ie just write:

(: special-add (-> Integer Integer Integer))
(define-special (special-add x y)
  (+ x y))

(: special-add (-> String String String))
(define-special (special-add x y)
  (string-append x y))

I guess it would be pretty hard, since the type signature has to be coupled more tightly to a specific function than TR requires right now, i.e. I'd have to write (define-special (special-add [x : String] [y : String]) to make the link explicit. Anyway, if it's not possible right now, totally fine.

      

Regarding refinement types for symbols, I have no idea how useful it would be, as the only example I came up with was the above one, which I think is better dealt with in a different way.

Cheers,
Marc

[Ben Greenman]

Right, I don't think that's possible now.

The extensible-functions package helps with overloadings, but (iiuc)
you need to pick a type at the top:

https://pkgs.racket-lang.org/package/extensible-functions