Refining Structured Type System

This is my first more serious paper on Structured Type System.

[Abstract]
...
As every theory needs some syntax form to express its elements, a road to a theory about theories leads through a syntax defining land, so structured type system, in the first place, provides a flexible generalized text parser that builds up internal abstract syntax trees (AST) from input data. The other aspect of theory about theories inevitably covers the meaning of input data. This is called semantics, and this is the point where structured type system provides a possibility to define deeper connections between syntactic elements of AST-s. For this purpose, structured type system uses a kind of functions known from functional programming paradigm. These functions are able to process any data corpus, being natural or artificial language translation, which in turn happens to be just enough for running any complexity task used to analyze existing and calculate new data from an input.
...

In short, we use BNF-ish grammars as types for function parameters and function results. Some nice constructions can be made by combining grammars and functions. One of the most important properties of structured type system is its ability to additionally extend grammars outside the grammars definitions, all based on function result types. It is fairly simple: where a certain type of expression is expected, there a grammar that results with the same type can be used, and there goes syntax extensibility. Conveniently, we can combine grammar definitions and their inputs in the same source code file.

I was hoping to get some feedback and critics from this community before attempting to get more publicity to the paper. This is an important milestone to me and I want to thank You all for being so inspirational community during my research.

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

Nice

It's very interesting and I want to mine it for ideas on extensible syntax. One thing I wonder about is the interoperability between different syntaxes and the introduction of "higher order" notations. For example, imagine I would like to share the notion of BinaryOp between boolean algebra and arithmetic expressions, and I want to introduce shorthand that applies to all binary expressions, like slice notation, e.g. (< 2). Can that be encoded in a natural way? Or even more challenging, could you introduce a shorthand for introducing new binary operators that allows you to name their precedence relative to other operators?

Higher order notations

could be managed either by (1) dependent terms (aka dependent types), either by (2) metaprogramming that is handled in a natural way of thinking. In the case of metaprogramming, after applying parameters to a function, the function could return a case-expression controlled parts or wholes of sequences, alternations, implications, or even another functions. It seems that metaprogramming takes a full swing with structured type system.

Precedence of operators

Precedence of operators is somewhat complex matter. It is meant to be handled from the starting first syntax definition and taking care on further syntax extensions. Let's see an example of simple math calculator:

@Parsed (
    Sum <- (
        (
            Add <- (
                Left <- @Sum,
                "+",
                Right <- @Fact
            )
        ) => @DefaultMath (@Add.Left + @Add.Right) |
        Fact <- (
            (
                Mul <- (
                    Left <- @Fact,
                    "*",
                    Right <- @Primary
                )
            ) => @DefaultMath (@Mul.Left * Mul.Right) |
            Primary <- (
                Integer <- @Int
            )
        )
    )
)


Now we want to extend this syntax by exponential operator. To control its precedence, we have to pick symbols of the depth of our interest. If we want it to have the highest precedence, we have to put it between symbols "@Sum.Fact.Primary" and "@Sum.Fact.Primary.Integer":

@Parsed (
    (
        Pow <- (
            Left <- @Sum.Fact.Primary,
            "^",
            Right <- @Sum.Fact.Primary.Integer
        )
    ) => @DefaultMath (@Pow.Left ^ @Pow.Right)
)


If we want the same precedence as multiplication, we put it between symbols "@Sum.Fact" and "@Sum.Fact.Primary":

@Parsed (
    (
        Pow <- (
            Left <- @Sum.Fact,
            "^",
            Right <- @Sum.Fact.Primary
        )
    ) => @DefaultMath (@Pow.Left ^ @Pow.Right)
)


If we want the same operator precedence as addition, we put it between symbols "@Sum" and "@Sum.Fact":

@Parsed (
    (
        Pow <- (
            Left <- @Sum,
            "^",
            Right <- @Sum.Fact
        )
    ) => @DefaultMath (@Pow.Left ^ @Pow.Right)
)


But, if we want the least precedence, have to write a wrapper above "@Sum":

@Parsed (
    Exp <- (
        (
            Pow <- (
                Left <- @Exp,
                "^",
                Right <- @Sum
            )
        ) => @DefaultMath (@Pow.Left ^ @Pow.Right) |
        Sum <- @Sum
    )
)


In all cases, we can call "@Sum (1+2*3^4)".

Numeric Precedence

Personally I prefer to define the precedence of an operator as a number, which allows the precedence of any operator to be changed independently of other operators. This can be achieved with something like a Pratt parser.

Metaprogramming

I'd have to check it with metaprogramming. Theoretically, it should be possible to generically construct a compound term with this or that precedence of its subterms, as a result of a function which would take the subterms and their precedence numbers as parameters.

