Fri Jan 21 10:43:09 EST 2011

Racket units and the type class trick

Yesterday I was thinking that maybe a dynamic dispatch generic
function approach would be useful.  However, that doesn't seem to be
necessary.  Using units it is possible to get the necessary abstract
interpretation by simply building different implementations of the
num^ signature that defines the basic arithmetic operations.

This is what I have:


#lang scheme

;; The interfaces.  Basic language syntax and a single-function module.
(define-signature num^ (add sub mul lit))
(define-signature fun^ (fun))

;; The language interpretations.
(define-unit num-eval@
  (export num^)
  (define add +)
  (define sub -)
  (define mul *)
  (define (lit x) x))

(define-unit num-gen@
  (export num^)
  (define (add a b) `(add ,a ,b))
  (define (sub a b) `(sub ,a ,b))
  (define (mul a b) `(mul ,a ,b))
  (define (lit x) `(lit ,x)))

;; A test program
(define-unit fun@
  (import num^)
  (export fun^)
  (define (fun x y)
    (let ((a (add x y))
          (b (sub x y)))
      (mul a b))))

;; Test program linked to interpretations.
(define-compound-unit/infer fun-eval@
  (export fun^ num^) 
  (link fun@ num-eval@))

(define-compound-unit/infer fun-gen@
  (export fun^ num^)
  (link fun@ num-gen@))


Now it's possible to evaluate the test function defined in the `fun@'
unit using two different number models:

box> (define-values/invoke-unit/infer fun-gen@)
box> (fun (lit 1) (lit 2))
(mul (add (lit 1) (lit 2)) (sub (lit 1) (lit 2)))

box> (define-values/invoke-unit/infer fun-eval@)
box> (fun (lit 1) (lit 2))

Next: access instantiated modules as values without relying on name
bindings.  It seems there is a very straightforward workaround.  Just
wrap it in a function body:

box> ((lambda () (define-values/invoke-unit/infer fun-gen@) fun))

Skipping the explicit fun2 + num-gen@ linking this can be done as:

box> ((lambda () (define-values/invoke-unit/infer (link fun@ num-gen@)) fun))

Nope, that doesn't work as expected..  No shortcut: figure out how to
use the units as first class values.