Type Syntax

[keean]

This is for discussion of the syntax used for types (type annotations and printing types). What we have so far:

• Type variables are ALL_CAPS
• Type constructors are first letter capitalised, and at least one lower case letter
• Type constructor argument lists (comma separated) are in angle brackets '<>'
• Type infix operators are symbols, so far just the function arrow '->' is defined.

[keean]

The 'Product' type constructor is parsed and printed as a type-list in angle-brackets, like this:

<A, B> -> <B, A>

[keean]

After using the type syntax for a while, I now think that the angle brackets '<>' look overused, being part of the arrow syntax as well. I have swapped to Scala-like '[]' for type-lists which makes sense as they should behave like lists. The above type would now be written:

[A, B] -> [B, A]

[keean]

I have been looking at PureScripts use of row types, and row polymorphism, and I think this is the way I want to go for effects and union types (at least for now). I want to experiment to see if this can provide the kind of union types we need. This all relates back to the HList paper I co-authored, and is in effect introducing the HList as a primitive type.

The first step will be to introduce a row type:

{label1 : Type1, label2 : Type2}

and a constructor for this type:

let x = {label1 = value1, label2 = value2}

[keean]

@shelby3

JavaScript Objects can be represented by a row type like this

forall E . { label1 : Type1, label2 : Type2 | E }

Its basically a way of saying we want an object with properties "label1" of "Type1" and "label2" of "Type2", and we don't care what the other properties of the object are.

[shelby3]

I knew already row polymorphism. I don't understand the context in which you discussed it:

and I think this is the way I want to go for effects and union types (at least for now). I want to experiment to see if this can provide the kind of union types we need. This all relates back to the HList paper I co-authored, and is in effect introducing the HList as a primitive type.

[shelby3]

I have been looking at PureScripts use of row types, and row polymorphism, and I think this is the way I want to go for effects and union types (at least for now). I want to experiment to see if this can provide the kind of union types we need. This all relates back to the HList paper I co-authored, and is in effect introducing the HList as a primitive type.

I prefer not to get a discussion about the merits and drawbacks of row polymorphism at this time (not a priority issue for me right now). We did mention/discuss row polymorphism in the past here, here, here, here, here, here, here, here, here, and here (this last link contains a post from @keean that links to a research paper claiming improvements for Ocaml's polymorphic variants).

The answers on the following are probably relevant:

http://stackoverflow.com/questions/15237598/why-doesnt-ocaml-support-record-subtyping

More:

http://cs.stackexchange.com/questions/53998/what-are-the-major-differences-between-row-polymorphism-and-subtyping

http://cs.stackexchange.com/questions/71282/difference-between-row-polymorpism-and-bounded-polymorpishm

Quildreen Motta wrote:

Notice that in the second case the values in the list don't have the same shape, but they still work with the predicate correctly. In this case, this is a constraint from Haskell's type system, which wouldn't be a problem if Haskell supported row polymorphic records (like PureScript, Elm, MLPolyR, etc).

[keean]

Nice discussion of why Scala and Java have unsound type systems that was posted on the Rust Internals forum: https://raw.githubusercontent.com/namin/unsound/master/doc/unsound-oopsla16.pdf

[shelby3]

Nice discussion of why Scala and Java have unsound type systems that was posted on the Rust Internals forum: https://raw.githubusercontent.com/namin/unsound/master/doc/unsound-oopsla16.pdf

It’s because of assignment of null instances which have a type of supertype of top (⊤) and subtype of bottom (⊥), so they can be assigned to any type, even types which are nonsense. And then by transitivity this can allow unsound casts without the compiler enforcing a downcast dependency.