A shortcut to switching precedence order of binary operations

Here it is:

(
    List <- ( // a typed list
        (Type <- @Any) => (
            Item <- @Type,
            Next <- (@List (@Type) | @Unit) // @Unit is used to denote the end of a list
        )
    ) |

    BinOp <- ( // afterwards we will pass these in a list
        Op <- @String,
        Calc <- (
             (Left <- @Int, Right <- @Int) => @Int             
        ) // and we will pass functions needed for calculations here
    ) |

    Main <- (
        BinOpCalc <- (
            (
                Operators <- @List (@BinOp) // here we take a list of operators
            ) => @Parsed (
                (
                    Iterator <- (
                        (I <- @List) => (
                            @Iff (@I == @Unit,      // if we reached the last item
                                @Int,               // this is recursion terminator
                                Parent <- (         // otherwise, this is basic parser parent-child pattern
                                    (
                                        (
                                            // here we parse specific operator
                                            (Left <- @Parent, @I.Item.Op, Right <- @Child)
                                        ) => (
                                            // and here we calculate it
                                            @I.Item.Calc (@Left, @Right)
                                        )
                                    ) |
                                    Child <- @Iterator (@I.Next) // recursing the iterator
                                )
                            )
                        )
                    )
                ) (@Operators) // we apply the list to iterator
            )
        )
    )
).Main // exposing BinOpCalc to outer space

...

// default math precedence order. Precedence is determined by a position in list
x <- @BinOpCalc (
    ("+", (Left <- @Int, Right <- @Int) => @DefaultMath (@Left + @Right)),
    ("*", (Left <- @Int, Right <- @Int) => @DefaultMath (@Left * @Right)),
    ("^", (Left <- @Int, Right <- @Int) => @DefaultMath (@Left ^ @Right))
)
...
x1 <- @x (1+2*3^4) // x1 now holds the result of 1+(2*(3^4)), that is 163

...

// reversed precedence order
y <- @BinOpCalc (
    ("^", (Left <- @Int, Right <- @Int) => @DefaultMath (@Left ^ @Right)),
    ("*", (Left <- @Int, Right <- @Int) => @DefaultMath (@Left * @Right)),
    ("+", (Left <- @Int, Right <- @Int) => @DefaultMath (@Left + @Right))
)
...
y1 <- @y (1+2*3^4) // y1 now holds the result of ((1+2)*3)^4, that is 6561

...

// mixed precedence order
z <- @BinOpCalc (
    ("^", (Left <- @Int, Right <- @Int) => @DefaultMath (@Left ^ @Right)),
    ("+", (Left <- @Int, Right <- @Int) => @DefaultMath (@Left + @Right)),
    ("*", (Left <- @Int, Right <- @Int) => @DefaultMath (@Left * @Right))
)
...
z1 <- @z (1+2*3^4) // z1 now holds the result of (1+(2*3))^4, that is 2401

Same precedence

What about operator like "+" and "-" that normally have the same precedence as binary operators?

It is fairly simple

It is fairly simple to do it. In the "basic parser parent-child pattern" part (see the commented code above), we have to generically unfold elements that have the same operator precedence to an alternation representing them, instead of a single element between Parent and Child. Of course, to express the same precedence, we have to change input parameters structure also.

For example, here is how to generically construct an alternation from a list:

(
    Iterator <- (
        (I <- @List) => (
            @Iff (@I == @Unit, // remember that @List is terminated by @Unit
                @None, // we terminate the recursion by the empty alternation
                (
                    @I |                 // this is an alternation member
                    @Iterator (@I.Next)  // this is the rest of alternations
                )
            )
        )
    )
) (@SomeList)

Certainly, of the great usability are terms @None (that stands for the empty alternation) and @Unit (that stands for the empty sequence).

@None has these properties:

(X | @None) === X
(@None | X) === X
(X | @None | Y) === (X | Y)


while @Unit has these properties:

(X, @Unit) === X
(@Unit, X) === X
(X, @Unit, Y) === (X, Y)


@None can be used to terminate generic alternations, while @Unit can be used to terminate generic sequences. The third term from a triad is @Any that stands for any concievable term in structured type system, and can be used to pass around unapplied or applied terms (so functions also, as a function is a term).

These are great questions. I think I'll include them in the final version of the paper if I have your permission.

Associativity for Precedence

Personally I find numeric precedence hard work: is 1 most binding or least binding? (Different languages vary.)

Are 9 precedence levels enough? Consider (for example) all the operators introduced in the Lens libraries, or in a typical DSL.

Yes you need to be able to change the precedence for individual operators. Perhaps there are different ways to skin that cat.

