Re: [Axiom-developer] B#

[Gabriel Dos Reis]

"Page, Bill" <address@hidden> writes:

[...]

| > re: B-natural
| > 
| > B-natural won't replace the interpreter because the real
| > semantics of an expression is carried in the type. B-natural
| > has the essential goal of hand-waving away the type issues
| > to make it easier for people who don't care about the type.
| 
| No. Have you read the actual B# paper? There is no "hand
| waving". The user interacts with only one type - the UserType.
| The UserType in turn has a well-defined relationship to the
| underlying types defined in the Axiom library.

Hi Bill,

  By now, I have some familiarity with the B# paper.  I do believe
there is a "hand waving" concerning how the B# interpreter works with
types.  The subsection "Types" in §5.3 does not say much.  I also read
the paper 

   "The Type Inference and Coercion Facilities in the Scracthpad II
   Interpreter" by the duo Sutor & Jenks.

The description there is informal, sufficient to convey the general
feeling of how the type system works.  However, it lacks the "essence"
that would make it acceptable to a compiler writer, or even at a
contemporary programming language conferences :-)
I suspect the meat must be the papers refered to as [1] [3] [4], [5],
[7] [8].  I currently have access to none of them, except [1].

-- Gaby