This bush datatype from the Nested Datatypes paper

[alpha...@orange.fr]

Merry Christmas to you Shen hackers,

I have this bush datatype from the Nested Datatypes paper by Richard Bird & Lambert Meertens.
https://www.cs.ox.ac.uk/richard.bird/online/BirdMeertens98Nested.pdf

(tc +)

(datatype bush
   ______________
   [] : (bush A);
 
   H : A; T : (bush (bush A));
   ===========================
   [H | T] : (bush A);)

(define bush-example
   {--> (bush number)}
   ->
   [ 4
   [ 8 [5] [[3]] ]
   [ [7] [] [[[7]]] ]
   [ [ [] [[0]] ] ] ])

Until here everything and more is OK.
But now i want to access the datatype members via an index.
My best try is :

/* an index is a path from the root to a member */
(datatype bush-index
   __________________________
   bush-z : (bush-index Z Z);

   I : (bush-index A Z);
   ========================================
   (@p bush-h I) : (bush-index (bush A) Z);

   I : (bush-index (bush A) Z);
   ================================
   (@p bush-t I) : (bush-index A Z);)

(define bush-member
   {(bush-index A Z) --> (bush A) --> Z}
    _ [] -> (error "bush-member : index out of bounds")
       bush-z    [A|ABB] -> A
   (@p bush-h I) [A|ABB] -> (bush-member I A)
   (@p bush-t I) [A|ABB] -> (bush-member I ABB))

The interaction i expect is :  
   
(bush-member bush-z (bush-example))
4 : number

(bush-member (@p bush-t bush-z) (bush-example))
[ 8 [5] [[3]] ] : (bush number)

(bush-member (@p bush-t (@p bush-h bush-z)) (bush-example))
8 : number

Can you help me, please ?

Thanks

- damien

[Mark Tarver]

Just got up to steam my head - as one does ;).

I've looked at your solution; but haven't looked at the paper (not since a couple of months ago).  I guess your bush of As is a list structure whose ultimate elements are As.  That is, if you flatten a bush of As you get a list of As.

I think it is useful to begin with a more general data structure we'll call a mass.  A bush in the above terms is a special case of a mass which is a list structure.

(datatype mass
   
   [X | Y] : (list (mass A));
   ==========================
   [X | Y] : (- (mass A));
   
   X : (mass A) >> P;
   __________________________
   X : (- (list (mass A))) >> P;
   
   ______________
   [] : (mass A);
   
   X : A;
   ______
   X : (- (mass A));)

4 is a mass of numbers and so is [4].   A bush is then a limiting case.

(datatype bush

  [X | Y] : (mass A);
  ===================
  [X | Y] : (- (bush A));)

 What you are looking for, I think, is a way of searching a bush using a series of navigating commands.

We can use h for head and t for tail.   Here is a script.

(2+) (define bush-example

   {--> (bush number)}
   ->
   [ 4
   [ 8 [5] [[3]] ]
   [ [7] [] [[[7]]] ]
   [ [ [] [[0]] ] ] ])

(fn bush-example) : (--> (bush number))

(3+) (define search-bush
  {(bush A) --> (list symbol) --> (mass A)}
   [X | _] [h] -> X
   [_ | Y] [t] -> Y
   [[X | Y] | _] [h | Search] -> (search-bush [X | Y] Search)
   [_ Y | Z] [t | Search] -> (search-bush [Y | Z] Search))
(fn search-bush) : ((bush A) --> ((list symbol) --> (mass A)))

(4+) (search-bush (bush-example) [h])
4 : (mass number)

(5+) (search-bush (bush-example) [t h])
[8 [5] [[3]]] : (mass number)

(6+) (search-bush (bush-example) [t h h])
8 : (mass number)

Right, back to bed.

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 view this discussion on the web, visit https://groups.google.com/d/msgid/qilang/00f21e42-c2d4-4e79-8cf2-7af1a5e35b47n%40googlegroups.com.

[alpha...@orange.fr]

Good morning Mark,

Your solution is much more than what i expected.
My hint is you have to publish this mass datatype along with mass-map, mass-fold, mass-size, mass sum, mass-member. Then Haskell-ers and ML-ers have to push their limiting Generalized Algebraic Data Type until they give up and surrender to Shen.

Regards,

- damien

[nha...@gmail.com]

Wasn't there another post about this nested datatype?

[Mark Tarver]

On Wed, Dec 28, 2022 at 10:53 AM alpha...@orange.fr <alpha...@orange.fr> wrote:

Good morning Mark,

Your solution is much more than what i expected.
My hint is you have to publish this mass datatype along with mass-map, mass-fold, mass-size, mass sum, mass-member. Then Haskell-ers and ML-ers have to push their limiting Generalized Algebraic Data Type until they give up and surrender to Shen.

Regards,

- damien

People generally never give up on their programming languages; a program may do the equivalent of their partner turning up drunk at 2 a.m. and being

sick on the carpet because of language limitations but they'll excuse it because they've invested a lot of effort in mastering it.   And like the old man on the 

mountain I live up here in the Shen  group. 

Regarding mass-map, masses are rather heterogeneous objects and the most natural object for mapping are the non-list elements inside the mass.

This is generally called walking rather than mapping.   To define this function we need to isolate these elements.

We extend the type mass by an extra rule (in red).

(datatype mass
   
   [X | Y] : (list (mass A));
   ==================

   [X | Y] : (- (mass A));
   
   X : (mass A) >> P;
   _____________________

   X : (- (list (mass A))) >> P;
   
   ______________
   [] : (mass A);
   
   X : A;
   ______
   X : (- (mass A));
   

   (not (list? X)) : verified, X : A >> P;
   ___________________________________
   (not (list? X)) : verified, X : (mass A) >> P;)

We define your example and use mass instead of bush.

(define bush-example
   {--> (mass number)}

   ->
   [ 4
   [ 8 [5] [[3]] ]
   [ [7] [] [[[7]]] ]
   [ [ [] [[0]] ] ] ])

Here is walk

(define walk
  {(A --> B) --> (mass A) --> (mass B)}
   F X      -> (F X)    where (not (list? X))
   _ []       -> []
   F [X | Y]  -> [(walk F X) | (map (/. Z (walk F Z)) Y)])  
   
(define list?
  {A --> boolean}
   X -> (or (empty? X) (cons? X)))

Here is an application.

(22+) (walk (+ 1) (bush-example))
[5 [9 [6] [[4]]] [[8] [] [[[8]]]] [[[] [[1]]]]] : (mass number)

Mark

[Mark Tarver]

There was and I gave a different answer based I think on the paper.

The answers here are based on a more direct reading of what (I think)

alpha is trying to do here.

Mark

[Mark Tarver]

I think we have a private chat on this.  I could indeed drop into the Haskell group and hit them with the mass datatype

and ask them something like 'Can you do this?'.  It will inevitably infuriate them if the answer is likely 'no' and for some

reason any programming group X hates questions of the form 'Comparing X to Y'.  They get defensive about their beloved X.

Even worse if it is the dreaded Tarver whose interest in Haskell is not that great and whose attitudes to academia are

summed up in Cromwell's assessment of parliament.  Might I suggest that somebody who is used to posting to that

group as yourself would find a better reception.

This goes to all here.   Take what you learn here and use it to teach others.

Mark