Suppose you could declare precedences as Associativity rules, and let the compiler figure it out. Your rules look like:


-- `==>` is the rewrite-as declaration
x + y ^ z * w ==> x + ((y ^ z) * w) ;
x > y && z + w == v -> NOT q ==> ((x > y) && ((z + w) == v)) -> (NOT q)

So those are examples rather than rules?

In that case, you could adopt a convention that all parens in the example should be removable and just write:

precedence example ((x > x) && ((x + x) == x)) -> (NOT x)

An operator precedence technique

In a paper Operator Precedence for Data-Dependent Grammars, found on Iguana parser site, I just saw a nice and clean method for managing operator precedence when dealing with data-dependent grammars (as they call it). Translated to structured type system, we get:

(
    Exp <- (
        (p <- @Int) => @Case (
            (@p >= 3) => (@Exp (3), ('+' | '-'), @Exp (2)) | 
            (@p >= 2) => (@Exp (2), ('*' | '/'), @Exp (1)) | 
            (@p >= 1) => (@Exp (1), ('^' | '√'), @Exp (0)) | 
            (@p >= 0) => /[0-9]+/
        )
    )
) (3)


I never doubted that human ingenuity has no limits, and this is no exception. Ali Afroozeh and Anastasia Izmaylova, thank You :)

Shorthand

Shorthand that applies to all binary expressions? I'm not sure what you mean.

Sections of operators

In Haskell, you can write (+ 1) for (\x -> x+1) or (< 1) for (\x -> x < 1). Essentially it partially applies the operator to a single operand, producing a unary function. This notation is preferably something you'd specify you'd specify once for all Binary Operators.

Slice

Here it is:

(
    Op <- (
        Plus <-  "+" |
        Times <- "*" |
        Power <- "^"
    ) |

    OpImplementation <- (
        (Left <- @Int, In <- @Op, Right <- @Int) => (
            (
                @Op.Plus  => @DefaultMath (@Left + @Right) |
                @Op.Times => @DefaultMath (@Left * @Right) |
                @Op.Power => @DefaultMath (@Left ^ @Right)
            ) (@In)
        )
    ) |

    Main <- (
        Slice <- (
            @Parsed (
                Op <- @OpImplementation.In,
                Right <- @OpImplementation.Right,
            ) => (
                (Apply <- @Int) => @OpImplementation (@Apply, @Op, @Right)
            )
        )
    )
).Main
...
x <- @Slice (+3)     // x now holds (Apply <- @Int) => @OpImplementation (@Apply, "+", 3)
...
y <- @x (10)         // y now holds 13
...
z <- @Slice (*3) (4) // z now holds 12


I left out formalities about handling optional whitespace.

type specific languages

From your description, I am reminded of Jonathon Aldrich's work on the Wyvern language regarding type specific languages.

I generally like the idea of using the type system to guide interpretation of a program, except for the part where it doesn't easily work with 'interpretation' insofar as we need a static type checker and to process a bunch of grammars. My own approach to language extension has taken a decidedly different direction - focusing on projectional editors and editable views. But I'll take a deeper gander at your work, and I should probably review Wyvern's again too.

Graphical interfaces

Yes, I remember your idea of graphical interfaces to a source code, Dmbarbour, and I liked it very much. There is a big potential in that idea. What we have in the computer industry today are hard-coded solutions of wisiwig editors. Imagine if the users could be ones who define such interfaces that could extend to other areas than wisiwig editing.

[Edit]
Each function that could have its own customized graphical interface would be a lot easier learning material. It would be a huge step in programming science.

Abstract Categorial Grammars

If you haven't done it yet, you might be interested in checking out, also:

Towards Abstract Categorial Grammars

Reducing the number of primitive operators

I've managed to express syntax building operator "<-" by function operator "=>" on which is immediately applied its left side! The type system then constructs a sequence flattened to terminal leafs of the whole expression. It turns out that type checking system concludes left function sides from those leafs, playing a role of a BNF-ish parser.

This is the "<-" definition as non-primitive operator:

@Parsed (
    (A => @Symbol) (@A),
    '<-',
    (B => @Any) (@B)
) => @Parsed (
    (@A => @B) (@A)
)

Conclusion: Immediately applying all left sides of any function system transforms the function system into a parser system.

Subtyping

Thinking further, syntax building "<-" operator is nothing more than regular subtype operator ":>" known from type theory. That means that subtyping can be expressed in a terms of functions and their parameters application, which in turn can play a role of BNF-ish syntax definition language.

Suggestions?

