B-Tree example to showcase Shen?

[Matthew Lamari]

I don't know the practicality, it's certainly outside of my skill level
(I'm still very much a browser); but I wonder if an example like this
one could be replicated in Shen:

http://matthew.brecknell.net/post/btree-gadt/

What this video showed was the haskell (GHC + a stack of language
extensions) type system driving the developer toward a tiny subset of
legal solutions. The type-work basically guaranteed the balance of the
tree which was very impressive; but was not (at least for the example)
enough to guarantee many other properties (the tree generated did not
have static guards protecting the order of elements). It could be in a
dependent-typed example (shen style) the type theory could guarantee more.

A "show your working" video example like this one could be very
educational and inspirational.

[Mark Tarver]

A "show your working" video example like this one could be very 

educational and inspirational. 

Good idea - do it.   Should take about a working week.  Do something simple first.

The documentation, the  website content, the appeal video, most code examples since 2005, the Shen kernel are written by one person (= me).  Time for a bit of diversity and load-sharing.

I've attached a type secure balanced tree program by Justin Grant to this message.

Mark 

[Jacob]

Meh, I do not think it would be that inspirational at all.  What you need is a flashy, eye candy ridden, Asian themed, sparkling, flashing, epilepsy inducing, monstrosity of an app to impress people.

[Mark Tarver]

Well a  good video can impress people; but it takes a lot of work (having done one) and it doesn't lead to where we need to be right now.   

I'm not against the idea and will put up any decent video on the website.

Mark

[Matthew Lamari]

I'll be needing a link from which to buy the 2nd ed of the shen book
before such an undertaking ;)

