using the Shen20 dict w/ the type system

[Antti Ylikoski]

I would like to ask for some help from the Shen community.

I'm attempting to use the Shen20 dict capability with the Shen type

system.  The below is what I get.  First, the file dict-koe.shen:

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

\\ AJY 2017-07-22

\\

(datatype d

______________________________

(value *d*) : (dict symbol unit);

)

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

Then, the below happens.  What do I do wrong?

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

Microsoft Windows [Version 10.0.14393]

(c) 2016 Microsoft Corporation. Kaikki oikeudet pidätetään.

c:\Users\Antti Ylikoski\Dropbox\hopfield>.\shen

.\shen

Shen, copyright (C) 2010-2015 Mark Tarver

www.shenlanguage.org, Shen 20.0

running under Common Lisp, implementation: SBCL

port 2.0 ported by Mark Tarver

(0-) (load "dict-koe.shen")

type#d

run time: 0.01600000262260437 secs

loaded

(1-) (set *d* (dict 10))

(dict ...)

(2-) (dict-> (value *d*) name "Antti")

"Antti"

(3-) (<-dict (value *d*) name)

"Antti"

(4-) (tc +)

true

(5+) (dict-> (value *d*) surname "Y")

type error

(6+) (<-dict (value *d*) name)

"Antti" : unit

(7+) (<-dict (value *d*) surname)

value not found

(8+) (exit 0)

c:\Users\Antti Ylikoski\Dropbox\hopfield>

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

With the type system on, I can fetch the key value "Antti" from the

dict, but I cannot store the key value "Y" into the dict.  It will

generate a type error, above.

Some smart help would be very much appreciated.

yours, AJY

Finland, the EU

[Bruno Deferrari]

I think there is a misunderstanding about what 'unit' is.

Shen doesn't define `unit` anywhere, it only exists as a convention,
when you use `unit` you are just using a symbol that has not been
taken by any type definition, you may use `antti` if you want with the
same result.

Try this in the REPL:

- Enable `(tc +)`
- Enable `(spy +)`
- Attempt various combinations of `SomeValue : unit`

You will see that the typechecker will throw an error every time it
tries to verify that one value is of type `unit`, thats because there
is no such thing as a value of type `unit` (at least not until you
define your own theory).

Now, what follows if a very rough picture of whats going on, and I
hope it helps to make things clearer instead of more confusing, my
advice is to re-read the relevant sections of the Shen book and play
more with `(spy +)` to develop your intuition.

The types of the dict operations are:

<-dict : { (dict A B) --> A --> B }
dict-> : { (dict A B) --> A --> B --> B }

Since your dict is of type `(dict symbol unit)`, for dicts of such
type then any expression that looks like `(<-dict Dict Symbol)` will
look like this to the typechecker:

(dict A1 B1) --> A2 --> B2
(dict symbol unit) --> symbol --> unit

Every A has to match every other A (either by being the same or
compatible), same for every B.

A1 matches A2 and B1 matches B2, thats good, the result is tagged as
`unit`, thats why you see "Antti" : unit (even if we know "Antti" is a
string, the typechecker will not try to validate this because you are
not using the value for anything yet).

For `(<-dict Dict Symbol String)` the story is different:

(dict A1 B1) --> A2 --> B2 --> B3
(dict symbol unit) --> symbol --> string --> unit

Here not all B match, we have B1 and B3 being `unit` (thats ok), but
B2 is `string` (not good), and that is where the typechecking is
failing.

One of the options you have is to make a function that changes the
type of a value to `unit`:

(define mkunit X -> X)

(datatype mkunit
__________
mkunit : (A --> unit);)

which will allow this to work:

(dict-> (value *d*) surname (mkunit "Y"))


Another option is to add a definition for the specific case of dicts
with values of type `unit`.

> --
> 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+un...@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

[Antti Ylikoski]

