Type Specialiser Sources

You can try out the specialiser on small examples by entering an expression to specialise in the box below, and pushing the `specialize' button.

Here are some examples to get you started. You can modify the code in these examples to see the effect on specialisation.

• A static integer.
• A dynamic integer.
• A pair with a static and a dynamic component.
  Note the effect of void erasure: the first component is completely removed from the residual term.
• A dynamic let (not unfolded). Again note the effect of void erasure.
• Even when a variable is bound by a dynamic let, its static part is available.
• Specialising a dynamic function.
  Here void erasure deletes the residual parameter from f. Note the syntax for static arithmetic.
• Even functions passed as parameters can be specialised.
  Notice we don't have to unfold any calls in order to do this specialisation --- since static information is propagated by type inference.
• A specialisation that fails, since x would need to be assigned two different residual types.
• We can fix the problem by making f polyvariant, and specialising it at each use.
  let f=poly \x.lift (x+@1) in (spec f 3, spec f 4)
• Even functions passed as parameters can be specialised polyvariantly:
  (\f. (spec f 3, spec f 4)) (poly \x.lift (x+@1))
• As an alternative to polyvariant specialisation, we can wrap the two arguments in the specialisable constructor In, generating a sum type in the residual program.
  let f = \x. case x of In y: lift (y+@1) esac in (f (In 3), f (In 4))
  Notice again that the static data does not appear in the residual program.
• Most capitalised identifiers are static unary constructors
  Notice that the static constructors are preserved in the residual type, but not in the residual program.
• A dynamic sym type is available, with constructors Inl and Inr.
• Dynamic sums can very well have static components.
  let f = \x. case x of Inl y: lift y, Inr z: lift 0 esac in (f (Inl 3), f (Inr 4))
• Let's just look at the residual type of f in that example.
  let f = \x. case x of Inl y: lift y, Inr z: lift 0 esac in let y=(f (Inl 3), f (Inr 4)) -- force specialisation in f
  The residual type reported for the whole program is just the type of f.
• Static functions are marked with an `@' sign. They are always unfolded, and so can be applied to arguments with different residual types.
  let f=\@x.lift (x+@1) in (f@ 3, f@ 4)
• In the last example, the dynamic binding of f was deleted by void erasure, since its value was purely static. But a static function with dynamic free variables is not purely static, and so has a corresponding value in the residual program.
  -- introduce some dynamic free variables let u=lift 2 in let v=lift 3 in -- make them into real free vars! let f=\@x.fst (fst (lift (x+@1), u), v) in (f@ 3, f@ 4)
  Note the residual structure for f.
• There is also a static version of let, which is unfolded.
• Recursive values can be created using fix.
  Again note that the static constructor is deleted, and the way that recursive residual types are displayed.
• Here's the same example with a dynamic sum type instead.
• Here's a recursive length function on lists with a static spine. We make the result dynamic to prevent void erasure deleting its specialisations.
  let len=fix(\len.\xs. case xs of Cons yys: len(snd yys)+lift 1, Nil z: lift 0 esac) in len (Cons (lift 1, Cons (lift 2, Nil void)))
• Of course, specialisation failed because len is applied to different static arguments. We have to make it polyvariant:
  let len=fix(\len.poly\xs. case xs of Cons yys: spec len(snd yys)+lift 1, Nil z: lift 0 esac) in spec len (Cons (lift 1, Cons (lift 2, Nil void)))
  Now len specialises to a tuple of three functions.
• In this case, len could have been unfolded. We make it a static function instead.
  let len=fix(\len.\@xs. case xs of Cons yys: len@(snd yys)+lift 1, Nil z: lift 0 esac) in len@ (Cons (lift 1, Cons (lift 2, Nil void)))
• Here's a recursive function with a dynamic free variable.
  let u=lift 2 in let f=fix(\f.\x.(x,f u)) in f
• Watch what happens if we make the function static.
  let u=lift 2 in let f=fix(\f.\@x.(x,f@ u)) in f
• The static function is represented in the residual program by a cyclic structure; not the best representation for a simple recursive function. We can improve on that by making the recursion unfoldable too: ufix takes the fixpoint of a static function. Note how the representation of f in the residual program changes.
  let u=lift 2 in let f=ufix(\@f.\@x.(x,f@ u)) in f

This demo has introduced most of the language features that the specialiser supports. If you want to experiment some more, I suggest specialising the following interpreter for the typed lambda calculus to some simple lambda terms. Try modifying the interpreter and seeing how the result of specialisation changes.

The exciting thing about this interpreter is that value domain is a static sum type, and so the `type tags' in the interpreter do not appear in residual programs. Try modifying the interpreter so that eval is unfolded --- residual programs become a lot easier to read.