Shen types question

[Antti Ylikoski]

I have a non-expert question.  (I decided not any more to call myself

a Novice :))

In order to learn the use of types in Shen, I have been writing a

fully type secure stack as an abstract datatype, and as the lambda

expression version.

The stack as the lambda expression version comes in the attachment

file stackLambda.shen.  It will work.  The demo run is in the

attachment stackLambda.txt.

But when I attempt to make a fully type secure ADT version of it,

there occurs there an error which I cannot figure out.  The non

working version of the lambda ADT stack comes in the attachment

stackL.shen.

Any smart help would be very much appreciated.

yours, Dr A. J. Y.

HELSINKI

Finland, the EU

[Willi Riha]

I too have had a look at this genuinely abstract implementation.. It is extremely clever, and I am still trying to fully  understand it.

You say that you have found an error (or that it doesn't work) I can see no example of any failure in your attachments.

There is, however, an error in the code - I cannot rectify it, but surely Mark can.

If one attempts to inspect the top element of an empty stack,this should result in an error. Similarly, when you pop an empty stack there should be an errro,

unless one defines pop (empty-stack) = empty-stack.

Example:

(4-) (top (empty-stack))

#<FUNCTION (LAMBDA (X) :IN empty-stack) {25DA8345}>           should be an error!

(5-) (pop (empty-stack))     

#<FUNCTION (LAMBDA (X) :IN empty-stack) {25DA8345}>``should be an error!

(6-) (top(pop (empty-stack)))

this stack is empty                                    now it is !

This implementation is genuinely abstract - unlike a  list based implementation, which is concrete.

Notice the difference, Mark's stack implementation does not show you any detail of its representation, unlike yours, which clearly shows that a stack is a just a list,

and this information could be used to compromise the stack data type.

I am not against concrete implementations of any data type, because they are usually much more efficient in practice

I do not claim that Mark's very clever implementation is superior, because it isn't, as far as efficiency is concerned

But I still object, very strongly that an obviously concrete implementation should be called "abstract"

.

[Antti Ylikoski]

Dear Willi:

Abstract datatypes in computer science work as follows.

First one defines the data, ie. the data objects and the values they

may have; and also, one defines the operations on the data objects.

With Mark's Shen system, one clearly can see that this is done with

the

(datatype stack

[...]

)

definition.

Thereafter, the concrete implementation of the above abstract

definition is given.  First we define what is done, after that we

define how it is done, in practice.  The concrete implementation for

the abstract definition.

The selfsame (datatype [...] ) interface definition, as I might call

it, can be concrete implemented in multiple ways.  The

(datatype stack [...] )

interface can be given a list and head--tail--cons implementation.

Or, the same

(datatype stack [...] )

definition can be given a lambda expression implementation.  I agree

with you that Mark's work is extremely clever :)) The selfsame

(datatype stack [...]) interface even could be implemented with a

memory pool for the stack as a vector, this could be done, though not

very handy.

The practical usefulness of all this stuff is, that the types system

of Shen gives excellent support for the programmer, who is attempting

to make something truly complicated and complex.  This functionality

is completely missing from AI languages such as the Common LISP and

Prolog, even though the said functionality is highly useful, and even,

really necessary for the programmer.

Oh, by the way, I said to Mark, and I shall write here, that I myself

have studied university mathematics, and I know how significant a

personal achievement a PhD in mathematics is, you say that you have

earned one.  The maths-lib.shen is indeed good work.

yours, Dr A. J. Y.

HELSINKI

Finland, the EU

[Willi Riha]

Even though my reply might be of interest to other readers,

I am only mailing it to Antti.

On Wednesday, August 17, 2016 at 12:34:13 PM UTC+1, Antti Ylikoski wrote:

[Mark Tarver]

Antti; you have a bracketing error in your code; see red code.  It should be

(define empty-stack

    -> (/. X (if (or (= X pop) (= X top))

                 (error "~%This stack is empty~%")

(error "~A is not an operation on stacks~% X"))))

Mark

[Antti Ylikoski]

Thank you -- I'm so tired that I make typos........

Now the lambda stack as an ADT is in the form in the attachment file

stackL.shen, of this entry.

There still remains an error; the sample run is below.  I know that

this is a question of the finesses of the sequent calculus and the

Shen type theory, but I need some help in fixing the error, indeed

still being a Shen non-expert.

yours, A. J. Y.

HELSINKI

Finland, the EU

------------------------------------------------------------

antti@antti-HP-Compaq-dc7100-SFF-PE271ET ~/stack $ ./Shen

Shen, copyright (C) 2010-2015 Mark Tarver

www.shenlanguage.org, Shen 19.2

running under Common Lisp, implementation: CLisp

port 1.9 ported by Mark Tarver

(0-) (tc +)

true

(1+) (load "stackL.shen")

type#stack : symbol

empty-stack : (--> (stack A))

maximum inferences exceeded~%

(2+) 

------------------------------------------------------------

A. J. Y.

[fuzzy wozzy]

is this simulated stack programming and can anything useful be done with it?

[Mark Tarver]

(define push

    {symbol --> (stack A) --> (stack A) }

    X S -> (/. Y (if (= Y pop)

                     S

    (if (= Y top)

        X

        (error "~A is not an operation on stacks~%")))))

should be

(define push

    { A --> (stack A) --> (stack A) }

    X S -> (/. Y (if (= Y pop)

                     S

    (if (= Y top)

        X

        (error "~A is not an operation on stacks~%" Y)))))

But note that your datatype for stacks needs some looking at.

(datatype stack

S: (symbol --> A);

=============

S: (stack A);

\\ The stack is a lambda expression, which may return an object A,

\\ an item of the contents of the stack, or the said lambda expression

\\ may return a stack (when the stack has been popped), which is

\\ another lambda expression of the type (stack A).

S: (symbol --> (stack A));

==================

S: (stack A);

\\ The operations defs are not needed here

\\ since the function signatures are there

\\ Test variable

___________________________________

(value s) : (stack A);

)

Mark

[Mark Tarver]

What your defs say is that an object of (stack A) is simultaneously an object that if it receives a symbol outputs an A and if it receives a symbol outputs an object of type (stack A).  Actually not quite.  It is an object that if it receives a symbol outputs an object which is either an A or a (stack A). 

In logic it is the difference between   

(P => Q) & (P => R)

vs

P => (Q v R)

Mark

[Mark Tarver]

Try 

(datatype stack

  S : (symbol --> (or A (stack A)));

  =================================

  S : (stack A);

  

  S : (stack A);

  ______________

  (S top) : A;

  

  S : (stack A);

  ____________________

  (S pop) : (stack A);

  X : A;

  _____________________

  X : (mode (or A B) -);

  X : B;

  _____________________

  X : (mode (or A B) -);)

  

  Mark

[Antti Ylikoski]

Thank you once again.

Now, the type secure lambda expression stack as an ADT works as below:

------------------------------------------------------------

antti@antti-HP-Compaq-dc7100-SFF-PE271ET ~/stack $ ./Shen

Shen, copyright (C) 2010-2015 Mark Tarver

www.shenlanguage.org, Shen 19.2

running under Common Lisp, implementation: CLisp

port 1.9 ported by Mark Tarver

(0-) (tc +)

true

(1+) (load "stackL.shen")

type#stack : symbol

empty-stack : (--> (stack A))

push : (A --> ((stack A) --> (stack A)))

top : ((stack A) --> A)

pop : ((stack A) --> (stack A))

run time: 1.2599999867379665 secs

typechecked in 1182 inferences

loaded : symbol

(2+) (set s (empty-stack))

#<COMPILED-FUNCTION empty-stack-1> : (stack A)

(3+) (value s)

#<COMPILED-FUNCTION empty-stack-1> : (stack A)

(4+) (set s (push q (value s)))

#<COMPILED-FUNCTION push-1> : (stack symbol)

(5+) (set s (push w (value s)))

#<COMPILED-FUNCTION push-1> : (stack symbol)

(6+) (set s (push e (value s)))

#<COMPILED-FUNCTION push-1> : (stack symbol)

(7+) (value s)

#<COMPILED-FUNCTION push-1> : (stack A)

(8+) (top (value s))

e : A

(9+) (set s (pop (value s)))

#<COMPILED-FUNCTION push-1> : (stack A)

(10+) (top (value s))

w : A

(11+) (set s (pop (value s)))

#<COMPILED-FUNCTION push-1> : (stack A)

(12+) (top (value s))

q : A

(13+) (set s (pop (value s)))

#<COMPILED-FUNCTION empty-stack-1> : (stack A)

(14+) (top (value s))

This stack is empty

(15+) (tc -)

false : boolean

(16-) (QUIT)

antti@antti-HP-Compaq-dc7100-SFF-PE271ET ~/stack $

------------------------------------------------------------

A. J. Y.

HELSINKI

Finland, the EU

--
You received this message because you are subscribed to a topic in the Google Groups "Shen" group.
To unsubscribe from this topic, visit https://groups.google.com/d/topic/qilang/UZk0hRVB6bQ/unsubscribe.
To unsubscribe from this group and all its topics, send an email to qilang+unsubscribe@googlegroups.com.
To post to this group, send email to qil...@googlegroups.com.
Visit this group at https://groups.google.com/group/qilang.
For more options, visit https://groups.google.com/d/optout.

[Antti Ylikoski]

I needed this in my work, this is why I started working on the point.

A. J. Y.

[Mark Tarver]

That's not quite right. w : A is the wrong answer.   It should be w : symbol.

The culprit is your extra axiom

______________________

(value s) : (stack A);

which is not invariantly true.

(14+) (set s (push a (empty-stack)))

#<CLOSURE (LAMBDA (Y) :IN push) {27676785}> : (stack symbol)

(15+) (value s)

#<CLOSURE (LAMBDA (Y) :IN push) {27676785}> : (stack A)

(16+) (* 7 (top (value s)))

Argument X is not a NUMBER: a

The program is not type secure.

This is a good illustration of why Shen is both more powerful than ML and Haskell for prototyping ideas, but needs to be handled with care.   Like a jet fighter, it responds to the nuances of what you communicate to it.

Mark

[Antti Ylikoski]

I decided -- finally -- to write a functional program out of my

Hopfield ANN studies, for optimizing hard to handle functions.

Some professional researchers say that Hopfield nets cannot be used to

calculate NP-complete problems, some professional researchers say that

Hopfield nets can be used to calculate NP-complete problems.  I myself

have seen that this (ie. computing hard problems with Hopfield ANNs)

can be done in practice, and it will lead to results.  Indeed, many

questions as to ANNs still are research questions today.

If you have studied the ANN material by me under the user bluejay77 in

the GitHub, you have seen that I implemented the artificial neurons

with the object oriented style programming, using Ramil Farkhshatov's

DEFSTRUCT functions.

It turns out that the OO style can be done with Shen in multiple ways:

I) the R.F's defstruct.shen can be used;