Isn't it the case that for about a year ago, there was here some discussion as to the usage of the type
name "unit"?  I think Dr Tarver and Mark Thom and I took part in the discussion.

IIRC the type "unit" is "uninhabited" by default, and some definitions are needed to be able to use it as
a symbol denoting "no type information attached".

AJY

[Bruno Deferrari]

On Sat, Jul 22, 2017 at 5:20 PM, Antti Ylikoski
<antti.y...@gmail.com> wrote:
> Isn't it the case that for about a year ago, there was here some discussion
> as to the usage of the type
> name "unit"? I think Dr Tarver and Mark Thom and I took part in the
> discussion.
>
> IIRC the type "unit" is "uninhabited" by default, and some definitions are
> needed to be able to use it as
> a symbol denoting "no type information attached".
>
> AJY
>

Thats correct. The same can be said about `aeroplane`, `antti`,
`bruno`, etc etc, what I wanted to clarify is that `unit` has no
special meaning for the typechecker, it is just a convention. So like
for any other type that has not been defined already, you will have to
give it the meaning you want explicitly, because it comes with none.

[Antti Ylikoski]

Thank you very much, BD.  The below mentioned will work:

(I needed a dictionary where one can store/retrieve several different
types.)

First, the file dict-koe.shen:

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

\\ AJY 2017-07-22
\\

(datatype d

______________________________

(value *d*) : (dict symbol ANY);

)

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

Then, see what will happen:

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

antti@antti-HP-Compaq-6715s-GR618ES-AK8:~/Dropbox/hopfield$ shen

Shen, copyright (C) 2010-2015 Mark Tarver
www.shenlanguage.org, Shen 20.0
running under Common Lisp, implementation: SBCL
port 2.0 ported by Mark Tarver

(0-) (tc +)
true

(1+) (load "dict-koe.shen")

type#d : symbol
run time: 0.1809999942779541 secs

typechecked in 30 inferences
loaded : symbol

(2+) (set *d* (dict 10))
(dict ...) : (dict symbol A)

(3+) (dict-> (value *d*) name "Antti")
"Antti" : string

(4+) (dict-> (value *d*) surname ylikoski)
ylikoski : symbol

(5+) (<-dict (value *d*) name)
"Antti" : A

(6+) (<-dict (value *d*) surname)
ylikoski : A

(7+) (exit 0)
antti@antti-HP-Compaq-6715s-GR618ES-AK8:~/Dropbox/hopfield$

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

And this will solve the problem.  Thanks.

yours, AJY
Finland, the EU

[Bruno Deferrari]

Be careful with that, while it my solve your initial problem, it is
unsafe because now code like this typechecks:

(3+) (define should-not-typecheck
{ number --> number }
X -> (+ X (<-dict (value *d*) name)))
should-not-typecheck : (number --> number)

What you want instead is something like:

(datatype anything
_________
X : anything;)

(datatype d
______________________________
(value *d*) : (dict symbol anything);)


(I used `anything` here, but you may as well use `unit` with the same result)

And now this fails to typecheck as expected:

(4+) (define should-not-typecheck
{ number --> number }
X -> (+ X (<-dict (value *d*) name)))
type error in rule 1 of test

You can use `(spy +)` to see why.

[Bruno Deferrari]

Sorry, make that:

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

The version I sent earlier is unsafe too as it introduces a big hole
that makes stuff like this typecheck in the REPL:

(6+) (+ 1 three)
~s is not a number: three

--
BD

[Antti Ylikoski]

I have one wish for the developers of Shen.

When using the type system of Shen, and there is there a type error,
then the error message that the user will get, is not any more
informative than, typically:

type error in rule 2 of for-col-aux

If the said rule 2 is nontrivial, then it may be truly difficult for
the user to discover what kind of a type error there is there.

The above example was such that not even the (spy +) was sufficiently
helpful in pinpointing the error.

I do admit that I'm being a little bit lazy here.  Some industrious
study of the Shen type system certainly would have uncovered the error.

