Re: [racket-users] TR dependent types cannot check equality of symbols
On 2/24/20, Marc Kaufmann wrote: > 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. 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 -- 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/CAFUu9R6niER6eOakB2bOaDmQowRZJ5GK4JAe4ZfizQZ4V9zrCw%40mail.gmail.com.
Re: [racket-users] TR dependent types cannot check equality of symbols
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 On Sunday, February 23, 2020 at 6:33:33 PM UTC+1, Ben Greenman wrote: > > 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 > -- 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/98151240-f930-4dee-a8de-45f8ce6797ac%40googlegroups.com.
Re: [racket-users] TR dependent types cannot check equality of symbols
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 -- 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/CAFUu9R4dWHoufCbiEzJ7q3nyVifHscvQ1oXkLSwCnZ8mD2OUJQ%40mail.gmail.com.
[racket-users] TR dependent types cannot check equality of symbols
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.
