How to use typed scheme/racket

Question

I am trying to learn typed scheme/racket(?). Down below I have an example from my code:

#lang typed/racket
(: add (Real Real -> Real))
(define (add x y)
  (+ x y))

I would like to implement a procedure "check" which checks if two datatypes are allowed with an operator. For example,

(check '(+ int int))

Should result in

int

But

(check '(* int (+ real int)))

Should result in something like this:

The operator '+' must have two operands of the same (numerical) type.

That is, check should take a list.

Questions:

How do I implement "check"? Firstly I though "ok, I have a list, so let's use car and cdr" to get the operator and the operands but it didn't work and I don't even know why it doesn't work. I also though about making if statements like (if (and (= x y) (or (= x int) (= y int)) and so on to make the checks but... don't think this is the right way to go.

Should I make a procedure "add" or not? Is there any other way to do this? Int the examples it looks like they are only using "+", "-" and so on. Lastly; How do I check that the input "int" is an int and then gives int as output.

I am pretty lost right now and I am sorry for my pretty vaugue questions but I would be really happy if someone could help me out to understand this.

Note: the procedure add takes real numbers and output a real number so it doesn't follow along with the example too well. But I hope you grasp the idea. Thanks :)

It's a little unclear what you're asking here. Do you want to use Typed Racket's typechecking machinery to implement check, or do you want to implement your own typechecker using Typed Racket? If it's the former, my guess is that it will be hard or even completely infeasible—Typed Racket doesn't expose any reflection on types because it only typechecks entire modules at once, and types are erased once a program is fully expanded. — Alexis King

John Clements John Clements · Accepted Answer · 2015-11-22T20:30:02

You're asking a fascinating question, and it doesn't have a simple answer.

The program that you're trying to write is essentially a type-checker. That is, it takes an expression, and checks to see whether the given function's domain includes the arguments it's being called with. We can write one of those, but I suspect you're going to be unsatisfied. Here, let me go write one now....

#lang typed/racket

(require typed/rackunit)

;; a type is either
;; - 'number, or
;; - (list 'fn list-of-types type)

;; examples of types
'number
'(fn (number number) number)

(define-type FnTy (List 'fn (Listof Ty) Ty))
(define-type Ty (U 'number FnTy))

;; given an expression, returns a type
;; or signals an error
(: check (Any -> Ty))
(define (check input)
  (cond [(and (list? input)
              (pair? input)
              (symbol? (car input)))
         (define fn-ty (lookup-fn-type (car input)))
         (define arg-types (map check (rest input)))
         (cond [(equal? (cadr fn-ty) arg-types)
                (caddr fn-ty)]
               [else (error 'check
                            "expression didn't type-check: ~v\n"
                            input)])]
        [(number? input)
         'number]
        [else (raise-argument-error
               'check
               "well-formed expression"
               0 input)]))

(: lookup-fn-type (Symbol -> FnTy))
(define (lookup-fn-type fn-name)
  (match fn-name
    ['+ '(fn (number number) number)]
    [other (raise-argument-error 'lookup-fn-type
                                 "known function name"
                                 0 fn-name)]))


(define TEST-INPUT '(+ 3 43))

(check-equal? (check TEST-INPUT)
              'number)
(check-equal? (check '(+ (+ 3 4) 129837))
              'number)

Does this answer any part of your question?

How to use typed scheme/racket

1 Answers