But the above addition to the error messages would very much help the
task of the diligent programmer.

yours, A. J. Y.
Finland, the E.U.

[Antti Ylikoski]

(Corrected entry.)

I have some difficulties in the use of the (dict ...) with the Shen
type system.  The below will generate a type error:

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

(define mk-neuron
    { number --> number --> (dict A B) }
    Indx Indx2 ->
        (let
        N (dict 10)
        _ (dict-> N row Indx)
        _ (dict-> N col Indx2)
        N))


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

Examining the functionality of the Shen type system with the (spy +)
would not help.

Is this somehow associated with the fact that a global var can and
needs to be type declared, but the local (let ...) form variable "N"
above cannot be given any type declaration?

yours, A. J. Y.
Finland, the E.U.

lauantai 22. heinäkuuta 2017 22.16.41 UTC+3 Antti Ylikoski kirjoitti:

[Bruno Deferrari]

On Sun, Jul 23, 2017 at 3:20 PM, Antti Ylikoski <antti.y...@gmail.com> wrote:
>
> (Corrected entry.)
>
> I have some difficulties in the use of the (dict ...) with the Shen
> type system.  The below will generate a type error:
>
> --------------------------------------------------
>
> (define mk-neuron
>     { number --> number --> (dict A B) }
>     Indx Indx2 ->
>         (let
>         N (dict 10)
>         _ (dict-> N row Indx)
>         _ (dict-> N col Indx2)
>         N))
>
>
> --------------------------------------------------
>
> Examining the functionality of the Shen type system with the (spy +)
> would not help.
>
> Is this somehow associated with the fact that a global var can and
> needs to be type declared, but the local (let ...) form variable "N"
> above cannot be given any type declaration?
>
> yours, A. J. Y.
> Finland, the E.U.
>

What you have there is not a `(dict A B)`, it is intead a `(dict symbol number)` after you have done those calls to `dict->`.
If you update the signature to include that info it will work.

You will face the same situation when using vectors:

this fails to typecheck:

(define does-not-work
  { number --> (vector A) }
  N -> (let V (vector 10)
            _ (vector-> V 3 N)
         V))

but this works:

(define does-work
  { number --> (vector number) }
  N -> (let V (vector 10) 
            _ (vector-> V 3 N)
         V))

[Antti Ylikoski]

What I'm attempting to do, needs some pretty sophisticated Shen type
system programming.

First define:

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

Then, I try to make a (dict ...) where one can store/retrieve
different type values (numbers, strings, dicts etc....) using symbols
as keys.

An artificial neuron has a number of fields: a Hopfield neuron here
has two number coordinates; a string documentation; other dicts as
fields; the result that I attempt to make, would look like the below:

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

(datatype hfield

X : (dict symbol anything);
===========================
X : hfield;)


(define mk-neuron
    { number --> number --> .... --> hfield }
    X Y Doc Inputs Weights Outputs .... ->
        (let
        N (dict 20)
        _ (dict-> N row X) ; store a number
        _ (dict-> N col Y) ; store another number
        _ (dict-> N doc Doc) ; store a string
        _ (dict-> N inputs Inputs) ; store a (dict ...)
        _ (dict-> N weights Weights) ; store a (dict ...)
        .......
        _ (dict-> N outputs Outputs) ; store a list
        N)) ; return the (dict ...) which is the neuron

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

Can this be done elegantly with the Shen type system?

I understand that it can be done, but the type system programming is
too difficult for me.

Certainly I cannot expect anyone to do my programming for me; but I
feel that this example has some general interest, therefore it is
here.

yours, AJY
Finland, the EU

[Mark Tarver]

I've looked very quickly at the dict code - perhaps look at TBoS 19.7?  Just a thought.

Mark

(datatype dictionary
	Indexes : (list number);
	Store : (vector (list (@p A B)));
	======================
	(absvector symbol Keys Store) : dictionary;)

