Treat types as compile-time expressions

[evincarofautumn]

Types are currently parsed specially. It would be simpler and more consistent if they were treated as ordinary compile-time expressions, which happen to produce types for use by the typechecker. This would be a big step toward static metaprogramming. Thoughts on how to do this:

• Type applications should look like function applications:
  • Stream@a → a Stream
  • These@(a, b) → a b These
• Vectors might be called something like T vector instead of [T]
• The type of stack-products must be explicit: a, b instead of a b
• Kind sigils are not required: s instead of s...
• Stack variables might need to be explicit: s, a -> s, a, a instead of a -> a a
• Type operators and value operators might need to live in separate namespaces, so that a | b can denote a sum type or a bitwise OR without dealing with overloading (yet (again))

[dmbarbour]

I think this is a great direction to go. It allows abstraction of the type descriptors. Do keep in mind the possibility of: "a b -- b a" parseType.

On Wed, Oct 1, 2014 at 8:21 PM, Jon Purdy notifications@github.com wrote:

Types are currently parsed specially. It would be simpler and more consistent if they were treated as ordinary compile-time expressions, which happen to produce types for use by the typechecker. This would be a big step toward static metaprogramming. Thoughts on how to do this:

• Type applications should look like function applications:
  • Stream@a → a Stream
  • These@(a, b) → a b These
  • Vectors might be called something like T vector instead of [T]
• The type of stack-products must be explicit: a, b instead of a b
• Kind sigils are not required: s instead of s...
• Stack variables might need to be explicit: s, a -> s, a, a instead of a -> a a
• Type operators and value operators might need to live in separate namespaces, so that a | b can denote a sum type or a bitwise OR without dealing with overloading (yet (again))

— Reply to this email directly or view it on GitHub https://github.com/evincarofautumn/kitten/issues/132.

[brendanzab]

So would types more or less follow the same syntax as expressions, like in Haskell?

[evincarofautumn]

@dmbarbour A parseType function sounds perfectly feasible—it could just call the compiler, actually—but I wonder how useful it would actually be.

@bjz Yes, they would have exactly the same syntax, just a different set of operators.

I would like a way to avoid requiring stack variables, because they would be on every function. We could have two different function arrows:

[a] -> [a, a]
r, (r => s) => s

Or “type holes”:

_, a -> _, a, a

, is a nice operator for stack-conses, but it conflicts slightly with vectors [1, 2, 3]. We could change vectors to [1; 2; 3] like in OCaml. That would allow a value-level , operator for tuples:

["one", 1; "two", 2; "three", 3] vectorToDictionary

Vectors were originally [1 2 3], but having a separator turned out to be useful for providing type error messages.

[jeaye]

I believe I see a potential problem with this. There is an ambiguity if ever you support non-type template params (which I'd really like you to). The special syntax allows you to be clear that foo<4> is an instantiation and not calling foo with 4 as 4 foo may imply. If you can resolve this by checking whether or not foo expects template params, I wonder if it's still easier on the reader to see the explicit specialization.

(forgive my C++ terms, I'm still adjusting)