On 9/3/07 6:54 PM, "Christopher Diggins" <cdiggins@...> wrote:

I did look at your paper and read it with great interest. I am not really
competent
to judge the details, so I cannot help you in any substantial way. I had
some
superficial acquaintance with natural deduction rules for typing, but have
never
used the them in earnest. But it is a formalism which I should study and
perhaps
use to describe typed Joy. Actually the type inference that I use for the
Joy-to-Prolog
compiler is so automatic when writing in Prolog that it is barely visible.
It is simply
this:

IF a turns S into T1
AND b turns T2 into U1
AND c turns U2 into V
THEN [a b c] turns S into V

where there have to be the unifications T1=T2 and U1=U2. All that is
automatic.
There are two compilers at present, both about 18 lines long. One produces
lengthy Prolog code which is still more efficient than the Joy source. The
other produces optimised Prolog code in which all the stack-and
list-shuffling
is done at compile time and leaves no trace in the Prolog code. All thanks
to
Prologıs unification.

I also had a look at your implementation in C#. It looks much cleaner than
my Joy implementation. Thanks in part perhaps to C#, but only in part.
You are also a better programmer than I am. Well done.

- Manfred
>
>
>> > For a long time I had been dreaming of static type checking for Joy,
>> >
> Have you looked at the most recent Cat paper
> (http://www.cat-language.com/paper.html)? It could prove to be a useful
> starting point for designing a type system and type checker for Joy (and
> even a type inference algorithm).
>
> Cheers, Christopher
>



[Non-text portions of this message have been removed]