I'm extending the paper to include some serious examples. I'm thinking of implementing some axiomatic set theory, but I'm not sure which one is the most recent. Simplicity also matters, and I would like to take some optimal least amount of definition rules, achieving the most complete realization.

Is Zermelo–Fraenkel set theory enough to get mathematicians interested, or does anyone have other suggestions?

Negating types

May I ask a simple question? I've been playing with "negation" (complement, or whatever analog) operator on types, and forming universe types. It is clear that we may define:

  • empty sum that may stand for nothing value
  • empty product that may stand for unit value

As sum may be seen as existentially quantified set, and product may be seen as universally quantified set, I understand that they are interchangeable by the following expressions:

  • ¬(∃x.P(x)) -> ∀x.¬P(x)
  • ¬(∀x.P(x)) -> ∃x.¬P(x)

The question is: what types are formed when we "negate" empty sum and empty product? By the intuition derived from classical logic, this is what may happen:

  • "negating" empty sum would give universally quantified anti-nothing set (all of nothingcomplement)
  • "negating" empty product would give existentially quantified anti-unit set (any of unitcomplement)

Am I doing a mistake with this assumption? Is it really necessary to introduce anti-values like classical set complement, or we may just use the set of all elements? If anyone has a link, or an opinion with details on this kind of operation, I would highly appreciate if you would share it here. Thank you all in advance.

Re: negating types

I think your framework is a bit messed up here.

The "empty sum" nothing value is just a value in type (1+a). You can't negate the value and speak of it as equivalent to negating the type. (Or do you mean an empty Sigma type?)

Also, the "empty product" is just one example of type 1. In many languages, the unit value and unit type are primitive. But type `1` is really just any type with a single inhabitant, and hence carrying no runtime data. For example, `forall a . a->a` or `forall a,b,c. (a,b,c) -> (c,a,b)`. Naturally, there is an infinite set of unit types. We could feasibly use unit types to encode static data.

For logical negation, I'd recommend looking at the question through the lens of Curry-Howard correspondence and simpler Church encodings of data types. A sum type (a+b) can be encoded as `forall c. (a -> c) -> (b -> c) -> c`. A product (a*b) as `forall c. (a -> b -> c) -> c`. How would you complement these propositions? (Note that `a -> b` can be encoded in propositional logic as `b or not a`.)

Seems like a bunch of arrows should get turned around. I don't have a good intuition in general, but there is likely a relationship to duality in category theory. Sums and products are known to dual each other, for example. Try negation on lots of Church-encoded types, including a few single inhabitant types, to get an intuition. (My cold doesn't leave me up to doing this, but getting an intuition isn't something I could do for you anyway.)

is Unit equal to any consistent type?

For logical negation, I'd recommend looking at the question through the lens of Curry Howard correspondence. And simpler Church encodings of types. A sum type can be encoded as `forall a,b,c. (a->c) -> (b -> c) -> c`. A product as `forall a,b,c. (a -> b -> c) -> c`. How would you complement these propositions? (Note that `a -> b` can be encoded in propositional logic as `b or not a`.)

I'm afraid that labmda calculus doesn't perfectly maps to propositional logic. True, some analogies hold, but generally, I think the problem is in the rightmost sides of nested functions.

Try negation on lots of types to get an intuition, and let me know what you learn.

this is where I come from: in logic, `true` corresponds to Unit, while `false` corresponds to Zero.

  • Existential quantifier can be seen as a disjunction of set elements (sum).
    Empty disjunction gives us `false`, by the book. If we negate it, we get `true`. However, isn't negation of empty disjunction a "full conjunction", a product of all elements not contained in the starting disjunction, which is empty? If this is true, then full conjunction equals `true` (see up). Note that empty conjunction also equals `true`.

    Hence, empty conjunction == full conjunction == `true` == Unit.

    Thinking further, couldn't we put *any* true formula wherever says `true`? And that is the most intriguing thing I've ran into lately: instead of `true`, we can write `Unit`, like we can write any true formula. Thus, Unit could stand for any true formula in specific rule set, including tautologies in general case, not only a constant `true`.

    Drawing a parallel with a type system, Unit should stand for *any* conceivable type that is consistent.

  • And now the analogy: universal quantifier can be seen as a conjunction of set elements (product).
    Empty conjunction gives us `true` by the book. If we negate it, we get `false`. However, isn't negation of empty conjunction a "full disjunction", a sum of all elements not contained in the starting conjunction, which is empty? If this is true, then full disjunction equals `false` (see up). Note that empty disjunction also equals `false`.

    Hence, empty disjunction == full disjunction == `false` == Zero.

    Thinking further, couldn't we put *any* false formula wherever says `false`? And that is the more obvious analogy: instead of `false`, we can write `Zero`, like we can write any false formula. Thus, Zero could stand for any false formula in specific rule set, including contradictions in general case, not only a constant `false`.

    Drawing a parallel with a type system, Zero should stand for *any* conceivable type that is erroneous.

