Follow

Type system idea: the three type composition operators are ^ (product), | (sum), and ~ (name). Structs are just product types with each part having a name.

type point = x~int ^ y~int

type bool = true~() | false~()

type shape =

circle~(c~point ^ r~int)

| square~(tl~point ^ br~point)

Should ^ be commutative? If each side is named, then I would want that, but that seems a little inconsistent.

x~int ^ y~int === y~int ^ x~int

but

x^y !== y^x

Thoughts?

Good points. Perhaps this is too greedy, but I wanted to have row-polymorphism as well; a function that accesses a property on one of its parameters must reflect that in its type.

I was thinking I could making the product a binary operator, which means A*B*C would be parsed as A*(B*C). Operations on product types would treat them similar to cons-lists.

@philipwhite Typles are different from lists in the sense that the latter are monomorphic and have variable length. The difference with vectors is only the monomorphicity.

While in the languages with polymorphic lists (Lisps etc.) the structures do not possess any algebraic operations.

Generally speaking, a record is a map from symbols into a values, just like array is a map from numbers (indices).

@amiloradovsky My goal is to unify records and tuples, as well as unions and discriminated unions. In addition, I want to make the syntax for types and values the same, so if A*B is a type, then a*b is a value of that type (that's why I chose ^, to not clash with multiplication).

Still thinking this all through though, so there are a lot of inconsistencies.

The product type is actually defined through currying:

A * B -> C is read as A -> B -> C, and A -> B * C is read as having two maps A -> B and A -> C.

The respective expression for the pairs appears on the other side of the colon (a: A, b: B |- (a, b): A * B; and analogously for the projections).

So I'm not sure where you're going with that unification of the syntax.

@philipwhite Meanwhile, w.r.t. the commutativity, in some substructural logics, judgements a: A and b: B can't be transposed. So A * B and B * A can't be a priori treated as equivalent.

For example, dependent sums are essentially pairs, but you can't just swap the components and still "feel the same way" about it :)

Dependent types may be defined as x: X |- E(x), where E is a type family indexed by X. Then you may have sequents like this:

x: X, e: E(x) |- (x, e): ∑{x: X}, E(x).

Let a: A, b: B |- a * b: A * B is a rule. Then there is no way to distinguish expressions like A * B from those like a * b, and I expect the projections pl: a * b -> a and pr: a * b -> b to exist just from the facts above; how would one define them?

These are not the same thing as taking the first and second component of a pair, those have signatures A * B -> A and A * B -> B, different types.

@amiloradovsky I'm beginning to agree with you. The benefits I have in mind are only aesthetic, so perhaps I should quit trying to be clever about this.

My original intention is for this to be used in a language with hindley-milner type inference, and with types being distinguished from values. In such a language, I'm certain I could find some way to make everything work together fine (though not theoretically correct). Is there a benefit to it? I doubt it.

@philipwhite Things can't "work fine" and yet not be "theoretically correct", IMO. The inconsistency will pop up sooner or later, rather sooner.

BTW, the distinction between (-, -) and - * - is not that types are distinguished from values, but those are just different expressions used in different contexts to express different intentions:

- you may well have a pair of types (A, B): U * U, for example, or

- A and B being themselves a universes, and thus a: A and b: B being themselves a types.

@philipwhite That is, something like

(a, b): A * B, u: a, v: b |- E(a, b, u, v)

or, more illustrative,

x: A * B, u: pl x, v: pr x |- F(c, u, v)

But sure in a simpler language you need to take less care of splitting hairs, and clearly distinguishing the concepts.

@amiloradovsky The language knows whether or not a symbol refers to a type or a value. If the symbols refer to types, then * creates a new pair type, but if they refer to values, then * creates a value. For example,

A: U, B: U |- A*B: U

a: A, b: B, A: U, B: U |- a*b: A*B

I hope I got the notation correct; I'm not super used to it (I'm not much of a mathematician, not matter how hard I try).

The compiler sees the expression x * Y, what are the types of x and Y, and what is allowed for them?

Can I use them for type constructors, like f: x -> Y, or can I pass them as arguments to or return from a function, like X = g x or y = h Y?

It probably can be done in principle, a la Haskell, where the expression (-, -) is interpreted differently, depending on where it is encountered, but it's ugly anyways, IMO.

@philipwhite What if they weren't introduced yet? The compiler will just complain about undefined names? No more precise?

Those are just that, conventions. Capital letters may also name modules and module types. Or they may be reserved for constructors of types.

What if I wrote x * Y, where Y is established to be a type and x is established to be a value? Just an obscure error? How it would formulate?

To recap, I don't think mixing these two kinds of syntax is a good idea. It'll only confuse.

@philipwhite * oops, c = x

@philipwhite * can't {"work fine" and yet not be "theoretically correct"}

*reads post* "wat".

*looks at instance* "aaaaaaahh"

:D

seems interesting, i find the single character operators a little hard to read though

Andrew Miloradovsky@amiloradovsky@functional.cafe@philipwhite The field names are essentially just projections of the product type onto it's components.

They may be actually defined not for every piece of the "internal state" (as in private "variables" / "slots" of objects / modules).

And there may be more projections than the product components (as in accessors, additional "getters" & "setters").

The fields may be also accessed by their numbers, assuming their order is fixed and transparent.