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?

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

@philipwhite WRT commutativity, it's about the equivalence. And by default there is not even associativity: (A * B) * C, A * (B * C), and A * B * C are all considered different types in ML.

@amiloradovsky

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 Of course we can't append two tuples together like with lists. I wasn't trying to say product types are exactly the same as lists, but just share the nested structure. They still have a fixed length because the type is totally determined.

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

@philipwhite In the Calculus of Inductive Constructions, there is no difference between types and values, they're all just terms.
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 :)

@philipwhite To elaborate:
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).

@amiloradovsky The syntax for making a value of type A*B from a:A and b:B is (a, b). That is, (a, b):A*B, as you described. Wouldn't it be more consistent to be like a*b:A*B?

@philipwhite Consistent with what? It seems rather confusing, conflating the two kinds of expressions.
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)

@amiloradovsky Hmmm, I think I'm sort of following. I meant that it would work fine in my language because the language would distinguish between types and values (and of course wouldn't have dependent types either). Thus, it would work fine because it would disallow programs that would trigger the inconsistency that exists.

@philipwhite I'm not sure how the lack of cumulative universes (that is V: T, T: U |- V: U) would help distinguishing type constructors (- * -) from value constructors (-, -).
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).

@philipwhite You should first introduce A and B, then a and b. Whatever:
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.

@amiloradovsky It knows the type of x and Y because of how they were introduced. It seems the convention is that capital letters are types, so Y is a type and x is a value of some type. Y cannot be passed as a value to a function, but it can be used in type constructors. What Haskell does with pair syntax is pretty much exactly what I'm thinking.

@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 * can't {"work fine" and yet not be "theoretically correct"}

@philipwhite

*reads post* "wat".

*looks at instance* "aaaaaaahh"

:D

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

Sign in to participate in the conversation
Functional Café

functional.cafe is an instance for people interested in functional programming and languages.