Is there any way to declare a type representing all the callable procedures(any procedure which is callable) in Typed Racket?

Question

I'm working on SICP's metacircular-evaluator with Typed Racket and stuck when preparing primitive procedures beforehand with a list of cons of symbol and the procedure object. In the book the authors prepare primitive-procedures as below, however, when I mimic it in Typed Racket and define accessors on it, I simply can't extract procedures nor symbols because I need to explicitly instantiate car or cdr with a type which I cannot write down, that is, all the union of procedure types in the list. So I thought that if I can declare a type representing all the callable procedures(without keyword args but with rest args), I can finally annotate the list below. I seriously googled and tried many ways myself but I have come up with no good idea. Can anyone think of a good way to define such a type? Or even better, can anyone come up with a better idea to prepare all the primitive procedures?

(define primitive-procedures
    (list (cons 'car car)
          (cons 'cdr cdr)
          (cons 'list list)
          ...))

Yes, I have already done it and the result was somewhat meaningless. The type signature of apply was (All (a b) (-> a * b) (Listof a) b), and (-> a * b) didn't fit in our type signature of primitve-procedures. For example though I declare the type of primitive-procedures as (: primitive-procedures : (All (a b) (Listof (Pairof (Symbol (-> a * b))))), the type checker still claims that the type declared beforehand differs from every procedure in the actual list. — lisperatsa
SICP is a very difficult textbook. It is better for you to do in mit-scheme, in order to be able to execute the code from the book. The SICP course does not cope with types. If you are very beginner you will not be able to execute it in racket with types. SICP takes many years to finish, even for a professional computer engineer. After you finish it, you can study types from other textbooks, in the same spirit as SICP. Give up typed languages and do it in a simpler way, in untyped scheme. — alinsoar
@alinsoar Thank you for all the advice. To tell the truth, the untyped version of metacircular-evaluator is already working well in untyped Racket without SICP module. That's why I wanted work on typed version. What's more, right after this post I came up with the idea that I can put all the primitive procedures in the environment at first hand when I initialize the environment structure. Maybe this should work well. Thank you. — lisperatsa
IN typed scheme you will never be able to run combinators like this one en.wikipedia.org/wiki/Fixed-point_combinator. When you arrive to the point to write the programs in CPS you will not be able to use any more typed language. — alinsoar

Alex Knauth Alex Knauth · Accepted Answer · 2019-12-16T16:53:28

The problem is with trying to fit a heterogeneous set of function types into a homogeneous list type / homogeneous lookup-result type.

In the comments you noted that you cannot give the type primitive-procedures : (All (a b) (Listof (Pairof Symbol (-> a * b))) because the type declared differs from every procedure in the actual list. You probably tried adding All because you were trying to accommodate all the heterogeneous types in there. But the Listof type, and more importantly the lookup function you use to get primitives out of the list, have fundamentally homogeneous types. You'll have to make the type homogeneous and work around the types within the list.

If the values in your target language are the same as your host for a meta-circular interpreter, the simplest choice for this homogeneous function type is (-> Any * Any).

(: primitive-procedures : (Listof (Pairof Symbol (-> Any * Any))))
(: lookup-primitive : (-> (Listof (Pairof Symbol (-> Any * Any))) Symbol (-> Any * Any)))

Then the use of lookup-primitive should be fine using apply. However the most complicated part is the definition of primitive-procedures with this homogeneous type.

Just using

(define primitive-procedures
  (list (cons 'car car)
        (cons 'cdr cdr)
        (cons 'list list)
        ...))

isn't enough and gives a type mismatch.

car cannot be used as (-> Any * Any). It can be used as (-> (Pairof Any Any) Any).
cdr cannot be used as (-> Any * Any). It can be used as (-> (Pairof Any Any) Any).
list can be used as (-> Any * Any). That's good.

So we must wrap car and cdr somehow, with functions that check the number of arguments and check that the argument is a pair, before passing the arguments to car and cdr.

(lambda [args : Any *]
  (match args
    [(list arg)
     (unless (pair? arg) (error 'car "wrong argument type"))
     (car arg)]
    [_
     (error 'car "wrong number of arguments")]))

Now this lambda expression can be used as (-> Any * Any), but it's clunky. It's even worse when you consider we would have to do this for every primitive that doesn't already fit:

(define primitive-procedures
  (list (cons 'car (lambda [args : Any *]
                     (match args
                       [(list arg)
                        (unless (pair? arg) (error 'car "wrong argument type"))
                        (car arg)]
                       [_
                        (error 'car "wrong number of arguments")])))
        (cons 'cdr (lambda [args : Any *]
                     (match args
                       [(list arg)
                        (unless (pair? arg) (error 'cdr "wrong argument type"))
                        (cdr arg)]
                       [_
                        (error 'cdr "wrong number of arguments")])))
        (cons 'list list)
        ...))

This code is ugly and repeats itself a lot. I would define a macro called prim to do this pattern for me:

(require syntax/parse/define)

(define-simple-macro (prim (arg-pred ...) proc)
  #:with (arg-id ...) (generate-temporaries #'(arg-pred ...))
  (lambda [args : Any *]
    (match args
      [(list arg-id ...)
       (unless (arg-pred arg-id) (error 'proc "wrong argument type")) ...
       (proc arg-id ...)]
      [_
       (error 'proc "wrong number of arguments")])))

Then we can use it in primitive-procedures like

(define primitive-procedures
  (list (cons 'car (prim (pair?) car))
        (cons 'cdr (prim (pair?) cdr))
        (cons 'list list)
        ...))

And now it is finally defined with the homogeneous type (Listof (Pairof Symbol (-> Any * Any))).

Is there any way to declare a type representing all the callable procedures(any procedure which is callable) in Typed Racket?

1 Answers