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))
--
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 [email protected].
To view this discussion on the web visit
https://groups.google.com/d/msgid/racket-users/98636cef-0f0c-42bb-bb87-af2824355175%40googlegroups.com.
