{'fraction_non_alphanumeric': 0.03653941849719201, 'fraction_numerical': 0.0036255065045851993, 'mean_word_length': 4.549973698053656, 'pattern_counts': {'":': 0, '<': 0, '<?xml version=': 0, '>': 1, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 2, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
Truly Visual Polymorphic Algebraic Data Structures through Maramafication

This paper presents a so-called maramafication of an essential part of functional programming languages such as Haskell or Clean: the construction of fully polymorphic well-typed algebraic data structures based on type definitions with at most one type parameter. As such, this work extends our previous work, in which only a very limited form of polymorphism was present. Maramafication means the design of visual 'twins' of existing programming constructs using spatial metaphors rooted in common sense or inborn spatial intuition, to achieve self-explanatoriness. This is, among others, useful to considerably reduce the gap between programmers and non-programmers in the creation of programs, for educational purposes, for inclusion of non-typical programmers and for invoking enthusiasm among non-programmers.


Introduction
It would be highly beneficial if non-programmers could co-program software applications. The Marama-paradigm, as introduced in previous work, is a paradigm that is intended to considerably reduce the gap between programmers and non-programmers. The basis of the Marama-paradigm consists of designing 'twins' of programming constructs using metaphors rooted in common sense or inborn intuition, making the constructs almost entirely self-explanatory. This work has coined the term internal semantics for this purpose: the semantics of constructs is evident without an external definition. This may lower the threshold for non-programmer participation. Other application areas of maramafication include education and fostering an inclusive society. For example, some dyslexics may have a latent talent for programming that never surfaces in a world dominated by textual programming languages. Some authors have argued that these people would be a great asset to the programmer's community, because they believe there is a correlation between dyslexia and the capability to think more creatively than the average. This work coins the term maramafication for this design process. In other words, if such a twin has been designed for a language construct from for example Clean [1] or Haskell [3], it has been 'maramafied'. In the remainder of this article, the prefix 'M-' indicates 'maramafied', for example, an M-constructor, is a maramafied constructor.
Related work, among others in the field of visual general purpose programming languages, to the best of our knowledge, does not truly and fully employ this principle of internal semantics. Note that visualisation itself is not equal to having an internal semantics. Many 'visual' constructs occurring in visual programming languages are not self-explanatory. What is more, most of such languages do not even visualise most of the programming constructs. They are still 'contaminated' with many constructs of a textual nature. Typically, in such programming languages the truly 'visual' part consists of boxes connected with arrows, while the content of the boxes contains much textually expressed programming code, such as textually defined typing information and data-structures. Hence, these languages require the user to still largely move within the original not-so-accessible textual programming paradigm. The hardest parts to truly capture with internal semantics are, possibly unconsciously, left in a textual form. In this article, however, we cover such a hard and nontrivial part.
This paper focusses on a fragment of the 'maramafication-challenge': it presents a new way to (truly) visually represent fully polymorphic algebraic data structures (ADSs) as they occur in modern functional programming languages, and does so in line with the aforementioned paradigm. The design is modular: it can be adopted straightforwardly into any visual functional programming language.
ADSs are designed in such a way that type consistency is entirely forced by the form of the M-constructs (maramafied constructs). In other words, a user of these constructs cannot create ill-typed values, simply because the 'pieces will not fit'. In this sense, the approach in this paper is genuinely visual: the semantics of the visual blocks is embodied by their visual structure and spatial manipulation options, and does not require a definition by textual or spoken means. Hence, a beginner using the M-constructs can find out how to program with them, without any prior textual or spoken explanation about how these constructs work.
Another way to phrase it, is that the semantics of the visualisation of polymorphy and datastructures proposed in this paper solely relies on shared human intuition for manipulation of 3D objects.
In this article, the term spatial necessity is coined for the aforementioned property of the visual designs, the property that given the laws of mechanics (as far as they are intuitively understood by the majority of humans) it is only possible to construct something that is correct. An example of such a widely shared intuition on which the spatial necessity design paradigm can rely, is that most people from an already very young age will predict that a ball that is held in the air, and then let lose, will move downward.
The design covers ADSs based on algebraic data type definitions with at most one type-parameter (but is easily extensible with any number of typeparameters), can cope with polymorphic constructors, and can classify a given ADS polymorphically (through 'typing statements').
Section 2 presents the textual languages used to show the textual equivalences of the M-constructs. Section 5 introduces a predecessor to this work: Madawipol-α: a maramafication of M-constructors that is already sufficiently expressive to deal adequately with recursively defined types [2]. However, Madawipol-α does not yet support full parametric polymorphism. Section 5 introduces Madawipol-β, an adaptation of Madawipol-α that adds parametric polymorphism. Section 6 provides definitions of essential aspects of Madawipolα.
It is important to note that this paper explains the constructs primarily from the perspective of a programming language designer, the targeted readers of this article. The reader has to keep in mind that the targeted users of the language, however, will learn how the constructs work by a playful and wordless exposure to maramafied ADSs or parts thereof only. No textual explanations will be provided. Moreover, the users of the language will use an interactive 3D-editor. The static representation in this article, therefore, required some alternative ways to represent aspects of the design. It is important that the reader does not confuse these with the actual, and more 'intuitive', way the language will occur to the user.

Textual languages
This section presents the textual languages that are used in this article to show the textual equivalences of the M-constructs presented in this paper. Because the M-constructs covered in this paper only deal with a fragment of a modern functional programming language (FPL) such as Clean or Haskell, this article also defines a textual language that is (isomorphic to) the relevant fragment of such an FPL. The language is called Algepoly1. We suffice with introducing the textual languages by example, their semantics as identical to the corresponding parts of Clean.

Algepoly1
Example 1 (Algebraic Data Type Definitions). The following Algebraic Data Type Definitions define a number of algebraic data types: Note that this paper does not cover a visual counterpart to algebraic data type definitions. However, it is important to include them in the textual language for explanatory and definitory purposes.
In this paper it is important to be able to talk about algebraic data structures that are still under construction. For this purpose, we add the following construction. The ' ' stands for an 'empty spot'. Such an ' ' may only occur at the argumentposition of a constructor application.
This paper also deals with polymorphic constructors. These normally do not occur in languages such as Clean as 'stand-alone' constructors. To be able to talk about them in isolation, Algepoly1 contains the following constructs. is in a spoken phrase expressed as "the 'Cons' of 'List Bool'.". Such a statement only makes sense in the context of an algebraic data type definition, in which the constructor has been defined. Lets assume that this algebraic data type definition is the one in example 1. Then this statement expresses that 'Cons' is the constructor that one would get by substituting 'Bool' for the typeparameter in the given algebraic data type definition. In this case that would be the 'Cons' with the following type: 'Bool (List Bool) -> List Bool'. Another way to phrase it, is that it is the instance of 'Cons' with result-type 'List Bool'.
Another instance of 'Cons' is "the 'Cons' of 'List (List a)'." This instance of 'Cons' is, clearly, polymorphic.

Algepoly1 +
For didactic purposes, it turned out to be useful to introduce a slight extension of the language Algepoly1: Algepoly1 + (the '+' stands for 'too flexible'). It allows constructors to have any type, including the most general polymorphic result-type 'a' and non-polymorphic argument-types, or no results or arguments at all. (Hence, they are reminiscent of generalised algebraic data types [7].) Note that the language itself is not intended for use in a real language. It is 'too flexible' and would lead to type-technical and semantical difficulties. It serves as a way to create 'minimal examples' to demonstrate certain behaviours of M-constructors. Note that the notation of the type is written down in the opposite order of what is commonly used, which one can witness by the reversed direction of the arrow. The result type is written down first, then the arrow follows, and finally the argument types are provided. This has been done for convenience: the result and the arguments are now in the same order as they appear when the constructor is applied, both in the textual version as in the maramafied version.
The following defines Algepoly1 + by means of examples.
Example 5. The following definition:  Madawipol-α, created in our previous work, is a maramafication that covers ADSs based on algebraic data type definitions with at most one type parameter, and can cope with a limited form of polymorphic constructors: those without arguments [2]. This section suffices with defining Madawipol-α by example, among other due to space limitations, but also because the successor Madawipolβ is the focus of this paper. For an elaborate formal definition of Madawipol-α, see [2]. Throughout the online version of this document, clicking any image shows an online high resolution version of it, which can be zoomed into. The reader is strongly recommended to follow these links to investigate the figures in much more detail. The same holds for many textual descriptions. For off-line readers there is an additional 'appendix'-document that contains an enlarged version of each figure, either to print or to store locally. It is available from the same location as this article. Figure 1 shows examples of the simplest possible ADSs: atomic ADSs. In particular, note the form of the joints. The values of type 'Bool' have the same joint-form, while 'Sat' has another. Every type-constructor has a unique form associated with it, its type-constructor form. In this case, 'Bool' corresponds with the triangle in the figure, and 'WeekendDay' with the pentagon in the figure. (The type-constructor forms have to comply with some additional conditions, these are covered in [2].) The square form around them is not explicitly part of the type. It is the alignment square, needed to align joints correctly when fitting them together. To provide examples of molecular ADSs (ADSs with constructors that take arguments), fig. 2 introduces all M-constructors that belong to the type 'List Bool' and 'List (List Bool)'. Note that Madawipol-α does not yet support polymorphism for constructors with arguments. Therefore, it can only provide non-polymorphic instantiations of 'Cons'. M-Nil, however, is polymorphic. (Note that "M-Nil" is an example of the notation of specific M-constructors.) Hence, it can be shared among the different instantiations of 'Cons'. This explains why there is only one M-Nil in fig. 2.
Note the forms of the three joints of M-Cons:[List Bool]. It has one male joint, that corresponds with the result-type 'List Bool', and two female joints, one corresponding to the type 'Bool', and the other to 'List Bool'. The circle corresponds with the type-constructor 'List'. It is an essential aspect of the design that joint-forms that correspond with a complex type, such as 'List Bool', are compositionally related to their textual form. The 2D projection of the joint-form along a line perpendicular to the bottom of the joint, is called the type-form. I.e. it is the 2D form one sees when viewing a joint along a line of sight that is perpendicular to the bottom of the joint. This is an adequate abstraction. After all, if one assumes that male and female joints have matching heights and depths, the only aspect that determines whether they fit is the typeform. The textual type can be read from the type-form by starting with the outermost form (skipping the alignment square) and then walking one's way to the adjacent one, all the way down to the center form, while reading out loud the type-constructor that is associated with each form. The reader is invited to verify that all joints of M-Cons:[List (List Bool)] also comply with this structure. A polymorphic type, such as 'List a', is created by leaving the space within the innermost type-constructor form empty. The joint of M-Nil is an example.
Also  Madawipol-α is type-safe. Figure 4 gives a simple example. The power of Madawipol-α however, lies in how it enforces type-safety of more complex types, such as types that consist of more than one type-constructor, polymorphic types, and recursively defined types. This is the non-trivial part of the design. With the compositional translation of textual types into type-forms, as illustrated in the aforementioned, every type can be translated into a type-form that behaves type-safely, and that reflects the relation between both. We challenge the reader to create a type-incorrect value with the M-constructors provided so far.

Polymorphic surfaces
A part of Madawipol-β consists of so called polymorphic surfaces. These surfaces do not exist as independent objects within Madawipol-β, but are, among other things, integrated into polymorphic M-constructors. However, for clarity this section explains the polymorphic surfaces in isolation. The most central part of the explanations focus on the laws that govern the behaviour of the polymorphic surfaces. The reader is recommended to first try to guess what happens in the figures, and after that read the accompanying explanation. Figure 5 shows a gray surface in the center of which a polymorphic surface polSurf is attached. (Note that the figure has to be read as a comic strip.) polSurf has a side with a red colour (in the figure at the top-side) and a side with a blue colour (in the figure at the bottom-side). To demonstrate the behaviour of polSurf , a gray cylinder C is moved into it. As can be seen in the figure, the part of C that touches polSurf moves downwards with the cylinder. The part that is not touched by C, however, moves in the opposite direction over the same distance. polSurf does not tear in the process, and remains attached to the gray surface. In that sense it behaves as an elastic surface.   : Two pairs of polymorphic surfaces, interacting with a cylinder, seen from three perspectives. Each pair is connected to one, separate object. Figure 8 shows two polymorphic surfaces. polSurf 1 (left) and polSurf 2 (right). polSurf 1 's orientation is the opposite of polSurf 2 . One can derive this from the orientation of the colours: in polSurf 1 , red is on top, in polSurf 2 it is on the bottom. polSurf 2 mimics the behaviour of polSurf 1 , and because of its orientation, the movement is also reversed with respect to the gray surface. Note that this figure is a natural consequence of the laws already exposed in previous figures. It does not introduce any new laws, but is included for clarity.

Differentiation of polymorphic surfaces
Some terminology is needed for explanations in the rest of this article. If a polymorphic surface is fully deformed it is differentiated. The opposite notion is 'undifferentiated '. A polymorphic surface always starts in a fully undifferentiated state: a perfectly flat surface as indicated in the examples before. A polymorphic surface can also be partially differentiated, as will be shown in later examples. The parts of a polymorphic surface that are differentiated are called differentiated regions. The opposite notion is 'differentiated region'. A part of a polymorphic surface that is differentiated as a consequence of mimicking another surface, is called a mimicking region.
If a region of a polymorphic surface is not mimicking another surface, nor being deformed by an object that is pushed into it then that region is called a free region. In the examples provided so far, each polymorphic surface started out as a completely free region, while no free regions were left once insertion of an object started. Note that the region of the polymorphic surface that moves in the opposite direction of the regions being touched by the inserted object, is not a free region either: although it does not touch the inserted object it is clearly being deformed.

Law: mimicking regions are rigid
A law that is not demonstrated in this article is that mimicking regions of a polymorphic surface behave like rigid (non-deformable) forms with respect to the objects onto which it exerts a force. As a consequence, if such a mimicking region exerts a force onto an undifferentiated region of another polymorphic surface, the latter will start to deform as well and become differentiated. Another consequence is that if the other surface is already differentiated, and does not have a matching form, the forms will not fit into each other and movement will halt.

Law: free regions return to an undifferentiated state
All examples provided thus far, also work in the reverse direction. When objects are taken out again, the polymorphic surfaces move back to their original position. These examples can simply be obtained by reading the comic strips in the reverse order. The underlying law is formulated as follows: free regions return to their undifferentiated state. In other words: any region of a polymorphic surface that is not being pushed by a shape, nor mimicking another surface, returns to its undifferentiated state.

Experimentation
Note that a quite extensive experimental study has been carried out to test the understandability of the laws mentioned in this section among secondary school students with promising results. For clarity, in some of the following examples the correspondence between parts of the visual and the textual representation is shown. It is essential to note that these are not put there for definitory purposes: for a user of Madawipol-β the semantics is contained in the construction possibilities of the building blocks. The correspondence is merely put here to provide the reader of this paper, who is probably well-versed in textual functional languages, a quick insight into the fact that these visualisations indeed exhibit the same relevant behaviours as their textual counterparts.
The essential building block of the extension is formed by polymorphic surfaces, covered in section 4.
In Madawipol-β, polymorphic surfaces are part of polymorphic M-constructors. For didactic purposes it easier to first illustrate important aspects of how they function within M-constructors in maramafications of the 'flexible textual language' Algepoly1 + . It allows 'minimal examples' 1 to be more minimal.
For the sake of simplicity and the purpose of this article, the type-constructor forms in this section have been chosen such that 2D cross-sections provide all information needed. This simplifies the creation of examples in static 2D media, such as this article. These cross-sections, however, are not intended as viable alternatives for the 3D models. Among other things, it is harder to discern the different type-constructor forms in them. For example, the human visual apparatus will immediately recognise a circle that contains a triangle, as two separate objects with a distinct form, while the 'ridges and edges' in the 2D cross-sections give it much less to hold on. The users, however, will work with the 3D models.
To achieve the situation that 2D cross-sections contain all information needed, fig. 9 redefines the forms of several type-constructors that have been defined earlier. The latter can be interpreted as viewing a male joint along a line of sight that is perpendicular to the bottom of the joint. We remind the reader that in the electronic version of this document, each image contains clickable links that lead to much higher resolution versions of the image.  The rest of this section introduces the behaviours of these M-constructors by providing examples. It will indicate for each example whether it "introduces a new law", or whether it merely "illustrates existing laws". The latter type of examples should be perfectly predictable and are, among other things, added to allow the reader to verify his or her understanding.

Reverse reading of examples
Let the reader be reminded that all examples provided in the following sections also work in the reverse direction, following the law that has been explained in section 4.3. The rest of fig. 11 illustrates that the intra-M-constructor propagation takes place as expected, whether it is propagation from a male joint to a female joint, from a female joint to a male joint, or from a female joint to a female joint.

Law: scaling of polymorphic surfaces
(Introduces a new law.) Figure 13 demonstrates scaling of polymorphic surfaces. The polymorphic surface at the left (polSurf 2 ) is smaller than the one at the right (polSurf 1 ). As expected, polSurf 2 mimics polSurf 1 , however its vertical size is scaled down. The scaling factor is, in this case, equal to the ratio between the sizes of both polymorphic surfaces. This scaling process, a linear transformation to be precise, plays the central role in the maramafication of the application of type constructors (i.e. creating joints of types such as '(SimpleType a)' or '(SimpleType (List (SimpleType a)))'. For example, the joint that corresponds with '(SimpleType a)' consists of an alignment square (the two outer 'pins'), the type-constructor 'SimpleType' (the inner two 'pins'), and the type parameter 'a' (the scaled down polymorphic surface). This will be explained in more detail in sections 6.2 and 6.3. Figure 13: 'PolyCons Red'.

Joining 'super'-and 'sub'types
(Introduces a new law.) Figure 14 shows an example of joining polymorphic surfaces where the female joint is a strict super-type of the male joint. In other words, the types are different, yet unifiable. In the figure, a female joint with type 'a' is connected with a male joint with type 'SimpleType a'. As one can see, the undifferentiated region of a polymorphic surface that meets an undifferentiated region of the polymorphic surface of the opposing joint, remains in an undifferentiated state. The rest of the polymorphic surface takes the shape of the opposing joint.
(Implications of existing laws.) It also demonstrates that the M-constructors can fully deal with recursively defined types. (These are types in which a typeconstructor occurs both in the left-hand side and the right-hand side of the algebraic data type definition, such as in the definition of 'PolyCons'.) The left-most joint takes the shape that corresponds with the type 'SimpleType (SimpleType a)'. The reader is invited to verify that if yet another M-PolyCons would be inserted in the right M-PolyCons, it would lead to the left-most joint taking the form M-'SimpleType (SimpleType (SimpleType a))'. The notation M-'Type' means the type-form of the given type. Figure 14 introduces an additional law.  The final example, fig. 17 shows a cross-section of a full 3D example. It uses the original type-constructor forms (section 3).

Definition and correctness of Madawipol-β
This section defines essential aspects of Madawipol-β. It does so in a semiformal way, both to save space, and to be more legible for a wider audience. [2] contains a more formal definition of Madawipol-α. There is a great degree of overlap between Madawipol-α and Madawipol-β. A reader that appreciates additional precision, may therefore be considerably served by the latter article.
The syntax and semantics of Madawipol-β is defined by means of a translation between Madawipol-β and the textual language (Algepoly1). This way, the already existing semantics of the textual language is transferred to Madawipol-β. Note, however, that a mere definition is not sufficient. Madawipol-β should also exhibit the same relevant behaviours as its textual counterparts: type-safety. This article suffices to support this with the intuitive examples that have been provided so far. [2] provides a mathematical proof of, among other things, type-safety of Madawipol-α. This proof could serve as an inspiration for a proof for Madawipol-β. However, this is beyond this article's scope. Nevertheless, section 7 briefly reflects on a proof strategy.

The translation configuration
The translation from Algepoly1 and Madawipol-β is defined recursively on the structure of Algepoly1. For this purpose, predefined 'atomic' translation information from Algepoly1 has to be supplied to this translation. This information is provided in the translation configuration.
The translation configuration consists of the following elements: 1. A set of algebraic data type definitions ADTDset.
2. The type-constructor mapping: A mapping from each type-constructor occurring in ADTDset to a type-constructor form.
3. The constructor block mapping: A mapping that maps a given constructor occurs in ADTDset with a solid 3D object that is the M-constructor in its rough form: it does not yet contain the joints.
4. The constructor argument-location mapping: A mapping from each constructor ADTDset and an argument position, to the location and orientation of the joint that corresponds with the textual argument position.
(For example, it would map the first argument-position of 'Cons' to the location and orientation of the joint on the top in fig. 10.) 5. The constructor's result-type location mapping: A mapping from each constructor in ADTDset to the location and orientation of the male joint, hence the result type of the constructor.
The translation configuration should comply with a number of conditions to be valid. Some of these are covered in the rest of this section. The rest of this section explains some core concepts of the translation configuration more precisely. One of these is the way types expressed in Algepoly1 are mapped to type-forms.

Type-constructor forms
A more precise definition of type-constructor forms follows now. We revisit fig. 9: it provides a list of examples, when reinterpreting them as 2D projections of the joints perpendicularly to the bottom of the joint. The outer squares in this figure, the alignment square is not part of the type-constructor form.
Let T be a type-constructor. The type-constructor form T f of T is a pair consisting of a rigid part T R and, if applicable, a polymorphic subspace T S : T f = (T R , T S ). T R is a surface in 2D space. In fig. 9 all gray forms with exclusion of the alignment squares are examples. For referencing purposes, assume that the origin of this plane is in the center of the alignment square.
If T has a type-parameter, then T f has a polymorphic subspace. This is a pair that consists of a polymorphic surface T P and a type-constructor argument transformation T A . Hence, T S = Optional[(T P , T A )] 2 . T P is a surface in 2D space, too. In fig. 9 these are indicated with a red colour. The figure contains an example that contains a polymorphic subspace: 'List a'.
The type-constructor argument transformation T A is a linear transformation. This transformation is, loosely speaking, used to scale down the argument of a maramafied type-constructor, so that it fits within its polymorphic subspace. In fig. 9 this type-constructor argument transformation is simply indicated with a green square. In the case of 'List a', the green square coincides with the edge of the polymorphic subspace. A precise explanation of type-constructor argument transformations follows in .
If T does not have a type-parameter, then it does not have a polymorphic subspace (hence, T S is None).

Type-forms
Each algebraic data type has a corresponding type-form in Madawipol-α. In fact, we have already seen some of these in fig. 9: these are all examples of type-forms of types that contain exactly one type-constructor. A type-form also consists of a pair, that contains a rigid part and, possibly, a polymorphic subspace.
Examples of type-forms of more complex types, such as M-'List (List Bool)', are provided in fig. 18. Such complex type-forms can be obtained by means of an inductively defined procedure applied to the type-constructors and type-parameters that occur in the type. For the procedure, first two definitions are needed that define how to scale down an argument of a maramafied type-constructor.
Definition 1 (type-constructor argument transformation application). Let S be a subset of the 2D plane, and L a 2D linear transformation. Then L · S is the transformation of S with L, i.e. the set of all points in S, interpreted as a set of 2D vectors, transformed by means of L. Moreover, let L be another 2D linear transformation. Then L · L is the transformation that is obtained by composing L and L , hence by first applying L and then applying L. This is all 'just' standard linear algebra [5].
Definition 2 (type-constructor argument transformation application to a type--constructor). Let L be a linear transformation and T f a type-form. Then L applied to T f is defined as applying L to all elements of T f . More precisely, let T f = (T R , (T P , T A )), where T R is the rigid part of T f , T P its polymorphic surface, and T A its type-constructor argument transformation. Then L · T f = (L · T P , (L · T R , L · T A )).
These definitions allows the definition of typeFormProcedure: Definition 3 (typeFormProcedure). The procedure typeFormProcedure determines the type-form for a given algebraic data type. In words, it is defined as follows. The definition uses 'List (List a)' as a running example.
• Let T be the outermost type-constructor, and T f = (T R , (T P , T A )) its type-constructor form. (Example: recursive pass 1: T is 'List', recursive pass 2: T = 'List'.) • If T does not have an argument, or if it has an argument that is a typeparameter, then return T f . (Example: the condition only holds for pass 2: T has argument 'a'.) • Otherwise, let T be the argument of T . Note that T contains at least one type-constructor. Now apply recursion: apply typeFormProcedure to T , and let T f be the resulting type-form. (Example: the condition only holds for pass 1: T = 'List a' and T f is M-'List' (See fig. 9)).) • Now apply the type-constructor argument transformation of T f to T f . Then, add the rigid part of T f to the rigid part of the latter application. Return the result. An alternative precise formulation: return (T R ∪ (T A · T R ), (T A · T P , T A · T A )). (Example: only applies to pass 1: the result is the form in fig. 18 with M-'List (List a))' underneath.) The reader is invited to verify that the type-forms in fig. 18 are indeed constructed in accordance with typeFormProcedure, by applying the procedure to the types underneath each form.
Note that the original type can be immediately recognised in the type-form by starting with the outermost type-constructor form and then walking your way to the adjacent one, all the way down to the center form, while reading out loud the associated type-constructors. The reader is invited to verify that, in the examples in fig. 18, that indeed leads to reading out loud the types written underneath each form.
Also, it may be clear that due to its recursive nature, this procedure defines a transformation of any type into a type-form.

Male joint-form
In precise terms, the 3D male joint-form for a type-form is obtained as follows. The rigid part of the male joint-form is obtained as follows. First add an alignment square to the type-form's rigid part. Then add a third spatial axis to the type-form's space, turning it into a 3D space, and extrude the rigid part of the type-form vertically upwards over a distance of vJntSz (the vertical joint size). The front side of the joint is defined as the part before extruding began, so the part in the plane z = 0. In other words, if the joint is joined, it is this part that enters the opposing joint first. Hence, note that when facing the joint from the front, it will be a mirror image of the type-form. Complete the rigid part by adding a bottom to the joint by adding a square surface that covers the joint's complete bottom (so, at height z = vJntSz ).
The polymorphic surface of the joint is obtained, by first painting the bottom side of polymorphic surface red, and the top side blue, and then moving (not extruding) the polymorphic surface of the form upwards over a distance of 1 2 vJntSz .

Female joint-form
The 3D female joint-form for a type-form T f is obtained as follows. The rigid part is obtained as follows. First take the union U of an alignment square, T f 's rigid part and T f 's polymorphic surface. (T f 's polymorphic surface is included, because this creates space for the placement of the joint's polymorphic surface in the next step.) Then take the complement of U enclosed within the outer edge of the alignment square, leading to U . Then extrude U vertically downwards over a distance of vJntSz . Then add a bottom to the joint by adding a square surface that covers the joint's complete bottom (so, at height z = −vJntSz ). The front side of the joint is, again, defined as the part before the extruding began. Note that the female joint-form aligns exactly with the type-constructor form. It is not a mirror image.
The joint's polymorphic surface is obtained by first painting its top blue and its bottom red. Move (so, not extrude) T f 's polymorphic surface downwards over a distance of 1 2 vJntSz . Then, extrude only the edge of this polymorphic surface further downwards over the rest of the distance of the joint, so another 1 2 vJntSz . The latter is needed to attach the polymorphic surface to the joint's bottom, otherwise it would be free-floating. The material created by extruding this edge is rigid: it is not part of the joint's polymorphic surface.

Condition type-constructor forms
A condition that type-constructor forms have to meet is that each pair of distinct type-constructor forms, should be such that their corresponding male joint-form and female joint-form do not fit into each other. The following expresses this condition in a precise and operational form.
Let T f be a type-form or type-constructor form . The female bottom region of T f is the region of T f that in the corresponding female joint-form is at the height of the bottom of the joint, or can go down to that level. In precise terms, it is equal to the union of T f 's rigid part and its polymorphic surface, with exception of the edge of this polymorphic surface. For example, in M-'List a''s form in fig. 9 it is equal to the inner thick square plus the inner square region, minus the edge of the inner square region.
Let T f and T f be two type-constructor forms. One can prove that the following holds: a male joint with form T f will not fit into a female joint of T f if, and only if, the rigid part of T f contains points that are not in female bottom region of T f .
The condition can now be formulated as that for any pair of type-constructor forms present in the translation configuration, the rigid part of the first contains points that are not in the female bottom region of the second, and vice versa: the rigid part of the second contains points that are not in the female bottom region of the first.

Translation
Madawipol-β's expressivity is limited to ADSs. Therefore, the translation trans from textual language (Algepoly1) to Madawipol-β consists of a translation between ADSs. These ADSs may be unfinished (see example 3). It can be defined recursively on the structure of ADSs. trans takes two arguments, an ADS ads from Algepoly1 and a translation configuration tConf , hence an application can be written as trans(ads, tConf ). It is, sketch-wise, defined as follows. If ads is atomic, then use the information expressed in tConf to build the corresponding M-constructor. Otherwise, translate the top-level arguments of ads, and join these with the corresponding joints of the translation of the outermost constructor of ads. If at any moment in this process, some joints cannot be joined, then the translation results in unjoinable. The technical description of the translation is beyond the scope of this article.

Proof of semantical equivalence of Madawipolβ and Algepoly1
Just as Algepoly1, Madawipol-β, should be type-safe. This may now be intuitively clear, based on the examples developed so far. A proof is beyond the scope of this article, however, some reflections on it follow now. Type-safety is equivalent to stating that trans never maps a welltyped ADS to unjoinable, and conversely, that the inverse translation trans −1 of any M-ADS from Madawipol-β is well-typed in Algepoly1. Such a proof has been provided for Madawipol-α [2]. In Madawipol-β there is an extra challenge because of type-propagation. A proof strategy is to interpret each M-algebraic data structure as a typing statement. Joining of M-constructors, then, can be regarded as a form of typing derivation, and, hence, as part of a type-system [6,Sec. 8]. After all, by reading the types that occur in the joints after Mconstructors are joined, one has derived the type. This means that the proof of type-safety can be realised by showing that the latter type system is isomorphic to the type system of Algepoly1. In other words, for each typing derivation rule of the type system of Algepoly1 one has to define a counterpart based on joining M-constructors from Madawipol-β, and then one has to prove that these behave congruently.

Unifiable = joinable
An important part of the type-safety of Madawipol-β leans on the fact that any pair of types is unifiable if, and only if the corresponding male and female jointforms fit into each other, assuming that both forms were undifferentiated before the fitting started. In other words: "unifiable = joinable". This is a central lemma in a proof of type-safety. To build some intuition that this lemma is true, the reader could try to verify this for the following statements, by using fig. 18. Hence, investigate for each of the following statements whether the male joint with the first type-form, joins with the female joint with the second type-form, and whether the male joint with the second type-form, joins with the female joint with the first type-form if, and only if the types are unifiable. Whether they are is indicated with = u (types are unifiable) or = u (they are not). [2, Lemma 2, p. 11] is a proof of this lemma for Madawipol-α. A proof for Madawipol-β is beyond this article's scope. However, it is very similar. A proof-sketch follows now. If T and T are unifiable, then either T = T , and then the joints trivially fit, or T and T consist of a sequence of type-constructorapplications that have an identical beginning sequence, starting from the outermost type-constructor. After this beginning sequence, either T or T ends in a type-parameter. Assume it is T that does so. Example: T ='List (Pair (List a))' and T ='List (Pair (List (List Bool)))'. Here, the identical beginning sequence is 'List (Pair (List ...', after which T ends in the typeparameter 'a', while T contains additional type-constructors. The part of the joint-forms that are a result of the translation of this beginning sequence will always fit. One can easily see this by investigating how typeFormProcedure works: each type-constructor form is only influenced by the translation of the preceding type-constructors, never the later. The rest of the joints also fit. The type-parameter of T is translated into a polymorphic surface. Due to the linear transformation it went through, it will completely cover the translation of the remaining sequence of type-constructors of T (in the example: 'List Bool'). Hence, these parts of the joints will also fit. It is easy to see that this works both for a male version of T into the female version of T , and the male version of T into the female version of T .
If T and T are not unifiable, then there must be a minimal position n where the type-constructor of T is different from that of T . For example, with T =M-'List (Pair (Pair a))' and T ='List (Pair (List (List Bool)))' this is the case at the 3 rd position, so n = 3. The corresponding type-constructor forms at position n of both joints is linearly transformed in exactly the same way by typeFormProcedure, because the sequence of type-constructors that precedes them is identical. Joints with different type-constructor forms do not fit into each other. This is a requirement of the translation configuration (see section 6.6). Obviously, they also do not fit after going through the same linear transformation. Consequently, the joints do not fit.
A formal proof of the previous sketch can easily be obtained by induction.

Related work
The scientific literature on designs related to capturing polymorphic data structures, in particular algebraic data structure with type-parameters is to the best