What is the mechanic you would use for depth guarantees? In the Haskell
one it was a faux number type N = Z | S N (number is zero or successor
of number) - would a shen-ish depth guarantee be based on that or
something else? (I won't even ask about the numeric ordering for now).


I'm going to go off onto some semi-related but different questions.
Related in that they all connect to a tree-based immutable map container.

Imagine an *ideal* Shen library tree-based immutable container, probably
based on an RB-tree, meant to not just store data but fit in if called
upon in support of heavily-statically checked code.

1. Is it idiomatic, desirable, or possible to have it statically
defined that an object added to that container is in the container?
I.e. provable that ((originalMap.Add(key, value)).Lookup(key) =
value ?
2. From where would that guarantee come? Would a masterfully-written
RB-tree implementation of "add/insert" automatically prove this
property? Or would it be some extra information you add to the
container's library code after getting the tree-work settled, sort of
"and oh by the way, trust me - adding something to this container
guarantees you get it back".

I'm not asking you to do a ton of dirty-work on these; but figure you'd
have a feel for where such dirty-work would be headed, and what's possible.


On 1/23/2014 5:22 AM, Mark Tarver wrote:
> *A "show your working" video example like this one could be very *
> *educational and inspirational. *

>
> Good idea - do it. Should take about a working week. Do something simple
> first.
>

> The documentation, the website *content*, the appeal video, most code

[Mark Tarver]

On Friday, 24 January 2014 13:54:16 UTC, Matthew Lamari wrote:

I'll be needing a link from which to buy the 2nd ed of the shen book
before such an undertaking ;)

What is the mechanic you would use for depth guarantees?  In the Haskell
one it was a faux number type N = Z | S N  (number is zero or successor
of number) - would a shen-ish depth guarantee be based on that or
something else?  (I won't even ask about the numeric ordering for now).

Generally successor notation is used

Shen 2010, copyright (C) 2010 Mark Tarver

released under the Shen license

www.shenlanguage.org, version 14.1

running under Common Lisp, implementation: SBCL

port 1.7 ported by Mark Tarver

(0-) (tc +)

true

(1+) (datatype numeric

   ___________

   [] : (len 0 A);

  X : A; Y : (len N A);

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

 [X | Y] : (len (succ N) A);)

type#numeric : symbol

(2+) (define mytl

  {(len (succ N) A) --> (len N A)}

   [_ | Y] -> Y)

mytl : ((len (succ N) A) --> (len N A))

(3+) (define myhd

       {(len (succ N) A) --> A}

        [X | _] -> X)

myhd : ((len (succ N) A) --> A)

(4+) (define mycons

       {A --> (len N A) --> (len (succ N) A)}

        X Y -> [X | Y])

mycons : (A --> ((len N A) --> (len (succ N) A)))

(5+) (mytl [a b c d])

[b c d] : (len (succ (succ (succ 0))) symbol) 

I'll look at the rest of your questions when I have a bit more time.

Mark

[Mark Tarver]

1.  Is it idiomatic, desirable, or possible to have it statically
defined that an object added to that container is in the container?
I.e.  provable that     ((originalMap.Add(key, value)).Lookup(key) =
value     ?
2.  From where would that guarantee come?  Would a masterfully-written
RB-tree implementation of "add/insert" automatically prove this
property?  Or would it be some extra information you add to the
container's library code after getting the tree-work settled, sort of
"and oh by the way, trust me - adding something to this container
guarantees you get it back".

" ((originalMap.Add(key, value)).Lookup(key) = value" is really not a type-theoretic statement; there are no types involved as I can see.  

That said, in Shen I've experimented with the type 'set' where X : (set A) iff X : (list A) and X contains no repeated elements.  

This requires a guarantee that the container does not contain a (repeated) element.

Shen 2010, copyright (C) 2010 Mark Tarver

released under the Shen license

www.shenlanguage.org, version 14.1

running under Common Lisp, implementation: SBCL

port 1.7 ported by Mark Tarver

(0-) (tc +)

true

(1+) (datatype set

   _____________

   [] : (set A);

   X : A; Y : ((set A) & (without X));

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

   [X | Y] : (mode (set A) -);

   X : (set A);

   _____________

   X : (list A);

   X : P; X : Q;

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

   X : (mode (P & Q) -);

   ________________

   [] : (without X);

   if (not (= X Z))

   Y : (without Z);

   ______________________

   [X | Y] : (without Z);

   ______________________________________________

   (not (element? X Y)) : verified >> Y : (without X);)

type#set : symbol

(2+)

 (define union'

   \\ not efficient but works

   {(set A) --> (set A) --> (set A)}

    [] S -> S

    [X | Y] S -> [X | (union' Y S)]     where (not (element? X (union' Y S)))

    [_ | Y] S -> (union' Y S))

union' : ((set A) --> ((set A) --> (set A)))

(3+) (union' [a b c] [c d e])

[a b c d e] : (set symbol)

(4+) (union' [a b c] [c d e e])

type error

Mark

[Mark Tarver]

This set stuff was part of an experiment with abstract algebra - the type of all gruppoids (groupoids).  Uses macros.

(10+) (define every

  {(list A) --> (A --> boolean) --> boolean}

   [] _ -> true

   [X | Y] F -> (and (trap-error (F X) (/. E false)) (every Y F)))

every : ((list A) --> ((A --> boolean) --> boolean))

(11+) (defmacro every-macro

  [every X D P] -> [every D [lambda X P]])

every-macro : unit

(12+) (defmacro exists-macro

  [exists X D P] -> [exists D [lambda X P]])

exists-macro : unit

(13+) (define exists

  {(list A) --> (A --> boolean) --> boolean}

   [] _ -> false

   [X | Y] F -> (or (trap-error (F X) (/. E false)) (every Y F)))

exists : ((list A) --> ((A --> boolean) --> boolean))

(14+)  (datatype gruppoid

            \\ a gruppoid is a pair composed of a set S of As and a closed operation on S.

    S : (set A); O : (closed (A --> A --> A) S);

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

    (@p S O) : (mode (gruppoid A) -);

    O : (A --> A --> A) >> P;

    ____________________________________

    O : (closed (A --> A --> A) S) >> P;

    __________________________________________________________

    (every X S (every Y S (element? (O X Y) S))) : verified >> O : (closed (A --> A --> A) S);)

type#gruppoid : symbol

(15+) (define logor

  {number --> number --> number}

   1 1 -> 1

   0 1 -> 1

   1 0 -> 1

   0 0 -> 0

   _ _ -> (error "not defined for logor"))

logor : (number --> (number --> number))

(16+) (define gruppoid

        \\ returns a gruppoid if the input is one

  {((set A) * (A --> A --> A)) --> (gruppoid A)}

   (@p S O) -> (@p S O)  where (every X S (every Y S (element? (O X Y) S)))

   G -> (error "~S is not a gruppoid~%" G))

gruppoid : (((set A) * (A --> (A --> A))) --> (gruppoid A))

(17+) (gruppoid (@p [1 0] (function logor)))

(@p [1 0] #<FUNCTION (LAMBDA (V1010)) {25BDC7C5}>) : (gruppoid number)

(18+) (gruppoid (@p [1 0 6] (function logor)))

(@p [1 0 6] #<FUNCTION (LAMBDA (V1015)) {2609767D}>) is not a gruppoid

Never used it for anything - just a study.

Mark

[Mark Tarver]

Semi-groups ..... you can probably do groups etc.  Perhaps wrt RB tress more for stimulating imagination.

(28+)  (datatype semigroup

    (@p S O) : (gruppoid A);  O : (associative S);

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

    (@p S O) : (semigroup A);

    __________________________________________________________________

    (every X S

      (every Y S

        (every Z S (= (O X (O Y Z))

                    (O (O X Y) Z))))) : verified >> O : (associative S);)

type#semigroup : symbol

(29+) (define semigroup

  {(gruppoid A) --> (semigroup A)}

    (@p S O) -> (@p S O)  where (every X S

                                  (every Y S

                                    (every Z S (= (O X (O Y Z))

                                                (O (O X Y) Z)))))

     G -> (error "~S is not a semigroup~%" G))

semigroup : ((gruppoid A) --> (semigroup A))

(30+) (semigroup (gruppoid (@p [1 0] (function logor))))

(@p [1 0] #<FUNCTION (LAMBDA (V1257)) {2597D4E5}>) : (semigroup number)

Mark

[Matthew Lamari]

Yeah, maybe it just would speak to a specific strength to a specific
audience.

The RBTree thing appealed to me in that it's an algorithm that I've
ported before, that's so troublesome (especially the delete case) that
even porting it from a working reference is fraught with pain, and "unit
testing" it a goofy comical exercise (a lot of corner cases that are
just a mirror of the products of code sections).

What was interesting was seeing the compiler basically slapping him into
a correct solution through the nastiest parts of the problem (well,
within limits, e.g. the order thing). Oh, I leverage some of that in C#
and F# within language limits; but don't get to use GADTs, or what may
be one step up again, "dependent typing" and/or shen-style constraints.

On 1/23/2014 11:47 AM, Jacob wrote:
>
>
> Meh, I do not think it would be that inspirational at all. What you need
> is a flashy, eye candy ridden, Asian themed, sparkling, flashing, epilepsy
> inducing, monstrosity of an app to impress people.
>
>
> On Thursday, January 23, 2014 6:22:49 AM UTC-5, Mark Tarver wrote:
>>

>> *A "show your working" video example like this one could be very *
>> *educational and inspirational. *
>>

>> Good idea - do it. Should take about a working week. Do something
>> simple first.
>>

>> The documentation, the website *content*, the appeal video, most code

[Matthew Lamari]

I'm piecing bits of understanding and tools together out of examples in
my reach between code scraps I can find, and see that there is something
very special here in all of this (using the Shen form of constraints on
programs).

Please critique code below. It comes from a lot of false starts where I
attempted too much, that I needn't share with posterity - I pulled back
to a specific part of the problem; but one where I think my
over-expressing the constraints (redundant or excessive clauses) is a
teachable moment for how the system really works.

I'm interested too in the "make-node" function if there's a way to
constrain the return as both a node and a nodes-under (succ A), if it's
idiomatically good form to do so, and if that's something that should be
done by naming another thing in the datatype. I'm aware too that in a
wider well-designed system, this may be the wrong question anyway - any
thoughts appreciated.

(tc +)
(datatype node-stuff

LChild : node; RChild : node; LChild : (nodes-under A); RChild :
(nodes-under A);
==============
[LChild RChild] : node;

LChild : (nodes-under A); RChild : (nodes-under A);
_________
[LChild RChild] : (nodes-under (succ A));

X : (nodes-under A);
_________
X : node;

_________
[] : (nodes-under 0);

_________
[] : node;


)

(define make-node-1
{(nodes-under A) --> (nodes-under A) --> (nodes-under (succ A))}
L R -> [L R])

(define make-node-2
{(nodes-under A) --> (nodes-under A) --> node}
L R -> [L R])

[Matthew Lamari]

Thanks - this "set" container example is very useful in a few areas.

I'm not sure what "mode" is in here, or what it means to the clauses
that mention it. I'm guessing it's a reserved word or type as renaming
it caused errors; but couldn't find it anywhere. What's its purpose,
and role in those clauses where it is mentioned?

Thanks,
Matt

[Matthew Lamari]

Just an addendum/complimennt

I changed to the abbreviation for left/right rules

X : (nodes-under A);
==============
X : node;

And the system detects that the 2 uses of X are the same type, such that
this new function typechecks

(define double-up
{node --> node}
X -> (make-node-2 X X))

Impressive!

[Mark Tarver]

The mode declaration (mode ... -) enforces pattern-matching and not  unification on the term within its scope 

TBoS 2nd edition p. 363

[Mark Tarver]

Good you are making progress and getting what you want; it's a bit difficult for people to give feedback w.o. seeing your work in the context of a working program.

Mark

[matt....@gmail.com]

Digging off an old thread, your "set/union" example.  I've modified it below to represent a list sorted from smallest to biggest; but it's just a play on your "set".

A key difference is that by using < (both in the "if" in the R-rule, and in "smallerthanhead" call) it's hardcoded to work for type number.

If I wanted (orderedlist X) where X could be anything, I can see 2 routes. . . 1 would be defining that X had to be of a closed set of types, whereupon a single hard function that matched on the type could perform the comparison.  The other would be to have it work on *any*thing; but I can't see how to do that without needing a datatype for each type you come up with, so that it can be written to use the right comparison function (e.g. perhaps with a macro that you expand once for each "type"?).  And that the alternatives may be unprovable, with no great way to tie the type of the container contents to a runtime comparison function. . . .

Just asking what the optimal approaches are to reuse the type and constraint work would be for something like this in order to make it a general-purpose container.

https://groups.google.com/d/msg/Qilang/D3tmhQvfnOE/fKgddlbhWxwJ  <-- I'm not sure if this 'groupoid' work was suggested as applicable to this or something else.

My code:  Hardwired for numbers.




(tc +)

(define smallerthanhead
        {number --> (list number) --> boolean}
        N [] -> true
        N [X | _] -> (< N X))


(datatype orderlist

   _____________
   [] : orderlist;

   X : number; Y : (orderlist & (biggerthan X));
   ===================================
   [X | Y] : (mode orderlist -);

   X : orderlist;
   _____________
   X : (list number);

   X : P; X : Q;
   ====================
   X : (mode (P & Q) -);

   ________________

   [] : (biggerthan X);

   if (> X Z)
   Y : (biggerthan Z);
   ______________________
   [X | Y] : (biggerthan Z);

   ______________________________________________
   (smallerthanhead X Y) : verified >> Y : (biggerthan X);)


(define inserth
   {number --> orderlist --> (list number) --> orderlist}
   N L [] -> [N | L] where (smallerthanhead N L)
   N L [RH | RT] -> (inserth RH [N | L] RT) where (smallerthanhead N L)
   N [H | T] R -> (inserth N T R) where (= N H)
   N [H | T] R -> (inserth N T [H | R]) )


(define insert
   {number --> orderlist --> orderlist}
   N L -> (inserth N L []))

(define union'
   \\ not efficient but works

   {orderlist --> orderlist --> orderlist}  
    [] S -> S
    [X | Y] S -> (union' Y (insert X S)))

(union' [1 3 5] [2 4 6])

[Mark Tarver]

That's really impressive; probably the most intricate piece of type theory anybody has posted here using Shen.

(14+) (union' [1 3 5] [2 4 6])

[1 2 3 4 5 6] : orderlist

Must have devoted much time to this.

Mark

[fuzzy wozzy]

Types or not, Shen's versatility (perhaps due to being functional with easy list notation?) allows someone who took a look at
the 15 minute tutorial to easily handle any problems from set theory of any kind any complexity. Present a challenging problem
 from the obscure corner of the set theory,if you will, and some newcomer will find a solution in a cinch and go,
"What else?"

[fuzzy wozzy]

Maybe this B-tree thing is so easy and trivial to do in Shen is why no one has bothered with it thus far,
showcasing notwithstanding.

[fuzzy wozzy]

ok I'll come up with B-tree code in Shen somehow. Maybe a week or two, maybe longer...

No fancy videos, just plain old ASCII, if successful. If I succeed, then it will persuade some
Shenturians as to Shen's showcase-worthiness. If not, they'll have to find other ways to persuade
themselves of something that's obvious to others.

[fuzzy wozzy]

If anyone has a nice algorithm that would make for a good starting point, I think.
Otherwise, it will be like reinveting the wheel, I guess.

[fuzzy wozzy]

I have a basic way in mind to show the b-tree as shown in the example video.

Insertion/deletion, but probably too simplistic a model (and no type) to barely get
a chuckle or two from Shenturians before they move on to more important things
of the day, I'm sure. 

[matt....@gmail.com]

Thanks.  I'm (very) slowly getting the hang of this.

When I finally got over the R-rule problem I was having (the big obstacle I kept trying to dodge around), I figured out how to make it parametric on the type and predicate (containers forced to < and numbers are of little interest to me).

The container consciously accepts and preserves duplicates, you can of course build an = out of < if uniqueness is required. . . .

Couple of test lines at the bottom demonstrating "union" against lists based on > and < ordering, and an insert call, just to show everything works.  There is nothing hardcoded to numbers but the test call inputs.



(tc +)


(datatype orderedcontainer


   _____________
   [] : (orderlist A C);

   X : A; Y : ((orderlist A C) & (goesafter X C));
   ===================================
   [X | Y] : (mode (orderlist A C) -);


   X : (orderlist A C);

   _____________
   X : (list A);

   X : P; X : Q;
   ====================
   X : (mode (P & Q) -);

   ________________

   [] : (goesafter X C);

   _________________________________
   goesbeforeorathead : ((A --> A --> boolean) --> A --> (list A) --> boolean);

   if (goesbeforeorathead C Z [X | Y])
   Y : (goesafter Z C);
   ______________________
   [X | Y] : (goesafter Z C);

   ______________________________________________
   (goesbeforeorathead C X Y) : verified >> Y : (goesafter X C);

   C : ((A --> (A --> boolean)) & CT); L : (orderlist A C);
   ========================================
   (@p C L) : (mode (orderedcontainer A CT) -);
)

(define goesbeforeorathead-h \\ keeps dupes
   {(A --> A --> boolean) --> A --> A --> boolean}
   F N X -> true where (F N X)
   F N X -> false where (F X N) \\ reverse
   _ _ _ -> true \\ must be equal - current design keeps dupes
   )

(define goesbeforeorathead \\ keeps dupes
        {(A --> A --> boolean) --> A --> (list A) --> boolean}
        _ N [] -> true
        F N [X | _] -> (goesbeforeorathead-h F N X))

(define inserth \\ third param is backlog
   {A --> (orderedcontainer A C) --> (list A) --> (orderedcontainer A C)}
   N (@p C L) [] -> (@p C [N | L]) where (goesbeforeorathead C N L)
   N (@p C L) [RH | RT] -> (inserth RH (@p C [N | L]) RT) where (goesbeforeorathead C N L)
   N (@p C [LH | LT]) R -> (inserth N (@p C LT) [LH | R]))

(define insert
   {A --> (orderedcontainer A C) --> (orderedcontainer A C)}

   N L -> (inserth N L []))

(define union' \\ can probably speed this up just
               \\ punching one list reversed direct into
           \\ inserth's accumulator/backlog
               \\ union' just here for demo interest though
   {(orderedcontainer A C) --> (orderedcontainer A C) --> (orderedcontainer A C)}
    (@p _ []) S -> S
    (@p C [X | Y]) S -> (union' (@p C Y) (insert X S)))

\\ Test smaller-than
(union' (@p < [10 30 50]) (@p < [20 40 60]))

\\ Test greater-than
(union' (@p > [50 30 10]) (@p > [60 40 20]))

\\ Just insert
(insert 45 (@p < [10 30 50]))

[fuzzy wozzy]

I think I'm mistaken.
Probably an algorithm as important as RBTree has been written in Shen already somewhere.
This thread is about how to do it in a type secure way.
That's something beyond me anyway.
Even if there is no library for RBTree in Shen, someone could write one up quick.
APL functions were known to be quicker to write one from scratch than use someone else's.

One thing I noticed from the video is that while the codes looked Greek to me, the verboseness
was comforting for some reason. And the sense of community around and behind Haskell libaries
was really nice, also. I don't have a clue what GADT stands for, but it sounds like something
important that could do some serious work if need be.

[fuzzy wozzy]

Shen would of course allow concepts and implementations of nodes, if one wanted to.
But the whole RBTree may fit into one single list, it seems (maybe of millions of depths/breadths, I don't know).
That may be the power and flexibility of Shen, who knows.
There are some one-liner B-Tree programs online, done in apl, python, java, what have you.
Probably not that unusual a thing, though I don't know about RBTree one-liners.
If you put the whole RBTree in one single list, then the list notation obviates the need for explicit nodes, I think.
(or can be thought to implicitly encompass/encapsulate the concept/implementation of nodes)
You still need a few more functions for calculation and such.

There was a question on this thread about if one does "insert/delete" on a tree how does one know for sure that
it's really done. If the tree is not too big then you can probably see the whole tree in one line and see for yourself that yes, it was inserted/deleted/recovered, or whatever.
If the tree has millions of depths or millions of breadths then you could use "from" function that was used in other discussions,
which is really just doing (hd (tl (tl...))) until the element you wish to retrieve or look at has been reached. But to save any changes
on a permanent basis you have to go deeper than Shen, to save an image, I once heard.

There's probably a million ways to do RBTree in Shen, and maybe eventually people will have done them all.
But some of that energy could've been used for some other project maybe.
That's why other languages have a hub site for gathering all newly developed libraries, maybe.

[Mark Tarver]

I think it is in the standard test suite I use for making sure that releases are OK.   If you download the Shen sources look in the Test Programs directory; Justin Grant comes to mind as the author.

Mark

[Ramil Farkhshatov]

fuzzy wozzy <swtch...@gmail.com> wrote:

> That's why other languages have a hub site for gathering all newly
> developed libraries, maybe.

I could totally miss the point but there is

http://shenlanguage.org/library.html

and

https://github.com/vasil-sd/shen-libs

But they're slightly harder to find than I expected.

[Mark Tarver]

cool - do you need

_____________________________________________________________

   goesbeforeorathead : ((A --> A --> boolean) --> A --> (list A) --> boolean);

You seem to have proved it.

mark

--
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 http://groups.google.com/group/qilang.
For more options, visit https://groups.google.com/d/optout.

[fuzzy wozzy]

Yes. It's in the test programs folder. But no deletion, only insertion.

 Thank you for the links to the Shen library.

You can put nested empty lists in Shen REPL, [[[]]], up to about 9000 nested lists,
before reaching stack overflow.
So maybe that might be the depth limit, or less if the lists aren't empty.
And using lists allows for RBTree with numbers, alphabets, words, sentences,
special symbols, etc (with simple workarounds).
And you could have a separate list that keeps track of node values that were deleted,
even several times, to undo and restore original value/values later as the user wishes.

To make nodes implicit using nested lists, if some pseudonodes look like this,

                [a      f]
               /           \
       [b c d e]      [g h i]

It can be put into a list form such as,

[[a f] [[b c d e] [g h ]]].

 

 

[willi riha]

just a test; I'm having problems

Willi

[Willi Riha]

Fuzzy wozzy's enthusiasm about Shen and its virtues is unique!

Like Mark, I sometimes wonder what his examples are all about, what insight they should give us about the strenghts  (or the deficiencies?) of Shen.

Fuzzy wozzy has admitted in one of his postings that he is not a programmer. It would appear though that he is an advanced student of data structures, at least as knowledgable as a graduate in Computer Science. Maybe not!?
He is talking about B-trees - a very sophisticated data structure which is not easy to implement in any language. I rather believe that he is referring to ordinary, mundane, binary trees - easy to implement, but practially not very useful.
I remember, many years ago, in the 90's when I was still teaching, I set as an assignment the implementation of B-trees. Not many students could do it, and I have to confess that I found it very hard too.

Just in case, readers are not familiar with B-trees, I quote

B-tree

From Wikipedia, the free encyclopedia

Not to be confused with Binary tree. In computer science, a B-tree is a tree data structure that keeps data sorted and allows searches, sequential access, insertions, and deletions in logarithmic time. The B-tree is a generalization of a binary search tree in that a node can have more than two children (Comer 1979, p. 123). Unlike self-balancing binary search trees, the B-tree is optimized for systems that read and write large blocks of data.

Read the full article at http://en.wikipedia.org/wiki/B-tree

While I was trying to post this message, fuzzy wozzy has mentioned RB-trees, again not trivial to implement in any language.

Good luck - fuzzy wozzy!

Willi

[fuzzy wozzy]

I always thought that this forum felt incomplete without the presence of regular contributors.

So it's nice to have a feedback from regular contributors, if only every now and again.
Maybe this is what I meant by a sense of community that's heavily present in Haskell and other forums.

Of course binary tree structures are the simplest possible, then red-black trees and other unbalanced trees
with more than two children in child nodes are more generalized forms.
But unless there's a function that cannot be emulated in Shen (simple functions, since I do not know how to do macros)
and within the limits of stack overflows, I don't think it's an issue as to how many children can be in nodes and how unbalanced
a tree is, or whatever unique and different algorithms may be used (since people come up with new algorithms all the time, for
red-black trees, for example).

[fuzzy wozzy]

I wish I could say I'm as knowledgeable as computer science students, all without formal training.
But it's not me, it's Shen, made to be easy to use even for 10 year old (this was one of Dr. Tarver's goal of making Shen).
Shen is like Logo, easy to use for 10 year olds, but powerful enough to do advanced programming with.
I didn't know how binary tree structure worked but I saw a couple of tutorial videos online this weekend,
and while it was boring, it was educational. I haven't watched any of the RBTree tutorials yet, they look a bit more involved.
But it's just a generalization of binary trees, so it's like if you know that (+ 2 3)=5, then you can figure out what (+ 2 3 5) is.
If you don't want to give me credit that I might be able to deduce what (+ 2 3 5) is from knowing that (+ 2 3)=5, that's fine too.
Anyway, I showed in the previous post how the tree structure can be written as a single list with nested inner lists, and that's
probably enough for Shenturians to make their own RBTree programs in minutes. If not, I would be surprised.

RBTrees are for more sophisticated tree structures to be sure, and Shen can probably do more than the conventional 2-3 trees
or 2-3-4 trees easily, but it's not true that the ordinary binary trees are not good for complicated data structures, at least not
when it comes to Shen, because you could search/retrieve an element "b" from some node and most programs would stop at that,
but if you're doing Shen and that "b" happens to be a function, (define b -> [list of millions of data]), then you have yet another
level of complex data structure to query upon.

With Shen, each node can be a single number, a single letter, a character, a symbole, words, sentences, paragraphs,
 a whole book (keeping in mind that one list takes about 20 million or so single elements before stack overflow)
or any combination of them, and will work without a doubt, yes, even for ordinary binary trees or red-black trees,
or any other trees whose algorithms are not yet devised.

Even though Shen can do without explicit nodes and such, it would be good to understand them to follow the Haskell code in the video.
Datatypes are not going away anytime soon, in fact they're becoming more in demand as evidenced by all the newly emerging languages
using them if only as a safety measure for extra caution.

[Matthew Lamari]

Oh yeah - I added that just before pasting it to the list thinking I had
to after moving the function definition from above the datatype to below.

"You can take the boy out of C; but you can't take the C out of the boy"
haha.

[Matthew Lamari]

Immutable B-Tree (the Bracknell) or RBTree (what I would attempt)
algorithms can be represented in any language and form the basis for
some core-library sets and maps.

They are represented everywhere. I've done it myself.

Without pattern matching you have to if-storm from some reference
Haskell or ML version from running code or the Okasaki book, with near
certainty of botching up "Delete". *With* pattern matching, you may get
it right. But you won't know, you'd just play with it for a while and
observe it working properly over time.

Many people look at any given language from different perspectives that
impacts what they may want to or can get from a demo. I come heavily
biased to the practical side, "what can I get that helps me write big
programs".

The value, to me, of a small demo is to impart tools demonstrated in
context that you can apply to your own problems. The video I pasted
here months back showed how to use the haskell type-system to constrain
his B-Tree program, via GADTs, into assisting him in writing a very
troublesome algorithm, using machine assistance in place of having to
run the scenarios through his head.

The value of the exercise in that video wasn't ending up with the B-Tree
implementation but in seeing how to get the compiler to assist you in
obtaining one, and thus a different program.

From experience, having a immutable <Key,Value> store is immeasurably
valuable - so having one available to your wider program would be
useful, even if typed in out of a book in (tc -). But it would also be
a useful exercise (in Shen or something dependently typed) to see how
much the compiler and type-work (type checked) can assist in enforcing a
correct implementation of insert and delete, and perhaps to see how much
its type properties could extend automatically to end-users of the
container.

The former (un-type-checked implementation of RBTree with its insert and
delete) could be punched in out of a book faster than I could write this
email, and it would be practically useful in the first sense, although
no different to what you could punch in in (pre-GADT) Haskell, or any
given ML.

But that would have nothing to do with what I was talking about in
opening this thread.

[fuzzy wozzy]

I'm not considering types so that's probably a major part of this that makes it tough.
Types are important, of course, but since red-black tree is basically about comparing numbers,
rotating to match the color requirements, I'm unsure why the types come into play so much
other than of course to show that it can be done and as an intellectual exercise, as well as ensuring
type safeness for the program itself. I was thinking also that "(Key Value)" has other important functions
it can perform besides just for insertion/deletion. Even with the tree being represented as a single list
of inner nested lists, (Key Value) for any particular node can be obtained, it's hidden away, ready for use.

The video example shows what I think is a red-black tree code in Haskell, so I know it can be done in
many languages.  Is there a short program in any language that you can show, maybe even re-written in Shen?
(with/wthout nodes/types)

I think the post got lost where I was showing how a tree can be shown as a list of nested inner lists, so I'll give
brief example here,
                    
                         [4 30]
                        /         \
                    [2 4]      [22 30]

can be shown as, [[4 30] [[2 4][22 30]]]

[fuzzy wozzy]

What is the reason you're not confident that delete will delete and insert will insert?

And why does GADT work this way?

[fuzzy wozzy]

http://frenchy64.github.io/2013/10/02/rbt-tree-preview.html

The author of the above website chose red-black tree for his first project using Typed Closure.
He's now been seeking crowdfunding for 12 months of full time development on Typed Closure since October last year.
So whoever suggested typed red-black tree as a way to showcase Shen was correct.
It is, at the very least, worthy of one-year crowdfunding request.
Typed Closure was able to solve red-black tree in milliseconds.
It's not for me, but maybe for the experienced hardcore Shenturians.

[Mark Tarver]

Right, thankfully my connection is restored - I hope.  Bills, bills and more bills :(.

OK; generally some of what you are trying to do here depends on the implicit connection between the variables in the pattern and the variables in the type.  In TBoS no such connection is assumed; i.e.if you have a variable in the signature inside {....} and you happen to use the same variable in the body of the function then this is treated as a mere accident.

In logical terms when you place a variable in a type,it is a shorthand for a universally quantified variable.  So T* is effectively treating quantifiers as either restricted to terms or types.  It is easy to extend the treatment to obviate this by tweaking one piece of code. However I was uncertain about the consequences of this change and so I left it out of the standard though at one point I included it in the code as an experiment.  I think Dmitry used it.  I tend to be cautious about making extensions to the logic of the system,even if they seem intuitive.  It is so easy to make an error which seems intuitively sound.  For this reason proofs are always important. Frege's disaster with Axiom V is an illustration.  Poor guy never recovered from his mistake.

I'll tell you a true story about this in the development of Qi. Long ago I was teaching an early version of my work which used a different type system and included a rule which I felt doubts over.  Despite my misgivings I could not find a counterinstance.  At the time I was dating a healer who used dowsing and I jokingly said 'Can you dowse for the correctness of an axiom set?'and she said'I'll have a go'.  She did and said 'It's wrong'.   So I fell to thinking and deep in thought crossing the park, spotted the counterinstance and entered it into the computer- sure enough it malfunctioned.  I felt a sort of triumph. 

I replaced the faulty rule by the current one.  It was at this point I recognised the importance of formal proof and began to sketch out the correctness proof of the system - the proof that you can find in TBoS.   But uncertain of making a mistake, I wrote to Barendregt in Holland, perhaps the leading theorist in lambda calculus, on this very point.  He did not deliver a judgement, but instead referred me to a senior figure at Imperial College who had done the most work in that area.

This senior figure was a professor (I omit his name) and I wrote to him, sketching my problem and offering the solution I had formulated. He wrote back to me saying that my solution was still wrong and he had the only definitive solution worked out in the early '90s which was in a published paper. I was pleased and asked for his formulation. And lo! He sent me my original faulty axiom.

I then sent him the counterinstance. He struggled with it and went completely silent.  Finally after a few days,he wrote back,a rather disjointed letter admitting his version was wrong and effectively bidding me good luck.   It was then that I returned to my own work and completed the correctness proof and that system now powers Shen.   

I think the story is a good example of why it is important to be cautious and humble in this sort of work.  The God of mathematics punishes hubris and carelessness of all kinds. I don't know whether the professor retracted his paper or went back over his theorems to see if they still followed from the revised version.  It is quite possible that there is now a body of work out there based on a false axiom system. I kept his name private and was not interested in making capital from his mistake - which was mine at one point. 

Back to Shen. If you want to reinstate the connection between pattern variables in the function and type variables in the signature, you can do it in one line in t-star.shen.  

X -> (concat &&& X)        where (variable? X)

replace &&& by &&. But bear in mind, this is experimental and the usual disclaimers apply.

Re your program, I'm a bit lost as to what you are doing.  Your 'containers' are lists of objects that satisfy integrity constraints and carry those constraints with them. Is that right?

Mark 

[Samuel Chase]

Wow. That's a wonderful story Dr. Tarver.

[Matthew Lamari]

I think what you're asking about containers is what I meant. The
constraint is on the items in the container, and the relationship
between them. My difficulties in practice have been it matching back
from patterns that contain the constraint (e.g. the (@p < [1 2 3]) form)
and the type-work bearing that constraint. I don't assert that I've
been trying to do it correctly, that it can be done correctly, nor even
that it is worth attempting however.

[Matthew Lamari]

My responding under this (old RBTree) thread in the group may have
cluttered things. I put the "container/list" code here only in response
to your set example.

The part you responded to - I mentioned that an RBTree example under (tc
-) would not be much of a demo. This doesn't mean a good (tc +) version
could exist, nor that I could write it.

The other is sharing my attempts to understand type and what is provable
using a spinoff of the "set" that you provided, and I think you're
addressing in part in your response.

I'm under no illusion that the "orderedcontainer" experiment is doing
anything right or valid, nor is headed toward anything provable, there
is no caution but let me assure you there is humility (I know I'm
clueless). I will be processing your answer further over the next day
or so. That there isn't some minor language syntax I'm missing but that
the premise of it is itself headed off into the weeds is a useful hint.

To the specific middle goal I was aiming for with the "container" code -
to explore the degree to which the type system could aid with or
constrain the operators against data objects both in their
implementations and to impose constraints upon their users.

The "orderedcontainer" that I presented was not able to statically
constrain the callers of union' to providing the same ordering of list
for both parameters.

On 8/27/2014 8:06 AM, Mark Tarver wrote:

[Artella Coding]

"So T* is effectively treating quantifiers as either restricted to terms or types.  It is easy to extend the treatment to obviate this by tweaking one piece of code."

But is it really possible to have variables crossing the term-type boundary in shen?, given the fact when shen compiles down to klambda type information is erased (klambda is typeless)? (Not sure if I am misinterpreting what you mean by quantifier). You could I guess apply the same argument to other languages since ultimately everything compiles down to assembly which itself is typeless, so there must be something I am missing....

[fuzzy wozzy]

Maybe the senior professor would be delighted to know that the faulty axiom has now been corrected and has proven
to be correct enough to run a powerful language called Shen and maybe the professor might even contribute his own
musings on Shen. Formal proofs and presentations are wonderful. Quick and dirty that does the job are also wonderful.

 

[Artella Coding]

There is also a nice explanation of quantifiers here : https://groups.google.com/d/msg/qilang/hFIBTmJwnb8/tUSEdMdnwTYJ

On Wednesday, August 27, 2014 2:06:06 PM UTC+1, Mark Tarver wrote:

[Mark Tarver]

Well all this stuff takes place above KLambda.  This is about working with dependent types.

There is a kind of asymmetry between the power of sequent calculus to express types (virtually unlimited) and the power of T* to compute with them (limited) because T* was designed for automatic verification and makes certain assumptions to do so.  A solution would be to be able to integrate some form of interactive system which would take Shen into the area of formal methods.   This would make it comparable with Coq etc.

Mark