`any` type (was "Re: Problems w/ the Shen type system")

[Bruno Deferrari]

On Thu, Aug 3, 2017 at 6:48 PM, Mark Tarver <dr.mt...@gmail.com> wrote:

It's better;  though the goal of typing heterogeneous lists still fails

[1 2 [a j 5]] : (list any)

fails

as does

[1 2 [a j 5]] : any

Basically he needs the concept of an s-expr which is used in the Ring.  However this type is so general as to provide no assurance for most operations he would want to do.  Hence I suspect that the types need to be redefined.

Mark

Oh I see. Solving `(OP any)` is easy, but then of course, I then have to solve `(OP1 (OP2 any))` and it starts to get interesting.

This is good material for a wiki entry, will add one when I figure it out (along with the explanations for other interesting types that have shown up in this mailing list, like `not`).

 

On Thursday, August 3, 2017 at 6:36:15 PM UTC+1, Bruno Deferrari wrote:

On Thu, Aug 3, 2017 at 2:27 PM, Mark Tarver <dr.mt...@gmail.com> wrote:

It is certainly an improvement; but I don't think that Antti's program will type check even under this rule.  You cannot multiply anys to get a guaranteed number.  The datatypes need to be properly defined for this program.

Mark

Ah yeah, I just meant in general, as a definition of "any" that doesn't introduce holes, not related to Antti's program.

 

On Thu, Aug 3, 2017 at 4:57 PM, Bruno Deferrari <uti...@gmail.com> wrote:

Would this be enough?

(datatype any
  X : Type;
  ______
  X : (mode any -);)

On Thu, Aug 3, 2017 at 5:46 AM, Mark Tarver <dr.mt...@gmail.com> wrote:

Basically your axiom doesn't do things you need it to and does things you don't need it to.  You can't multiply two inputs which are anys and get a number which is what multiplication expects to deliver - that's the problem in your code in activation-level-1.  You can however enter the typing (* 7 a) : any and get it through, though it delivers a type error.  The axiom is not right.

Mark

On Thursday, August 3, 2017 at 9:32:04 AM UTC+1, Mark Tarver wrote:

I'm not sure that your any does what you think it does.  Willi had an any which was somewhat different.  Room perhaps for a metaphysical discussion on the nature of anyness.

Mark

On Friday, July 28, 2017 at 7:15:11 AM UTC+1, Antti Ylikoski wrote:

No; the datatype "any" has been given the below definition:

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


\\ "Any" type definition, needed for nonhomogenous lists: any

(datatype any
   _________
   X : (mode any -);)


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

... in the file bpropmll.shen

yours, AJY
Finland, the EU


torstai 27. heinäkuuta 2017 22.03.01 UTC+3 Mark Tarver kirjoitti:

I'd say offhand that the problem comes at activation-level-1 where you multiply two anys together where nothing is said about what an any is.

Mark

On Monday, July 24, 2017 at 3:07:21 AM UTC+1, Antti Ylikoski wrote:

I decided to continue my Shen ANN work.

But, I'm having problems with the Shen type system.  I attach one of

my ANN programs, for several reasons.

It is a nice example about how to build a nontrivial abstract datatype

capability.  And there are there some hints as how to program type

system concordant neural net software with Shen.  As I have written,

some individuals here are doing ANN work, and they might want to carry

out this work with Shen.

And: the file that I attach will make the Shen type system infinite

loop.  The infinite loop will happen in the function

activation-level-1.  Why this happens, I could not find out.

For clarity, the said function is below:

\\ The activation function of the perceptron

\\

\\ NOTA BENE: the bias, which bias == +1, handled separately

\\ Sum of inputs * weights + bias (=df 1.0) * weight of bias

(define activation-level

  { pctron --> number }

  N -> (+ (activation-level-1

              (pIns N) \\ inputs list

     (pWts N) \\ weights list, In the identical order

     0)

 (* 1.0 (pBias N)))) \\ plus the addition from the bias

\\ Compute the sum of the products of the

\\ input numbers from pairs, and the weights from the pairs

(define activation-level-1

  { (list (list any)) --> (list (list any)) --> number --> number }

  [] _ Sum -> Sum \\ All partial sums done?

  [ [Inp Name1] | T1] [ [Wt Name2] | T2] Sum ->

      (activation-level-1

          T1 T2

          (+ Sum (* Inp Wt))))

I think that someone compared Shen to a fine sports car: it will go

very fast, but the tuning and the maintenance and its use are

nontrivial.

yours, AJY

Finland, the EU

--
You received this message because you are subscribed to the Google Groups "Shen" group.
To unsubscribe from this group and stop receiving emails from it, 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.

--

BD

