Re: [stack] Notation for typed arrays in Cat

On Wed, Apr 9, 2008 at 3:44 AM, Manfred Von Thun
<[email protected]> wrote:
> On 5/4/08 1:26 AM, "Christopher Diggins" <[email protected]> wrote:
>
> > I am again playing with the idea of how to introduce typed arrays in to
> Cat.
> >
> Before you do that, consider the various uses of typing annotations. Note
> that this list is sort of cumulative:
>
> 1. To help the implementer/maintainer to understand the implementation
>
> 2. To help the user (as part of the manual or help facility). This is how I
> did it in Joy, the typing information is part of the help message. (A very
> primitive way of doing it.) But the typechecking is done independently in
> the interpreter.
>
> 3. To become part of the implementation for an interpreter: before an
> operator is executed, the current stack is checked against the typing
> requirement for that operator. This guarantees that the manual and the
> implementation actually agree (what an extraordinary thought!).
>
> 4. To become part of a compiler which checks whether the output-stack from
> one operator is suitable as the input-stack for the next operator. For a
> definition it should check the body, from the input-stack for the first
> operator it should determine the input-stack for the whole body, and from
> the output-stack of the last operator it should determine the output stack
> of the whole body.
>
> Clearly (4.) is the most desirable, it encompasses all others before.

FWIW I think your list is accurate and useful.

> The
> way to do it is with pattern matching ­ available in Prolog, ML(?) and
> Haskell(?), and probably in some versions of Lisp. But you need a good
> pattern notation to apply it to. This is how I tried to do it with my
> experiments on Joy in Prolog. a year ago. If I did it again, I would change
> quite a few things, but the central idea was essentially right. I give an
> outline:
>
> Stacks, written as Prolog lists:
>
> [A, B, C | D] is a stack of at least 3 elements A is an empty stack
> (suitable only suitable for push) [A, B, C] would be a stack of exactly 3
> elements (hardly useful)
>
> swap turns [A, B | C) into [B, A | C). # This is the Prolog code !

That is very cool.

> Stack elements, have typing information when the type matters: Assume that
> we have a general numeric type, with two subtypes
>
> A:num:B is a numeric stack element, subtype unspecified:
>
> + turns [A:num:B, C:num:D | E) into [F:num:G | E] :- F is A + C. # Prolog !
>
> A:num:int is an integer numeric stack element.
>
> A:num:float a a float numeric stack element.
>
> Note that addition and several other operators work on both subtypes, but
> not all do:
>
> succ turns [A:num:int | B] into [C:num:int | B] :- C is A +1. #Prolog
>
> Assume that we have a similar notation for lists, possibly with subtypes:
> A:list:B is a list of elements of unspecified type A:list:num:float is a
> list of floats. A:list:list:B is a list of lists of unspecified type.
>
> cons turns [A:list:B, C:B | D] into [[C:B, A]:list:B | D].
>
> And so on for all operators. Now the important bit, the concatenative
> principle: output stack from one operator must match input stack for next.
> In the first line below, E is the intermediate stack pattern. Here is the
> interpreter ( = exterm() in Joy, John Cowan might recognise).
>
> [A | B] turns C into D :- A turns C into E, B turns E into D. [] turns A
> into A.
>
> Now the marvellous bit: given the definition foo == bar baz zot, where bar
> baz zot are primitives or have been previously defined, Prolog automatically
> works out the input and output stacks for foo. I did not have to write any
> code for this, in fact it took me some time to notice that Prolog had done
> it. Such is the power of unification.

Your approach to directly expose Prolog as the language for expressing
type is elegant and very powerful. My only hesitation is the syntax of
prolog, which may be accessible to a logician, are not great for
someone with only some collegial level math. In general the problem I
am having is with constructing an accessible syntax for people.

Currently I am now heavily leaning towards:

cons : (list['a] 'a -> list['a])
uncons : (list['a] -> list['a] 'a)
etc.

> So, even if your implementation language is not Prolog, you should consider
> whether similar techniques could be written in your implmentation language.
> I have to confess that I have never written a unifier, but I have seen very
> short (half a page) versions. It may even be that for the above purposes
> only a very simple version is needed.

Unifiers can be quite simple, given the right abstractions. I have
seen incredibly short versions in Scheme for instance. My unification
code is horribly naive. ;-)

> Best wishes with the project.

Thank you very much! And thank you for the little Prolog tutorial, it
was quite informative.

> - Manfred

- Christopher