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