Type Type and Type And this is what I get
I have been quite for some time here, work is calling, family is calling and a new version of Qi ready to be explored was released. Now in the mean time I have been studying the sequent calculus and the Qi source code to learn how to mod it to my taste.
So perhaps my coolest hack is a type driven macro framework. So a little code,
(def-tp-macro ex1 X : A -> (? Usage number) where (ask? Usage)
[X : num Y : num] : A -> (simple-num-num X Y) where (element? simple Usage)
[X : num Y : str] : A -> (simple-num-str X Y) where (element? simple Usage)
[X : num Y : num] : A -> (complex-num-num X Y) where (element? complex Usage)
[X : num Y : str] : A -> (complex-num-str X Y) where (element? complex Usage))
The first line says that at any kind of arguments and type of evaluation context first ask for it usage and the return values will be stored in Usage. This will send out the type-system to track usages according to some mechanism, this is done the first time. The next time if not inhibited (ask? Usage) will be negative and the system goes down to expand according to function signature and the properties of the The Value of Usage. In (? Usage T), T is the type that is returned from the function in the non ask context, e.g. (+ (ex1 X1 Y1) (ex1 X2 Y2)) should type-check!!
It works stupidly by type-checking repeatedly and whenever something is asked for a retry is done. A process that can be made much more effective by remembering the type deduction and use this memory at nonvolatile sites in the deduction tree a property that somehow has to be passed up the deduction tree. Anyway (ask? Usage) will be true if someone later in the deduction have inhibited it. Such if a ex1 value is used in the argument of ex2 that also asks for information in this case ex2 inhibits ex1 when it asks for information. (To speed up this deduction process ex1 should be marked as nonvolatile)
Actually macros can work on code fragments like this
(def-tr-macro ex3 [adv [X : number Y : str] Z : symbol] : A -> [Z X] ...)This is a quite general construct and of cause the process of macro-expansion, usage information exchange and so on can be repeated recursively.
So the macro can use information how the result of the form is used later on in the code and under what signature the type-system thinks that this form will be evaluated under. So there is a message system that works in both directions in the code graph (what signals do I get from the arguments and what context or what features of what I provide is used.
There are weak points to this construct but I think now have one big chunk that can be put to use when I go deep into optimizations of loop macros. At least I now have a powerful tool to do optimizations by using the computer as much as possible and my coding fingers as little as possibly