The big question is: is Unit equal to any consistent type? It seems reasonable to think that an unit is one piece of something, whatever it is.

We can also ask ourselves:
1) is empty sum equal to full sum, equal to `Zero`? Look in math, what do we get when we sum all the positive and all the negative numbers?
2) is empty product equal to full product, equal to `Unit`? Again, what would math say about product of all the numbers greater than or less than one?

I have a feeling that I opened a space wormhole here :-)

(ignore)

In retrospect, I think it's better you just focus on the root logic errors rather than that boldface question... see next reply.

Some bad logic

Regarding your bullet points: Negation of an empty disjunction is the empty conjunction. By De Morgan's law.

Rather than true and false you would be wiser to think in terms of satisfiability. Unit types are satisfiable in exactly one way, but are not equivalent to `true` because there are observations we can make other than satisfiability. To negate a proposition, we must use De Morgan's law to preserve structure for these other observations.

Also, I did not suggest mapping lambda calculus terms to propositional logic. I suggested mapping types of Church encodings to propositional logic. There's a big difference. For example, there is a countably infinite set of natural number terms, but they can all be represented under the same Church-encoding type `forall a. a -> (a -> a) -> a`. If you want to "negate" the type of natural numbers, that's a good place to start.

Ok

Negation of an empty disjunction is the empty conjunction

Ok, got it. So "complement" of empty sum should equal to empty product, if I may. But that's not the case in math. -0 still equals 0.

I'd still pronounce Unit type as a type of all consistent types. It should be one of anything except Zero, somehow. I'm hoping for some arguments if I'm about to implement it in the language.

Unit

You'll just end up confusing your future readers if you insist on using "unit" to describe "one of anything". It's "one of one thing". And consequently requires zero variable bits at runtime.

Also, you should not be so quick to conflate the sum data type directly with a logical disjunction. In type (a+b), the choice is exclusive. In (a+a) we need to somehow preserve ordering information. In proposition (a \/ b), it is not exclusive, and order is irrelevant.

I still recommend my suggestion from my first reply, regarding use of Curry-Howard correspondence on basic Church encoded types. But I won't try to convince you further.

Church encoding

Actually, I kind of hope for following analogies:

empty sum == empty set == accepting no type
empty product == universe set == accepting any type

I'm still finding reasons to do it this way, I wouldn't like to just do it, I have to know what are the consequences. A motive is having defined all the basic boolean and other operations, including math and logic, in a consistent way. However, I might consider finding my own name to a universe set that "could be" a result of empty product in proposed new construct. Maybe `XUnit`.

I still recommend my suggestion from my first reply, regarding use of Curry-Howard correspondence on basic Church encoded types.

I didn't forget to check it out, I just didn't find any inspiration there. I'm somewhat familiar with Church encoding of numbers and operations on them in lambda calculus. Viewing them from the recent aspect, I didn't get further than having a disjunction of numbers. When we apply De Morgan's law, we get a negated conjunction of negations of the numbers. But, what could a logical negation mean for a number when a number isn't a boolean? The closest thing to a train of thought considering a set of numbers are again predicates "is element of" and "is not element of" set, possibly empty, which again lifts me out of internal number encoding structure. Do you have any other idea?

In a meanwhile, I also checked dependent product type (for universal quantifier) versus dependent sum type (for existential quantifier). Didn't ring my bell either.

Negation and Numbers

Regarding the negation of numbers, you can't really do it in first order logic, because it involves infinite elements. 'not(3 \/ 2) is the infinite set of all numbers that are (not 3) and (not 2). Fundamentally logic (which deals only in truth) cannot do this. You need to introduce constraints.

Logic has one constraint, equality, as we can only ask if something is equal to true. To handle negation you need disequality as well. Then:

forall x . not(x = 2 \/ x = 3)
forall x . not(x = 2) /\ not(x = 3)
forall x . x /= 2 /\ x /= 3

If we write

If we write:

forall x . x = 2

does it mean that
1) we set the (= 2) predicate as true for all x, or
2) we pick all x that are equal to 2?

#1

Although I wouldn't think of it as "setting" it as such, but rather just a proposition that all x (out of some set?) are equal to 2. This could be proven true with a term taking all x to a term of type x=2.

assertions vs. boolean check

So, if we write

forall x . not (x = 2)

we are actually not picking a set of x-es that are not equal 2. We are saying that no x equals 2. But aren't we asserting here that x is an element of {2}complement?