--
You received this message because you are subscribed to the Google Groups "Shen" group.
To unsubscribe from this group and stop receiving emails from it, 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.

--
You received this message because you are subscribed to the Google Groups "Shen" group.
To unsubscribe from this group and stop receiving emails from it, 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.

--

BD

--
You received this message because you are subscribed to the Google Groups "Shen" group.
To unsubscribe from this group and stop receiving emails from it, 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.

--

BD

[Bruno Deferrari]

On Thu, Aug 3, 2017 at 8:42 PM, Bruno Deferrari <uti...@gmail.com> wrote:

On Thu, Aug 3, 2017 at 6:48 PM, Mark Tarver <dr.mt...@gmail.com> wrote:

It's better;  though the goal of typing heterogeneous lists still fails

[1 2 [a j 5]] : (list any)

fails

as does

[1 2 [a j 5]] : any

Basically he needs the concept of an s-expr which is used in the Ring.  However this type is so general as to provide no assurance for most operations he would want to do.  Hence I suspect that the types need to be redefined.

Mark

Oh I see. Solving `(OP any)` is easy, but then of course, I then have to solve `(OP1 (OP2 any))` and it starts to get interesting.

This is good material for a wiki entry, will add one when I figure it out (along with the explanations for other interesting types that have shown up in this mailing list, like `not`).

Ok, actually, it may not be needed. Here is what I have in mind (can't test now, will do tomorrow and report back):

(datatype any
  X : Type;
  ________
  X : (mode any -);

  X : (Op any);
  __________

--

BD

[Bruno Deferrari]

On Thu, Aug 3, 2017 at 8:47 PM, Bruno Deferrari <uti...@gmail.com> wrote:

On Thu, Aug 3, 2017 at 8:42 PM, Bruno Deferrari <uti...@gmail.com> wrote:

On Thu, Aug 3, 2017 at 6:48 PM, Mark Tarver <dr.mt...@gmail.com> wrote:

It's better;  though the goal of typing heterogeneous lists still fails

[1 2 [a j 5]] : (list any)

fails

as does

[1 2 [a j 5]] : any

Basically he needs the concept of an s-expr which is used in the Ring.  However this type is so general as to provide no assurance for most operations he would want to do.  Hence I suspect that the types need to be redefined.

Mark

Oh I see. Solving `(OP any)` is easy, but then of course, I then have to solve `(OP1 (OP2 any))` and it starts to get interesting.

This is good material for a wiki entry, will add one when I figure it out (along with the explanations for other interesting types that have shown up in this mailing list, like `not`).

Ok, actually, it may not be needed. Here is what I have in mind (can't test now, will do tomorrow and report back):

(datatype any
  X : Type;
  ________
  X : (mode any -);

  X : (Op any);
  __________

  X : (mode any -);)

 

An important detail here is that I used `(Op any)` instead of  `(Op Var)`, expecting for that to trigger a recursive check on the parameter of `Op` so that it is compatible with the `(mode any -)` declaration. My assumption here may be wrong, which is what I have to test (and of course, this doesn't handle cases like `(any * any)`, `(any --> any)`, etc which are not covered by `(Op any)`).

--

BD

[Mark Tarver]

(datatype s-expr

    X : atom;

    _______

    X : s-expr;

    [X | Y] : (list s-expr);

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

    [X | Y] : s-expr;

    X : boolean;

    __________

    X : atom;

    X : string;

    ________

    X : atom;

    X : symbol;

    _________

    X : atom;

    X : number;

    _________

    X : atom;

    __________

    [] : atom;)

will define symbolic expression.   

[Bruno Deferrari]

On Fri, Aug 4, 2017 at 3:26 AM, Mark Tarver <dr.mt...@gmail.com> wrote:

(datatype s-expr

    X : atom;

    _______

    X : s-expr;

    [X | Y] : (list s-expr);

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

    [X | Y] : s-expr;

    X : boolean;

    __________

    X : atom;

    X : string;

    ________

    X : atom;

    X : symbol;

    _________

    X : atom;

    X : number;

    _________

    X : atom;

    __________

    [] : atom;)

will define symbolic expression.   

Thank you. Not what I'm trying to do with `any`, but still very useful.

What I want to make with `any` is something like `dynamic` in C#.

I tried the definition I gave before and it seems to work fine (no need to handle tuples and functions like I thought before, because those are mixed already):

Example REPL interaction here testing various values (including user defined types), and safety: https://gist.githubusercontent.com/tizoc/e358f5a4be85d3a02fdc6f23124bdb6c/raw/f616b320a7c1eab33896717460463ec86c622637/any.shen

Does anyone see something that I may have missed?

--

BD