II) Mark created a "o-o.shen" library, which I planned to extend and

use;

III) Neal Alexander recently here wrote an implementation with the OO

semantics;

IV) a data structure with the object oriented style semantics can be

defined as a lambda expression, quite in the style of the lambda stack

(push ...) function.

As you will recall, the lambda stack push function is as follows:

------------------------------------------------------------

(define push

    X S -> (/. Y (if (= Y pop)

                     S

    (if (= Y top)

        X

        (error "~A is not an operation on stacks~%")))))

------------------------------------------------------------

and an OO style data record can be defined as a lambda expression

analogously:

------------------------------------------------------------

(define make-hopfield-neuron

    Name Doc Inputs Weights Xfer-Function ->

        (/. OP

   (cases

       (= OP h-name)

   Name \\ eg. "Neuron #45"

(= OP h-doc)

   Doc \\ eg. "Neuron 45 for optimizing the TSP"

(= OP h-inputs)

   Inputs \\ eg. [1.55 0.546 0.4 0.89]

(= OP h-weights)

   Weights \\ eg. [1 1 1 1]

(= OP h-xfer)

   (/. (Xfer-Function)) \\ the transfer function

true

   (error

   "Not a defined operation on a Hopfield neuron")

)))

------------------------------------------------------------

so this is why I began to study the lambda stack as an ADT.