But, if we put it on the left side of a consequence:

forall x . not (x = 2) -> Interesting(x)

we are actually saying that for each x that is not equal 2, we know that x is interesting. Here we boolean check the set {2}complement.

There is something odd going on with logic, dealing with assertions (in the first case) versus boolean check (in the second case).

Consequences

I think the first case is simply false, as if x can be literally anything then one of those things is 2.

You are right the second is more what I was intending, but I was trying to keep it as simple as possible.

Negating types, not terms

You're eager to discuss negation of specific numbers, like 2 or 3. But in type systems, 2 and 3 just refer to types with two or three values respectively. Perhaps ask instead, what is the negation of type (1+1).

I'm not a fan of set theory or set-based models of types. They are a bad fit for substructural types, for example. I'd prefer to start from a constructive or computational logic.

Aside: I feel that you're trying to fit your intuition into a theory where instead (as a scientist of computing) you should be using examples you know to be valid to grasp a valid intuition or hypothesis and test your assumptions. The whole "finding reasons to do it this way" line (and many similar comments you've made) makes me feel suspicious about confirmation bias.

Set theory models.

In computer science we are using types to define the interpretation of a region of objects in memory, where objects are simply extents. So what is the data from byte 32 to byte 36? Is it 4 characters, or an integer or a floating point number. They clearly are concrete representations that we are dealing with. The problems of mathematical set theory like the Russel paradox simply cannot happen. This is because the question what is the type of type is clearly absurd, as it has no representation in memory. The only way to do it is to put an enum in memory and match each value to a type. As long as we remember what types represent, you cannot go wrong.

representation

This is because the question what is the type of type is clearly absurd, as it has no representation in memory.

Is the problem that it has no representation or that determining its representation is undecidable (or unsound as a logical principle, ie: Girard's paradox)?

The unit type has no representation in memory, nor do any types that terminate staging (e.g. quoted expression types, type-level values, compile-time network connections, etc).

Put in the terms you described it, you might have 4 bytes in memory and describe them as a tuple of one int and a million units, or a hundred units followed by an int followed by a quoted expression and a compile-time network connection, etc.

The type of type

Both:

It is unsound logically: Any concrete value in memory is a value, and not a type by definition. So they bit pattern at address 1234 is a value, and a type is not a value. If a type is a value, then you fall foul of Russel's paradox, because you no longer have stratification, and that permits the question "that is the type of all types that are not members of themselves". This can be explained by considering a value like "1.2", is it a member of type "Int"? If types are values then it must be possible to have a Type of a Type (as we need a type to interpret the encoding of an extent of bytes), so now we can ask is "type-a" a member of "type-b" in the same way we can ask if any value is a member of any type.

In terms of representations, we cannot independently compile two modules for runtime linking and have them determine the 'values' of types, as we cannot guarantee that the same representation wont be used for different types. The closest we could get is to hash the structure of the type, but then a hash-collision would result in big problems. Still this may be good enough in practice for many situations, we still have the fundamental problem of the paradox above.

We can avoid these problems if we simply consider things in memory to be values, and types are something else.

staging

If types are values then it must be possible to have a Type of a Type (as we need a type to interpret the encoding of an extent of bytes), so now we can ask is "type-a" a member of "type-b" in the same way we can ask if any value is a member of any type.
[...]
We can avoid these problems if we simply consider things in memory to be values, and types are something else.

I take your point that you can't say that 'type' has type 'type'. But isn't this "typical ambiguity" just resolved with nested "universes" or perhaps viewed another way -- ordered stages? Like "stage-0 type is a stage-1 type" and it's always possible to shunt something off to "the next stage".

I mean, as a practical matter, you might want to use '42' at stage-0 (compile time?) as in the type description 'char[42]' or you might want to use '42' at stage-1 (run time?) as in 'printf("%d",42)'.

In a similar way, you can have a memory representation for type descriptions and have a way to read/write them, and stage later computations predicated on the "value" of those type descriptions -- so at stage-0 you run a "typical value-level function" to read a type description from a file, which then determines how you interpret subsequent data in stage-1. We do this a lot in this project I've been working on, there's a lot of practical value to this view.

I guess I'm not really disagreeing with you but just trying to find the best language for thinking about these issues of types, values and staging. Often we only have to think about two stages and can use "type" and "value" as shorthands to name those stages, but maybe there's an opportunity to reduce a lot of compiler/language machinery and do some interesting things here.

Perhaps a type may be known at a later stage, in which case it does have some memory representation (just as types have some representation in memory in a compiler). And also values may have no memory representation when their types terminate staging, as with values of the unit type, values of type '42', quoted expressions, compile-time network connections, etc.

Flattening

You can always flatten all stages if your type system is rich enough. For example, if you have `Op` operator in stage 1, and you want to define it in stage 2, you can flatten it in its result, back to stage 1:
Op -> (
   //         stage 2                      stage 1
   (Param1 <- @T1, Param2 <- @T2) -> (@Param1 Op @Param2)
)
...
x -> @Op ("t1","t2") // x now holds stage 1 value: ("t1" Op "t2")
That way you can practically define a `top type` as a type that maps values back to the first stage, piece by piece. Then you don't need a built-in version of top type, and you can call it whatever you want, as it is a type like any other.

Dangerous

I think (but I'm not sure, because it depends exactly what you are doing), that it is this "flattening" that is causes the paradoxes.

You need to keep the stratification, which means any result must be one stage 'higher' than the arguments. In effect this prevents self-referential definitions. We can be a bit more precise (as done in Datalog) and say that results can be in the same stage as the 'highest' of the two arguments if the result is not negated, and the highest stage + 1 if it is negated.

Universes and Categories.

Yes, of course you can. My point was more that you can avoid the nesting of universes if you have a concrete model where types cannot be values, and you do not allow types to have types. Types do represent a bunch of values, or perhaps more category theoretically - a bunch of endo functions from a value to itself. If we think of it this way, it is this 'function' that prevents a type actually being represented in memory, because it doesn't exist in the computer at all, but in the intention of the programmer.

Unit, another try

How would you feel about this definition of unit:

Product could be defined as an abstraction. Quotient could be defined as an application. In other words, `x: a * b * c` would be the same as `x: a -> b -> c`, while `x / a / b / c` would be the same as `x a b c`. These examples (if they are appropriate) lead us to forming an expression: `y / y` that would be considered as *an* unit.

If you would agree with that, unit could be considered as a fully saturated expression (where there is no more space for applying new parameters). Thus, there would be multiple forms of unit, each of them consisted of different, but fully saturated expressions. This would be a point of view on unit from an aspect of openness for accepting new parameters. It aligns with a way of defining natural numbers by an amount of abstraction / application steps (I will write about this soon - an alternative to Church encoding).

Is this definition of unit digestible?

distinguishing top type from unit type

If we define equality between two notions as equality of expressions that can apply to the notions, then it doesn't matter how we reached unit. It could be `x / x`, or it could be `(x + y) / (x + y)`, the result of both of them is equal, and that would be unit.

But what happens with `1 / x` expressions? If we introduce a rule by which we can divide only by what we have multiplied before, the situation is clear: we can't have that kind of quotient values because the term `1 / x` would report a type error (I'm still using a model by which a product is an abstraction and a quotient is an application).

However, we can imagine the following system: until an expression reaches the unit state, we can divide it only by predefined expressions by which we previously multiplied the numerator. When we reach the unit point, we can imagine proceeding to the other side, to completely unbounded quotient values. The dual constraint we would expect would be the dual to that of division: when additionally multiplying quotient values, we can multiply them only by values that are super sets of previous dividing values. Looking at the unit from this aspect, it would behave exactly as top type with some constraints on what can be multiplied by after division.

But, with our new arrangement, equality (and possibly other) comparison would be undecidable because expressions that could be applied to any other expression are not completely constrained, as expectation of new parameters turns into top type after reaching the unit point.

The conclusion is: if we define a product as an abstraction and a quotient as an application, we can not form `1 / x` kind of values because equality would be undecidable. The consequence is that we can not equalize the unit type with the top type if we want equality to be decidable.

[Don't confuse type product and quotient with math multiplication and division. Those operations would be defined at higher levels above type product and quotient, while plain product and quotient could be used to represent addition and subtraction, with unit representing zero]

Negative Unit

Did you know that there exist a "Negative Unit"?

Negation vs negative

Negative and fractional types are things, but they aren't the things you were asking about. I was originally going to mention them, but decided not to further muddy an already confusing issue.

DeMorgan

Also, you should not be so quick to conflate the sum data type directly with a logical disjunction. In type (a+b), the choice is exclusive. In (a+a) we need to somehow preserve ordering information. In proposition (a \/ b), it is not exclusive, and order is irrelevant.

Just an intimation.

Logic: ¬(x /\ y) <-> (¬x \/ ¬y)
Types (speculation): ~(x × y) = (~x × y) + (x × ~y) + (~x × ~y)
                              = (~x + ~y) 

Logic: ¬(x \/ y) <-> (¬x /\ ¬y)
Types (speculation): ~(x + y) = (~x × ~y)

Somehow makes sense, but I can't prove or deny it. A consequence of the proof would be that empty product equals complement of empty sum. If the complement of empty sum is any type, we would conclude that unit type equals any type.

Try using Church-encodings

Try using Church-encodings and Curry-Howard to prove or deny it.

Negation

What about negation in logic versus negation in types? Curry-Howard correspondence seems not to deal with that.

[Edit] Ignore, I'm learning about negative and fractional types.

Negative and fractional types

That's an interesting paper, but it seems like there's a much more obvious correspondence, namely simply that subtraction eliminates alternatives from a sum and that division eliminates projections from a product. Subtraction naturally occurs in case analysis:


match x: X
| case y: A =>
| case z: B =>
| otherwise => ;; X - A - B
| Zero ;; unreachable

Which is equivalent to throwing an exception. E.g in Java there is/was a syntax like:

class Foo {
     static int Doit(int arg) throws Fail;
};

Which you can think of as transforming

int => (int + Fail) into int => int by subtracting Fail

Division would seem to correspond to linear projection.

Projection

May I ask, what do you mean by a projection? Can you show it by an example? And what would be eliminating a projection from `Unit`?

I have to emphasize that a type product is not necessarily commutative in all instances (example: Cartesian product).

Projection

https://ncatlab.org/nlab/show/projection

In mainstream programming languages the "dot" operator.

1/X would correspond to a type which will eliminate an X when paired with an X.

Negative/Fractional types do not work

Note that the paper on negative/fractional types was never published: the denotational semantics turned out to be bogus. The operational semantics still work, but if you're looking at those types for deep insight in to negation, you won't find it.

See here and here.

A report

I did some homework, and this is what I've found out:

Type operators: abstraction, application, sum and product, could be used as primitive operators in which any other operator can be defined.

Set operators: subset, complement, union and intersect, are a kind of application, sum and inverted sum. Stating that X is an element of a set A is a kind of abstracting X from A. Testing if X is an element of A is testing application of X to A for errors. Complement test is similar to testing if an element is not in some set. As we know, DeMorgan's laws apply to set operations.

Boolean operators are a special case of set operators where we are dealing only with an empty set (false) and non-empty set (true), while each set that is non-empty is considered being equal one to other. Boolean operations, basically being special set operations, also hold on DeMorgan's laws.

Other uses of type operators (like in math, for example) may or may not apply to DeMorgan's laws, depending on specific definitions. Universal negation and reciprocity are still opened questions in my research.

Negation on types

I have usually seen 'not(T)' interpreted as a continuation accepting a T or 'T -> 0' -- it's a continuation because it never returns a value (which IMHO is a reasonable interpretation of the empty type).

Negating

I'm using a definition where negating top type yields bottom type, while negating bottom type yields top type. Negating any other type yields top type without negated type.

I define negation as:

Neg => (
    (P <- @Any) => (@None @P)
)

As you see, @None type inverts what is applied to it. Applying @Any to P reports an error, while any other value is returned inverted. To recover from an error I use:

... @None => ThisOrThat ...

Interesting ideas

I can't seem to access your google doc, perhaps you haven't granted public access?

About this:

We can also ask ourselves:
1) is empty sum equal to full sum, equal to `Zero`? Look in math, what do we get when we sum all the positive and all the negative numbers?
2) is empty product equal to full product, equal to `Unit`? Again, what would math say about product of all the numbers greater than or less than one?

I think that we have some similar thoughts in the Morgan Stanley hobbes project. We also use a structured type system there, and compile-time induction on product and sum types works as you say (bottoming out in unit for products, void for sums).

For example, a generic 'print' function for records over printable types gets defined like:


class PrintRec r where
  printRec :: ([char],r) -> ()

instance PrintRec () where
  printRec _ _ = ()
instance (r={h*t}, Print h, PrintRec t) => PrintRec r where
  printRec pfx r = do { putStr(pfx++recordHeadLabel(r)++"="); print(recordHeadValue(r)); printRec(", ", recordTail(r)); }

instance (PrintRec r) => Print r where
  print r = do { putStr("{ "); printRec("",r); putStr(" }"); }

So if a user types e.g. '{x=1,y=2}' (which has type '{x:int,y:int}') then this definition derives the right function to print it back. And there's a similar way to generically deconstruct variants the same way, terminating in the void type (0).

We also do some things with dynamic grammars, and of course the structure of grammars maps to these "algebraic types" directly.

I'm curious to read more about your ideas, if/when the google drive permission bit gets flipped. :)

PDF link

Thank you for your interest.

It seems you got a real living project there. I'm still miles away from my implementation.

Google doc link looks fine to me. If you still can't access it, try PDF version here.