[Antti Ylikoski]

Yes: I could use an absvector for that purpose, but I think not with

the Shen type system.  See

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

Microsoft Windows [Version 10.0.14393]

(c) 2016 Microsoft Corporation. Kaikki oikeudet pidätetään.

c:\Users\Antti Ylikoski\Dropbox\hopfield>.\shen

.\shen

Shen, copyright (C) 2010-2015 Mark Tarver

www.shenlanguage.org, Shen 20.0

running under Common Lisp, implementation: SBCL

port 2.0 ported by Mark Tarver

(0-) (absvector 10)

<0 0 0 0 0 0 0 0 0>

(1-) (tc +)

true

(2+) (absvector 10)

type error

(3+) (exit 0)

c:\Users\Antti Ylikoski\Dropbox\hopfield>

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

I think that the Book of Shen mentions that the absvectors are not a

part of the Shen type system.

It would be very nice if I could use the Shen (dict ...) capability in

a manner analogous to the Common LISP hashtables, or the Python hash

facility.

Perhaps update the Shen?  I feel that this capability were very useful

for many programmers.

yours, AJY

Finland, the EU

[Bruno Deferrari]

Being that the keys are all known (at least it seems so to me from your examples), you are not assigning arbitrary key/value bindings, so what you need is not dicts, but structs/records. 

You may find Ramil's defstruct library useful: https://github.com/vasil-sd/shen-libs/blob/master/defstruct/defstruct.shen

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

[Antti Ylikoski]

Yes, very true.

I used the R.F. defstruct facility, but it does not work with the Shen
type system.

I attempted to convert the R.F. defstruct.shen into a form which would
work with types, and did some successful work: for example I
discovered that the macros are included in the type system, and how.

But, it turned out that this conversion work could not be done.  The
defstruct.shen uses the (intern ...) function, which will not work
with the type system, as Dr Tarver recently noted.

Dr Tarver authored an o-o.shen package, which I might attempt to
convert for this work.

Would it however be somehow possible to make the (intern ...) work
with the Shen type system?  I would need such a capability.

yours, AJY
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/UVmygCFqalM/unsubscribe.
To unsubscribe from this group and all its topics, send an email to qilang+unsubscribe@googlegroups.com.

[Bruno Deferrari]

I don't understand what doesn't work with defstruct.

If you load it, then enable `(tc +)` before defining your structs, it works fine, with the constructors, setters and getters it generates all properly typed.

Could it be that you tried to load it with typechecking enabled? if thats so, make sure it is disabled before you load the library, and only enable it after it has been loaded.

[Bruno Deferrari]

Example:

Shen, copyright (C) 2010-2015 Mark Tarver

www.shenlanguage.org, Shen 20.1

running under Scheme, implementation: chez-scheme

port 0.16 ported by Bruno Deferrari

(0-) (load "defstruct.shen")

..snip...

run time: 0.04157700000000003 secs

loaded

(1-) (tc +)

true

(2+) (defstruct person

    (name string)

    (last-name string)

    (gender symbol)

    (age number))

type#person : symbol

mk-person : (string --> (string --> (symbol --> (number --> person))))

person-age-> : (person --> (number --> person))

person-gender-> : (person --> (symbol --> person))

person-last-name-> : (person --> (string --> person))

person-name-> : (person --> (string --> person))

person-age : (person --> number)

person-gender : (person --> symbol)

person-last-name : (person --> string)

person-name : (person --> string)

(3+) mk-person

mk-person : (string --> (string --> (symbol --> (number --> person))))

(4+) (let Person (mk-person "John" "Doe" male 100) 

          Age1 (person-age Person)

          _ (person-age-> Person 50)

          Age2 (person-age Person)

      [Age1 Age2])

[100 50] : (list number)

(5+) (mk-person "John" "Doe" male 100)
<"John" "Doe" male 100> : person

--

BD