rackettypecheckingtyped-racket

How to use typed scheme/racket


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 :)


Solution

  • 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?