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