yours, A. J. Y.

FINLAND

The EU

[Willi Riha]

On Wednesday, August 17, 2016 at 12:34:13 PM UTC+1, Antti Ylikoski wrote:

[Willi Riha]

Antti,

So, you are not interested in stacks, after all!

Your attempts at implementing a type-secure stack data type have failed, and so you discovered Mark’s implementation in terms of lambda functions, which is truly abstract. I cannot think of any tricks that would compromise the integrity of this implementation.

Aside: I have now discovered why (top (empty-stack)) and (pop (empty-stack)) did not work for me, even though I pasted the code directly from the book. In my copy of the 3^rd edition the definition of empty-stack starts

 

               (define empty-stack

                 _ -> (/.X etc

 

where the underscore _ should not be there.

I do not understand what you are trying to achieve with your ANN-program. I freely admit that I do not understand it, neither do I want to get involved in it.

Having said that, it appears to me that your attempt to use lambda functions to simulate OO-programming, even though it might be possible, seems extremely inefficient to me (I cannot prove it – Mark will know more about it).

I believe that using absvector (a powerful – but not purely functional - addition to Shen) is the way forward.  It is comparatively easy to emulate C++ classes, alas, not completely.

I do not want to elaborate, but I have learnt it from TBoS, 3^rd edn. p.97 (maybe with a few additional hints from Mark).

Good luck with your ANN!

 

Willi

On Wednesday, August 17, 2016 at 12:34:13 PM UTC+1, Antti Ylikoski wrote:

[Antti Ylikoski]

Ah, you are not interested in ADTs at all!

To say that I were not interested in the stack datatype is not

correct.  I wanted to work with the stack datatype, in order to

clarify my understanding concerning the Shen types theory, as for the

ADTs, and the finesses of the sequent calculus.

"Your attempts at implementing a type-secure stack data type have

failed, and so you discovered Mark’s implementation in terms of lambda

functions, which is truly abstract. I cannot think of any tricks that

would compromise the integrity of this implementation."

Your attempts to nullify the type secure (?) stack datatype, with the

list (cons--head--tail) implementation, have failed.... What are you

saying?

Absvectors are not a part of the Shen type system.

yours, Dr A. J. Y.

HELSINKI

Finland, the EU

[Willi Riha]

Antti,

What a shame that you could not have enlightened me 40 or so years ago, as to the true nature of ADTs.!

I now feel so guilty that I have taught, at least tw,o generations of students the wrong idea, about ADTs.

I will also need to inform a former colleague, who has published numerous papers on this subject., that he has got it wrong.

I am aware that appealing to a person's authority, in order to prove a point, is philosophically untenable. 

This is known as "argumentum ad authoritatem (or vericundiam)

For example, one could claim that somebody who has written 3 books on a certain subject, must be an expert.

It is a fallacy, because what this person has written might be complete nonsense.

But even if a community of "experts" agree that a certain fact is true, or that a certain definition is meaningful, there  will be people

just like Antti, who either don't comprehend it, or believe they know better.

I prefer to join in with the "experts"

tWhatever,, I declare herewith that Antti has won the argument,

 I am only sorry for all the hundreds of students I have taught facts about ADTs, which are obviously wrong (accordding to Anti)i

All the best with your ANNs! 

No more comments for some time!

Willi

PS. I rather like Antti for his enthusiasm.I tried to help him, but he knows better!

On Wednesday, August 17, 2016 at 12:34:13 PM UTC+1, Antti Ylikoski wrote: