added type refinements

[shriram]

Joe, can you take a look at this? This is a branch from demo-home for the type refinement feature.

It's not ready to commit to demo-home because:

In examples/refinement.js, I want only the definition of insert (and the check block) to be visible, whereas I want definition of is-sorted-ascending to be hidden. This is because

1. It's makes the example too tall to fit on screen.
2. It's more complicated than the actual function, which makes it look like refinements are themselves problematic.
3. It's the kind of thing someone might want to assign as a homework.

I don't know how to use the export API to have that function be "loaded automatically but hidden".