Lambda the Ultimate

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 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)".

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.

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.

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

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

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.

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)

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)

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 that applies to all binary expressions? I'm not sure what you mean.

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.

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.

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.

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.

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.)

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 :-)

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

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.

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.

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.

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.

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:

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?

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.

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).

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.

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.

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.

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.

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.

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.

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")

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.

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.

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?

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]

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

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.

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 and Curry-Howard to prove or deny it.

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.

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.

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).

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.

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.

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.

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).

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 ...

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.