- Complete specification of names in expressions chapter.

- Complete name expansion: functions get_declared_type and
  get_declared_value (and any others)

Are these exposed to the user or simply a part of the semantic
definition?  I believe we had these declared in a version of the
strawman.  It's still around somewhere if you want to start with
those.

- Review specification of types, and specifically of polymorphic and
  dependent types.  It would probably be wise to define specific
  syntax for type schema denoting polymorphic and dependent types, so
  that we can appeal to the existing literature.  Our notion of a
  function denoting a polymorphic/dependent type is shaky and leads to
  definitional problems.

We support a form of parametric polymorphism that is exemplified by
System F.  Specifically, type variables that are held abstract during
type checking.  (I don't think we support existential types anywhere.)
We have ways of defining type variables in function declarations and
facet declarations.  Given that we have reflection, this would seem to
give us enough to write functions that generate types.  I remember
talking about this awhile back and thinking we had reached a solution
with the addition of universal types.  However, the devil is in the
details.

  The same might also be said of domains as types.  Perhaps a specific
  type schema denoting facets derived from a given domain would be
  more appropriate than using the domain itself as the type.

Is it not enough to use the facet identifier in a syntactic position
that requires a type?  Specifically, facet f(p::in T)::domain is...
By knowing that a type is expected following the :: token, can we not
simply treat the domain syntax differently?

There are certainly cases where we are defining new types that this
might not work for.  But, I can't think if anything specific offhand.

- Review specification of universal type formation in expressions
  chapter.  Currently, set(universal) is not appropriate, since it
  doesn't take account of the way polymorphic and dependent types are
  represented.  However, if type schema are introduced, then all types
  really would be sets again, and scheme just ways to denote
  particular sets.  Then set(universal) should be ok.  Check this.

Okay, I'll bite.  What needs to happen for us to introduce type
schemas?  Am I understanding correctly that we are, in effect,
defining a type language?  I am certainly not opposed to separating
the type language from the term language if we can maintain that type
values are values just like anything else.

- Review denotational semantics of let expressions.  Need to nail this
  down a bit more rigorously.

We should be able to rely on a derived form.  Will this work:

  let x::T be t in term == <*(x::T)::typeof(term) term*>(t)

There are context details, but ignore those for the time being.  This
will of course not work for the let form that can encapsulate several
terms in a facet.  If that is the let form you're referring to, ignore
this and we'll try again.

- Review type rules.  Can they be defined only in terms of the kernel
  language, or are there cases where type rules need to be specified
  for full language constructs?

Not sure here.  I can't think of anything specific offhand, but I've
not thought carefully about it.

  Is it sufficient to say that a full-language specification is well
  typed iff its simplified and resolved form is well typed?

I hope so.  What we're saying is that t::T == elab(t)::elab(T), or
typing relations are invariant over elaboration.  We do this in
another of the languages that I'm working on.  It seems to work fine
there and it would be very nice if it worked here.

- Specify semantics of facet instantiation.

Yes.

- Specify semantics of facet inclusion.

As well as the relationship between instantiation and inclusion. This
has never been completely clear.

- Specify denotational semantics of an anonymous facet.

How is the semantics of an anonymous facet different than a named
facet?

- Review simplification semantics for components.

Definitely.  These definitions have not been reviewed for some time
and I think will be very useful for specifiers.

- Review transformation semantics for domains.

Can you clarify what this issue is about?  I think I understand, but I
want to make sure.

- Complete language design for translators:

    - Application using tick operations

I think Peter proposed introducing a general purpose attribute and
using the attribute 'at to define this.  I thought this was a great
idea.

    - Features for specifying default translators (on included facets,
      on use clauses, in domains)

We had a proposal sometime back for explicitly specifying translators,
but specifying the default case was not specifically discussed.
Frankly I think this comes back to specifying what an interaction
between domains defines.  The default translator functions would seem
to be best specified there.

    - Extensions to name expansion and representation of resolved
      names to support default translators

I'm not touching that one right now.

- Review and complete model-of-computation (MoC) domains.

Definitely.  This and interactions are my #1 priority.

- Develop useful translators between MoC domains.

Once we have useful MoC domains and specification mechanisms, I hope
this won't be overly difficult.

- Review interactions - are they needed?  If not in the form proposed,
  then in what form?

Definitely not in the form originally proposed in the strawman.  I
think we know how facets in different domains interact.  We can define
functors and pullbacks now with algebra combinators to come later.
The difficult part is how to package this up into an interaction in
some reasonable way.

- Define consistency of a specification.

I took a shot at this in the old strawman, but I think it is woefully
inadequate now.

- Review Bugzilla issues:

    - Address unresolved issues.

    - Check previously resolved issues and make sure they are either
      addressed in the LRM or are no longer pertinent.

No argument with these.