Typed def and DIM

[jarcane]

As discussed in the Racketfest 2019 presentation, I would like to consider adding predicate typing to function and variable declarations.

This would necessitate changes in three places: def, def fn, and possibly let. Syntax support would need to be added to these forms, and additional semantics to support type checking of references both at creation and function application.

One proposed solution that remains in the spirit of the BASIC roots of Heresy is the DIM keyword, which is used for array declarations in 8-bit BASICs, but later in many dialects for type predefinitions. A possible syntax would look like this:

(dim fact : (number?) -> (number?))
(def fn fact (n)
  ...)

(dim foo : (number?))
(def foo (fact 10))

This has the advantage of not conflicting with existing def syntax, but has the disadvantage of potentially requiring some pretty tricky code rewriting magic, or even actually just requiring a type registry of some kind. Investigation of the methods in Typed Racket and Hackett may be instructive here.

I see two possible solutions off hand:

• dim is a declaration form that binds a name to a type registry of some kind, basically a separate namespace of names to their type predicates, and then we modify the default #%app further to check the values of a function application against the stored types before calling the function, while plain def's macro is modified to check the value about to be assigned.
• dim must live on the line above a def, and actually rewrites the code below it somehow to inject the necessary code for type checking. This seems like how at least Typed Racket does it.

[jarcane]

After considerable recent though, I think the first of the two options, or rather something like it, is possible.

In fact, if my thinking is correct, we don't need any kind of "type registry" at all. The normal process of function definition is more than sufficient.

We create dim as suggested, and dim acts as a type declaration, or at least appears to be one.

What it actually is, is a function declaration. The dim macro expands to define a function, of the given name modified by some standard symbol, that takes as many arguments as are given in the input portion of the declaration, plus the function itself. So for example:

(dim str-idx (number? string?) -> string?)

Would expand into something like:

(define str-idx-chk (fun n1 s1)
  (if (not (and (number? n1)
                      (string? s1)))
    (error "bad argument")
    (let [result (apply fun n1 s1)]
      (if (not (string? result))
        (error "bad return value")
        result))))

Then our custom #%app, whenever it finds a function, it first checks the local namespace for a matching function predicate, appended by the symbol. If it finds it, it applies the function via the defined check function. If it doesn't, it applies as normal.

Typing so far has been optional, and in that regard, it is not a problem if there is no check function defined, but it does mean one could inadvertently typo the dim's name and not realize their function isn't being checked. A solution for this escapes me at the present time.

The big question is is this possible in a system with hygienic macros. That I do not actually know yet. If there is not some macro wizardry to do what is outlined, then another solution will have to be found.

[jarcane]

If this macrofuckery is not actually possible, I think the simplest proposal then is to add additional syntax to def itself and embed the check behavior within the function itself.